Assignment 3

For your final project you can choose between three problems/algorithms:

Mergesort
Quicksort
List permutations

In the first two you have to prove correctness of the sorting algorithm. The latter is a combinatorial problem. In all three problems you don't have to write any code. Moreover, if you follow the line of proof we had in mind, you will probably need no additional lemmas.

Instructions:

Copy PVS source files into your working directory.

For Mergesort these are: ms.pvs, ms.prf, sorting.pvs and sorting.prf.
For Quicksort: qs.pvs, qs.prf, sorting.pvs and sorting.prf.
For List Permuations: perm.pvs and perm.prf.

Some explanations

The sorting algorithms share the file sorting.pvs containing specifications of basic notions and properties such as list permutation, sorted lists etc. There is also an induction principle called list_length_induction that can be used to prove properties about the quicksort function itself. All pvs-specifications are split up into several theories containing definitions that more or less belong together. It should not be hard to figure out what each of these theories is supposed to cover. The prepared project on permutations consists of a single pvs-file perm.pvs. In this file, the theory Perm contains a function perm that, when applied to a list, generates all permuations of that list. Herein, the auxiliary funtion insert is used that inserts an element in a list at all possible positions.

What to do?

Mergesort

The main task is to prove the main theorem about mergesort ms_sorted. As warming up, you could start with proving the lemmas drop_take and nth_append. The first lemma is a straightforward property about the list functions drop and take; the second lemma is about the combination of the functions nth and append. Thereafter, your task will get more challenging: prove lemma merge_sorted. This lemma is indispensable for your main theorem. Although the property itself is quite straightformward, the proof is pretty complicated because it involves many non-trivial steps. After finishing this lemma, the main goal should be a piece of cake.

Quicksort

The main task is to prove the main theorem about quicksort qs_sorted. As warming up, you could start with proving the lemma nth_append: a straightforward property about the combination of the functions nth and append. Then you should try the lemmas sorted_append and split_lwb_upb. Finally, try to prove the main goal.

List Permutations

The main task is to prove that the number of permuations of a list with length n is n! (factorial of n) (lemma perm_fac). As a warming up, you could start with with proving the lemmas map_flatten, map_all and insert_sameLength. To prepare for the main goal, prove lemma perm_length. Think about what this lemma implies, and how you can use it in your final proof. Finally, prove perm_fac

Notes and Hints:

The files with a .prf extension contain proofs. Although you can open these files in an ordinary text editor, their contents will not be very informative. A better way to view a proof of a certain property is to go to it in the corresponding .pvs file and invoke the stepping mode of the theorem prover by typing M-x step-proof. Your window will split with on one side the proof tree and on the other the sequence of proof steps. With Tab 1 you can execute the next proof command.
For the sorting problems, we advice you to have a look at the proofs of ms_perm or qs_perm, because these proofs might help you to discover the right approach for proving the main theorem. Btw, the proofs of only a few lemmas have been included.
In order to prove any of the properties no more new proof commands are necessary. More specifically, the commands you will (probably) need are: (induct ...), (skolem ...), (flatten), (split ...), (expand ...), (case ...), (lemma ...),(replace ...),(lift-if ...),(assert),(inst ...),(copy ...).
The (skeep) command introduces Skolem constants by keeping the original names of the quantified variables
Use (lift-if) to handle/eliminate CASES...ENDCASES expressions.
With (inst? fnum) PVS will try to find an instantiation for the quantified formula fnum. This can save you a lot of typing. Just try it! If it fails you can always use undo.
The command (copy fnum) makes a copy of formula fnum. You probably need this one to copy you induction hypothesis when you are proving something about quicksort itself.
You can use (grind) to finish a branch of your proof tree that is more or less trivial. If the latter is not the case, you should not use this command.
With (undo) you go one (or more) step(s) back in your proof tree.
With M p you get the last input typed to the prover; further uses of M p cylce back in the input history. M n works in the opposite direction.
If you have a run-away prover command (e.g. (grind)), you can type C-c C-c (while in the *pvs* buffer), which will drop you into Lisp:
Error: Received signal number 2 (Keyboard interrupt) [condition type: INTERRUPT-SIGNAL] Restart actions (select using :continue): 0: continue computation [1c] <rcl> At the <rcl> prompt, type (restore) to get back to the previous sequent.