defopener - ACL2 Book

Included Books

bash

other

(in-package "ACL2")

include-book

(include-book "bash")

other

(program)

other

(set-state-ok t)

splitter1-pfunction

(defun splitter1-p
  (lit hyps-list found-negation)
  (cond ((null hyps-list) found-negation)
    ((member-term lit (car hyps-list)) (splitter1-p lit (cdr hyps-list) found-negation))
    ((member-complement-term lit (car hyps-list)) (splitter1-p lit (cdr hyps-list) t))
    (t nil)))

splitterfunction

(defun splitter
  (hyps hyps-list)
  (cond ((endp hyps) nil)
    ((splitter1-p (car hyps) hyps-list nil) (car hyps))
    (t (splitter (cdr hyps) hyps-list))))

concl-as-equiv-and-lhs-1function

(defun concl-as-equiv-and-lhs-1
  (equiv lhs concls)
  (cond ((endp concls) nil)
    (t (let ((term (car concls)))
        (case-match term
          ((!equiv !lhs &) (concl-as-equiv-and-lhs-1 equiv lhs (cdr concls)))
          (('not !lhs) (concl-as-equiv-and-lhs-1 equiv lhs (cdr concls)))
          (& (msg "The last literal of each clause generated is expected to ~
                   be of the form (equiv lhs rhs) for the same equiv and lhs. ~
                   The equiv for the last literal of the first clause is ~x0 ~
                   and its lhs is ~x1; but the last literal of one clause ~
                   generated is:~|~%~x2"
              equiv
              lhs
              term)))))))

concl-as-equiv-and-lhsfunction

(defun concl-as-equiv-and-lhs
  (concls equiv)
  (assert$ concls
    (let ((term (car concls)))
      (case-match term
        ((!equiv lhs &) (let ((msg (concl-as-equiv-and-lhs-1 equiv lhs (cdr concls))))
            (cond (msg (mv nil msg)) (t (mv equiv lhs)))))
        (('not lhs) (let ((msg (concl-as-equiv-and-lhs-1 equiv lhs (cdr concls))))
            (cond (msg (mv nil msg)) (t (mv equiv lhs)))))
        (& (mv nil
            (msg "The last literal of each clause generated is expected ~
                        to be of the form (equiv lhs rhs), the but last ~
                        literal of the first clause generated is:~|~%~x0"
              term)))))))

remove-termfunction

(defun remove-term
  (lit cl)
  (cond ((variablep lit) (remove1-eq lit cl))
    ((fquotep lit) (remove1-equal lit cl))
    ((member-equal lit cl) (remove1-equal lit cl))
    ((or (eq (ffn-symb lit) 'equal) (eq (ffn-symb lit) 'iff)) (let ((new-lit (fcons-term* (ffn-symb lit) (fargn lit 2) (fargn lit 1))))
        (assert$ (member-equal new-lit cl)
          (remove1-equal new-lit cl))))
    (t (assert$ (eq (ffn-symb lit) 'not)
        (let ((atm (fargn lit 1)))
          (assert$ (and (nvariablep atm)
              (not (fquotep atm))
              (or (eq (ffn-symb atm) 'equal) (eq (ffn-symb atm) 'iff)))
            (let* ((new-atm (fcons-term* (ffn-symb atm) (fargn atm 2) (fargn atm 1))) (new-lit (fcons-term* 'not new-atm)))
              (assert$ (member-equal new-lit cl)
                (remove1-equal new-lit cl)))))))))

split-cl-listfunction

(defun split-cl-list
  (splitter hyps-list
    concls
    pos-hyps-list
    pos-concls
    neg-hyps-list
    neg-concls)
  (cond ((endp hyps-list) (mv (reverse pos-hyps-list)
        (reverse pos-concls)
        (reverse neg-hyps-list)
        (reverse neg-concls)))
    ((member-term splitter (car hyps-list)) (split-cl-list splitter
        (cdr hyps-list)
        (cdr concls)
        (cons (remove-term splitter (car hyps-list)) pos-hyps-list)
        (cons (car concls) pos-concls)
        neg-hyps-list
        neg-concls))
    (t (assert$ (member-complement-term splitter (car hyps-list))
        (split-cl-list splitter
          (cdr hyps-list)
          (cdr concls)
          pos-hyps-list
          pos-concls
          (cons (remove-term (dumb-negate-lit splitter) (car hyps-list))
            neg-hyps-list)
          (cons (car concls) neg-concls))))))

index-of-shortest-recfunction

(defun index-of-shortest-rec
  (lst-lst len ans i)
  (cond ((endp lst-lst) ans)
    (t (let ((new-len (length (car lst-lst))))
        (if (< new-len len)
          (index-of-shortest-rec (cdr lst-lst) new-len i (1+ i))
          (index-of-shortest-rec (cdr lst-lst) len ans (1+ i)))))))

index-of-shortestfunction

(defun index-of-shortest
  (lst-lst)
  (declare (xargs :guard (and (true-list-listp lst-lst) lst-lst)))
  (index-of-shortest-rec (cdr lst-lst)
    (length (car lst-lst))
    0
    1))

member-equal-allfunction

(defun member-equal-all
  (x lst-lst)
  (cond ((endp lst-lst) t)
    (t (and (member-equal x (car lst-lst))
        (member-equal-all x (cdr lst-lst))))))

intersection-equal-with-allfunction

(defun intersection-equal-with-all
  (lst lst-lst)
  (cond ((endp lst) nil)
    ((member-equal-all (car lst) lst-lst) (cons (car lst)
        (intersection-equal-with-all (cdr lst) lst-lst)))
    (t (intersection-equal-with-all (cdr lst) lst-lst))))

all-set-difference-equalfunction

(defun all-set-difference-equal
  (lst-lst lst)
  (cond ((endp lst-lst) nil)
    (t (cons (set-difference-equal (car lst-lst) lst)
        (all-set-difference-equal (cdr lst-lst) lst)))))

defopener-remove1-by-positionfunction

(defun defopener-remove1-by-position
  (index lst)
  (if (endp lst)
    nil
    (if (zp index)
      (cdr lst)
      (cons (car lst)
        (defopener-remove1-by-position (1- index) (cdr lst))))))

split-clauses-to-term-recfunction

(defun split-clauses-to-term-rec
  (hyps-list concls)
  (let* ((splitter (splitter (car hyps-list) (cdr hyps-list))))
    (cond (splitter (mv-let (pos-hyps-list pos-concls neg-hyps-list neg-concls)
          (split-cl-list splitter hyps-list concls nil nil nil nil)
          (mv-let (flg1 neg)
            (split-clauses-to-term-rec neg-hyps-list neg-concls)
            (mv-let (flg2 pos)
              (split-clauses-to-term-rec pos-hyps-list pos-concls)
              (mv (or flg1 flg2)
                (if (equal neg pos)
                  pos
                  (fcons-term* 'if splitter neg pos)))))))
      ((null (cdr concls)) (mv nil (fargn (car concls) 2)))
      (t (mv t
          (let* ((i (index-of-shortest hyps-list)) (hyps (nth i hyps-list))
              (concl (nth i concls))
              (hyps-list (defopener-remove1-by-position i hyps-list))
              (concls (defopener-remove1-by-position i concls))
              (common-hyps (intersection-equal-with-all hyps hyps-list))
              (hyps-list (all-set-difference-equal hyps-list common-hyps))
              (hyps (set-difference-equal hyps common-hyps))
              (tbr (fargn concl 2)))
            (mv-let (flg fbr)
              (split-clauses-to-term-rec hyps-list concls)
              (declare (ignore flg))
              (if (equal tbr fbr)
                tbr
                (fcons-term* 'if
                  (conjoin (dumb-negate-lit-lst hyps))
                  tbr
                  fbr)))))))))

split-clauses-to-flg-term-pairfunction

(defun split-clauses-to-flg-term-pair
  (hyps-list concls)
  (mv-let (flg term)
    (split-clauses-to-term-rec hyps-list concls)
    (cons flg term)))

split-out-conclsfunction

(defun split-out-concls
  (cl-list hyps-list concls)
  (cond ((endp cl-list) (mv (reverse hyps-list) (reverse concls)))
    (t (split-out-concls (cdr cl-list)
        (cons (butlast (car cl-list) 1) hyps-list)
        (cons (car (last (car cl-list))) concls)))))

flatten-ifs-to-condfunction

(defun flatten-ifs-to-cond
  (term)
  (case-match term
    (('if tst ('if x y z) fbr) (flatten-ifs-to-cond `(if ,(CONJOIN2 TST X)
          ,Y
          (if ,(CONJOIN2 TST (DUMB-NEGATE-LIT X))
            ,Z
            ,FBR))))
    (('if tst tbr fbr) `(if ,(CONJOIN (FLATTEN-ANDS-IN-LIT TST))
        ,TBR
        ,(FLATTEN-IFS-TO-COND FBR)))
    (& term)))

bash-sim-fnfunction

(defun bash-sim-fn
  (form hints equiv ctx state)
  (er-let* ((cl-list (with-ctx-summarized ctx
         (simplify-with-prover form hints ctx state))))
    (mv-let (hyps-list concls)
      (split-out-concls cl-list nil nil)
      (mv-let (equiv lhs)
        (concl-as-equiv-and-lhs concls equiv)
        (cond (equiv (value (split-clauses-to-flg-term-pair hyps-list concls)))
          (t (er soft ctx "~@0" lhs)))))))

defopener-bodiesfunction

(defun defopener-bodies
  (call hyp equiv hints flatten ctx state)
  (let* ((equiv (or equiv 'equal)) (form0 (list equiv (list 'hide call) call))
      (form (if hyp
          `(implies ,HYP ,FORM0)
          form0))
      (wrld (w state)))
    (er-let* ((flg-rhs0-pair (bash-sim-fn form hints equiv ctx state)))
      (let* ((flg (car flg-rhs0-pair)) (rhs0 (cdr flg-rhs0-pair))
          (rhs1 (if flatten
              (flatten-ifs-to-cond rhs0)
              rhs0))
          (hidden-rhs (list 'hide (untranslate rhs1 nil wrld)))
          (rhs (untranslate rhs1 nil wrld)))
        (value (if hyp
            `((implies ,HYP (,EQUIV ,CALL ,HIDDEN-RHS)) (implies ,HYP (,EQUIV ,CALL ,RHS))
              ,HIDDEN-RHS . ,FLG)
            `((,EQUIV ,CALL ,HIDDEN-RHS) (,EQUIV ,CALL ,RHS)
              ,HIDDEN-RHS . ,FLG)))))))

defopener-hint-deffunction

(defun defopener-hint-def
  (flatten-failed-flg)
  `(defun defopener-hint
    (id clause world stable-under-simplificationp)
    (declare (ignore id world))
    (and stable-under-simplificationp
      (let ((term (car (last clause))))
        ,(COND
  (FLATTEN-FAILED-FLG
   '(CASE-MATCH TERM ((& & ('HIDE X)) (LIST :EXPAND (LIST (LIST 'HIDE X))))
                ((& ('HIDE X) &) (LIST :EXPAND (LIST (LIST 'HIDE X))))
                (('NOT ('HIDE X)) (LIST :EXPAND (LIST (LIST 'HIDE X))))
                (& NIL)))
  (T
   '(CASE-MATCH TERM
                ((& & ('HIDE X))
                 (LIST :EXPAND (LIST (LIST 'HIDE X)) :IN-THEORY
                       '(THEORY 'MINIMAL-THEORY)))
                ((& ('HIDE X) &)
                 (LIST :EXPAND (LIST (LIST 'HIDE X)) :IN-THEORY
                       '(THEORY 'MINIMAL-THEORY)))
                (('NOT ('HIDE X))
                 (LIST :EXPAND (LIST (LIST 'HIDE X)) :IN-THEORY
                       '(THEORY 'MINIMAL-THEORY)))
                (& NIL))))))))

chk-namemacro

(defmacro chk-name
  (name ctx ev-form)
  (let ((deflabel-form (list 'deflabel name)))
    `(make-event (let ((table-val (cdr (assoc-eq ',NAME (table-alist 'defopener-table (w state))))))
        (if table-val
          (if (equal table-val ',EV-FORM)
            (value '(value-triple t))
            (mv-let (erp val state)
              (er soft
                ',CTX
                "The name ~x0 was applied to an earlier, different ~
                           defopener event:~|~X12"
                ',NAME
                table-val
                nil)
              (declare (ignore erp val))
              (mv "Name check failed (see error message above)."
                nil
                state)))
          (mv-let (erp val state)
            (with-output :off :all (ld '(,DEFLABEL-FORM)
                :ld-error-action :error :ld-user-stobjs-modified-warning :same))
            (declare (ignore val))
            (if erp
              (mv-let (erp val state)
                (er soft
                  ',CTX
                  "The name ~x0 appears not to be new, as the form ~
                            ~x1 failed."
                  ',NAME
                  ',DEFLABEL-FORM)
                (declare (ignore erp val))
                (mv "Name check failed (see error message above)."
                  nil
                  state))
              (value '(value-triple nil :on-skip-proofs t)))))))))

other

(defxdoc defopener
  :parents (miscellaneous)
  :short "Create a defthm equating a call with its simplification."
  :long "<p>For a related tool, see @(see defopen).</p>

<p>Example:</p>

@({
  (include-book "misc/defopener" :dir :system)
  (defopener append-open
    (append x y)
    :hyp (and (true-listp x) (true-listp (cdr x)))
    :hints (("Goal" :expand ((append x y)))))
})

<p>The above example creates the following theorem.</p>

@({
  (DEFTHM APPEND-OPEN
    (IMPLIES (AND (TRUE-LISTP X)
                  (TRUE-LISTP (CDR X)))
             (EQUAL (APPEND X Y)
                    (IF (NOT X)
                        Y
                        (CONS (CAR X) (APPEND (CDR X) Y))))))
})

<p>In general, the form</p>

@({
  (defopener name
    term
    :hyp hyp
    ...)
})

<p>attempts to create a theorem of the form</p>

@({
  (DEFTHM NAME
    (IMPLIES HYP
             (EQUAL TERM rhs)))
})

<p>where @('rhs') is generated by ACL2's simplification routines.  If @(':hyp') is
omitted, then of course the resulting form has the expected shape:</p>

@({
  (DEFTHM NAME
    (EQUAL TERM rhs)).
})

<p>If an equivalence relation symbol is supplied for @(':equiv'), then
@('EQUAL') above will be replaced by that symbol.</p>

<p>The output can be rather verbose.  Once @('rhs') as above has been produced,
ACL2 will print out the theorem to be proved before starting its proof,
indicated as follows.</p>

@({
  @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

  >>> STARTING PROOF OF:

  (DEFTHM NAME
          ...)

  @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
})

<p>To abbreviate the above message, you can specify an @(tsee
evisc-tuple) using the @(':evisc-tuple') keyword of @('defopener'),
which is @('nil') by default.</p>

<p>The simplification that takes place uses a prover interface that is also
used in the distributed book @('misc/bash'), in which the following hint is
automatically generated for @('"Goal"'), though they can be overridden if
explicitly supplied in the @('defopener') form for @('"Goal"'):</p>

@({
  :do-not (generalize eliminate-destructors fertilize eliminate-irrelevance)
})

<p>A suitable @(':do-not-induct') hint is also generated, so that induction is
avoided during the simplification process.  This too can be overridden.</p>

<p>If you only want to see the generated theorem, and not the attempted proof
of it, use @(':debug t').  Alternatively, you may want to run without that
addition and then submit @(':')@(see pcb!) to grab the generated @(see
encapsulate) form to put into the book that you are developing.  Otherwise, the
@('defopener') form will call the ACL2 simplifier twice each time you certify
your book: once to generate the theorem, and once to prove it.</p>

<p>The @(':flatten') keyword is @('t') by default, and causes the result to be
of the form @('(cond (c1 v1) (c2 v2) ... (ck vk) (t v))').  That result is
actually produced from a more primitive tree-based result, of the form @('(if c
v1 v2)'), where @('v1') and @('v2') can themselves be calls of @('if').  If you
prefer the more primitive form, use @(':flatten nil').</p>

<p>None of the arguments of this macro is evaluated.</p>

<p>This tool is heuristic in nature, and failures are possible.  The error
message might provide debugging clues.  Let us consider an example that
actually occurred that generated an error message of the following form.</p>

@({
ACL2 Error in (DEFOPENER MY-DEFOPENER-RULE ...):  The last literal
of each clause generated is expected to be of the form (equiv lhs rhs)
for the same equiv and lhs. The equiv for the last literal of the first
clause is EQUAL and its lhs is (HIDE (FOO X Y)) but the last literal of
one clause generated is:

(MY-PREDICATE (HIDE (FOO X Y)))
})

<p>The message suggests that each goal (i.e., clause) after the first should be
of the form @('(implies ... (equal (HIDE (FOO X Y)) ...))') or simply
@('(equal (HIDE (FOO X Y)) ...)'); but in this case, one goal was actually of
the form @('(IMPLIES ... (MY-PREDICATE (HIDE (FOO X Y))))').  After first
executing @('(set-gag-mode nil)') and then running @('defopener') again, the
proof log helped to discover a rewrite rule of the following form.</p>

@({
(equal (equal (f1 a)
              b)
       (and (my-predicate b)
            ...))
})

<p>ACL2 was able to match the term @('(EQUAL (HIDE (FOO X Y)) (F1 A)')) with
the left-hand side of the above rule, thus rewriting it to a conjunction whose
first conjunct was @('(MY-PREDICATE (HIDE (FOO X Y)))').  The error disappeared
after that rule was disabled.</p>")

defopenermacro

(defmacro defopener
  (&whole ev-form
    name
    call
    &key
    hyp
    equiv
    hints
    debug
    (flatten 't)
    (evisc-tuple 'nil))
  (let* ((ctx (cons 'defopener name)) (form `(er-let* ((name-chk (chk-name ,NAME ,CTX ,EV-FORM)))
          (if name-chk
            (value '(value-triple :redundant))
            (er-let* ((_defopener-bodies (defopener-bodies ',CALL
                   ',HYP
                   ',EQUIV
                   ',HINTS
                   ',FLATTEN
                   ',CTX
                   state)))
              (let* ((hidden-body (car _defopener-bodies)) (unhidden-body (cadr _defopener-bodies))
                  (hidden-rhs (caddr _defopener-bodies))
                  (flatten-failed-flg (cdddr _defopener-bodies))
                  (defthm-form1 (list 'defthm
                      'defopener-temp
                      hidden-body
                      ,@(AND HINTS `(:HINTS ',HINTS))
                      :rule-classes nil))
                  (defthm-form2 (list 'defthm ',NAME unhidden-body))
                  (defthm-form (append defthm-form2
                      (list :hints (list (list "Goal"
                            :use 'defopener-temp
                            :expand (list hidden-rhs)
                            :in-theory '(theory 'minimal-theory))))))
                  (table-ev '(table defopener-table ',NAME ',EV-FORM)))
                (pprogn (fms "@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@~|~%"
                    nil
                    (proofs-co state)
                    state
                    ,EVISC-TUPLE)
                  (if flatten-failed-flg
                    (warning$ ',CTX
                      nil
                      "An incomplete case split for ~
                                      distinguishing hypothesis lists may ~
                                      lead to failure.")
                    state)
                  ,(IF DEBUG
     'STATE
     `(FMS ">>> STARTING PROOF ~
                                 OF:~|~%~x0~|~%@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@~|~%"
           (LIST (CONS #\0 DEFTHM-FORM2)) (PROOFS-CO STATE) STATE ,EVISC-TUPLE))
                  (value `(encapsulate nil
                      ,TABLE-EV
                      (local (encapsulate nil
                          (local ,(DEFOPENER-HINT-DEF FLATTEN-FAILED-FLG))
                          (add-default-hints '(defopener-hint))
                          ,DEFTHM-FORM1))
                      ,DEFTHM-FORM)))))))))
    (if debug
      form
      `(make-event (mv-let (erp val state)
          ,FORM
          (if erp
            (mv "Defopener failed.  Error messages above should ~
                         explain."
              nil
              state)
            (value val)))))))