Child pages
  • CSU 290 (Spring 2008)

Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.
Comment: Migrated to Confluence 5.3

...

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 Features", top right icon is an envelope. Press that button. That will register you as watching this page. Basically, every time the page changes, you get an email saying so. Keeps you from having to check the page regularly.

...

February 15: Formal

...

Proof for ~(t=nil)

Here is a complete formal proof for ~(t=nil) using the axioms I gave in class. (This is the proof that I started on Monday, but ran out of time 5 steps into the proof.)

...

EDIT: Let me add the following properties that you can assume to. too:

No Format
  (booleanp z) => (andp z t) = z
  (booleanp z) => (andp t z) = z
  (booleanp z) => (orp z nil) = z
  (booleanp z) => (orp nil z) = z

...

These may come in handy in the proofs of the next theorems.

For *EDIT*: note that proving the above gives you that the following two theorems are true:

  • (and-foldp (app x y)) = (andp (and-foldp x) (and-foldp y))
  • (or-foldp (app x y)) = (orp (of-foldp x) (or-foldp y))

These may come in handy in the proofs of the next theorems.

the next few theorems, you will want to prove the following lemma first:

...

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

...

April 9: Topics for Exam #6

Topics covered include everything we have learned about the ACL2s theorem prover, lectures 25 to 29 on the web page; of course, you should not forget the basics of proving theorems.

Here are the main things we will test.

  1. Understanding ACL2s proof attempts
    That was the largest component of these last two weeks.
    In particular, understand the waterfall model (cf lecture 25), and be able to extract lemmas to be proved when ACL2s is stuck on a proof.
  2. Understand rewriting
    Cf lecture 26 and the textbook, and see below.
  3. Understand decision procedures for propositional reasoning and congruence closure
    Cf lecture 29 and see below.

Rewriting

Recall that when you prove a theorem (possibly with hypotheses) with a conclusion of the form LHS = RHS, this defines a rewrite rule that rewrites occurrences of LHS into RHS. (Note the direction!) Variables in the LHS are taken to be placeholders, that can be substituted for when rewriting happens.

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

  1. 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 ...).
  2. Rewriting occurs with the latest rewrite rules defined tried first, all to way to the oldest rewrite rules. In other words, if two (or more) rewrite rules are applicable to a given expression, the most recently admitted rewrite rule is used.

Decision Procedure for Propositional Reasoning

How does ACL2s decided whether a Boolean expression is a tautology or not? 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, that contains essentially the same information.) Here's how it does it. For simplicity, here, I will only consider the case where there are no occurrence of functions others than implies, and, not, and or in the Boolean expression. (It's an interesting exercise to figure out what happens when you do allow other functions.)

First, it rewrites the Boolean expression so that it does not contain any implies, and, or, and not. It does so by replacing every occurrence of those functions by a corresponding if expression. Here are the replacements:

No Format

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

(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.)
Thus, for example:

No Format

(and (not a) a) = (if (if a nil t) a nil)     # expanding out and and not

Once that is done, you are left with a bunch of if expressions. For reasons that will become clear, we want to simplify the condition of those if expressions as much as possible. In particular, 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.)

No Format

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

(Convince yourself that you understand why applying this transformation does not change the value returned by the whole expression.)
Do this repeatedly until all if expressions have a variable (or t or nil) as a condition.
Continuing our example above:

No Format

(and (not a) b) = (if (if a nil t) a nil)    # expanding out and and not
                = (if a                      # applying transformation above
                      (if nil a nil)
                    (if t a nil))

Now, let's simplify things further.
First, take every if expression, from the outermost to the innermost:

  1. if the expression is of the form (if t X Y), replace it by X, and repeat going into X.
  2. if the expression is of the form (if nil X Y), replace it by Y, and repeat going into Y.
  3. 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).

Continuing our example:

No Format

(and (not a) b) = (if (if a nil t) a nil)    # expanding out and and not
                = (if a                      # applying transformation above
                      (if nil a nil)
                    (if t a nil))
                = (if a                      # replacing a by t in THEN clause 
                      (if nil t nil)
                    (if t a nil))
                = (if a                      # replacing a by nil in ELSE clause
                      (if nil t nil)
                    (if t nil nil))
                = (if a                      # (if nil t nil) -> nil
                      nil                 
                    (if t nil nil))
                = (if a nil nil)             # (if t nil nil) -> nil

When you're done all of this, you have an expression with only if expressions and with the property that for any "path" through the conditionals, you encounter every variable only once, in the condition of an if. A Boolean expression is a tautology exactly when every "path" through the conditionals lead to a value that is guaranteed to be non-nil.

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 conditionals that led to the values that is not guaranteed to be non-nil, setting 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 right branch of the conditional.

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 guaranteed 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 tautology.

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 simplified form (if a (if b t t) (if b nil t)). There is one "path" in the conditionals that lead to a value not guaranteed to be non-nil, and 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=nil,b=t is a counterexample to the initial conjecture.

Decision Procedure for Equivalences

This decision procedure is used to establish whether an implication where the hypotheses are equalities and the conclusion is also an equality is true, in the special case where this information can be decided without relying on the definition of the functions in the expression. (For instance, this 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.)

Let's be more concrete. Suppose that we have no information about functions f and g, but we are asked to prove that:

No Format

(implies (and (= a c)
              (= (f a) b)
              (= (g c) c)
         (= (f (g a)) b))

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

No Format

(f (g c)) = (f (g a))  # because a = c
          = (f c)      # because (g c) = c
          = (f a)      # because a = c
          = b          # because (f a) = b

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

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

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 expression, 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 increasing complexity:

No Format

a  
b  
c  
(f a)  
(g c)  
(g a)  
(f (g a))

Note that (g a) is a subterm because it appears in (f (g a)).

Good. Now, the procedure is to repeatedly look at the equations in the hypotheses (there are three in our example), and "lump" together the terms in 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.

Let's start. Let's look at the first equation a = c. It tells you to lump together a and c. Let's do that:

No Format

a  c  
b  
(f a)  
(g c)  
(g a)  
(f (g a))

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 equations we have been looking at. Knowing that a and c are equal tells you also that (g a) and (g c) are equal, so we can lump those two together too:

No Format

a  c  
b  
(f a)  
(g c)  (g a)  
(f (g a))

That's it, we cannot lump things together any further based on what we know.

Let's look at the second equation, (f a) = b. It tells you to lump together (f a) and b. Easy enough:

No Format

a  c  
b  (f a)  
(g c)  (g a)  
(f (g a))

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

Let's look at the last equation, (g c) = c. It tells you to lump together (g c) and c. Now, because c is already lumped with something, and (g c) is also already lumped with something, let's merge the respective lumps. (After all, lumping just means that things can be proved equal.)

No Format

a  c  (g c)  (g a)  
b  (f a)  
(f (g a))

Oh, now we've learned a lot, in particular, that (g a) = a. This means that (f (g a)) = (f a), so that we can lump (f a) and (f (g a)) together:

No Format

a  c  (g c)  (g a)  
b  (f a)  (f (g a))

And that's it, we cannot lump things any further. And we've exhausted all 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 asks whether the three equations imply that (f (g a)) = b; in other words, do the three equations ensure that (f (g a)) and 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.

...

April 21: Study Guide

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

So what did those tests cover?

Test 1:

  1. the basics of the ACL2 programming language
  2. total functions,
  3. the use of the design recipe to develop functions

Test 2:

  1. lists and true lists
  2. quotation
  3. design recipe for recursive functions over true lists

Test 3:

  1. Boolean logic
  2. proving theorems using equational reasoning
  3. falsifying conjectures

Test 4:

  1. the induction principle (give proof obligations)
  2. proving proof obligations

Test 5:

  1. more difficult inductions (idenfitication of lemmas)
  2. generalization
  3. using different substitutions in the inductive proof obligation

Test 6:

  1. The ACL2s theorem prover and the waterfall model
  2. rewriting
  3. understanding proof reports, including identifying interesting checkpoints
  4. decision procedures for Boolean logic and congruence closure