...

`(endp x) => (and-foldp (rev x)) = (and-foldp x)`

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

`(endp x) => (or-foldp (rev x)) = (or-foldp x))`

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

...

## March 17: Proof of `(true-listp x) => (rev (rev x)) = x`

Here is the proof of `(true-listp x) => (rev (rev x)) = x`

that I did in class, complete with all auxiliary lemmas.

We proceed by induction on `x`

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

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

`(consp x) & ((true-listp (cdr x)) => (rev (rev (cdr x))) = (cdr x)) & (true-listp x) => (rev (rev x)) = x`

**Proof** of `(endp x) & (true-listp x) => (rev (rev x)) = x`

:

No Format |
---|

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

This proof relies on the following lemma, which says that if we have a true 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.

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

No Format |
---|

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

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

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

:

No Format |
---|

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

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

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

:

No Format |
---|

```
t
= {by hypothesis}
(true-listp x)
= {by def of true-listp, hypothesis, if axiom}
(true-listp (cdr x))
``` |

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

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

:

No Format |
---|

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

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

is a true list for any `b`

. I left it as an exercise for you to prove for next time.