		Search-engine friendly clone of the ACL2 documentation.

Introduction-to-the-theorem-prover

Logic-knowledge-taken-for-granted-rewriting-repeatedly

Further information on expanding definitions via rewriting

We assume you've read about ``instances'' and picked up our basic terminology including the ideas of matching a pattern term to a target term, obtaining a substitution and how to instantiate a term with a substitution. We use these notions below without further citation.

In addition, we assume you've read about ``rewriting'' where we introduced the idea of treating a theorem (axiom, definition, or lemma) as a conditional rewrite rule and replaced one term by an equivalent one provided we can relieve the hypotheses.

Suppose you're trying to prove formula1 and you transform it to formula2 by rewriting. What happened?

formula1: 
(implies (and (not (consp z)) 
              (true-listp z)) 
         (equal (rev (rev z)) z)) 
 
formula2: 
(implies (and (not (consp z)) 
              (equal z nil)) 
         (equal (rev (rev z)) z))

Evidently we replaced (true-listp z) by (equal z nil). But how did that happen? What really happened was the sequential application of several unconditional rewrites and the use of replacement of equals by equals.

The definition of true-listp is:

(defun true-listp (x)
  (if (consp x)
      (true-listp (cdr x))
      (equal x nil))).

By rewriting once with the definition of true-listp, we transform formula1 to:

formula1': 
(implies (and (not (consp z)) 
              (if (consp z) 
                  (true-listp (cdr z)) 
                  (equal z nil))) 
         (equal (rev (rev z)) z)).

Note how the call of true-listp has been replaced by the entire body of true-listp.

Next, note that the first hypothesis above is that (consp z) is false. That is, (not (consp z)) is the same as (equal (consp z) nil). Thus, replacement of equals by equals means we can transform formula1' to

formula1'': 
(implies (and (not (consp z)) 
              (if nil 
                  (true-listp (cdr z)) 
                  (equal z nil))) 
         (equal (rev (rev z)) z)).

(We will explore replacement of equals by equals later.)

Furthermore, we know the basic axiom about if:

Axiom if-nil: 
(if nil x y) = y.

Rewriting with this particular axiom, using (if nil x y) as the pattern and y as the replacement, will transform formula1'' to

formula2: 
(implies (and (not (consp z)) 
              (equal z nil)) 
         (equal (rev (rev z)) z)).

Often when we say we derived one formula from another by ``expansion'' and or by ``rewriting'' we take many rewrite steps, as here. We typically use hypotheses of the formula without noting ``replacement of equals by equals'' as when we replaced (consp z) by nil, and we typically omit to mention the use of basic axioms like if-nil above.

Now use your browser's Back Button to return to the example proof in logic-knowledge-taken-for-granted.