Goal of exercise
- Better understand PVS equality, by comparing it to Leibniz equality;
- Learn how to use PVS prelude (Meta-x view-prelude-file), rather than re-inventing the wheel;
- See how PVS judgements may be used (instead of lemmas) to specify simple properties, thus enhancing PVS type inference capability.
Step by step
- According to Leibniz, x is equal to y provided that any property satisfied by x is also satisfied by y.
- Create a leibniz theory in a new ~login/pvs/equality/ directory (use Meta-x new-pvs-file command to create this new theory) and define equals predicate according to Leibniz. Then:
- Look for definitions of reflexive, symmetric and transitive predicates in PVS prelude
- Prove that equals is reflexive (easy!);
- Prove that equals is symmetric (not so easy);
- Prove that equals is transitive (easy!);
- Deduce that equals is an equivalence relation (and state this result as a JUDGEMENT);
- Prove that equals is exactly PVS equality (=).
DO NOT IMMEDIATELY LOOK AT Dump (without proofs): ~gloess/pvs/2.4/equality/2.4.equality.18nov2003.leibniz.noproof.dmp.txt.