• 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

Do-not-hint

Give :do-not hints automatically.

Do-not-hint is a computed hint (~l[computed-hints]) that gives :do-not and perhaps :do-not-induct hints automatically. For instance:

(local (do-not generalize fertilize))
(defthm thm1 ...)
(defthm thm2 ...)
...

is roughly equivalent to:

(defthm thm1 ... :hints (("Goal" :do-not '(generalize fertilize))))
(defthm thm2 ... :hints (("Goal" :do-not '(generalize fertilize))))

except that the :do-not hints are actually given at stable-under-simplificationp checkpoints. This is kind of useful: the hints will apply to forced subgoals in addition to regular subgoals, and won't clutter proofs that never hit a stable-under-simplificationp checkpoint.

The do-not macro expands to some table events that update the do-not-table. It should typically be made local to a book or encapsulate since globally disabling these proof engines is likely to be particularly disruptive to other proofs.

The arguments to do-not can be any of the keywords used for :do-not hints, and may also include induct which results in :do-not-induct t hints.

Definitions and Theorems

Function: do-not-hint

(defun do-not-hint (world stable-under-simplificationp state)
 (declare (xargs :stobjs state))
 (b* (((unless stable-under-simplificationp)
       nil)
      (tbl (table-alist 'do-not-table world))
      (things (cdr (assoc 'things-not-to-be-done tbl)))
      (inductp (cdr (assoc 'do-not-inductp tbl)))
      ((when (and (atom things) (not inductp)))
       nil)
      (- (or (gag-mode)
             (cw "~%;; do-not-hint: prohibiting ~x0.~|"
                 (if inductp (cons 'induct things)
                   things))))
      (hint (if inductp '(:do-not-induct t) nil))
      (hint (if (consp things)
                (append (cons ':do-not
                              (cons (cons 'quote (cons things 'nil))
                                    'nil))
                        hint)
              hint)))
   hint))