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.