PVS‎ > ‎exercises‎ > ‎

Leibniz

 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 preludeProve 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.