• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
          • Tutorial3-phonebook-example
          • Tutorial1-towers-of-hanoi
          • Tutorial2-eights-problem
          • Solution-to-simple-example
          • Tutorial4-defun-sk-example
          • Tutorial5-miscellaneous-examples
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Emacs
      • About-ACL2
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Annotated-ACL2-scripts

Tutorial4-defun-sk-example

Example of quantified notions

This example illustrates the use of defun-sk and defthm events to reason about quantifiers. See defun-sk. For a more through, systematic beginner's introduction to quantification in ACL2, see quantifier-tutorial.

Many users prefer to avoid the use of quantifiers, since ACL2 provides only very limited support for reasoning about quantifiers.

Here is a list of events that proves that if there are arbitrarily large numbers satisfying the disjunction (OR P R), then either there are arbitrarily large numbers satisfying P or there are arbitrarily large numbers satisfying R.

; Introduce undefined predicates p and r.
(defstub p (x) t)
(defstub r (x) t)

; Define the notion that something bigger than x satisfies p.
(defun-sk some-bigger-p (x)
  (exists y (and (< x y) (p y))))

; Define the notion that something bigger than x satisfies r.
(defun-sk some-bigger-r (x)
  (exists y (and (< x y) (r y))))

; Define the notion that arbitrarily large x satisfy p.
(defun-sk arb-lg-p ()
  (forall x (some-bigger-p x)))

; Define the notion that arbitrarily large x satisfy r.
(defun-sk arb-lg-r ()
  (forall x (some-bigger-r x)))

; Define the notion that something bigger than x satisfies p or r.
(defun-sk some-bigger-p-or-r (x)
  (exists y (and (< x y) (or (p y) (r y)))))

; Define the notion that arbitrarily large x satisfy p or r.
(defun-sk arb-lg-p-or-r ()
  (forall x (some-bigger-p-or-r x)))

; Prove the theorem promised above.  Notice that the functions open
; automatically, but that we have to provide help for some rewrite
; rules because they have free variables in the hypotheses.  The
; ``witness functions'' mentioned below were introduced by DEFUN-SK.

(thm
 (implies (arb-lg-p-or-r)
          (or (arb-lg-p)
              (arb-lg-r)))
 :hints (("Goal"
          :use
          ((:instance some-bigger-p-suff
                      (x (arb-lg-p-witness))
                      (y (some-bigger-p-or-r-witness
                          (max (arb-lg-p-witness)
                               (arb-lg-r-witness)))))
           (:instance some-bigger-r-suff
                      (x (arb-lg-r-witness))
                      (y (some-bigger-p-or-r-witness
                          (max (arb-lg-p-witness)
                               (arb-lg-r-witness)))))
           (:instance arb-lg-p-or-r-necc
                      (x (max (arb-lg-p-witness)
                              (arb-lg-r-witness))))))))

; And finally, here's a cute little example.  We have already
; defined above the notion (some-bigger-p x), which says that
; something bigger than x satisfies p.  Let us introduce a notion
; that asserts that there exists both y and z bigger than x which
; satisfy p.  On first glance this new notion may appear to be
; stronger than the old one, but careful inspection shows that y and
; z do not have to be distinct.  In fact ACL2 realizes this, and
; proves the theorem below automatically.

(defun-sk two-bigger-p (x)
  (exists (y z) (and (< x y) (p y) (< x z) (p z))))

(thm (implies (some-bigger-p x) (two-bigger-p x)))

; A technical point:  ACL2 fails to prove the theorem above
; automatically if we take its contrapositive, unless we disable
; two-bigger-p as shown below.  That is because ACL2 needs to expand
; some-bigger-p before applying the rewrite rule introduced for
; two-bigger-p, which contains free variables.  The moral of the
; story is:  Don't expect too much automatic support from ACL2 for
; reasoning about quantified notions.

(thm (implies (not (two-bigger-p x)) (not (some-bigger-p x)))
     :hints (("Goal" :in-theory (disable two-bigger-p))))