• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
      • Z3-installation
      • Smt-hint
      • Tutorial
      • Status
      • Developer
        • Verified
          • Uninterpreted-fn-cp
          • Smt-hint-interface
          • Function-expansion
          • Smt-config
          • Fty-support
          • Smt-computed-hints
          • Add-hypo-cp
          • Smt-hint-please
          • Type-extract-cp
          • Smt-extract
          • Smtlink-process-user-hint
          • Smt-basics
          • Smt-type-hyp
          • Smt-magic-fix
        • Trusted
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Verified

Smt-hint-please

The function hint-please in SMT is for passing hints to subgoals using the clause-processor and computed-hint mechanism.

Definitions and Theorems

Function: hint-please

(defun hint-please (hint)
  (declare (xargs :guard (listp hint)))
  (declare (ignore hint) (xargs :guard t))
  (let ((acl2::__function__ 'hint-please))
    (declare (ignorable acl2::__function__))
    nil))

Theorem: hint-please-forward

(defthm hint-please-forward
  (implies (hint-please hint) nil)
  :rule-classes :forward-chaining)

Function: remove-hint-please

(defun remove-hint-please (cl)
  (declare (xargs :guard (pseudo-term-listp cl)))
  (let ((acl2::__function__ 'remove-hint-please))
    (declare (ignorable acl2::__function__))
    (b* ((cl (pseudo-term-list-fix cl))
         ((unless (consp cl)) (list cl)))
      (case-match cl
        ((('hint-please &) . term) (list term))
        (& (list cl))))))

Theorem: pseudo-term-list-listp-of-remove-hint-please

(defthm pseudo-term-list-listp-of-remove-hint-please
  (b* ((cl-removed (remove-hint-please cl)))
    (pseudo-term-list-listp cl-removed))
  :rule-classes :rewrite)

Theorem: ev-remove-hint-please-constraint-0

(defthm ev-remove-hint-please-constraint-0
 (implies
  (and (consp acl2::x)
       (syntaxp (not (equal acl2::a ''nil)))
       (not (equal (car acl2::x) 'quote)))
  (equal
      (ev-remove-hint-please acl2::x acl2::a)
      (ev-remove-hint-please
           (cons (car acl2::x)
                 (kwote-lst (ev-lst-remove-hint-please (cdr acl2::x)
                                                       acl2::a)))
           nil))))

Theorem: ev-remove-hint-please-constraint-1

(defthm ev-remove-hint-please-constraint-1
  (implies (symbolp acl2::x)
           (equal (ev-remove-hint-please acl2::x acl2::a)
                  (and acl2::x
                       (cdr (assoc-equal acl2::x acl2::a))))))

Theorem: ev-remove-hint-please-constraint-2

(defthm ev-remove-hint-please-constraint-2
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'quote))
           (equal (ev-remove-hint-please acl2::x acl2::a)
                  (cadr acl2::x))))

Theorem: ev-remove-hint-please-constraint-3

(defthm ev-remove-hint-please-constraint-3
 (implies
      (and (consp acl2::x)
           (consp (car acl2::x)))
      (equal (ev-remove-hint-please acl2::x acl2::a)
             (ev-remove-hint-please
                  (caddr (car acl2::x))
                  (pairlis$ (cadr (car acl2::x))
                            (ev-lst-remove-hint-please (cdr acl2::x)
                                                       acl2::a))))))

Theorem: ev-remove-hint-please-constraint-4

(defthm ev-remove-hint-please-constraint-4
  (implies (not (consp acl2::x-lst))
           (equal (ev-lst-remove-hint-please acl2::x-lst acl2::a)
                  nil)))

Theorem: ev-remove-hint-please-constraint-5

(defthm ev-remove-hint-please-constraint-5
  (implies (consp acl2::x-lst)
           (equal (ev-lst-remove-hint-please acl2::x-lst acl2::a)
                  (cons (ev-remove-hint-please (car acl2::x-lst)
                                               acl2::a)
                        (ev-lst-remove-hint-please (cdr acl2::x-lst)
                                                   acl2::a)))))

Theorem: ev-remove-hint-please-constraint-6

(defthm ev-remove-hint-please-constraint-6
  (implies (and (not (consp acl2::x))
                (not (symbolp acl2::x)))
           (equal (ev-remove-hint-please acl2::x acl2::a)
                  nil)))

Theorem: ev-remove-hint-please-constraint-7

(defthm ev-remove-hint-please-constraint-7
  (implies (and (consp acl2::x)
                (not (consp (car acl2::x)))
                (not (symbolp (car acl2::x))))
           (equal (ev-remove-hint-please acl2::x acl2::a)
                  nil)))

Theorem: ev-remove-hint-please-constraint-8

(defthm ev-remove-hint-please-constraint-8
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'not))
           (equal (ev-remove-hint-please acl2::x acl2::a)
                  (not (ev-remove-hint-please (cadr acl2::x)
                                              acl2::a)))))

Theorem: ev-remove-hint-please-constraint-9

(defthm ev-remove-hint-please-constraint-9
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'if))
           (equal (ev-remove-hint-please acl2::x acl2::a)
                  (if (ev-remove-hint-please (cadr acl2::x)
                                             acl2::a)
                      (ev-remove-hint-please (caddr acl2::x)
                                             acl2::a)
                    (ev-remove-hint-please (cadddr acl2::x)
                                           acl2::a)))))

Theorem: ev-remove-hint-please-constraint-10

(defthm ev-remove-hint-please-constraint-10
  (implies (and (consp acl2::x)
                (equal (car acl2::x) 'hint-please))
           (equal (ev-remove-hint-please acl2::x acl2::a)
                  (hint-please (ev-remove-hint-please (cadr acl2::x)
                                                      acl2::a)))))

Theorem: ev-remove-hint-please-disjoin-cons

(defthm ev-remove-hint-please-disjoin-cons
  (iff (ev-remove-hint-please (disjoin (cons acl2::x acl2::y))
                              acl2::a)
       (or (ev-remove-hint-please acl2::x acl2::a)
           (ev-remove-hint-please (disjoin acl2::y)
                                  acl2::a))))

Theorem: ev-remove-hint-please-disjoin-when-consp

(defthm ev-remove-hint-please-disjoin-when-consp
  (implies (consp acl2::x)
           (iff (ev-remove-hint-please (disjoin acl2::x)
                                       acl2::a)
                (or (ev-remove-hint-please (car acl2::x)
                                           acl2::a)
                    (ev-remove-hint-please (disjoin (cdr acl2::x))
                                           acl2::a)))))

Theorem: ev-remove-hint-please-disjoin-atom

(defthm ev-remove-hint-please-disjoin-atom
  (implies (not (consp acl2::x))
           (equal (ev-remove-hint-please (disjoin acl2::x)
                                         acl2::a)
                  nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ev-remove-hint-please-disjoin-append

(defthm ev-remove-hint-please-disjoin-append
  (iff (ev-remove-hint-please (disjoin (append acl2::x acl2::y))
                              acl2::a)
       (or (ev-remove-hint-please (disjoin acl2::x)
                                  acl2::a)
           (ev-remove-hint-please (disjoin acl2::y)
                                  acl2::a))))

Theorem: ev-remove-hint-please-conjoin-cons

(defthm ev-remove-hint-please-conjoin-cons
  (iff (ev-remove-hint-please (conjoin (cons acl2::x acl2::y))
                              acl2::a)
       (and (ev-remove-hint-please acl2::x acl2::a)
            (ev-remove-hint-please (conjoin acl2::y)
                                   acl2::a))))

Theorem: ev-remove-hint-please-conjoin-when-consp

(defthm ev-remove-hint-please-conjoin-when-consp
  (implies (consp acl2::x)
           (iff (ev-remove-hint-please (conjoin acl2::x)
                                       acl2::a)
                (and (ev-remove-hint-please (car acl2::x)
                                            acl2::a)
                     (ev-remove-hint-please (conjoin (cdr acl2::x))
                                            acl2::a)))))

Theorem: ev-remove-hint-please-conjoin-atom

(defthm ev-remove-hint-please-conjoin-atom
  (implies (not (consp acl2::x))
           (equal (ev-remove-hint-please (conjoin acl2::x)
                                         acl2::a)
                  t))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ev-remove-hint-please-conjoin-append

(defthm ev-remove-hint-please-conjoin-append
  (iff (ev-remove-hint-please (conjoin (append acl2::x acl2::y))
                              acl2::a)
       (and (ev-remove-hint-please (conjoin acl2::x)
                                   acl2::a)
            (ev-remove-hint-please (conjoin acl2::y)
                                   acl2::a))))

Theorem: ev-remove-hint-please-conjoin-clauses-cons

(defthm ev-remove-hint-please-conjoin-clauses-cons
 (iff
     (ev-remove-hint-please (conjoin-clauses (cons acl2::x acl2::y))
                            acl2::a)
     (and (ev-remove-hint-please (disjoin acl2::x)
                                 acl2::a)
          (ev-remove-hint-please (conjoin-clauses acl2::y)
                                 acl2::a))))

Theorem: ev-remove-hint-please-conjoin-clauses-when-consp

(defthm ev-remove-hint-please-conjoin-clauses-when-consp
 (implies
    (consp acl2::x)
    (iff (ev-remove-hint-please (conjoin-clauses acl2::x)
                                acl2::a)
         (and (ev-remove-hint-please (disjoin (car acl2::x))
                                     acl2::a)
              (ev-remove-hint-please (conjoin-clauses (cdr acl2::x))
                                     acl2::a)))))

Theorem: ev-remove-hint-please-conjoin-clauses-atom

(defthm ev-remove-hint-please-conjoin-clauses-atom
  (implies (not (consp acl2::x))
           (equal (ev-remove-hint-please (conjoin-clauses acl2::x)
                                         acl2::a)
                  t))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: ev-remove-hint-please-conjoin-clauses-append

(defthm ev-remove-hint-please-conjoin-clauses-append
 (iff
   (ev-remove-hint-please (conjoin-clauses (append acl2::x acl2::y))
                          acl2::a)
   (and (ev-remove-hint-please (conjoin-clauses acl2::x)
                               acl2::a)
        (ev-remove-hint-please (conjoin-clauses acl2::y)
                               acl2::a))))

Theorem: correctness-of-remove-hint-please

(defthm correctness-of-remove-hint-please
 (implies
  (and
    (pseudo-term-listp cl)
    (alistp b)
    (ev-remove-hint-please (conjoin-clauses (remove-hint-please cl))
                           b))
  (ev-remove-hint-please (disjoin cl) b))
 :rule-classes :clause-processor)