This is the resource page for Section 2 of Logic and Computation= , CSU 290 (Spring 2008). Welcome.

=20The purpose of this page is to simply complete the lectures, partly to k= eep us in sync with the other section, partly because there is only so much= time and much interesting things to discuss.

=20These notes are meant to supplement the lectures, the readings and the l= ecture notes (available on the course web site) and not = replace them.

=20Feel free to comment at the bottom of the page if you have any questions= or anything is unclear. (Select "Add Comment" under "Add Content" down bel= ow.) I will generally merge your comments and questions into the main text = when I get to them.

=20**What you should do right now**: Make sure you are logged =
into the wiki. (Select "Log In" under "Your Account" below if not, use you =
CCIS credentials to log in.) Look at the bottom of the page, under "Other F=
eatures", top right icon is an envelope. Press that button. That will regis=
ter you as *watching this page*. Basically, every time the page chan=
ges, you get an email saying so. Keeps you from having to check the page re=
gularly.

=20

`~(t=3Dnil)`

Here is a complete formal proof for `~(t=3Dnil)`

using the ax=
ioms I gave in class. (This is the proof that I started on Monday, but ran =
out of time 5 steps into the proof.)

You should be able to understand all the steps in that proof, if not be = able to come up with the proof yourself. We will not ask you to come up wit= h these kind of formal proofs in this course. Instead, we will use the more= informal "chain of equals" or "chain of relations" approach I presented in= class.

=20In the proof below, I write `~A`

for "not `A`

" and=
`A & B`

for "`A`

and `B`

".

=20

1. ~(equal (car (cons x y) x) x) =3D nil [ axiom for equal/car/= cons=20 2. ~(equal (car (cons a b) a) a) =3D nil) [ instantiation of 1 with x= ->a, y->b=20=20

Okay, so 2 is something we will use later on. Let's remember it.

=20=20

3. ~(x =3D y) =3D> (equal x y) =3D nil [ axiom for equ= al=20 4. ~(car (cons a b)) =3D a =3D> (equal (car (cons a b)) a) =3D nil [ instantiation of 3 with x= ->(car (cons a b)), y->a=20 5. ~(~(car (cons a b)) =3D a) [ by MT applied to 4 and 2= =20 6. ~(~A) =3D> A [ tautology of Boolean l= ogic=20 7. ~(~(car (cons a b)) =3D a) =3D> (car (cons a b)) =3D a [ instantiation of 6 with A= ->(car (cons a b))=20 8. (car (cons a b)) =3D a [ by MP applied to 7 and 5= =20 9. x=3Dy =3D> (equal x y) =3D y [ axiom for equal=20 10. (car (cons a b)) =3D a =3D> (equal (car (cons a b)) a) =3D t [ instantiation of 9 with x= ->(car (cons a b)),y->a=20 11. (equal (car (cons a b)) a) =3D t [ by MP applied to 10 and 8=20

Excellent. So now we can see that 2 and 11 together essentially give us =
that `t /=3D nil`

.

We just have to work some to get that to =
come out of the proof.

=20

12. (A & B =3D> C) =3D> (A & ~C =3D> ~B) [= tautology of Boolean logic (check it!)=20 13. ((equal (car (cons a b)) a) =3D t & t =3D nil =3D>=20 (equal (car (cons a b)) a) =3D nil)) [ instantiation of 12 with= =20 =3D> ((equal (car (cons a b)) a) =3D t [ A->(equal (car (= cons a b)) a) =3D t & ~(equal (car (cons a b)) a) =3D nil)) [ B->(t=3Dnil) =3D> ~(t =3D nil)) [ C->(equal (car (= cons a b)) a) =3D nil=20 14. x =3D y & y =3D z =3D> x =3D z [ axiom of tra= nsitivity=20 15. (equal (car (cons a b)) a) =3D t [ instantiation of 14 with= =20 & t =3D nil =3D> [ x->(equal (= car (cons a b)) a) (equal (car (cons a b)) a) =3D nil [ y->t and z->nil 16. (equal (car (cons a b)) a) =3D t [ by MP applied to 13 and 1= 5 & ~(equal (car (cons a b)) a) =3D nil =3D> ~(t =3D nil)=20

And we are just about done. We have both antecedents of the implication = in 16.

=20=20

17. ~(t=3Dnil) [ by MP applied to 16,= 11, and 2=20

=20

Here is what we have seen until now as far as proving theorems are conce= rned.

=20We reviewed Boolean logic and the concept of a tautology of Boolean logi= c. Recall that a tautology is just a Boolean formula that is always true, i= rrespectively of the truth values you give to the Boolean variables in the = formula.

=20We shall take Boolean (aka propositional) reasoning for granted.

=20We introduced the ACL2 logic, as essentially Boolean logic augmented wit= h the ability to reason about basic formulas of the form EXP1 =3D EXP2, whe= re EXP1 and EXP2 are ACL2 expressions.

=20The ACL2 logic is defined formally using the following axioms and rules = of inferences:

=20- =20
- Every tautology of Boolean logic is an axiom =20
`x =3D x`

(reflexivity) =20
`x =3D y =3D> y =3D x`

(symmetry) =20
`x =3D y /\ y =3D z =3D> x =3D z`

(transitivity) =20
`x1 =3D y1 /\ ... /\ xn =3D yn =3D> (f x1 ... xn) =3D (f y1 ...= yn)`

for every function symbol`f`

of arity n =20
- From
`F`

derive`F`

/s (where`F`

is an= arbitrary formula, and s is a substitution of ACL2 expressions for free va= riables in`F`

) =20
- From
`F`

and`F =3D> G`

derive`G`

= (modus ponens) =20

We also have axioms corresponding to the different primitives of the lan= guage. The basic ones are:

=20- =20
`x =3D y =3D> (equal x y) =3D t`

=20
`x /=3D y =3D> (equal x y) =3D nil`

(where`/=3D represents "not equal to")`

`x =3D nil =3D> (if x y z) =3D z`

=20
`x /=3D nil =3D> (if x y z) =3D x`

=20
`(car (cons x y)) =3D x`

=20
`(cdr (cons x y)) =3D y`

=20
`consp (cons x y) =3D t`

=20
`consp (nil) =3D nil`

=20
`(integerp x) =3D t =3D> (consp x)=3Dnil`

=20

```
=20
```

```
=20
```Additionally, we can take as axioms the basic properties of arithmetic t=
hat you have seen in high school and discrete maths. Thus, when proving the=
orems, you will be free to perform standard simplification of arithmetic.=20

A formal proof of `F`

is a sequence of formulas such that eve=
ry formula in the sequence is either an axiom or derived from previous form=
ulas using an inference rule, and such that the last formula of the sequenc=
e is `F`

itself.

=20
I gave you a formal proof of `t /=3D nil`

above. We shall not=
write a lot of formal proof, and you certainly will not have to write any =
of them.

=20
Instead, we shall use some proof techniques to prove formulas that have =
a certain form. These techniques do not work for all formulas, but they wor=
k for enough of them to be interesting.

=20
**If the formula you want to prove is of the form EXP1 =3D EXP2, then one technique is to use a sequence of equalities to equate EXP=
1 and EXP2:**

**=20
=20
** EXP1
=3D=20
....
=3D=20
EXP2

=20
=20
where all the equalities are justified using the axioms or the inference=
rules above. By transitivity of =3D, this clearly shows that EXP1 =3D EXP2=
.

=20
Alternatively, it is sometimes easier to simplify both EXP1 and EXP2 int=
o a common expression EXP3.

=20
=20
EXP1=20
=3D=20
...
=3D=20
EXP3
EXP2
=3D=20
...
=3D=20
EXP3

=20
=20
Again, it should be pretty clear that this proves that EXP1 =3D EXP2. (B=
y transitivity of =3D once again.)

=20
**If the formula you want to prove is of the form HYPS =3D> EXP=
1 =3D EXP2**, where HYPS is some hypotheses (formulas), then you can=
use a variant of the above, that is, prove that EXP1 =3D EXP2 using a sequ=
ence of equalities (or simplify EXP1 and EXP2 to the same expression EXP3),=
except that when you derive the equalities you can in addition to the axio=
ms and inference rules use the hypotheses in HYPS to help you.

=20

=20
## Feb=
ruary 25: Solutions to Exam 3 Proof Questions

=20
Recall the definitions:

=20
=20
(defun add99 (l)
(if (endp l)
nil
(cons (cons 99 (car l)) (add99 (cdr l)))))
(defun same-lenp (l n)
(if (endp l)
t
(if (equal (len (car l)) n)
(same-lenp (cdr l) n)
nil)))
(defun len (l)
(if (endp l)
0
(+ 1 (len (cdr l)))))

=20
=20
Question 2. Prove ```
(consp x) =3D> (len (car (add99 x))) =3D (+ (=
len (car x)) 1)
```

=20
=20
(len (car (add99 x)))
=3D {def of add99 }
(len (car (if (endp x) nil (cons (cons 99 (car x)) (add99 (cdr x))))))
=3D { (endp x) =3D nil }
(len (car (cons (cons 99 (car x)) (add99 (cdr x)))))
=3D {car-cons axiom}
(len (cons 99 (car x)))
=3D {def of len }
(if (endp (cons 99 (car x)))
0
(+ 1 (len (cdr (cons 99 (car x))))))
=3D {endp(cons ...)=3Dnil}
(+ 1 (len (cdr (cons 99 (car x)))))
=3D {cdr-cons axiom}
(+ 1 (len (car x)))

=20
=20
Question 3. Prove `(endp x) =3D> (same-lenp (add99 x) y)`

<=
/p>=20

=20
(same-lenp (add99 x) (+ y 1))
=3D {def of add99}
(same-lenp (if (endp x) nil ...))
=3D { (endp x) =3D t }
(same-lenp nil (+ y 1))
=3D {def of same-lenp }
(if (endp nil) t ...)
=3D { (endp nil)=3Dt }
t

=20
=20
Question 4. Prove ```
((same-lenp x y) /\ (consp x) /\ (same-lenp (add=
99 (cdr x)) (+ y 1))) =3D> (same-lenp (add99 x) (+ y 1))
```

=20
(You can use the fact that ```
((same-lenp x y) /\ (consp x)) =3D> =
(+ 1 (len (car x))) =3D (+ 1 y)
```

.)

=20
=20
(same-lenp (add99 x) (+ y 1))
=3D {def of add99}
(same-lenp (if (endp x) nil (cons (cons 99 (car x)) (add99 (cdr x)))) (+ =
y 1))
=3D {(endp x) =3D nil}
(same-lenp (cons (cons 99 (car x)) (add99 (cdr x))) (+ y 1))
=3D {def of same-lenp}
(if (endp (cons (cons 99 (car x)) (add99 (cdr x))))
t
(if (=3D (len (car (cons (cons 99 (car x)) (add99 (cdr x))))) (+ y 1))
(same-lenp (cdr (cons (cons 99 (car x)) (add99 (cdr x)))) (+ y 1))
nil))
=3D { (endp (cons ...)) =3D nil }
(if (=3D (len (car (cons (cons 99 (car x)) (add99 (cdr x))))) (+ y 1))
(same-lenp (cdr (cons (cons 99 (car x)) (add99 (cdr x)))) (+ y 1))
nil)
=3D { car-cons and cdr-cons axioms}
(if (=3D (len (cons 99 (car x))) (+ y 1))
(same-lenp (add99 (cdr x)) (+ y 1))
nil)
=3D { def of len }
(if (=3D (if (endp (cons 99 (car x)))
0
(+ 1 (len (cdr (cons 99 (car x)))))) (+ y 1))
(same-lenp (add99 (cdr x)) (+ y 1)))
nil)
=3D { (endp (cons ...)) =3D nil
(if (=3D (+ 1 (len (cdr (cons 99 (car x)))) (+ y 1)))
(same-lenp (add99 (cdr x)) (+ y 1)))
nil)
=3D { car-cons axiom }
(if (=3D (+ 1 (len (car x)) (+ 1 y)))
(same-lenp (add99 (cdr x)) (+ y 1)))
nil)
=3D { by fact above }
(same-lenp (add99 (cdr x)) (+ y 1))
=3D { by hypothesis }
t

=20
=20

=20
## February 26: On Term=
ination

=20
Here is the argument that, at least in Scheme, it is impossible to write=
a function that correctly determines whether another function terminates. =
We argue by contradiction.

=20
Suppose that we could write a function (terminates? f x) that returns #t=
(true) when (f x) terminates, and returns #f (false) when (f x) does not t=
erminate. I don't care how terminates? is written - just suppose you manage=
d to write it. I will not show that you get something completely absurd as =
a result.

=20
In particular, I can now write the following perfectly legal scheme func=
tion:

=20
=20
(define (loop-forever) (loop-forever))
(define (oops f x)
(if (terminates? oops empty)
(loop-forever)
1))

=20
=20
My question: does (oops empty) terminate?

=20
Let's see. It either does or doesn't. So let's consider both cases.

=
=20
=20
- If (oops empty) terminates, then by assumption (terminates? oops empty)=
must be true, and therefore, by the code of oops, (oops empty) must loop f=
orever, i.e., not terminate, contradicting that (oops empty) terminates.=20

=20
=20
- if (oops empty) does not terminate, then by assumption (terminates? oop=
s empty) must be false, and therefore by the code of oops, (oops empty) ret=
urns 1 immediately, i.e., terminates, contradicting that (oops empty) does =
not terminate.
=20

=20
Because we get a contradiction no matter what, it must be that what we i=
nitially assumed was wrong, i.e., that terminates? works correctly. In othe=
r words, we cannot write a correct terminates? function in Scheme.

=20
It turns out that this argument can be made to work for any programming =
language, but you'll have to wait for CSU 390 to see it.

=20
One approach to arguing that a recursive function terminates is to argue=
that we are making progress towards the base case. The design recipe that =
we gave you and that you learned in 211 is in fact meant to ensure exactly =
this, at least for the kind of functions that we have seen until now.

=
=20
It is sometimes a little subtle to argue that you are indeed making prog=
ress towards termination. In particular, consider the following ACL2 functi=
on:

=20
=20
(defun foo (n)
(cond ((zp n) 0)
((=3D n 1) 1)
((evenp n) (foo (/ n 2)))
((oddp n) (foo (+ n 1)))))

=20
=20

`(Assume that we have correct definitions for `

.) I claim that this terminates for all inputs. Clearly, if th=
e input is not a natural number, it terminates immediately. (Why?) Otherwis=
e, can we argue that we are making progress towards the base cases (either =
0 or 1)? Here are two arguments: the first, the one raised in class on Mond=
ay, is that that even though when the input is odd the recursive call is do=
ne on a bigger number (that therefore does not immediately progresses towar=
ds the base case), (foo (+ n 1)) will be called on an even number, which me=
ans that at the following iteration, foo will be invoked on (/ (+ n 1) 2), =
which is smaller than n. Thus, even though at every step we are not making =
progress towards the base case, we are making progress towards the base cas=
e at either every step or every two steps, depending on whether the input i=
s even or odd. That's actually sufficient to establish termination. (Why?)<=
/p>=20
`evenp`

and

Here's another way of thinking about it that actually shows progress tow= ards termination at every step. Write the input as a binary number, and con= sider the following number <n> derived from the input n:

=20=20

<n> =3D the number of 1's in the binary representation of n + 2 * (the length of n in binary) - the number of 0's in the binary representation of n to the right = of the rightmost 1.=20

Thus,

=20- =20
- 4 is 100 in binary, so <4> =3D 1 + (2 * 3) - 2 =3D 1 + 6 - 2 =3D = 5, =20
- 5 is 101 in binary, so <5> =3D 2 + (2 * 3) - 0 =3D 2 + 6 =3D 8,=20
- 6 is 110 in binary, so <6> =3D 2 + (2 * 3) - 1 =3D 2 + 6 - 1 =3D = 7. =20

You can check that at every recursive step of the function, foo is calle= d on an input n whose <n> is strictly smaller than the original input= to the function. And we are making progress towards the base case, with &l= t;1> =3D 3.

=20However, this doesn't work for every function, even those that look simi= lar to the above. One of the most famous examples is the following so-calle= d Collatz function:

=20=20

(defun collatz (n) (cond ((zp n) 0) ((=3D n 1) 1) ((evenp n) (collatz (/ n 2))) ((oddp n) (collatz (+ (* 3 n) 1)))))=20

It is unknown whether this function terminates on all inputs. Plot out a= few calls for small values of n, and you'll get a sense for how long some = of the iterations take. Termination has been checked for all natural number= s up to 10^16, but for all we know it fails to terminate on some input grea= ter than 10^17. We just don't know enough about number theory to say anythi= ng else.

=20I posted some more mathematical references to this function here.

=20=20

```
(len (add1 =
a)) =3D (len a)
```

I went over it quickly at the end of lecture today, so it pays to look a= t it more slowly.

=20Recall the definitions I gave in class:

=20=20

(defun len (l) (if (endp l) 0 (+ 1 (len (cdr l))))) (defun add1 (l) (if (endp l) l (cons (+ 1 (car l)) (add1 (cdr l)))))=20

I claimed that in order to prove that `(len (add1 a)) =3D (len a), it suffices to prove the following two theorems:`

```
=20
=20
``` Add1EndP: (endp a) =3D> (len (add1 a)) =3D (len a)
Add1ConsP: (consp a) /\ (len (add1 (cdr a))) =3D (len (cdr a)) =3D> =
(len (add1 a)) =3D (len a)

=20
=20
We saw that these are actually quite easy to prove. (Do it again if you'=
re shaky on the details.)

=20
We need to argue, though, that `Add1EndP`

and ```
Add1ConsP=
```

together give you that `(len (add1 a)) =3D (len a)`

for =
all possible `a`

in the ACL2 universe.

=20
We are going to argue this by contradiction. So assume that it is *no=
t* the case that `(len (add1 a)) =3D (len a)`

for all ```
=
a
```

.

=20
Let A be the set of all values in the ACL2 universe for which ```
((le=
n (add1 a))
```

is not equal to `(len a)`

. By assumption, A i=
s not empty.

=20
Let `s`

be an element of A that has smallest length amongst a=
ll elements of A. (If more than one element has smallest length, pick any o=
f them.)

=20

`First off, we know that `

must be a cons pair, that is, `s`

cannot be an atom. Why? Because w=
e proved `Add1EndP`

, which says that atoms cannot be in A. So `(consp s) =3D t`

.=20

Because `s`

is a cons pair, `(cdr s)`

must have le=
ngth strictly less than that of `s`

. Because `s`

was =
chosen to have smallest length in A, then `(cdr s)`

cannot be in=
A.

But because `(cdr s)`

is not in A, then it must be that ```
(len (add1 (cdr s))) =3D (len (cdr s)). (Recall how we defined A in=
the first place.)
```

So we know that `(consp s) =3D t`

, and that ```
(len (add1 =
(cdr s))) =3D (len (cdr s))
```

. But we proved `Add1Consp`

, w=
hich says that it must be the case that `(len (add1 s)) =3D (len s). And this contradicts the fact that `

`s`

is in A in the firs=
t place!

```
=20
```We derive a contradiction, so what we assumed in the first place must be=
false - so there cannot be *any* `a`

such that ```
(le=
n (add1 a))
```

is not equal to `(len a)`

, that is, ```
(le=
n (add1 a)) =3D (len a)
```

for all `a`

in the universe.

=
=20

=20
## March 11: Some=
Easy Proof Exercises

=20
Consider the following definitions:

=20
=20
(defun andp (x y)
(if x
(if y t nil)
nil))
(defun orp (x y)
(if x
t
(if y t nil)))

=20
=20
Make sure you understand them. You can assume the following properties a=
bout `andp`

and `orp`

:

=20
=20
(booleanp (andp x y))
(andp x y) =3D (andp y x)
(booleanp (orp x y))
(orp x y) =3D (orp y x)

=20
=20
**EDIT**: Let me add the following properties that you can =
assume too:

=20
=20
(booleanp z) =3D> (andp z t) =3D z
(booleanp z) =3D> (andp t z) =3D z
(booleanp z) =3D> (orp z nil) =3D z
(booleanp z) =3D> (orp nil z) =3D z

=20
=20
(You can give a shot at proving these, but the proof is a bit different =
than what we're used to - it requires case analysis, that you can do using =
only Boolean reasoning. For now, just take the properties above as true. I =
will talk about the proof technique for this in some other entry below.)=20

Now, let's write a function that applies `andp`

to a list of =
values, so that it returns true exactly when not all values in the list are=
nil.

=20
=20
(defun and-foldp (l)
(if (endp l)
t
(andp (car l) (and-foldp (cdr l)))))

=20
=20
Note what happens when we evaluate `(and-foldp '())`

, or when=
we evaluate `(and-foldp 5)`

, or when we evaluate ```
(and-fol=
dp '(t))
```

.

=20
Let's do something similar for `orp`

:

=20
=20
(defun or-foldp (l)
(if (endp l)
nil
(orp (car l) (or-foldp (cdr l)))))

=20
=20
Again, note what happens when we evaluate `(or-foldp '())`

, o=
r when we evaluate `(or-foldp 5)`

, or when we evaluate ```
(or=
-foldp '(t))
```

.

=20
Let's prove some theorems. (Many of these are proof obligations obtained=
from the induction principle - can you identify the formula that these pro=
of obligations end up proving?) Make sure that you understand what the theo=
rem you are trying to prove is actually saying! Otherwise, this exercise is=
just meaningless symbol pushing, which is going to be excruciatingly borin=
g.

=20
=20
`(endp x) =3D> (booleanp (and-foldp x))`

=20
```
(consp x) & (booleanp (and-foldp (cdr x))) =3D> (booleanp =
(and-foldp x))
```

=20
`(endp x) =3D> (booleanp (or-foldp x))`

=20
```
(consp x) & (booleanp (or-foldp (cdr x))) =3D> (booleanp (=
or-foldp x))
```

=20
`(and-foldp (cons a b)) =3D (andp a (and-foldp b))`

=20
`(or-foldp (cons a b)) =3D (orp a (or-foldp b))`

=20

=20
Prove the following theorems, using the standard definition of ```
app=
```

:

=20
=20
(defun app (x y)
(if (endp x)
y
(cons (car x) (app (cdr x) y))))

=20
=20
=20
```
(endp x) =3D> (and-foldp (app x y)) =3D (andp (and-foldp x) (a=
nd-foldp y))
```

=20
```
(consp x) & (and-foldp (app (cdr x) y)) =3D (andp (and-foldp =
(cdr x)) (and-foldp y)) =3D> (and-foldp (app x y)) =3D (andp (and-foldp =
x) (and-foldp y))
```

=20
```
(endp x) =3D> (or-foldp (app x y)) =3D (orp (or-foldp x) (or-f=
oldp y))
```

=20
```
(consp x) & (or-foldp (app (cdr x) y)) =3D (orp (or-foldp (cd=
r x)) (or-foldp y)) =3D> (or-foldp (app x y)) =3D (orp (or-foldp x) (or-=
foldp y))
```

=20

=20
**EDIT**: note that proving the above gives you that the fo=
llowing two theorems are true:

=20
=20
`(and-foldp (app x y)) =3D (andp (and-foldp x) (and-foldp y))`

```
=20
````(or-foldp (app x y)) =3D (orp (of-foldp x) (or-foldp y))`

=20

```
=20
```These may come in handy in the proofs of the next theorems.

=20
For the next few theorems, you will want to prove the following lemma fi=
rst:

=20
=20
`(consp x) =3D> (app (list (car x)) (cdr x)) =3D x`

=
=20

=20
(Recall that `(list z)`

is just an abbreviation for ```
(co=
ns z nil)
```

. You can use the following axiom for cons: ```
(consp x)=
=3D> (cons (car x) (cdr x)) =3D x
```

.)

=20
Use the standard definition of `rev`

:

=20
=20
(defun rev (x)
(if (endp x)
nil
(app (rev (cdr x)) (list (car x)))))

=20
=20
Prove the following theorems:

=20
=20
`(endp x) =3D> (and-foldp (rev x)) =3D (and-foldp x)`

=20
```
(consp x) & (and-foldp (rev (cdr x))) =3D (and-foldp (cdr x))=
=3D> (and-foldp (rev x)) =3D (and-foldp x)
```

=20
`(endp x) =3D> (or-foldp (rev x)) =3D (or-foldp x))`

=
=20
```
(consp x) & (or-foldp (rev (cdr x))) =3D (or-foldp (cdr x)) =
=3D> (or-foldp (rev x)) =3D (or-foldp x)
```

=20

=20

=20
## (rev(revx))=3D=
x">March 17: Proof of `(true-listp x) =3D> (rev (rev x)) =3D x`

```
=20
```Here is the proof of `(true-listp x) =3D> (rev (rev x)) =3D x that I did in class, complete with all auxiliary lemmas.`

```
=20
```We proceed by induction on `x`

, meaning that we have to prove=
the following proof obligations:

=20
=20
`(endp x) & (true-listp x) =3D> (rev (rev x)) =3D x`

<=
/li>=20
```
(consp x) & ((true-listp (cdr x)) =3D> (rev (rev (cdr x)))=
=3D (cdr x)) & (true-listp x) =3D> (rev (rev x)) =3D x
```

=
=20

=20
**Proof** of ```
(endp x) & (true-listp x) =3D> (r=
ev (rev x)) =3D x
```

:

=20
=20
(rev (rev x))
=3D { by def of rev, if axiom, hypothesis}
(rev nil)
=3D { by def of rev }
nil
=3D { by lemma 1 below, (endp x) & (true-listp x) =3D> x =3D nil }
x

=20
=20
This proof relies on the following lemma, which says that if we have a t=
rue list and it is an atom, then it must be `nil`

. Note that we =
use this lemma to add a new result to the *context*, that is, to the=
set of known facts that include the hypotheses.

=20
**Proof** of Lemma 1: ```
(endp x) & (true-listp x) =
=3D> x =3D nil
```

=20
=20
We first prove that (endp x) & (true-listp x) =3D> (equal x nil=
) =3D t:
t=20
=3D {by hypothesis}
(true-listp x)
=3D {by def of true-listp, hypothesis, if axiom}
(equal x nil)
This gives us that (equal x nil) =3D t, that is, x =3D nil (by the equal ax=
iom).

=20
=20
Back to the main proof, where we now have to prove the inductive case:=20

**Proof** of ```
(consp x) & ((true-listp (cdr x)) =
=3D> (rev (rev (cdr x))) =3D (cdr x)) & (true-listp x) =3D> (rev =
(rev x)) =3D x
```

:

=20
=20
(rev (rev x))
=3D {by def of rev, hypothesis, if axiom}
(rev (app (rev (cdr x)) (list (car x))))
=3D {by Lemma 2 below}
(app (rev (list (car x))) (rev (rev (cdr x))))
=3D {by induction hypothesis, knowing that (true-listp (cdr x)) using Lemm=
a 3 below}
(app (rev (list (car x))) (cdr x))
=3D {by def of rev}
(app (list (car x)) (cdr x))
=3D {by def of app}
(cons (car x) (cdr x))
=3D {by cons axiom, knowing that (consp x)}
x

=20
=20
The proof uses two lemmas. Let's take care of the third lemma first.

=
=20
**Proof** of Lemma 3: ```
(true-listp x) & (consp x) =
=3D> (true-listp (cdr x))
```

:

=20
=20
t
=3D {by hypothesis}
(true-listp x)
=3D {by def of true-listp, hypothesis, if axiom}
(true-listp (cdr x))

=20
=20
That was easy. Slightly harder is lemma 2, the one that Eric proved on t=
he board today.

=20
**Proof** of Lemma 2: ```
(rev (app a b)) =3D (app (rev b=
) (rev a))
```

:

=20
=20
By induction on a. (Why?)
Base case: (endp a) =3D> (rev (app a b)) =3D (app (rev b) (rev a))
Let's prove that both sides equal a common value.
(rev (app a b))
=3D {by def of app, hypothesis, if axiom}
(rev b)
(app (rev b) (rev a))
=3D {by def of rev, hypothesis, if axiom}
(app (rev b) nil)
=3D {by lemma (true-listp x) =3D> (app x nil) =3D x, knowing that (rev =
b) is a true-listp by Lemma 4 below}
(rev b)
Inductive case: (consp a) & (rev (app (cdr a) b)) =3D (app (rev b) (rev=
(cdr a))) =3D>=20
(rev (app a b)) =3D (app (rev b) (rev a))
Again, we prove that both sides equal a common value.
(rev (app a b))
=3D {by def of app, hypothesis, if axiom}
(rev (cons (car a) (app (cdr a) b)))
=3D {by def of rev, endp axiom, if axiom, car-cons axiom}
(app (rev (app (cdr a) b)) (list (car a)))
=3D {by induction hypothesis}
(app (app (rev b) (rev (cdr a))) (list (car a))
(app (rev b) (rev a))
=3D {by def of rev, hypothesis, if axiom}
(app (rev b) (app (rev (cdr a)) (list (car a))))
=3D {by lemma (app a (app b c)) =3D (app (app a b) c)}
(app (app (rev b) (rev (cdr a))) (list (car a)))

=20
=20
All that's missing now is Lemma 4, that says that `(rev b)`

i=
s a true list for any `b`

. I left it as an exercise for you to p=
rove for next time.

=20

=20
## April 9: Topics for Ex=
am #6

=20
Topics covered include everything we have learned about the ACL2s theore=
m prover, lectures 25 to 29 on the web page; of course, you should not forg=
et the basics of proving theorems.

=20
Here are the main things we will test.

=20
=20
- Understanding ACL2s proof attempts

That was the largest component o=
f these last two weeks.

In particular, understand the waterfall model =
(cf lecture 25), and be able to extract le=
mmas to be proved when ACL2s is stuck on a proof. =20
- Understand rewriting

Cf lecture 26=
and the textbook, and see below. =20
- Understand decision procedures for propositional reasoning and congruen=
ce closure

Cf lecture 29 and see below=
. =20

=20
### Rewriting

=20
Recall that when you prove a theorem (possibly with hypotheses) with a c=
onclusion of the form LHS =3D RHS, this defines a rewrite rule that rewrite=
s occurrences of LHS into RHS. (Note the direction!) Variables in the LHS a=
re taken to be placeholders, that can be substituted for when rewriting hap=
pens.

=20
The sequencing of rewrites when rewriting happens is important. The two =
main rules are:

=20
=20
- Rewriting occurs for inner expressions before outer expressions. Thus, =
if you have an expression
`(f (g x))`

, the rewriter will attempt=
to rewrite `(g x)`

first, and then attempt to rewrite ```
(f =
...)
```

. =20
- Rewriting occurs with the
**latest** rewrite rules defined=
tried first, all to way to the oldest rewrite rules. In other words, if tw=
o (or more) rewrite rules are applicable to a given expression, the most re=
cently admitted rewrite rule is used. =20

=20
### De=
cision Procedure for Propositional Reasoning

=20
How does ACL2s decided whether a Boolean expression is a tautology or no=
t? It could build a truth table, but it doesn't. (Well, actually, it almost=
does - it just uses a more efficient representation than a truth table, th=
at contains essentially the same information.) Here's how it does it. For s=
implicity, here, I will only consider the case where there are no occurrenc=
e of functions others than `implies`

, `and`

, ```
no=
t
```

, and `or`

in the Boolean expression. (It's an interesti=
ng exercise to figure out what happens when you do allow other functions.)<=
/p>=20

First, it rewrites the Boolean expression so that it does not contain an=
y `implies`

, `and`

, `or`

, and ```
not. It does so by replacing every occurrence of those functions by a corr=
esponding
````if`

expression. Here are the replacements:

```
=20
=20
```(implies X Y) -> (if X Y t)
(and X Y) -> (if X Y nil)
(or X Y) -> (if X t Y)
(not X) -> (if X nil t)

=20
=20
(Convince yourself that these are correct by trying out a few examples, =
that is, seeing whether `(or t nil)`

evaluates to `t`

=
when replaced by the corresponding `if`

expression, etc.)

T=
hus, for example:

=20
=20
(and (not a) a) =3D (if (if a nil t) a nil) # expanding out and an=
d not

=20
=20
Once that is done, you are left with a bunch of `if`

expressi=
ons. For reasons that will become clear, we want to simplify the *condit=
ion* of those `if`

expressions as much as possible. In parti=
cular, we want all `if`

to have simple variables as conditions. =
To do so, we will apply the following transformation to an `if`

=
expression that has a non-variable as a condition. (If it's not a variable,=
it has to be an `if`

expression itself.)

=20
=20
(if (if X Y Z) V W) -> (if X (if Y V W) (if Z V W))

=20
=20
(Convince yourself that you understand why applying this transformation =
does not change the value returned by the whole expression.)

Do this re=
peatedly until all `if`

expressions have a variable (or ```
t<=
/code> or
````nil`

) as a condition.

Continuing our example abov=
e:

```
=20
=20
```(and (not a) b) =3D (if (if a nil t) a nil) # expanding out and and=
not
=3D (if a # applying transformation ab=
ove
(if nil a nil)
(if t a nil))

=20
=20
Now, let's simplify things further.

First, take every `if expression, from the `*outermost* to the *innermost*:

```
=20
```

```
=20
```- if the expression is of the form
`(if t X Y)`

, replace it by=
`X`

, and repeat going into `X`

. =20
- if the expression is of the form
`(if nil X Y)`

, replace it =
by `Y`

, and repeat going into `Y`

. =20

`if the expression is of the form ``(if v X Y)`

, where ```
v=
```

is a variable, replace every occurrence of `v`

in ```
=
X
```

by `t`

and every occurrence of `v`

in ```
=
Y
```

by `nil`

, and repeat (going into `X`

and Y

). =20

=20
Continuing our example:

=20
=20
(and (not a) b) =3D (if (if a nil t) a nil) # expanding out and and=
not
=3D (if a # applying transformation ab=
ove
(if nil a nil)
(if t a nil))
=3D (if a # replacing a by t in THEN c=
lause=20
(if nil t nil)
(if t a nil))
=3D (if a # replacing a by nil in ELSE=
clause
(if nil t nil)
(if t nil nil))
=3D (if a # (if nil t nil) -> nil
nil =20
(if t nil nil))
=3D (if a nil nil) # (if t nil nil) -> nil

=20
=20
When you're done all of this, you have an expression with only ```
if<=
/code> expressions and with the property that for any "path" through the co=
nditionals, you encounter every variable only once, in the condition of an =
````if`

. A Boolean expression is a tautology exactly when every "pa=
th" through the conditionals lead to a value that is guaranteed to be non-n=
il.

```
=20
```If a branch has a return value that is not guaranteed to be non-nil (for=
instance, it is `nil`

, or it is a variable), you can read off a=
counter example (that is, an assignment of truth values to variables that =
makes the Boolean expression false) by looking at the "path" through the co=
nditionals that led to the values that is not guaranteed to be non-nil, set=
ting a variable to `t`

if you ended up going to the THEN branch =
of the conditional, or to `nil`

if you ended up going to the rig=
ht branch of the conditional.

=20
Thus, in the above example, we ended up with `(if a nil nil)`

=
; there are two "paths" into this conditional that lead to a value not guar=
anteed to be non-nil. One of those "path" is obtained by setting `a to ``t`

, and the other is obtained by setting `a`

=
to `nil`

. It's easy to check that both of those assignments to =
`a`

are counterexamples to the initial expression being a tautol=
ogy.

```
=20
```For a more complex example, consider ```
(implies (or (not a) b) (or a=
(not b)))
```

.

If you work through the above steps, you get the sim=
plified form `(if a (if b t t) (if b nil t))`

. There is one "pat=
h" in the conditionals that lead to a value not guaranteed to be non-nil, a=
nd that's the "path" that leads to the `nil`

, which is obtained =
by setting `a`

to `nil`

and setting `b`

to=
`t`

. And you can check that `a=3Dnil,b=3Dt`

is a cou=
nterexample to the initial conjecture.

=20
### Decision Pro=
cedure for Equivalences

=20
This decision procedure is used to establish whether an implication wher=
e the hypotheses are equalities and the conclusion is also an equality is t=
rue, in the special case where this information can be decided without rely=
ing on the definition of the functions in the expression. (For instance, th=
is may be interesting when we have *no* definition for the functions=
in the expression; that's what `defstub`

does, by the way, it "=
defines" a function without actually giving an actual definition.)

=20
Let's be more concrete. Suppose that we have no information about functi=
ons `f`

and `g`

, but we are asked to prove that:

=
=20
=20
(implies (and (=3D a c)
(=3D (f a) b)
(=3D (g c) c)
(=3D (f (g a)) b))

=20
=20
Here's an argument that us humans can come up with easily, written in in=
fix notation to simplify the presentation:

=20
=20
(f (g c)) =3D (f (g a)) # because a =3D c
=3D (f c) # because (g c) =3D c
=3D (f a) # because a =3D c
=3D b # because (f a) =3D b

=20
=20
No problem. How does ACL2s prove it, though? It uses a procedure called =
*congruence closure*. It has the advantage of working for an arbitra=
ry equivalence relation, not just equality.

=20
You can find precise definitions of the congruence closure algorithm in =
many places. See these slides on congru=
ence closure if you are curious. I will describe it at a very high leve=
l here.

=20
First off, take the formula you have, and extract all the subterms in it=
. The subterms are all the function applications that occur in the expressi=
on, and all the constants. List them all, the order is not important. Here =
are the subterms in the example above, listed in roughly in order of increa=
sing complexity:

=20
=20
a =20
b =20
c =20
(f a) =20
(g c) =20
(g a) =20
(f (g a))

=20
=20
Note that `(g a)`

is a subterm because it appears in ```
(f=
(g a))
```

.

=20
Good. Now, the procedure is to repeatedly look at the equations in the h=
ypotheses (there are three in our example), and "lump" together the terms i=
n our list that the equation force to be equal. Lumping terms together may =
lead to further lumping, because new things may be made equal that we didn'=
t know before were equal.

=20
Let's start. Let's look at the first equation `a =3D c`

. It t=
ells you to lump together `a`

and `c`

. Let's do that:=

=20
=20
a c =20
b =20
(f a) =20
(g c) =20
(g a) =20
(f (g a))

=20
=20
I am representing lumps by putting terms on the same line. Terms lumped =
together are simply terms that can be proved to be equal using the equation=
s we have been looking at. Knowing that `a`

and `c`

a=
re equal tells you also that `(g a)`

and `(g c)`

are =
equal, so we can lump those two together too:

=20
=20
a c =20
b =20
(f a) =20
(g c) (g a) =20
(f (g a))

=20
=20
That's it, we cannot lump things together any further based on what we k=
now.

=20
Let's look at the second equation, `(f a) =3D b`

. It tells yo=
u to lump together `(f a)`

and `b`

. Easy enough:

=
=20
=20
a c =20
b (f a) =20
(g c) (g a) =20
(f (g a))

=20
=20
That's it, we cannot lump things together any further.

=20
Let's look at the last equation, `(g c) =3D c`

. It tells you =
to lump together `(g c)`

and `c`

. Now, because ```
=
c
```

is already lumped with something, and `(g c)`

is also a=
lready lumped with something, let's merge the respective lumps. (After all,=
lumping just means that things can be proved equal.)

=20
=20
a c (g c) (g a) =20
b (f a) =20
(f (g a))

=20
=20
Oh, now we've learned a lot, in particular, that `(g a) =3D a. This means that ``(f (g a)) =3D (f a)`

, so that we can lump (f a)

and `(f (g a))`

together:

=20
=20
a c (g c) (g a) =20
b (f a) (f (g a))

=20
=20

```
And that's it, we cannot lump things any further. And we've exhausted al=
l of our equations in the hypotheses. So the lumps above represent all the =
different things that can be proved equal to each other. Our conjecture ask=
s whether the three equations imply that
````(f (g a)) =3D b`

; in o=
ther words, do the three equations ensure that `(f (g a))`

and <=
code>b

are lumped together by the above procedure? It is easy to see=
that yes, they are. Therefore, the algorithm (and ACL2s) will report that =
the conjecture is true.

=20

=20
## April 21: Study Guide

=
=20
As requested by a few students, here is a quick study guide for the fina=
l. (There is nothing here that has not been said already in class.) As we m=
entioned in class, the final will be a cross-section of all the tests we ha=
ve had during the semester. Roughly, there should be one question per exam.=

=20
So what did those tests cover?

=20
**Test 1:**

=20
=20
- the basics of the ACL2 programming language
=20
- total functions,
=20
- the use of the design recipe to develop functions
=20

=20
**Test 2:**

=20
=20
- lists and true lists
=20
- quotation
=20
- design recipe for recursive functions over true lists
=20

=20
**Test 3:**

=20
=20
- Boolean logic
=20
- proving theorems using equational reasoning
=20
- falsifying conjectures
=20

=20
**Test 4:**

=20
=20
- the induction principle (give proof obligations)
=20
- proving proof obligations
=20

=20
**Test 5:**

=20
=20
- more difficult inductions (idenfitication of lemmas)
=20
- generalization
=20
- using different substitutions in the inductive proof obligation
=20

=20
**Test 6:**

=20
=20
- The ACL2s theorem prover and the waterfall model
=20
- rewriting
=20
- understanding proof reports, including identifying interesting checkpoi=
nts
=20
- decision procedures for Boolean logic and congruence closure
=20