Homework Assignment

Meet PVS

Familiarize yourself with the PVS Prover Guide, the PVS Language Reference and the PVS System Guide.
In particular, study the third chapter of the Prover Guide, which explains the PVS logic and its reasoing rules.

Instructions:

1. The PVS source files A.pvs, B.pvs, and EQ.pvs, and have already been placed in subdirectory class/astudent/1 of your homework directory.
2. Move to subdirectory 1 and (on a departmental Linux machine) invoke pvs5. Using PVS, prove all the theorems in each file. Further instructions, restricting what proof-commands to use, are included as comments in these source files.
3. When you are done proving the theorems, while still in PVS, enter the command M-x prove-pvs-file to generate a buffer containing a status report. Save this buffer (using C-x C-w) under the name A.status (B.status, EQ.status respectively).
4. PVS has now created new files, A.prf, and B.prf and EQ.prf recording the proofs you have done; and A.status, B.status and EQ.status recording the status of your work. The commands:
   1. svn add *.prf *.status – tells SVN to include these new files in the repository. You must always explicitly add new files or directories. Adding a directory also adds everything it contains.
   2. svn commit -m "any string" 1 – Causes SVN to upload everything in directory 1 (that you have previously added) to the repository.

Notes and Hints:

• During PVS start-up you may see a PVS message asking whether it should create a context file for this directory. The context file is a hidden file named .pvs-context. PVS also creates a subdirectory pvsbin/ where it keeps binary state information. Do not svn add these files to your SVN registry. They are not useful and they take up space.

• In lecture, two PVS system commands were used:

  • M-x ff opens a PVS source file (.pvs)

  • M-x pr initiates a proof of the theorem under the cursor (i.e. open the PVS proof editor).

• The instructions in A.pvs, B.pvs, and EQ.pvs say what prover commands to use to complete the proofs:
  • For A.prf may use only the commands (SPLIT f) and (FLATTEN f). Your learning goal is to know (not guess) which command to use at a given point in the proof.
  • For B.prf you may use only the commands (SPLIT f), (FLATTEN f), (SKOLEM f name), and (INST f expression), Again, you want to get to the point of knowing (not guessing) which command to use and when.
  • For EQ.prf, in addition to (SPLIT), (FLATTEN), (SKOLEM) and (INST), You may use the commands (SIMPLIFY), (ASSERT), and (LEMMA "name").

• To get help for a prover command, in the PVS menu invoke help-pvs-prover-command (C-c C-c c), also available in the PVS → HELP menu.

• The prover's quantifier elimination commands are (It is important to include the quotation marks):

  • (INST f "t") instantiates the for-all (in the antecedent) or there-exists (in the conclusion) variable in formula i with the term t. For example,

    {-1} (FORALL x: P(x)) |------- {1} ... Rule? (inst -1 "f(a)") {-1} P(f(a)) |------- {1} ... Rule?

  • (SKOLEM f "v") introduces the skolem constant (dummy name) for the there-exists (in the antecedent) or for-all (in the consequent) variable in formula i. Example:

    {-1} (EXISTS x: NOT P(x)) |------- {1} ... Rule? (skolem -1 "A") {-1} NOT P(A) |------- {1} ... Rule?

• (SIMPLIFY) and (ASSERT) invoke PVS's arithmetic reasoning procedures. They are used when the goal formula(s) involve: Assertions about equality or inequality. These will be discussed in greater detail in lecture.
• (LEMMA "name") introduces a previously established fact (axiom, theorem, etc.) to the sequent. This, too, will be discussed further in lecture.