• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
      • Term
      • Ld
      • Hints
        • Lemma-instance
        • Computed-hints
        • Override-hints
        • Hints-and-the-waterfall
        • Goal-spec
        • Termination-theorem-example
        • Consideration
        • Hint-wrapper
        • Default-hints
        • Guard-theorem-example
        • Do-not-hint
        • Guard-theorem
        • Using-computed-hints
        • Termination-theorem
        • Custom-keyword-hints
        • Do-not
      • Type-set
      • Ordinals
      • Clause
      • ACL2-customization
      • With-prover-step-limit
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Gcl
      • Oracle-timelimit
      • Thm
      • Defopener
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Hints

Hint-wrapper

Supply hints in the statement of a theorem

Using the computed-hints mechanism, it is possible to place hints in the hypothesis of a theorem. The hint-wrapper utility implements this capability. Simply do the following:

(include-book "hints/hint-wrapper" :dir :system)
(add-default-hints '((hint-wrapper-hint clause)))

The include-book above defines a function of one argument, hint-wrapper, that always returns t but has following special property. When ACL2 attempts to prove a theorem with a hypothesis that is a call of hint-wrapper on a quoted hint keyword alist — that is, a form (quote (:key1 val1 ... :keyn valn)) — then the hints (:key1 val1 ... :keyn valn) will be applied.

The following example illustrates the use of this hint-wrapper mechanism. The form (add-default-hints '((hint-wrapper-hint clause))) installs this mechanism as a default hint, arranging that the mechanism is applied automatically. In this example, the final thm succeeds because the default hint extracts the indicated :in-theory hint from the hint-wrapper call in the hypothesis.

(defund foo (x)
  (cons x x))

(thm ; FAILS, because foo is disabled
  (equal (foo y) (cons y y)))

(add-default-hints '((hint-wrapper-hint clause)))

(thm ; SUCCEEDS, using hint-wrapper mechanism (default hint hint-wrapper-hint)
  (implies (hint-wrapper '(:in-theory (enable foo)))
           (equal (foo y) (cons y y))))

The process described above is actually applied to the first suitable such hypothesis, which will be expanded away; on subsequent passes through the waterfall (see hints-and-the-waterfall) that process will be applied to the first remaining such hypothesis, and so on. For the following example, assume that the above defund and add-default-hints calls have been evaluated. Initially, the indicated (though useless) :expand hint will be applied, since explicit hints on goals take priority over default hints. (See override-hints for how to avoid this prioritization.) Next, the first hint-wrapper call will be applied; it is, of course, useless, since mv-nth has nothing to do with this theorem. That first hint-wrapper call is expanded away, producing a subgoal, "Goal'", with the remaining two hint-wrapper hypotheses. The first of these two provides the hint to enable foo, which completes the proof.

(thm
  (implies (and (hint-wrapper '(:in-theory (enable mv-nth)))
                (hint-wrapper '(:in-theory (enable foo)))
                (hint-wrapper '(:in-theory (enable nth))))
           (equal (foo y) (cons y y)))
  :hints (("Goal" :expand ((append x y)))))

This hint-wrapper mechanism can actually be applied explicitly, rather than using a computed hint. Even if we omit the call of add-default-hints displayed above, the following succeeds.

(thm
  (implies (hint-wrapper '(:in-theory (enable foo)))
           (equal (foo y) (cons y y)))
  :hints ((hint-wrapper-hint clause)))

The implementation of the hint-wrapper mechanism is rather straightforward, and could be useful for understanding computed-hints in general. See community book hints/hint-wrapper.lisp.