Filtering...

remove-hyps

books/tools/remove-hyps

Included Books

top top
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
other
(defxdoc remove-hyps
  :parents (proof-automation debugging)
  :short "Macro for defining a theorem with a minimal set of hypotheses"
  :long "<p>For a call of @(tsee defthm), @(tsee defthmd), or @(tsee thm), the
 application of @('remove-hyps') attempts to produce a minimal set of
 hypotheses.  For example:</p>

 @({
 (remove-hyps
  (defthm nth-append
    (implies (and (true-listp x)
                  (natp n)
                  (true-listp y))
             (equal (nth n (append x y))
                    (if (< n (len x))
                        (nth n x)
                      (nth (- n (len x)) y))))
    :rule-classes nil))
 })

 <p>generates:</p>

 @({
 (DEFTHM NTH-APPEND
   (IMPLIES (NATP N)
            (EQUAL (NTH N (APPEND X Y))
                   (IF (< N (LEN X))
                       (NTH N X)
                     (NTH (- N (LEN X)) Y))))
   :RULE-CLASSES NIL)
 })

 <p>Note however that @('remove-hyps') works by removing one hypothesis at a
 time, with each resulting proof attempt made using a limited number of
 steps (see @(see with-prover-step-limit)) that depends on the number of steps
 taken before removing the hypothesis.  So if the removal of a hypothesis
 requires a proof that takes sufficiently many more steps than the original
 proof, or if two or more hypotheses must be removed together for the proof to
 succeed with fewer hypotheses, then the result will not have a minimal set of
 hypotheses.</p>

 <p>Acceptable forms are as follows, where @('HYP') can be a conjunction of
 hypotheses, @('(and HYP1 ... HYPn)'), and ``@('defthm NAME')'' may be
 replaced by ``@('defthmd NAME')'' or ``@('THM')''.</p>

 @({
 (defthm NAME (implies HYP CONCL) ...)
 (defthm NAME CONCL ...)
 (defthm NAME (let ... (implies HYP CONCL)) ...)
 (defthm NAME (let ... CONCL) ...)
 (defthm NAME (let* ... (implies HYP CONCL)) ...)
 (defthm NAME (let* ... CONCL) ...)
 })

 <p>Normally, before using @('remove-hyps'), one succesfully submits the given
 call of @('defthm'), @('defthmd'), or @('thm').  Thus by default,
 @('remove-hyps') evaluates silently.  To see output from proof attempts, add a
 non-nil optional argument.  For example, for event @('E'), use @('(remove-hyps
 E t)').</p>

 <p>Unless there is an error (for example, due to malformed input), then in the
 case of a call of @('thm'), the value returned is the keyword,
 @(':REMOVE-HYPS-COMPLETED'); otherwise, the value returned is the name of the
 theorem.  (Technically, the value returned is an error triple with such a
 value; see @(see error-triple).)</p>

 <p>Consider the case that a call of @('remove-hyps') is made in a context
 where proofs are normally skipped (see @(see ld-skip-proofsp)).  If this
 happens while including a certified book with @(tsee include-book), then
 proofs will indeed be skipped, because the earlier result of this
 @('remove-hyps') call was saved in the book's @(see certificate).  But
 otherwise, the tool temporarily turns off the skipping of proofs (that is,
 restores the act of doing proofs) while it tries to remove hypotheses, to
 avoid the undesirable situation that all hypotheses are removed merely because
 all proofs succeed when skipping proofs.</p>

 <p>Finally, note that when @('remove-hyps') is applied to a call of
 @('defthm') or @('defthmd'), then @('remove-hyps') will conclude by submitting
 the generated event to ACL2.  But since @('thm') does not modify the logical
 @(tsee world), @('remove-hyps') does not perform an extra such call at the end
 for calls of @('thm').</p>")
other
(set-state-ok t)
other
(program)
remove-hyps-formula-stepsfunction
(defun remove-hyps-formula-steps
  (steps)
  (min *default-step-limit* (+ 1000 (* 3 steps))))
dumb-implicatefunction
(defun dumb-implicate
  (hyps concl)
  (cond ((null hyps) concl)
    ((null (cdr hyps)) `(implies ,(CAR HYPS) ,CONCL))
    (t `(implies (and ,@HYPS) ,CONCL))))
make-defthmfunction
(defun make-defthm
  (deft name hyps concl kwd-alist let/let* bindings)
  (let* ((form0 (dumb-implicate hyps concl)) (form (if bindings
          `(,LET/LET* ,BINDINGS
            (declare (ignorable ,@(STRIP-CARS BINDINGS)))
            ,FORM0)
          form0)))
    (if (null name)
      (assert$ (eq deft 'thm) `(thm ,FORM ,@KWD-ALIST))
      `(,DEFT ,NAME ,FORM ,@KWD-ALIST))))
event-stepsfunction
(defun event-steps
  (form verbose-p extra-forms state)
  (let ((new-form `(with-output :stack :push :off :all :gag-mode nil
         (progn (make-event (pprogn (f-put-global 'our-steps nil state)
               (value '(value-triple nil))))
           ,(IF VERBOSE-P
     `(WITH-OUTPUT :STACK :POP ,FORM)
     FORM)
           (make-event (pprogn (f-put-global 'our-steps
                 (or (last-prover-steps state) 1)
                 state)
               ,@EXTRA-FORMS
               (value '(value-triple nil))))
           (defconst *bad*)))))
    (er-progn (trans-eval new-form 'event-steps state t)
      (value (f-get-global 'our-steps state)))))
remove-hyps-formula-1function
(defun remove-hyps-formula-1
  (name rev-init-hyps
    rest-hyps
    concl
    kwd-alist
    let/let*
    bindings
    steps
    verbose-p
    state)
  (cond ((endp rest-hyps) (value (reverse rev-init-hyps)))
    ((and (consp (car rest-hyps))
       (member-eq (caar rest-hyps) '(syntaxp bind-free synp))) (remove-hyps-formula-1 name
        (cons (car rest-hyps) rev-init-hyps)
        (cdr rest-hyps)
        concl
        kwd-alist
        let/let*
        bindings
        steps
        verbose-p
        state))
    (t (let ((form `(with-prover-step-limit ,STEPS
             ,(MAKE-DEFTHM 'DEFTHM NAME (REVAPPEND REV-INIT-HYPS (CDR REST-HYPS)) CONCL
  KWD-ALIST LET/LET* BINDINGS))))
        (er-let* ((event-steps (event-steps form verbose-p nil state)))
          (remove-hyps-formula-1 name
            (cond ((null event-steps) (cons (car rest-hyps) rev-init-hyps))
              (t rev-init-hyps))
            (cdr rest-hyps)
            concl
            kwd-alist
            let/let*
            bindings
            steps
            verbose-p
            state))))))
remove-hyps-formulafunction
(defun remove-hyps-formula
  (form name
    hyps
    concl
    kwd-alist
    let/let*
    bindings
    verbose-p
    ctx
    state)
  (do-proofs? t
    nil
    (mv-let (thmp name2 kwd-alist+)
      (assert$ (iff (eq (car form) 'thm) (null name))
        (if (null name)
          (mv t
            (gen-new-name 'remove-hyps-name (w state))
            (append kwd-alist '(:rule-classes nil)))
          (mv nil name kwd-alist)))
      (er-let* ((steps (event-steps (if thmp
               `(defthm ,NAME2 ,@(CDR FORM) :rule-classes nil)
               form)
             verbose-p
             nil
             state)))
        (cond ((null steps) (er soft ctx "Original theorem failed!"))
          (t (er-let* ((final-hyps (remove-hyps-formula-1 name2
                   nil
                   hyps
                   concl
                   kwd-alist+
                   let/let*
                   bindings
                   (remove-hyps-formula-steps steps)
                   verbose-p
                   state)))
              (value (if (equal (length hyps) (length final-hyps))
                  nil
                  (make-defthm (car form)
                    name
                    final-hyps
                    concl
                    kwd-alist
                    let/let*
                    bindings))))))))))
remove-hyps-fnfunction
(defun remove-hyps-fn
  (form name hyps concl kwd-alist let/let* bindings verbose-p)
  `(make-event (er-let* ((new-form (remove-hyps-formula ',FORM
           ',NAME
           ',HYPS
           ',CONCL
           ',KWD-ALIST
           ',LET/LET*
           ',BINDINGS
           ',VERBOSE-P
           'remove-hyps
           state)) (thmp (value (eq (car ',FORM) 'thm))))
      (pprogn (cond ((null new-form) (fms "Note: REMOVE-HYPS left its input unchanged.~|~@0"
              (list (cons #\0
                  (if thmp
                    ""
                    "Now silently submitting the original ~
                                         form.~|")))
              (standard-co state)
              state
              nil))
          (t (fms "New form from REMOVE-HYPS:~|~%~x0~|~%~@1"
              (list (cons #\0 new-form)
                (cons #\1
                  (if thmp
                    ""
                    "Now silently submitting the new ~
                                           form (above).~|")))
              (standard-co state)
              state
              nil)))
        (value (if thmp
            '(value-triple :remove-hyps-completed)
            (list 'with-output
              :off :all :gag-mode t
              (or new-form ',FORM))))))))
remove-hypsmacro
(defmacro remove-hyps
  (form &optional verbose-p)
  (or (and (consp form)
      (member-eq (car form) '(defthm defthmd thm))
      (mv-let (name form-without-name)
        (if (eq (car form) 'thm)
          (mv nil (cdr form))
          (mv (cadr form) (cddr form)))
        (case-match form-without-name
          ((('implies hyp concl) . kwd-alist) (let ((hyps (if (and (consp hyp) (eq (car hyp) 'and))
                   (cdr hyp)
                   (list hyp))))
              (remove-hyps-fn form
                name
                hyps
                concl
                kwd-alist
                nil
                nil
                verbose-p)))
          (((let/let* bindings ('implies hyp concl)) . kwd-alist) (and (member-eq let/let*
                '(let let*
                  b*))
              (let ((hyps (if (and (consp hyp) (eq (car hyp) 'and))
                     (cdr hyp)
                     (list hyp))))
                (remove-hyps-fn form
                  name
                  hyps
                  concl
                  kwd-alist
                  let/let*
                  bindings
                  verbose-p))))
          (& nil))))
    `(er soft
      'remove-hyps
      "Illegal argument to remove-hyps:~|~%~y0"
      ',FORM)))
other
(logic)
local
(local (include-book "arithmetic/top" :dir :system))
local
(local (remove-hyps (defthm nth-append
      (implies (and (true-listp x) (natp n) (true-listp y))
        (equal (nth n (append x y))
          (if (< n (len x))
            (nth n x)
            (nth (- n (len x)) y))))
      :rule-classes nil)))
other
(set-enforce-redundancy t)
local
(local (defthm nth-append
    (implies (natp n)
      (equal (nth n (append x y))
        (if (< n (len x))
          (nth n x)
          (nth (- n (len x)) y))))
    :rule-classes nil))
other
(set-enforce-redundancy nil)
local
(local (remove-hyps (defthm nth-append-alt
      (implies (and (true-listp x) (natp n) (true-listp y))
        (equal (nth n (append x y))
          (if (not (natp n))
            (car (append x y))
            (if (< n (len x))
              (nth n x)
              (nth (- n (len x)) y)))))
      :rule-classes nil)))
other
(set-enforce-redundancy t)
local
(local (defthm nth-append-alt
    (equal (nth n (append x y))
      (if (not (natp n))
        (car (append x y))
        (if (< n (len x))
          (nth n x)
          (nth (- n (len x)) y))))
    :rule-classes nil))
other
(set-enforce-redundancy nil)
local
(local (remove-hyps (defthm nth-append-alt-2
      (let ((xx x))
        (implies (and (true-listp xx) (natp n) (true-listp y))
          (equal (nth n (append xx y))
            (if (< n (len x))
              (nth n x)
              (nth (- n (len xx)) y)))))
      :hints (("Goal'" :induct t)))))
other
(set-enforce-redundancy t)
local
(local (defthm nth-append-alt-2
    (let ((xx x))
      (declare (ignorable xx))
      (implies (natp n)
        (equal (nth n (append xx y))
          (if (< n (len x))
            (nth n x)
            (nth (- n (len xx)) y)))))
    :hints (("Goal'" :induct t))))