Included Books
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
other
(defxdoc dft :parents (defthm events) :short "Provide an explicit proof, for example chaining equalities" :long "<p>@('Dft') is a proof-checking-like macro that allows you to chain together equalities. The name @('"dft"') is short for @('"defthm"'). In the @(see community-books) see @('books/misc/dft-ex.lisp') for some examples.</p> <p>This tool has not been used in big proofs and probably can be improved quite a bit. The author encourages users to build improved versions.</p>")
enable-disablemacro
(defmacro enable-disable (a b) `(set-difference-theories (enable ,@A) ',B))
undeft-termpmutual-recursion
(mutual-recursion (defun undeft-termp (x) (declare (xargs :mode :program)) (cond ((atom x) nil) ((not (true-listp x)) `(er soft 'deft "Untranslated terms encountered by DEFT must be true-lists, but ~p0 ~ is not." ',X)) ((eq (car x) 'quote) (cond ((= (length x) 2) nil) (t `(er soft 'deft "QUOTEd terms such as ~p0 must have length 2." ',X)))) ((or (not (symbolp (car x))) (member-eq (car x) '(cond let let*))) `(er soft 'deft "We do not permit ~p0 as a function symbol." ',(CAR X))) (t (undeft-termp-lst (cdr x))))) (defun undeft-termp-lst (lst) (declare (xargs :mode :program)) (cond ((atom lst) t) (t (or (undeft-termp (car lst)) (undeft-termp-lst (cdr lst)))))))
dterm-all-varsmutual-recursion
(mutual-recursion (defun dterm-all-vars (dterm vars) (declare (xargs :mode :program)) (cond ((atom dterm) (cond ((and (symbolp dterm) (eq (legal-variable-or-constant-namep dterm) 'variable)) (add-to-set-eq dterm vars)) (t vars))) ((eq (car dterm) 'quote) vars) (t (dterm-all-vars-lst (cdr dterm) vars)))) (defun dterm-all-vars-lst (lst vars) (declare (xargs :mode :program)) (cond ((atom lst) vars) (t (dterm-all-vars-lst (cdr lst) (dterm-all-vars (car lst) vars))))))
dterm-sublismutual-recursion
(mutual-recursion (defun dterm-sublis (alist dterm) (declare (xargs :mode :program)) (let ((pair (assoc-equal dterm alist))) (cond (pair (cdr pair)) ((atom dterm) dterm) ((eq (car dterm) 'quote) dterm) (t (cons (car dterm) (dterm-sublis-lst alist (cdr dterm))))))) (defun dterm-sublis-lst (alist lst) (declare (xargs :mode :program)) (cond ((null lst) nil) (t (cons (dterm-sublis alist (car lst)) (dterm-sublis-lst alist (cdr lst)))))))
dterm-sublis-subst-to-alistfunction
(defun dterm-sublis-subst-to-alist (alist subst) (declare (xargs :mode :program)) (cond ((null subst) nil) (t (cons (cons (caar subst) (dterm-sublis alist (cadr (car subst)))) (dterm-sublis-subst-to-alist alist (cdr subst))))))
dterm-sublis-substfunction
(defun dterm-sublis-subst (alist subst) (declare (xargs :mode :program)) (let ((alist2 (dterm-sublis-subst-to-alist alist subst))) (pairlis$ (strip-cars alist2) (pairlis$ (strip-cdrs alist2) nil))))
assoc-keys-other-thanfunction
(defun assoc-keys-other-than (lst alist) (declare (xargs :mode :program)) (cond ((null alist) nil) ((member-eq (caar alist) lst) (assoc-keys-other-than lst (cdr alist))) (t (cons (caar alist) (assoc-keys-other-than lst (cdr alist))))))
dterm-sublis-into-lmifunction
(defun dterm-sublis-into-lmi (alist lmi) (declare (xargs :mode :program)) (cond ((atom lmi) lmi) ((eq (car lmi) :instance) (list* :instance (dterm-sublis-into-lmi alist (cadr lmi)) (dterm-sublis-subst alist (cddr lmi)))) (t lmi)))
dterm-sublis-into-use-hintfunction
(defun dterm-sublis-into-use-hint (alist lst) (declare (xargs :mode :program)) (cond ((null lst) nil) (t (cons (dterm-sublis-into-lmi alist (car lst)) (dterm-sublis-into-use-hint alist (cdr lst))))))
convert-keyword-alist-to-alistfunction
(defun convert-keyword-alist-to-alist (bindings keyword-alist) (declare (xargs :mode :program)) (cond ((atom keyword-alist) nil) (t (cons (cons (car keyword-alist) (cond ((eq (car keyword-alist) :use) (cond ((and (consp (cadr keyword-alist)) (eq (car (cadr keyword-alist)) :instance)) (dterm-sublis-into-lmi bindings (cadr keyword-alist))) (t (dterm-sublis-into-use-hint bindings (cadr keyword-alist))))) (t (cadr keyword-alist)))) (convert-keyword-alist-to-alist bindings (cddr keyword-alist))))))
negate-dtermfunction
(defun negate-dterm (dterm) (declare (xargs :mode :program)) (cond ((equal dterm t) nil) ((equal dterm nil) t) ((and (consp dterm) (eq (car dterm) 'not)) (cadr dterm)) (t (list 'not dterm))))
conjoin-dtermsfunction
(defun conjoin-dterms (dterm1 dterm2) (declare (xargs :mode :program)) (cond ((equal dterm1 nil) nil) ((equal dterm2 nil) nil) ((equal dterm1 t) dterm2) ((equal dterm2 t) dterm1) (t (let ((lst1 (case-match dterm1 (('and . terms) terms) (& (list dterm1)))) (lst2 (case-match dterm2 (('and . terms) terms) (& (list dterm2))))) (cons 'and (append lst1 lst2))))))
implicate-dtermsfunction
(defun implicate-dterms (dhyp dconcl) (declare (xargs :mode :program)) (cond ((eq dhyp t) dconcl) (t (case-match dconcl (('implies hyps concl) (list 'implies (conjoin-dterms hyps dhyp) concl)) (& (list 'implies dhyp dconcl))))))
dterm-hypfunction
(defun dterm-hyp (dterm) (declare (xargs :mode :program)) (case-match dterm (('implies hyp &) hyp) (& t)))
dterm-conclfunction
(defun dterm-concl (dterm) (declare (xargs :mode :program)) (case-match dterm (('implies & concl) concl) (& dterm)))
apply-proof-stepfunction
(defun apply-proof-step (dhyp1 dterm) (declare (xargs :mode :program)) (let ((dhyp2 (dterm-hyp dterm)) (dconcl (dterm-concl dterm))) (case-match dhyp1 (('equal lhs rhs) (let ((dconcl2 (dterm-sublis (list (cons lhs rhs)) dconcl))) (cond ((equal dconcl2 dconcl) (implicate-dterms (conjoin-dterms dhyp2 dhyp1) dconcl)) (t (implicate-dterms dhyp2 dconcl2))))) (& (implicate-dterms (conjoin-dterms dhyp2 dhyp1) dconcl)))))
pairlis1function
(defun pairlis1 (x1 lst) (declare (xargs :mode :program)) (cond ((null lst) nil) (t (cons (cons x1 (car lst)) (pairlis1 x1 (cdr lst))))))
generalization-phrasepfunction
(defun generalization-phrasep (all-vars bindings phrase new-hyps alist) (declare (xargs :mode :program)) (cond ((atom phrase) (mv nil (dterm-sublis-lst alist (reverse new-hyps)) (reverse alist))) ((keywordp (car phrase)) (mv `(er soft 'deft "It is illegal to put a hint inside a generalization step. The ~ usual intent is to aid the proof of a restriction on some ~ variable, as in (GENERALIZE expr TO var WHERE (p var) ~p0...). ~ The proper way to achieve this is to OBSERVE that expr has the ~ desired property before its generalization to var, as in ~ (OBSERVE (p expr) ~p0 ...) (GENERALIZE expr TO ar)." ',(CAR PHRASE)) nil nil)) ((eq (car phrase) 'and) (generalization-phrasep all-vars bindings (cdr phrase) new-hyps alist)) ((and (consp (cdr phrase)) (eq (cadr phrase) 'to) (consp (cddr phrase)) (symbolp (caddr phrase)) (not (member-eq (caddr phrase) all-vars))) (let* ((expr (dterm-sublis bindings (car phrase))) (var (caddr phrase)) (hyp (if (and (consp (cdddr phrase)) (eq (cadddr phrase) 'where) (car (cddddr phrase))) (dterm-sublis bindings (car (cddddr phrase))) nil)) (phrase1 (if hyp (cdr (cddddr phrase)) (cdddr phrase)))) (generalization-phrasep (cons var all-vars) bindings phrase1 (if hyp (cons hyp new-hyps) new-hyps) (cons (cons var expr) alist)))) (t (mv `(er soft 'deft "Illegal GENERALIZATION step. We expected to see repetitions ~ of the phrases `expr TO var' or `expr TO var WHERE ~ restriction', possibly separated by `and', where var is a ~ variable not previously involved in the problem; ~p0 cannot be ~ parsed that way." ',PHRASE) nil nil))))
translate-proof1mutual-recursion
(mutual-recursion (defun translate-proof1 (dname dterm proof addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair) (declare (xargs :mode :program)) (cond ((null proof) (mv-let (er-form event addr1) (deft-fn dname dterm addr bindings `((:use . ,(REVAPPEND CNAMES (REVERSE USE-HINT))) (:in-theory quote nil)) nil :default nil) (cond (er-form (mv er-form nil nil)) (t (mv nil (cons event revents) addr1))))) (t (let ((proof-step (car proof))) (case-match proof-step (('case test . subproof) (let* ((case-name (packn `(* ,ADDR))) (test (if (eq test 'otherwise) otherwise-term (dterm-sublis bindings test))) (case-dterm (implicate-dterms test dterm))) (mv-let (er-form revents1 addr1) (translate-proof1 case-name case-dterm (if (member-equal subproof '((easy) (trivial))) nil subproof) (1+ addr) bindings revents t (dterm-hyp case-dterm) nil use-hint nil nil) (cond (er-form (mv er-form nil nil)) (t (translate-proof1 dname dterm (cdr proof) addr1 bindings revents1 (conjoin-dterms otherwise-term (negate-dterm test)) xhyp (cons case-name cnames) use-hint nil nil)))))) (('let var & expr) (translate-proof1 dname dterm (cdr proof) addr (cons (cons var (dterm-sublis bindings expr)) bindings) revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (('theorem dthm . h-alist) (let* ((theorem-name (packn `(* ,ADDR))) (pass-bindings-downp (and (consp h-alist) (eq (car h-alist) :pass-bindings-downp))) (h-alist (if pass-bindings-downp (cdr h-alist) h-alist))) (mv-let (er-form event addr1) (deft-fn theorem-name dthm (1+ addr) (if pass-bindings-downp bindings nil) (convert-keyword-alist-to-alist bindings h-alist) nil :default nil) (cond (er-form (mv er-form nil nil)) (t (translate-proof1 dname dterm (cdr proof) addr1 bindings (cons event revents) otherwise-term xhyp cnames use-hint nil (cons theorem-name dthm))))))) (('instantiate-just-proved-theorem . rest) (translate-proof1 dname dterm (cons (cons 'instantiate rest) (cdr proof)) addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (('instantiate . subst) (cond (thm-pair (let* ((alist (dterm-sublis-subst-to-alist bindings subst)) (subst (pairlis$ (strip-cars alist) (pairlis$ (strip-cdrs alist) nil))) (dthm-inst (dterm-sublis alist (cdr thm-pair)))) (translate-proof1 dname dterm (cdr proof) addr bindings revents otherwise-term (conjoin-dterms xhyp dthm-inst) cnames (cons `(:instance ,(CAR THM-PAIR) ,@SUBST) use-hint) nil thm-pair))) (t (mv `(er soft 'deft "It is illegal to use INSTANTIATE except when it ~ immediately follows THEOREM or another INSTANTIATE.") nil nil)))) (('generalize . generalization-phrase) (mv-let (er-form new-hyps alist) (generalization-phrasep (dterm-all-vars dterm nil) bindings generalization-phrase nil nil) (cond (er-form (mv er-form nil nil)) (t (translate-proof1 dname dterm `(,@(PAIRLIS1 'OBSERVE (PAIRLIS-X2 NEW-HYPS NIL)) (theorem ,(DTERM-SUBLIS (PAIRLIS$ (STRIP-CDRS ALIST) (STRIP-CARS ALIST)) (IMPLICATE-DTERMS (COND ((NULL NEW-HYPS) XHYP) ((NULL (CDR NEW-HYPS)) (CONJOIN-DTERMS XHYP (CAR NEW-HYPS))) (T (CONJOIN-DTERMS XHYP (CONS 'AND NEW-HYPS)))) (DTERM-CONCL DTERM))) :pass-bindings-downp :proof ,(CDR PROOF)) (instantiate ,@(PAIRLIS$ (STRIP-CARS ALIST) (PAIRLIS-X2 (STRIP-CDRS ALIST) NIL)))) addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair))))) (('so-it-suffices-to-prove . rest) (translate-proof1 dname dterm (cons (cons 'so rest) (cdr proof)) addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (('so new-dterm) (let ((new-dterm (dterm-sublis bindings new-dterm)) (goal-name-suff (packn `(* ,ADDR -sufficient))) (goal-name (packn `(* ,ADDR)))) (mv-let (er-form event addr1) (deft-fn goal-name-suff (implicate-dterms new-dterm dterm) (+ 2 addr) bindings `((:use . ,(REVAPPEND CNAMES (REVERSE USE-HINT))) (:in-theory quote nil)) nil :default nil) (cond (er-form (mv er-form nil nil)) (t (mv-let (er-form revents addr2) (translate-proof1 goal-name new-dterm (cdr proof) addr1 bindings (cons event revents) otherwise-term (dterm-hyp new-dterm) nil nil nil nil) (cond (er-form (mv er-form nil nil)) (t (mv-let (er-form event addr3) (deft-fn dname dterm addr2 bindings `((:use ,GOAL-NAME-SUFF ,GOAL-NAME) (:in-theory quote nil)) nil :default nil) (cond (er-form (mv er-form nil nil)) (t (mv nil (cons event revents) addr3)))))))))))) (('observe obs-dterm . h-alist) (let* ((obs-dterm (dterm-sublis bindings obs-dterm)) (step-name (packn `(* ,ADDR))) (pass-consider-dtermp (and (consp h-alist) (eq (car h-alist) :pass-consider-dtermp))) (h-alist (if pass-consider-dtermp (cdr h-alist) h-alist))) (mv-let (er-form event addr1) (deft-fn step-name (implicate-dterms xhyp obs-dterm) (1+ addr) bindings (convert-keyword-alist-to-alist bindings h-alist) nil :default nil) (cond (er-form (mv er-form nil nil)) (t (translate-proof1 dname dterm (cdr proof) addr1 bindings (cons event revents) otherwise-term (conjoin-dterms xhyp obs-dterm) cnames (cons step-name use-hint) (if pass-consider-dtermp consider-dterm nil) nil)))))) (('consider dterm1) (translate-proof1 dname dterm (cdr proof) addr bindings revents otherwise-term xhyp cnames use-hint (dterm-sublis bindings dterm1) nil)) (('= dterm1 . h-alist) (translate-proof2 '= 'equal dterm1 h-alist dname dterm proof addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (('<-> dterm1 . h-alist) (translate-proof2 '<-> 'iff dterm1 h-alist dname dterm proof addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (('-> dterm1 . h-alist) (translate-proof2 '-> 'implies dterm1 h-alist dname dterm proof addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (('< dterm1 . h-alist) (translate-proof2 '< '< dterm1 h-alist dname dterm proof addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (('<= dterm1 . h-alist) (translate-proof2 '<= '<= dterm1 h-alist dname dterm proof addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (('> dterm1 . h-alist) (translate-proof2 '> '> dterm1 h-alist dname dterm proof addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (('>= dterm1 . h-alist) (translate-proof2 '>= '>= dterm1 h-alist dname dterm proof addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair)) (& (mv `(er soft 'deft "Unrecognized proof step, ~p0." ',PROOF-STEP) nil nil))))))) (defun translate-proof2 (symbol fn dterm1 h-alist dname dterm proof addr bindings revents otherwise-term xhyp cnames use-hint consider-dterm thm-pair) (declare (xargs :mode :program)) (declare (ignore thm-pair)) (cond (consider-dterm (let ((dterm1 (dterm-sublis bindings dterm1))) (translate-proof1 dname dterm (cons `(observe (,FN ,CONSIDER-DTERM ,DTERM1) :pass-consider-dtermp . ,H-ALIST) (cdr proof)) addr bindings revents otherwise-term xhyp cnames use-hint dterm1 nil))) (t (mv `(er soft 'deft "The ~p0 relation, as in (~p0 ~p1 ...), may be used only immediately after CONSIDER ~ or another ~p0 or similar relation." ',SYMBOL ',DTERM1) nil nil)))) (defun translate-proof (name dterm proof addr bindings rule-classes otf-flg doc) (declare (xargs :mode :program)) (mv-let (er-form revents addr) (translate-proof1 name dterm proof addr bindings nil t (dterm-hyp dterm) nil nil nil nil) (cond (er-form (mv er-form nil nil)) (t (let* ((hints (cadr (assoc-keyword :hints (cdddr (car revents))))) (main `(defthm ,NAME ,DTERM ,@(AND DOC `(:DOC ,DOC)) ,@(AND (NOT (EQ OTF-FLG :DEFAULT)) `(:OTF-FLG ,OTF-FLG)) ,@(AND (NOT (EQ RULE-CLASSES :DEFAULT)) `(:RULE-CLASSES ,RULE-CLASSES)) ,@(AND HINTS `(:HINTS ,HINTS)))) (local-events (reverse (cdr revents)))) (cond ((null local-events) (mv nil main addr)) ((null (cdr local-events)) (mv nil `(encapsulate nil (local ,(CAR LOCAL-EVENTS)) ,MAIN) addr)) (t (mv nil `(encapsulate nil (local (encapsulate nil ,@LOCAL-EVENTS)) ,MAIN) addr)))))))) (defun deft-fn (name term addr bindings h-alist rule-classes otf-flg doc) (declare (xargs :mode :program)) (let ((proof (cdr (assoc-eq :proof h-alist)))) (cond (proof (let ((bad (assoc-keys-other-than '(:proof) h-alist))) (cond (bad (mv `(er soft 'deft "It is illegal to supply both a :PROOF hint and any other ~ proof-time advice. You supplied ~&1." ',BAD) nil nil)) (t (translate-proof name term proof addr bindings rule-classes otf-flg doc))))) (t (let ((bad (assoc-keys-other-than '(:proof :in-theory :enable :disable :use :expand :cases :induct :by :restrict :do-not :do-not-induct :hints) h-alist)) (in-theory (cdr (assoc :in-theory h-alist))) (enable (cdr (assoc :enable h-alist))) (disable (cdr (assoc :disable h-alist))) (use (cdr (assoc :use h-alist))) (expand (cdr (assoc :expand h-alist))) (cases (cdr (assoc :cases h-alist))) (induct (cdr (assoc :induct h-alist))) (by (cdr (assoc :by h-alist))) (restrict (cdr (assoc :restrict h-alist))) (do-not (cdr (assoc :do-not h-alist))) (do-not-induct (cdr (assoc :do-not-induct h-alist))) (hints (cdr (assoc :hints h-alist)))) (cond (bad (mv `(er soft 'deft "Unrecognized keyword argument~#0~[~/s~], ~&0." ',(REVERSE BAD)) nil nil)) ((and (or (assoc-equal "Goal" hints) (assoc-equal "goal" hints)) (or in-theory enable disable use expand cases induct by restrict do-not do-not-induct)) (mv '(er soft 'deft "It is not permitted to supply both a :HINTS argument for ~ "Goal" and any of :IN-THEORY, :ENABLE, :DISABLE, :USE, ~ :EXPAND, :CASES, :INDUCT, :RESTRICT, :BY, :DO-NOT, or ~ :DO-NOT-INDUCT (which are implicitly for "Goal") ~ because DEFT does not know how to combine hints.") nil nil)) ((and in-theory (or enable disable)) (mv '(er soft 'deft "It is not permitted to supply both an :IN-THEORY ~ argument and either of :ENABLE or :DISABLE, because DEFT ~ does not know how to combine theory hints.") nil nil)) (t (mv nil `(defthm ,NAME ,TERM ,@(AND DOC `(:DOC ,DOC)) ,@(AND (NOT (EQ OTF-FLG :DEFAULT)) `(:OTF-FLG ,OTF-FLG)) ,@(AND (NOT (EQ RULE-CLASSES :DEFAULT)) `(:RULE-CLASSES ,RULE-CLASSES)) ,@(AND HINTS (NOT (OR IN-THEORY ENABLE DISABLE USE EXPAND CASES RESTRICT INDUCT BY DO-NOT DO-NOT-INDUCT)) `(:HINTS ,HINTS)) ,@(AND (OR IN-THEORY ENABLE DISABLE USE EXPAND CASES RESTRICT INDUCT BY DO-NOT DO-NOT-INDUCT) `(:HINTS (("Goal" ,@(AND IN-THEORY `(:IN-THEORY ,IN-THEORY)) ,@(AND (OR ENABLE DISABLE) `(:IN-THEORY (ENABLE-DISABLE (,@(COND ((NULL ENABLE) NIL) ((OR (ATOM ENABLE) (KEYWORDP (CAR ENABLE))) (LIST ENABLE)) (T ENABLE))) (,@(COND ((NULL DISABLE) NIL) ((OR (ATOM DISABLE) (KEYWORDP (CAR DISABLE))) (LIST DISABLE)) (T DISABLE)))))) ,@(AND USE `(:USE ,USE)) ,@(AND EXPAND `(:EXPAND ,EXPAND)) ,@(AND CASES `(:CASES ,CASES)) ,@(AND RESTRICT `(:RESTRICT ,RESTRICT)) ,@(AND INDUCT `(:INDUCT ,INDUCT)) ,@(AND BY `(:BY ,BY)) ,@(AND DO-NOT `(:DO-NOT ,DO-NOT)) ,@(AND DO-NOT-INDUCT `(:DO-NOT-INDUCT ,DO-NOT-INDUCT))) ,@HINTS)))) addr)))))))))
delete-null-cdrsfunction
(defun delete-null-cdrs (alist) (declare (xargs :mode :program)) (cond ((atom alist) nil) ((null (cdar alist)) (delete-null-cdrs (cdr alist))) (t (cons (car alist) (delete-null-cdrs (cdr alist))))))
dftmacro
(defmacro dft (&whole event-form name term &key proof doc (rule-classes ':default) (otf-flg ':default) in-theory enable disable use expand cases induct by restrict do-not do-not-induct hints) (declare (ignore event-form)) (mv-let (er-form event addr) (deft-fn name term 1 nil (delete-null-cdrs `((:proof . ,PROOF) (:in-theory . ,IN-THEORY) (:enable . ,ENABLE) (:disable . ,DISABLE) (:use . ,USE) (:expand . ,EXPAND) (:cases . ,CASES) (:induct . ,INDUCT) (:by . ,BY) (:restrict . ,RESTRICT) (:do-not . ,DO-NOT) (:do-not-induct . ,DO-NOT-INDUCT) (:hints . ,HINTS))) rule-classes otf-flg doc) (declare (ignore addr)) (cond (er-form er-form) (t event))))