Date: Sun, 5 Feb 2023 06:47:33 -0500 (EST) Message-ID: <361859046.3629.1675597653700@maestro.ccs.neu.edu> Subject: Exported From Confluence MIME-Version: 1.0 Content-Type: multipart/related; boundary="----=_Part_3628_92118173.1675597653699" ------=_Part_3628_92118173.1675597653699 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Content-Location: file:///C:/exported.html CSU 290 (Spring 2008)

# CSU 290 (Spring 2008)

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

=20

The 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.

=20

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

=20

Feel 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
=20

## February = 15: Formal Proof for `~(t=3Dnil)`

=20

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

=20

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.

=20

In the proof below, I write `~A` for "not `A`" and= `A & B` for "`A` and `B`".

=20
=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
=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
=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
=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
=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
=20

## February 2= 0: Review of Proving Theorems

=20

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

=20

We 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.

=20

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

=20

We 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.

=20

The 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
=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")`
• ```=20 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 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 evenp and oddp`.) 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

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
=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
=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.

=20

However, 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
=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.

=20

I posted some more mathematical references to this function here.

=20
=20

## February 27: The Final Bit of the Proof that ```(len (add1 = a)) =3D (len a)```

=20

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

=20

Recall the definitions I gave in class:

=20
=20
```  (defun len (l)
(if (endp l)
0
(+ 1 (len (cdr l)))))

(if (endp l)
l
(cons (+ 1 (car l))
```
=20
=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 s cannot be an atom. Why? Because w= e proved Add1EndP, which says that atoms cannot be in A. So s``` must be a cons pair, that is, `(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.

=20

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

=20

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 ```
------=_Part_3628_92118173.1675597653699--