#|

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 upcoming 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)))))

" in is now predefined.

We will assume it is defined as:

(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 justification hint is "Def llen".
When you use a contract theorem, say for llen, your hint is
"Contract llen". The contract hints are often omitted, but it would
be good to point them out, so that you understand every single step
that's involved in having a complete proof.

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 tell ACL2s (and the proof checker, see below)
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. Ask questions on piazza
for any issues you encounter with the proof checker. We will not
require that your homework proofs pass the proof checker. The proof
checker is provided for you as an extra tool to help you practice
and check your proofs before hand.

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.

As a test, you should be able to submit this lab file already to the
proof checker without any change (even prior to entering your solutions)
and the proof checker should prove the example Conjecture 0 below.
It should give you warnings for the other conjectures that your proofs
are empty. Run the proof checker again when you enter your own proofs.

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).
Similarly, instead of x+y you will need to write (+ x y), instead of
true you will need to write t, instead of false nil, etc. 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.

We 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)) { 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
|#