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)