without-subsumption

Included Books

top eval

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

without-subsumptionmacro

(defmacro without-subsumption
  (form &key (cases 'nil))
  `(encapsulate nil
    (local (defun without-subsumption-disable-quick-and-dirty
        (x y)
        (declare (ignore x y)
          (xargs :guard t))
        nil))
    (local (defattach-system quick-and-dirty-srs
        without-subsumption-disable-quick-and-dirty))
    (set-case-split-limitations '(0 ,CASES))
    ,FORM))

local

(local (encapsulate nil
    (encapsulate ((pk (n params) t) (pk-k nil t) (pk-badguy (n params) t))
      (local (defun pk (n params) (declare (ignore n params)) t))
      (local (defun pk-k nil 1))
      (local (defun pk-badguy (n params) (declare (ignore n params)) 0))
      (defthm posp-pk-k
        (posp (pk-k))
        :rule-classes :type-prescription)
      (defthm natp-pk-badguy
        (natp (pk-badguy n params))
        :rule-classes :type-prescription)
      (defthm pk-badguy-range
        (implies (and (natp n) (not (pk n params)))
          (and (< (pk-badguy n params) n)
            (>= (pk-badguy n params) (- n (pk-k)))))
        :rule-classes (:linear :rewrite))
      (defthm pk-badguy-is-counterexample
        (implies (and (natp n) (not (pk n params)))
          (not (pk (pk-badguy n params) params)))))
    (defun pk-induction
      (n params)
      (if (or (zp n) (pk n params))
        t
        (pk-induction (pk-badguy n params) params)))
    (defthm pk-0
      (pk 0 params)
      :hints (("Goal" :use ((:instance pk-badguy-range (n 0))))))
    (defthm pk-holds
      (implies (natp n) (pk n params))
      :hints (("Goal" :induct (pk-induction n params))))
    (encapsulate ((q (n x y) t))
      (local (defun q (n x y) (declare (ignore n x y)) t))
      (defthm q-3-properties
        (and (q 0 x y)
          (q 1 x y)
          (q 2 x y)
          (implies (and (natp n)
              (<= 3 n)
              (q (- n 3) x y)
              (q (- n 2) x y)
              (q (- n 1) x y))
            (q n x y)))))
    (defun q-params
      (n params)
      (q n (nth 0 params) (nth 1 params)))
    (defun k-params-badguy
      (n k params)
      (if (zp k)
        n
        (if (zp n)
          0
          (let ((n (1- n)))
            (if (not (q-params n params))
              n
              (k-params-badguy n (- k 1) params))))))
    (defthm open-k-params
      (implies (syntaxp (quotep k))
        (equal (k-params-badguy n k params)
          (if (zp k)
            n
            (if (zp n)
              0
              (let ((n (1- n)))
                (if (not (q-params n params))
                  n
                  (k-params-badguy n (- k 1) params))))))))
    (local (include-book "std/testing/eval" :dir :system))
    (local (must-fail (defthmd q-params-holds-1
          (implies (natp n) (q-params n params))
          :otf-flg t
          :hints (("Goal" :use ((:functional-instance pk-holds
                (pk q-params)
                (pk-k (lambda nil 3))
                (pk-badguy (lambda (n params) (k-params-badguy n 3 params)))))
             :in-theory (disable open-k-params zp-compound-recognizer zp zp-open)) (and stable-under-simplificationp
              '(:in-theory (e/d (open-k-params) (zp-compound-recognizer zp zp-open))))
            (and stable-under-simplificationp
              '(:in-theory (enable zp-open zp)))))
        :with-output-off nil))
    (local (encapsulate nil
        (local (defthm q-params-holds-2
            (implies (natp n) (q-params n params))
            :otf-flg t
            :hints (("Goal" :use ((:functional-instance pk-holds
                  (pk q-params)
                  (pk-k (lambda nil 3))
                  (pk-badguy (lambda (n params) (k-params-badguy n 3 params)))))
               :in-theory (disable open-k-params)) (and stable-under-simplificationp
                '(:in-theory (e/d (open-k-params) (zp-compound-recognizer zp zp-open))
                  :restrict ((open-k-params ((k 3))))))
              (and stable-under-simplificationp
                '(:in-theory (e/d (open-k-params) (zp-compound-recognizer zp zp-open))
                  :restrict ((open-k-params ((k 2))))))
              (and stable-under-simplificationp
                '(:in-theory (e/d (open-k-params) (zp-compound-recognizer zp zp-open))
                  :restrict ((open-k-params ((k 1))))))
              (and stable-under-simplificationp
                '(:in-theory (enable zp-open zp))))))))
    (local (must-fail (defthm q-params-holds-3
          (implies (natp n) (q-params n params))
          :otf-flg t
          :hints (("Goal" :use ((:functional-instance pk-holds
                (pk q-params)
                (pk-k (lambda nil 3))
                (pk-badguy (lambda (n params) (k-params-badguy n 3 params))))))))
        :with-output-off nil))
    (without-subsumption (defthmd q-params-holds-4
        (implies (natp n) (q-params n params))
        :otf-flg t
        :hints (("Goal" :use ((:functional-instance pk-holds
              (pk q-params)
              (pk-k (lambda nil 3))
              (pk-badguy (lambda (n params) (k-params-badguy n 3 params)))))))))))

other

(defxdoc without-subsumption
  :short "Perform proofs without subsumption/replacement to preserve hypotheses that might otherwise be dropped."
  :parents (proof-automation)
  :long "
<p>
@('without-subsumption') is a simple macro that allows you to perform
proofs without subsumption/replacement to preserve hypotheses that
might otherwise be dropped during clausification.
</p>
<p>
In the course of a proof, ACL2 will sometimes drop hypotheses during
subsumption/replacement that would otherwise have allowed it to
complete the proof.
</p>
<p>
@('without-subsumption') uses both
@(tsee quick-and-dirty-subsumption-replacement-step) and
@(tsee case-split-limitations) to stop subsumption/replacement in various
stages of the ACL2 simplifier.  These hints can help preserve hypothesis
in a proof that the ACL2 simplifier might otherwise drop.  The
macro is defined as follows:
</p>
@({
 (defmacro without-subsumption(form &key (cases 'nil))
  `(encapsulate
       ()

     (local (defun without-subsumption-disable-quick-and-dirty (x y)
              (declare (ignore x y) (xargs :guard t)) nil))
     (local (defattach-system quick-and-dirty-srs
              without-subsumption-disable-quick-and-dirty))
     (set-case-split-limitations '(0 ,cases))
     
     ,form

     ))
})
<p>Usage:</p>
@({
 (include-book "tools/without-subsumption" :dir :system)
 (without-subsumption
   (defthm natp-implies-integerp
     (implies 
       (natp n)
       (integerp n)))
  )
 })

")