DEFUN-SK-EXAMPLE

Major Section:  DEFUN-SK

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