Child pages
  • CSU 290 (Spring 2008)

Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

  • (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.