Here are the solutions to the midterm, along with a postmortem of how people did in general, including the most egregious mistakes. The average is something like 72%, but there are a few people that got very low, skewing the average down. ---------------------------------------------------------------------- Question 1 (10 pts) A question checking that you know the meaning of some of the basic terms that we end up using when talking about proofs. Overall, most everyone did pretty well. (Anything between 7 and 10 is good.) Points were taking off when you were a bit too vague, or a bit too wrong. (a) What does it mean for an ACL2 logic formula to be valid? An ACL2 logic formula is valid if it is true whatever ACL2 values are substituted for the variables in the formula. (b) What does it mean for an ACL2 logic formula to be an instance of a propositional logic formula? An ACL2 logic formula is an instance of a propositional logic formula if it is obtained from the propositional logic formula by substituting ACL2 logic formulas for the propositional variables. ---------------------------------------------------------------------- Question 2 (30 pts) A question to see if you remembered the goal we were after - to establish that a formula was valid. (A proof is a way to prove a formula valid. Validity is what we're after here, since it says something about computations.) Most everyone did okay, although some missed that app does not necessarily returns true lists. 10 points per answer. (a) (true-listp (app x y)) Not valid. Note that (app x y) returns y when x is, for instance, nil. Thus, if y is not a true list, (app NIL y) is not a true list. Thus, a counter example has x be NIL and y be 5: (app NIL 5) returns 5, which is not a true list. (b) (true-listp (rev x)) Valid. Easy to see that anything returned by rev is a true list. (c) (= (rev (app x y)) (app (rev x) (rev y))) Not valid. Plug in any nonempty list for x and y: let x be '(1) and y be '(2). Then (app x y) is '(1 2), so (rev (app x y)) is '(2 1). But (rev x) is '(1) and (rev y) is '(2), so (app (rev x) (rev y)) is '(1 2). ---------------------------------------------------------------------- Question 3 (20 pts) A simple proof. Many of you got it, although a bit less than 20% had no idea what was going on. You were asked to prove something of the form C => (= ... ...). Remember that to prove this, you prove the (= ... ...) part, and you get to use formulas in the context C, generally by substitution. Some of you though that you had to prove the formulas in the context. No. You get to "assume" the formulas in the context. Remember what an implication is actually saying: if the formulas in C are true, then the (= ... ...) is true. Roughly 6 points each for all 3 of the key steps in the proof (expanding app, rev, and using A2), with partial credits for pointing out the axioms used. The formula to prove: (endp x) /\ (= (app (rev y) NIL) (rev y)) => (= (rev (app x y)) (app (rev y) (rev x))) First, let's identify the context, C = (endp x) /\ (= (app (rev y) NIL) (rev y)) and name the formulas of the context, to make it easier to refer to them. A1 : (endp x) A2 : (= (app (rev y) NIL) (rev y)) Here's the proof, just identifying the important intermediate points: (I also underline the bits that we substitute at each step) C => (= (rev (app x y)) (app (rev y) (rev x))) ^^^^^^^^^ by definition of app, A1, and if axiom C => (= (rev y) (app (rev y) (rev x))) ^^^^^^^ by definition of rev, A1, and if axiom C => (= (rev y) (app (rev y) NIL)) ^^^^^^^^^^^^^^^^^ by A2 C => (= (rev y) (rev y)) by reflexivity (and propositional reasoning) ---------------------------------------------------------------------- Question 4 (40 pts) Similar to the above, except that there is an additional assumption, that app is associative. People that were confused by 3 were also confused by this one - makes sense. A few people had difficulty with this proof because it was long. I agree, and it is essentially as long as it can get on a midterm, so you can feel better knowing that you won't have anything longer to prove on a midterm from now on. The proof itself is pretty straightforward, once you pick the right applications to expand at the beginning, and pay attention to where you can use the second formula in the context, and the associativity of app. Roughly 8 points each for the 5 keys steps in the proof (expanding app, rev, using A3, A1, and expanding rev again), with partial credits for pointing out the axioms used. The formula to prove: ~(endp x) /\ (= (rev (app (cdr x) y)) (app (rev y) (rev (cdr x)))) => (= (rev (app x y)) (app (rev y) (rev x))) Let A1 be the assumption (= (app a (app b c)) (app (app a b) c)) Let's identify the context C = ~(endp x) /\ (= (rev (app (cdr x) y)) (app (rev y) (rev (cdr x)))) and again name the formulas of the context to make them easier to refer to: A2 : ~(endp x) A3 : (= (rev (app (cdr x) y)) (app (rev y) (rev (cdr x)))) Here is the proof, again focusing on the important intermediate steps: (I also underline the bits that we substitute at each step) C => (= (rev (app x y)) (app (rev y) (rev x))) ^^^^^^^^^^ by definition of app, A2, and if axiom C => (= (rev (cons (car x) (app (cdr x) y))) (app (rev y) (rev x))) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ by definition of rev, endp axiom, if axiom C => (= (app (rev (cdr (cons (car x) (app (cdr x) y)))) (list (car (cons (car x) (app (cdr x) y))))) (app (rev y) (rev x))) by car and cdr axioms C => (= (app (rev (app (cdr x) y)) (list (car x))) (app (rev y) (rev x))) ^^^^^^^^^^^^^^^^^^^^^ by A3 C => (= (app (app (rev y) (rev (cdr x))) (list (car x))) (app (rev y) (rev x))) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ by A1 (associativity of app) C => (= (app (rev y) (app (rev (cdr x)) (list (car x)))) (app (rev y) (rev x))) ^^^^^^^ by definition of rev, A2, if axiom C => (= (app (rev y) (app (rev (cdr x)) (list (car x)))) (app (rev y) (app (rev (cdr x)) (list (car x))))) by reflexivity (and propositional reasoning)