...

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.

- 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. - Understand rewriting

Cf lecture 26 and the textbook, and see below. - 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:

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

. - 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*:

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

, replace it by`X`

, and repeat going into`X`

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

, replace it by`Y`

, and repeat going into`Y`

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

*Coming soon*