#| Lab 6. Equational Reasoning In this lab, we will practice equational reasoning proofs. So that we can focus on the reasoning part, we are using functions we have seen before. Do as much of the lab as you can and if you do not finish, use these problems to practice for the exam. |# (definec llen (x :tl) :nat (if (endp x) 0 (+ 1 (llen (rest x))))) (definec aapp (a :tl b :tl) :tl (if (endp a) b (cons (first a) (aapp (rest a) b)))) (definec rrev (x :tl) :tl (if (endp x) nil (aapp (rrev (rest x)) (list (first x))))) (definec in (a :all X :tl) :bool (and (consp X) (or (equal a (first X)) (in a (rest X))))) (definec del (a :all X :tl) :tl (cond ((endp X) nil) ((equal a (car X)) (del a (cdr X))) (t (cons (car X) (del a (cdr X)))))) #| Recall that for each of the definitions above we have both a definitional axiom, and a contract theorem. For example for llen, we have the definitional axiom: (implies (tlp x) (equal (llen x) (if (endp x) 0 (+ 1 (llen (rest x)))))) The contract theorem is: (implies (tlp x) (natp (llen x))) You can use definitional axioms and contract theorems for free, i.e., you don't have to prove anything. When you use a definitional axiom, say for llen, your hint is "Def llen". When you use a contract theorem, say for llen, your hint is "Contract llen". For the rest of your lab questions, you can assume that the following is a theorem. Lemma llen-aapp (implies (and (tlp x) (tlp y)) (equal (llen (aapp x y)) (+ (llen x) (llen y)))) When you use the lemma above, your hint is "Lemma llen-app". We need to ACL2s that the above is a theorem you can use. |# (defthm llen-aapp (implies (and (tlp x) (tlp y)) (equal (llen (aapp x y)) (+ (llen x) (llen y))))) #| We will also be using an equational reasoning proof checker to check our proofs. The checker is still a work in progress, but it useful for finding bugs in your proofs before you submit them. Go to http://checker.atwalter.com/. If you click on "Select a file" you can see some example proofs. If you then click on "Submit File" the proof checker will check the example. To check your proofs, below, click on "Browse" and select this file. Then click on "Submit File" and the proof checker will check your solution. To use the proof checker, you have to write legal ACL2s syntax, e.g., you can't write x=nil; instead you have to write (equal x nil). Also, we have to be able to parse your proofs, so you might see parser errors. If you do, look at the sample examples and the error message to fix the issues you get. Here is the structure of of proofs. Proofs should be in comments like this one that inside of hash-bar/bar-hash forms. I will use an example proof to show the proof format. |# #| Conjecture 0: (implies (tlp x) (implies (and (consp x) (not (equal a (first x))) (implies (tlp (rest x)) (implies (in a (rest x)) (in a (aapp (rest x) y))))) (implies (in a x) (in a (aapp x y))))) Exportation: (implies (and (tlp x) (consp x) (not (equal a (first x))) (implies (and (tlp (rest x)) (in a (rest x))) (in a (aapp (rest x) y))) (in a x)) (in a (aapp x y))) Contract Completion: (implies (and (tlp x) (tlp y) (consp x) (not (equal a (first x))) (implies (and (tlp (rest x)) (in a (rest x))) (in a (aapp (rest x) y))) (in a x)) (in a (aapp x y))) Context: C1. (tlp x) C2. (tlp y) C3. (consp x) C4. (not (equal a (first x))) C5. (implies (and (tlp (rest x)) (in a (rest x))) (in a (aapp (rest x) y))) C6. (in a x) Derived Context: D1. (tlp (rest x)) { Def tlp, C1, C3 } D2. (in a (rest x)) { Def in, C6, C3, C4 } D3. (in a (aapp (rest x) y)) { C5, D1, D2, MP } Goal: (in a (aapp x y)) Proof: (in a (aapp x y)) = { Def aapp, C1, C3 } (in a (cons (first x) (aapp (rest x) y))) = { Def in, car-cdr axioms, C3 } (or (equal a (first x)) (in a (aapp (rest x) y))) = { D3, PL } t QED |# #| You can skip the Exportation section if no exportation is possible and you can skip then Contract Completion section if that section would be equivalent to the section preceding it. You can skip the Context section if there are no hypotheses, something that rarely happens. You can skip the Derived Context if you have nothing to derive. If you derive nil, you can skip the remaining sections. Finally you need the QED to indicate the end of your proof. You can have multiple proofs in a file, so go ahead and try checking this proof. You will see that conjecture 0 passes but the rest of the conjectures do not because you need to populate the space between the conjectures and the QEDs with a proof. As you complete proofs, click on "Submit File" again to check them. You may have to add hints we normally do not add in class. One example is that you have to sometimes add Contract hints. If you need to use arithmetic, you can just write "arith" or "arithmetic". You can also use any propositional reasoning and can justify it by writing "PL". The proof checker always allows arithmetic and PL reasoning even if you don't provide the hints, but it is good style to do so and we will expect you to do that on exams. Easy layup question. Prove the following using equational reasoning. |# #| Conjecture 1: (equal (llen (aapp x y)) (llen (aapp y x))) QED |# #| Question 2: Prove the following related conjectures. |# #| Conjecture 2a: (implies (endp x) (equal (llen (rrev x)) (llen x))) QED |# #| Conjecture 2b: (implies (tlp x) (implies (and (not (endp x)) (implies (tlp (rest x)) (equal (llen (rrev (rest x))) (llen (rest x))))) (equal (llen (rrev x)) (llen x)))) QED |# #| Question 3: Prove the following related conjectures. |# #| Conjecture 3a: (implies (and (tlp x) (tlp y) (endp x)) (equal (llen (del a (aapp x y))) (+ (llen (del a x)) (llen (del a y))))) QED |# #| Conjecture 3b: (implies (tlp x) (implies (and (not (endp x)) (equal a (car x)) (implies (tlp (rest x)) (implies (tlp y) (equal (llen (del a (aapp (rest x) y))) (+ (llen (del a (rest x))) (llen (del a y))))))) (equal (llen (del a (aapp x y))) (+ (llen (del a x)) (llen (del a y)))))) QED |# #| Conjecture 3c: (implies (tlp y) (implies (and (not (endp x)) (not (equal a (car x))) (implies (and (tlp (rest x)) (tlp y)) (equal (llen (del a (aapp (rest x) y))) (+ (llen (del a (rest x))) (llen (del a y)))))) (equal (llen (del a (aapp x y))) (+ (llen (del a x)) (llen (del a y)))))) QED |#