PVS‎ > ‎exercises‎ > ‎


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.