|
|
|---|
|
|
|
|---|
A simple example using defun-sk
For a more through, systematic beginner's introduction to quantification in ACL2, see quantifier-tutorial.
The following example illustrates how to do proofs about functions defined with defun-sk. The events below can be put into a certifiable book (see books). The example is contrived and rather silly, in that it shows how to prove that a quantified notion implies itself, where the antecedent and conclusion are defined with different defun-sk events. But it illustrates the formulas that are generated by defun-sk, and how to use them. Thanks to Julien Schmaltz for presenting this example as a challenge.
(in-package "ACL2") (encapsulate (((p *) => *) ((expr *) => *)) (local (defun p (x) x)) (local (defun expr (x) x))) (defun-sk forall-expr1 (x) (forall (y) (implies (p x) (expr y)))) (defun-sk forall-expr2 (x) (forall (y) (implies (p x) (expr y))))) ; We want to prove the theorem my-theorem below. What axioms are there that ; can help us? If you submit the command ; :pcb! forall-expr1 ; then you will see the following two key events. (They are completely ; analogous of course for FORALL-EXPR2.) ; (DEFUN FORALL-EXPR1 (X) ; (LET ((Y (FORALL-EXPR1-WITNESS X))) ; (IMPLIES (P X) (EXPR Y)))) ; ; (DEFTHM FORALL-EXPR1-NECC ; (IMPLIES (NOT (IMPLIES (P X) (EXPR Y))) ; (NOT (FORALL-EXPR1 X))) ; :HINTS ; (("Goal" :USE FORALL-EXPR1-WITNESS))) ; We see that the latter has value when FORALL-EXPR1 occurs negated in a ; conclusion, or (therefore) positively in a hypothesis. A good rule to ; remember is that the former has value in the opposite circumstance: negated ; in a hypothesis or positively in a conclusion. ; In our theorem, FORALL-EXPR2 occurs positively in the conclusion, so its ; definition should be of use. We therefore leave its definition enabled, ; and disable the definition of FORALL-EXPR1. ; (thm ; (implies (and (p x) (forall-expr1 x)) ; (forall-expr2 x)) ; :hints (("Goal" :in-theory (disable forall-expr1)))) ; ; ; which yields this unproved subgoal: ; ; (IMPLIES (AND (P X) (FORALL-EXPR1 X)) ; (EXPR (FORALL-EXPR2-WITNESS X))) ; Now we can see how to use FORALL-EXPR1-NECC to complete the proof, by ; binding y to (FORALL-EXPR2-WITNESS X). ; We use defthmd below so that the following doesn't interfere with the ; second proof, in my-theorem-again that follows. (defthmd my-theorem (implies (and (p x) (forall-expr1 x)) (forall-expr2 x)) :hints (("Goal" :use ((:instance forall-expr1-necc (x x) (y (forall-expr2-witness x))))))) ; The following illustrates a more advanced technique to consider in such ; cases. If we disable forall-expr1, then we can similarly succeed by having ; FORALL-EXPR1-NECC applied as a :rewrite rule, with an appropriate hint in how ; to instantiate its free variable. See :doc hints. (defthm my-theorem-again (implies (and (P x) (forall-expr1 x)) (forall-expr2 x)) :hints (("Goal" :in-theory (disable forall-expr1) :restrict ((forall-expr1-necc ((y (forall-expr2-witness x))))))))