A theory of lists and trees based on the idea of so-called “shells” was introduced by Boyer & Moore as a part of their computational theory of recursive functions, and successfully implemented in their theorem prover, in the late seventies or early eighties. The ability of the latter to automatically prove lemmas by structural induction (a form of well founded induction) and generalization was fascinating at the time. This exercise is about such proofs, and is quite amusing with PVS, as these inductive proofs often trigger a cascade of “lemmas on the fly”, which are also proved by induction.
Goal - Introduce PVS datatypes, recursive definitions, and well founded induction;
- Improve your proof skills, and discover that proof is not always automatic, and may require some thought and intuition.
Step by step - Create a ~login/pvs/lists_trees/ directory, copy ~gloess/pvs/2.4/lists_trees/2.4.lists_trees.2nov2004.lists_or_trees.dmp.txt dump, and restore the library as usual, using Meta-x undump-pvs-files after starting PVS from your lists_trees context;
- Load lists_or_trees theory and bintree datatype using Ctrl-c Ctrl-f, and follow advice in lists_or_trees leading comments, so as to study list_adt prelude theory and induction lemmas available in prelude; ask questions ...; you can also look at bintree datatype and its expansion into theories, using Meta-x ppe from bintree buffer;
- Study app recursive definition and replay one of app associativity proof, e.g., app_associative_proved_by_induction, for which you can look here at an
- Prove rev_rev lemma on your own, using Meta-x pr: this should be a lot of fun! Hints:
- Use induct command; rely upon (expand ... :if-simplifies t) command to carry careful expansions of recursive calls, that really simplify the sequent;
- When you can no longer simplify, look at the current goal, and try to imagine a useful lemma, that will help proving the current goal. You may need to write or draw, take examples of lists, in order to support your intuition and imagination. Don't immediately look at this quite suggestive drawing
 but you may want to click on it for a full size version, if you are really stuck!- If you have an idea of the lemma as a formula of the form (FORALL (l1, l2: list[T]): ...), you can introduce it on the fly, using the command:
- (case "(FORALL (l1, l2: list[T]): ...)"): this will trigger two subgoals, one with this formula available as an hypothesis for the proof of your current goal; a second one committing you to prove this formula (you might as well remove all irrelevant hypotheses using (hide-all-but 1) command);
- introducing a lemma on the fly is convenient, because you do not need to quit the proof; however, if this lemma seems useful and interesting in it itself, it may be worth giving it a name, and adding it to the theory; for this exercise, we'll keep it “on the fly”;
- If the above drawing did not help you, and you are still stuck, and tired of it, you are welcome to look at it here;
- later in the proof, you will need another lemma on the fly, obtained by a simple generalization of the goal: if cannot guess it, you can look at it there.
- Improving your rev_rev proof:
- Partial skolemization, using “_” in the skolem command to keep useful variables, will simplify induction hypotheses, and thus make your proof clearer: you need to carefully decide which variables can be skolemized and which one are to remain free;
- Using auto-rewrite at the beginning of the proof, for rev and app, will greatly simplify the proof: careful expansions will be carried out automatically by PVS, upon execution of ground, assert, or do-rewrite commands, without any need for explicit expansion by means of (expand ... :if-simplifies t).
- Don't immediately look at rev_rev proof dump;
- Complementary exercises:
- prove revapp_app_rev, an equivalence between revapp function and app of rev;
- prove mc_flatten_app_flatten, an equivalence between mc_flatten function and app of flatten. For the latter, don't immediately look at
- mc_flatten hint and proof.
|
Sous-pages (1) :
mc_flatten
 Updating... Paul Y Gloess, 23 sept. 2013, 13:13
|