Assignment 2

More PVS

Instructions:

1. Copy the PVS source files D.pvs, and E.pvs to an appropriate place on your computer.
2. Trye to prove all theorems in both files. Note: in order to do this you will need to introduce some theorems of your own. Not all the results can be proved without additional facts.
3. Hand in modified .pvs files, and .prf and .status.
4. Make sure that from D.pvs at least theorem geom_sum is proven, and from E.pvs theorem thm_E_6

Notes and Hints:

• D.pvs:
  • In addition to commands you have already seen, proofs require the use of (INDUCT v), for induction over variable v.
  • Hint: If ASSERT doesn't work when you think it should, look for something to EXPAND.
• E.pvs

  • The Prover command (both-sides op arg fmla) applies the arithmetic operation op with argument arg to both sides of an (in)equality. For example, (both-sides "*" "X+3" 1) mulitplies both sides of the equation in formula 1 by X+3.

  • Take care not to EXPAND to far. If you do, you are likely to see conditional expressions in the sequent. The proofs for this file do not require you to manipulate conditionals—so back up.
    The command (EXPAND "name" f n) expands the n^th occurance of function name in formula f.

  • In case you want to manipulate the conditionals anyway, the commands LIFT-IF and CASE are used. Examples will be done in lecture.