Assignment 2: Assigned September 29, due Thursday, October 13 at 10:00am

For questions 1, 2, and 3 give a natural deduction proof.
1. p.79, 1.2 (3f)
2. p.80, 1.2 (3n)
3. p.80, 1.2 (3t)
4. Compute the complete truth table of the following 2 formulas and answer the question below:
   (p -> q) /\ (q -> p)
   (p \/ q) -> (p /\ q)
   Does the following hold? (See definition 1.34.)
   (p -> q) /\ (q -> p) |= (p \/ q) -> (p /\ q)

5. Do a proof in Coq of the sequent in Question 2 above (p.80, 1.2 (3n)).
6. Do a proof in Coq of the sequent in Exercise 1.2 (3s) on p.80.

   Notes on Coq proofs:

   • You may use any Coq commands learned in class except for "auto" and "tauto". You are not restricted to using only Coq commands that correspond to natural deduction inference rules. You may also use other commands you find in the Coq documentation, but if you are not sure a command is acceptable, please ask.
   • Your solutions to questions (5) and (6) must be sent to me by email, in one single file named YourLastNameFirstInitial.v. Please separate the proofs using different Coq sections. (Don't forget to begin and end all sections.) This file must be in text format (no Word documents or any other kind of document). A file saved from a CoqIDE session will work fine. I must be able to save the file, load it into CoqIDE, and successfully execute every line. All solutions must be submitted before class on the due date.
   • Recall that the "Save" command in Coq does not save to a file. It saves the current completed theorem into the environment so that it can be used as a lemma in later proofs. To save your work, save it into a file.
   • If desired, you may load Examples1.v which contains the derived rule "MT" and other rules. Do "Load Examples1." before starting your proof. This file is available from the course web page, by clicking on "The Coq Proof Assistant" and then on "Examples1.v".

7. Fill in the missing precondition or postcondition to form a Hoare triple that is satisfied under partial correctness. For postconditions, make sure the formula expresses as much information as possible. (You do not need to provide proofs.)

   a. (| ?? |) z=z+y-1; (| z >= y |)

   b. (| ?? |) x=x+1; (| x=y |)

   c. (| a=9 |) a=2; b=a+1; a=b*b; (| ?? |)

   d. (| i=-j |) i=i+1; j=j-1; (| ?? |)

   e. (| ?? |) if (z==0) {x=z+1;} else {x=z-2;} (| x=1 |)

8. p.300, 4.3 (1b)
9. p.300, 4.3 (5b)
10. Write down a program P such that (| T |) P (| a < (b - 2) + c |).