Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
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
(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
(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-listphas been replaced by the entire body of
Next, note that the first hypothesis above is that
(consp z) is false.
(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
Axiom if-nil: (if nil x y) = y.
Rewriting with this particular axiom, using
(if nil x y) as the pattern
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
Now use your browser's Back Button to return to the example proof in logic-knowledge-taken-for-granted.