Assignment 2: Assigned September 25, due Thursday, October 9 at 10:00
October 6: Question 7, part (a) corrected. This part is now extra credit.

For questions 1, 2, and 3, give a natural deduction proof.
1. p.80, 1.2 (3h)
2. p.80, 1.2 (3k)
3. p.80, 1.2 (3t)
4. p.82, 1.4 (2a). In addition answer the question: is this formula semantically entailed from the empty set of premises? (See definition 1.34.)
5. Do a proof in Coq of the sequent in Exercise 1.2 (3s) on p.80.
6. Do a proof in Coq of the sequent in Question 1 above (p.80, 1.2 (3h)).

   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 YourLastName.v. You can separate the proofs using different Coq sections. This file must be in text format (no Word documents or any other kind of document). I must be able to save the file and load it into Coq using the "Load" command. All solutions must be submitted before class on October 9.
   • 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, you must use an editor to create a file, and copy the sequence of commands that you type to Coq into this 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. (| ?? |) a=a+b+1; (| a >= b |)

   b. (| ?? |) z=z-1; (| z=y |)

   c. (| i=2 |) i=9; j=i+1; i=j*j; (| ?? |)

   d. (| x=-y |) x=x+2; y=y-2; (| ?? |)

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

8. p.300, 4.3 (1b)
9. p.300, 4.3 (5b)
10. p.300, 4.3 (6a)