Goal- Illustrate inductive set and fixed point theory, using the example of even numbers presented in PVS language slides;
- Learn how to use fixed point induction, as opposed to well founded induction: note that INDUCT proof command has not been extended to INDUCTIVE definitions; you need to make explicit use of specific induction axioms generated by PVS for each INDUCTIVE definition;
- Learn about a new PVS Emacs command: Meta-x ppe (a short for Meta-x pretty-print-expanded) lets you see an expanded version of the theory, where TCCs and axioms generated by PVS for certain constructions (like INDUCTIVE definitions), are mixed with user declarations and definitions.
Step by step
- create a new directory ~login/pvs/inductive;
- copy ~gloess/pvs/2.4/inductive/2.4.inductive.14november2006.induction_example.dmp.txt; into the above directory;
- launch PVS from your directory, then use Meta-x undump-pvs-file command to undump this dump into your directory;
- load induction_example theory, using Ctrl-c Ctrl-f, and follow advice given in leading comments;
- look at the definitions of even?, eveni? and ev?, then at the weak induction axioms generated by eveni? and ev? inductive definitions: these axioms are named
eveni?_weak_induction and ev?_weak_induction respectively;
- look at existing proofs (including proofs of TCCs), and try to complete incomplete ones. The most difficult one is the proof of even?_implies_eveni?: fixed point induction does not apply, because even? is not defined inductively. Well founded induction is required ... using INDUCT command, but the difficulty is to find the proper variable for induction.
- DO NOT LOOK IMMEDIATELY AT SOLUTION!
- the following complete solution of this exercise includes a proof of
ev?_mu_tau: LEMMA
ev? = mu(tau)
- using Bruno Dutertre library on fixed point induction:
|
|