Included Books
other
(in-package "ACL2")
include-book
(include-book "xdoc/top" :dir :system)
other
(defxdoc expander :parents (miscellaneous) :short "Routines for simplifying terms." :long "<p>NOTE: If you are looking for a simple interface to the ACL2 rewriter, see @(see rewrite$).</p> <p>The routines provided by the expander can be useful in generating theorems and simplifying expressions, under given assumptions.</p> <p>They were developed rather in a hurry and should be used without expecting the usual standards of care present in development of ACL2 code. Once these routines are used to generate theorems for you, you should check the theorems directly with ACL2.</p> <p>To load the expander, run:</p> @({ (include-book "misc/expander" :dir :system) })")
other
(set-state-ok t)
encapsulate
(encapsulate ((hidden-expander-function (x) t)) (logic) (local (defun hidden-expander-function (x) x)))
silly-rec-fn-for-rewrite*function
(defun silly-rec-fn-for-rewrite* (x) (declare (xargs :verify-guards t)) (if (consp x) (silly-rec-fn-for-rewrite* (cdr x)) x))
other
(program)
*valid-output-names-except-error*constant
(defconst *valid-output-names-except-error* (set-difference-eq *valid-output-names* '(error)))
tool1macro
(defmacro tool1 (hyps &key hints (prove-assumptions 't) inhibit-output) `(er-progn (tool1-fn ',HYPS state ',HINTS ',PROVE-ASSUMPTIONS ',INHIBIT-OUTPUT t t) (value :invisible)))
pop-clausesfunction
(defun pop-clauses (pool) (mv-let (signal pool-lst cl-set hint-settings pop-history new-pool) (pop-clause1 pool nil) (declare (ignore pool-lst hint-settings pop-history)) (cond ((or (eq signal 'win) (eq signal 'lose)) (mv signal cl-set)) (t (mv-let (signal rest-clauses) (pop-clauses new-pool) (cond ((eq signal 'win) (mv 'win (append cl-set rest-clauses))) (t (mv signal nil))))))))
prove-loop1-clausesfunction
(defun prove-loop1-clauses (pool-lst clauses pspv hints ens wrld ctx state) (sl-let (erp pspv jppl-flg state) (waterfall 0 pool-lst clauses pspv hints ens wrld ctx state (initial-step-limit wrld state)) (declare (ignore jppl-flg)) (cond (erp (mv step-limit t nil nil nil nil state)) (t (mv-let (signal new-clauses) (pop-clauses (access prove-spec-var pspv :pool)) (cond ((eq signal 'lose) (mv step-limit t nil nil nil nil state)) (t (mv-let (pairs new-pspv state) (process-assumptions 0 pspv wrld state) (mv-let (erp ttree state) (accumulate-ttree-and-step-limit-into-state (access prove-spec-var new-pspv :tag-tree) step-limit state) (assert$ (null erp) (mv step-limit nil ttree new-clauses pairs new-pspv state)))))))))))
prove-loop-clausesfunction
(defun prove-loop-clauses (clauses pspv hints ens wrld ctx state) (pprogn (increment-timer 'other-time state) (sl-let (erp ttree new-clauses pairs new-pspv state) (prove-loop1-clauses nil clauses pspv hints ens wrld ctx state) (pprogn (increment-timer 'prove-time state) (cond (erp (mv step-limit erp nil nil nil nil state)) (t (mv step-limit nil ttree new-clauses pairs new-pspv state)))))))
prove-clausesfunction
(defun prove-clauses (term pspv hints ens wrld ctx state) (prog2$ (semi-initialize-brr-wormhole state) (sl-let (erp ttree1 clauses pairs new-pspv state) (prove-loop-clauses (list (list term)) (change prove-spec-var pspv :user-supplied-term term :orig-hints hints) hints ens wrld ctx state) (cond (erp (mv step-limit t nil nil nil nil state)) (t (mv-let (erp val state) (chk-assumption-free-ttree ttree1 ctx state) (declare (ignore val)) (cond (erp (mv step-limit t nil nil nil nil state)) (t (pprogn (let ((byes (tagged-objects :bye ttree1))) (cond (byes (pprogn (io? prove nil state (wrld byes) (fms "To complete this proof you should try to ~ admit the following ~ event~#0~[~/s~]~|~%~*1~%See the discussion ~ of :by hints in :DOC hints regarding the ~ name~#0~[~/s~] displayed above." (list (cons #\0 byes) (cons #\1 (list "" "~|~ ~y*." "~|~ ~y*,~|and~|" "~|~ ~y*,~|~%" (make-defthm-forms-for-byes byes wrld)))) (proofs-co state) state nil)) state)) (t state))) (mv step-limit erp ttree1 clauses pairs (change prove-spec-var new-pspv :pool nil) state))))))))))
untranslate-clause-lstfunction
(defun untranslate-clause-lst (cl-lst wrld) (cond ((null cl-lst) nil) (t (cons (prettyify-clause1 (car cl-lst) wrld) (untranslate-clause-lst (cdr cl-lst) wrld)))))
tool1-printfunction
(defun tool1-print (print-flg runes clauses state) (cond (print-flg (fms "~%***OUTPUT OF TOOL1***~%~%Tag tree:~% ~x0~%~%List of simplified ~ hypotheses:~% ~x1~|~%" (list (cons #\0 runes) (cons #\1 (untranslate-clause-lst clauses (w state)))) *standard-co* state nil)) (t state)))
hide-special-hypsfunction
(defun hide-special-hyps (lst) "We do this stuff so that equalities and SYNP hyps won't be thrown out. Perhaps what we really need is a hyp simplifier with less aggressive heuristics." (cond ((null lst) nil) (t (let ((hyp (car lst))) (let ((new-hyp (case-match hyp (('equal x y) (let ((x1 (if (variablep x) (list 'hide x) x)) (y1 (if (variablep y) (list 'hide y) y))) (list 'equal x1 y1))) (('synp . x) (list 'hide (cons 'synp x))) (& hyp)))) (cons new-hyp (hide-special-hyps (cdr lst))))))))
fix-special-hypsfunction
(defun fix-special-hyps (lst) (cond ((null lst) nil) (t (let ((hyp (car lst))) (let ((new-hyp (case-match hyp (('not ('equal ('hide x) ('hide y))) (list 'not (list 'equal x y))) (('not ('equal ('hide x) y)) (list 'not (list 'equal x y))) (('not ('equal y ('hide x))) (list 'not (list 'equal y x))) (('not ('hide ('synp . x))) (list 'not (cons 'synp x))) (& hyp)))) (cons new-hyp (fix-special-hyps (cdr lst))))))))
add-key-val-pair-to-key-val-alistfunction
(defun add-key-val-pair-to-key-val-alist (key key1 val alist) (cond ((null alist) (list (list key key1 val))) ((equal key (caar alist)) (cons (list* key key1 val (cdar alist)) (cdr alist))) (t (cons (car alist) (add-key-val-pair-to-key-val-alist key key1 val (cdr alist))))))
get-assnsfunction
(defun get-assns (ttree remove-hidden) (cond (remove-hidden (remove-hidden-expander-term-from-cl-list (strip-cdrs (tagged-objects :bye ttree)))) (t (strip-cdrs (tagged-objects :bye ttree)))))
tool1-fn1function
(defun tool1-fn1 (hyps ctx ens wrld state hints prove-assumptions inhibit-output translate-flg print-flg) (er-let* ((hints (if (alistp hints) (value (add-key-val-pair-to-key-val-alist "Goal" :do-not (list 'quote '(generalize eliminate-destructors fertilize eliminate-irrelevance)) hints)) (er soft ctx "The hints must be an alist, but ~x0 is not." hints))) (thints (translate-hints 'tool1 hints ctx wrld state)) (thyps0 (if translate-flg (translate-term-lst hyps t t t ctx wrld state) (value hyps))) (thyps (value (hide-special-hyps thyps0))) (vars (value (all-vars1-lst thyps nil))) (tconc (translate (list 'hide (list 'hidden-expander-function (cons 'list vars))) t t t ctx wrld state)) (tterm (value (implicate (conjoin thyps) tconc)))) (sl-let (erp ttree clauses pairs new-pspv state) (prove-clauses tterm (make-pspv ens wrld state :displayed-goal (untranslate tterm t wrld) :otf-flg t) thints ens wrld ctx state) (prog2$ (chk-for-hidden-expander-function clauses) (cond (erp (mv erp nil state)) (prove-assumptions (er-let* ((thints (if (eq prove-assumptions t) (value thints) (translate-hints 'tool1 *bash-skip-forcing-round-hints* ctx wrld state)))) (state-global-let* ((inhibit-output-lst (if (eq prove-assumptions t) (@ inhibit-output-lst) (if (eq inhibit-output :prove) (remove1-eq 'prove (@ inhibit-output-lst)) (@ inhibit-output-lst))))) (er-let* ((new-ttree (prove-loop1 1 nil pairs new-pspv thints ens wrld ctx state))) (let ((runes (all-runes-in-ttree new-ttree (all-runes-in-ttree ttree nil))) (assumptions (get-assns new-ttree t))) (pprogn (tool1-print print-flg runes clauses state) (value (list* runes (dumb-negate-lit-lst-lst (remove-hidden-terms clauses)) assumptions)))))))) (t (let ((runes (all-runes-in-ttree ttree nil))) (pprogn (tool1-print print-flg runes clauses state) (value (list* runes (dumb-negate-lit-lst-lst (remove-hidden-terms clauses)) nil))))))))))
maybe-inhibit-output-lstfunction
(defun maybe-inhibit-output-lst (inhibit-output state) (cond ((eq inhibit-output :prove) (union-eq '(proof-tree prove) (@ inhibit-output-lst))) ((eq inhibit-output :all) *valid-output-names*) (inhibit-output *valid-output-names-except-error*) (t (@ inhibit-output-lst))))
tool1-fnfunction
(defun tool1-fn (hyps state hints prove-assumptions inhibit-output translate-flg print-flg) (state-global-let* ((ld-skip-proofsp nil) (inhibit-output-lst (maybe-inhibit-output-lst inhibit-output state))) (with-ctx-summarized "( TOOL1 ...)" (let ((wrld (w state)) (ens (ens state))) (tool1-fn1 hyps ctx ens wrld state hints prove-assumptions inhibit-output translate-flg print-flg)))))
tool1-fn0function
(defun tool1-fn0 (hyps ctx ens wrld state hints prove-assumptions inhibit-output translate-flg print-flg) (state-global-let* ((ld-skip-proofsp nil) (inhibit-output-lst (maybe-inhibit-output-lst inhibit-output state))) (tool1-fn1 hyps ctx ens wrld state hints prove-assumptions inhibit-output translate-flg print-flg)))
geneqv-from-g?equivfunction
(defun geneqv-from-g?equiv (g?equiv wrld) (if (symbolp g?equiv) (cadr (car (last (getprop g?equiv 'congruences nil 'current-acl2-world wrld)))) g?equiv))
tool2macro
(defmacro tool2 (term hyps &key hints g?equiv (prove-assumptions 't) inhibit-output (must-rewrite-flg 't) (ctx 'tool2)) `(tool2-fn ',TERM ',HYPS ',G?EQUIV state ',HINTS ',PROVE-ASSUMPTIONS ',INHIBIT-OUTPUT t t ,MUST-REWRITE-FLG ,CTX))
tool2-printfunction
(defun tool2-print (print-flg runes rewritten-term state) (cond (print-flg (fms "~%***OUTPUT OF TOOL2***~%~%Tag tree:~% ~x0~%~%Rewritten term:~% ~ ~x1~|~%" (list (cons #\0 runes) (cons #\1 (untranslate rewritten-term nil (w state)))) *standard-co* state nil)) (t state)))
expander-repeat-limitfunction
(defun expander-repeat-limit (state) (if (f-boundp-global 'expander-repeat-limit state) (f-get-global 'expander-repeat-limit state) 3))
rewrite*function
(defun rewrite* (term hyps ctx repeat-limit completed-iterations type-alist geneqv wrld state step-limit simplify-clause-pot-lst rcnst gstack ttree must-rewrite-flg) (sl-let (val new-ttree) (rewrite-entry (rewrite term nil 1) :obj '? :fnstack '(silly-rec-fn-for-rewrite*) :pre-dwp nil :ancestors nil :backchain-limit 500 :step-limit step-limit :rdepth (rewrite-stack-limit wrld) :pequiv-info nil) (cond ((equal val term) (cond ((or (not must-rewrite-flg) (eq hyps t)) (mv step-limit term ttree state)) (t (prepend-step-limit (erp val state) (er soft ctx "The term~% ~x0~%failed to rewrite to a new term under ~ hypotheses~% ~x1." (untranslate val nil wrld) (untranslate-lst hyps t wrld)))))) ((= repeat-limit completed-iterations) (pprogn (io? prove nil state (completed-iterations) (fms "OUT OF PATIENCE! Completed ~n0 iterations." (list (cons #\0 (list completed-iterations))) *standard-co* state nil)) (mv step-limit val new-ttree state))) (t (pprogn (if (eql completed-iterations 0) state (io? prove nil state (completed-iterations) (fms "NOTE: Starting ~n0 repetition of rewrite.~%" (list (cons #\0 (list (1+ completed-iterations)))) *standard-co* state nil))) (rewrite* val t ctx repeat-limit (1+ completed-iterations) type-alist geneqv wrld state step-limit simplify-clause-pot-lst rcnst gstack new-ttree must-rewrite-flg))))))
tool2-fn1function
(defun tool2-fn1 (term hyps g?equiv ctx ens wrld state thints prove-assumptions inhibit-output translate-flg print-flg must-rewrite-flg) (let* ((saved-pspv (make-pspv ens wrld state :displayed-goal term :user-supplied-term term :orig-hints thints))) (er-let* ((thyps (if translate-flg (translate-term-lst hyps t t t ctx wrld state) (value hyps))) (tterm (if translate-flg (translate term t t t ctx wrld state) (value term)))) (mv-let (erp pair state) (find-applicable-hint-settings *initial-clause-id* (add-literal tterm (dumb-negate-lit-lst thyps) t) nil saved-pspv ctx thints wrld nil state) (cond (erp (silent-error state)) (t (let ((hint-settings (car pair)) (thints (if pair (cdr pair) thints))) (mv-let (hint-settings state) (cond ((null hint-settings) (mv nil state)) (t (thanks-for-the-hint nil hint-settings nil state))) (er-let* ((pspv (load-hint-settings-into-pspv t hint-settings saved-pspv nil wrld ctx state))) (let ((bad-hints '(:do-not-induct :do-not :induct :use :cases :by))) (cond ((intersectp-eq bad-hints (strip-cars hint-settings)) (er soft ctx "It makes no sense in this context for hints at ~ "Goal" to include any of ~v0. Such hints, whether ~ explicit or from default hints, are therefore ~ illegal." bad-hints)) (t (pprogn (initialize-proof-tree *initial-clause-id* (list (list (implicate (conjoin thyps) tterm))) ctx state) (let* ((current-clause (dumb-negate-lit-lst thyps)) (rcnst (change rewrite-constant (access prove-spec-var pspv :rewrite-constant) :current-clause current-clause :force-info t)) (pts nil)) (mv-let (contradictionp type-alist fc-pair-lst) (forward-chain current-clause pts (access rewrite-constant rcnst :force-info) nil wrld (access rewrite-constant rcnst :current-enabled-structure) (access rewrite-constant rcnst :oncep-override) state) (declare (ignore fc-pair-lst)) (cond (contradictionp (er soft ctx "An attempt has been made to simplify the ~ following list of terms, perhaps to be used ~ as hypotheses for ~ simplification:~|~%~x0~|~%However, that list ~ is contradictory! (Technical note: the ~ contradiction was found using type-set ~ reasoning.)" hyps)) (t (sl-let (contradictionp simplify-clause-pot-lst) (setup-simplify-clause-pot-lst current-clause (pts-to-ttree-lst pts) nil type-alist rcnst wrld state (initial-step-limit wrld state)) (cond (contradictionp (er soft ctx "An attempt has been made to simplify the ~ following list of terms, perhaps to be ~ used as hypotheses for ~ simplification:~|~%~x0~|~%However, that ~ list is contradictory! (Technical note: ~ the contradiction was found using linear ~ arithmetic reasoning.)" hyps)) (t (let ((local-rcnst (change rewrite-constant rcnst :current-literal (make current-literal :not-flg nil :atm tterm))) (gstack (initial-gstack 'simplify-clause nil current-clause))) (sl-let (val ttree state) (rewrite* tterm hyps ctx (expander-repeat-limit state) 0 type-alist (geneqv-from-g?equiv g?equiv wrld) wrld state step-limit simplify-clause-pot-lst rcnst gstack nil must-rewrite-flg) (cond ((equal val t) (mv t nil state)) (t (sl-let (bad-ass ttree) (resume-suspended-assumption-rewriting ttree nil gstack simplify-clause-pot-lst local-rcnst wrld state step-limit) (cond (bad-ass (er soft ctx "Generated false assumption, ~x0! ~ ~ So, rewriting is aborted, just as ~ it would be in the course of a ~ regular Acl2 proof." bad-ass)) (t (let ((rewritten-term val)) (cond (prove-assumptions (mv-let (pairs pspv state) (process-assumptions 0 (change prove-spec-var saved-pspv :tag-tree (set-cl-ids-of-assumptions ttree *initial-clause-id*)) wrld state) (er-let* ((ttree (accumulate-ttree-and-step-limit-into-state (access prove-spec-var pspv :tag-tree) step-limit state)) (thints (if (eq prove-assumptions t) (value thints) (translate-hints 'tool2 *bash-skip-forcing-round-hints* ctx wrld state)))) (state-global-let* ((inhibit-output-lst (if (or (eq prove-assumptions t) (eq inhibit-output t)) (@ inhibit-output-lst) (if (eq inhibit-output :prove) (remove1-eq 'prove (@ inhibit-output-lst)) (@ inhibit-output-lst))))) (er-let* ((new-ttree (prove-loop1 1 nil pairs pspv thints ens wrld ctx state))) (let* ((runes (all-runes-in-ttree new-ttree (all-runes-in-ttree ttree nil))) (byes (get-assns new-ttree nil)) (val (list* runes rewritten-term byes))) (pprogn (tool2-print print-flg runes rewritten-term state) (value val)))))))) (t (let* ((runes (all-runes-in-ttree ttree nil)) (val (list* runes rewritten-term nil))) (pprogn (tool2-print print-flg runes rewritten-term state) (value val)))))))))))))))))))))))))))))))))
tool2-fn0function
(defun tool2-fn0 (term hyps g?equiv ctx ens wrld state hints prove-assumptions inhibit-output translate-flg print-flg must-rewrite-flg) (state-global-let* ((inhibit-output-lst (maybe-inhibit-output-lst inhibit-output state))) (prog2$ (semi-initialize-brr-wormhole state) (er-let* ((thints (translate-hints 'tool2 hints ctx wrld state))) (tool2-fn1 term hyps g?equiv ctx ens wrld state thints prove-assumptions inhibit-output translate-flg print-flg must-rewrite-flg)))))
tool2-fnfunction
(defun tool2-fn (term hyps g?equiv state hints prove-assumptions inhibit-output translate-flg print-flg must-rewrite-flg ctx) (let ((wrld (w state)) (ens (ens state))) (tool2-fn0 term hyps g?equiv ctx ens wrld state hints prove-assumptions inhibit-output translate-flg print-flg must-rewrite-flg)))
tool2-fn-lstfunction
(defun tool2-fn-lst (term runes hyps-lst assns g?equiv state hints prove-assumptions inhibit-output print-flg must-rewrite-flg ctx) (cond ((null hyps-lst) (value nil)) (t (mv-let (erp x state) (tool2-fn term (car hyps-lst) g?equiv state hints prove-assumptions inhibit-output nil print-flg must-rewrite-flg ctx) (cond (erp (tool2-fn-lst term runes (cdr hyps-lst) assns g?equiv state hints prove-assumptions inhibit-output print-flg must-rewrite-flg ctx)) (t (er-let* ((rst (tool2-fn-lst term runes (cdr hyps-lst) assns g?equiv state hints prove-assumptions inhibit-output print-flg must-rewrite-flg ctx))) (value (cons (list* (union-equal runes (car x)) (car hyps-lst) (cadr x) (union-equal assns (cddr x))) rst)))))))))
simplify-hypsfunction
(defun simplify-hyps (remaining-hyps rewritten-previous-hyps-rev runes assns g?equiv state hints prove-assumptions inhibit-output print-flg must-rewrite-flg ctx) (cond ((null remaining-hyps) (value (list* runes (list (reverse rewritten-previous-hyps-rev)) assns))) (t (er-let* ((x (tool2-fn (car remaining-hyps) (revappend rewritten-previous-hyps-rev (cdr remaining-hyps)) g?equiv state hints prove-assumptions inhibit-output nil print-flg must-rewrite-flg ctx))) (simplify-hyps (cdr remaining-hyps) (cons (cadr x) rewritten-previous-hyps-rev) (union-equal (car x) runes) (union-equal (cddr x) assns) g?equiv state hints prove-assumptions inhibit-output print-flg must-rewrite-flg ctx)))))
tool-fnfunction
(defun tool-fn (term hyps simplify-hyps-p g?equiv state hints prove-assumptions inhibit-output print-flg must-rewrite-flg ctx) (er-let* ((runes-hyps-assns (cond ((eq simplify-hyps-p :no-split) (simplify-hyps hyps nil nil nil g?equiv state hints prove-assumptions inhibit-output print-flg must-rewrite-flg ctx)) ((eq simplify-hyps-p t) (tool1-fn hyps state hints prove-assumptions inhibit-output nil print-flg)) (simplify-hyps-p (value (er hard 'tool-fn "Bad :simplify-hyps-p argument (should be ~v0): ~x1" (list t nil :no-split) simplify-hyps-p))) (t (value (list* nil (list hyps) nil)))))) (cond ((null (cdr runes-hyps-assns)) (er soft ctx "It does not make sense to simplify the term ~x0, because the ~ hypothesis list ~x1 is contradictory." (untranslate term nil (w state)) (untranslate-lst hyps t (w state)))) (t (pprogn (cond (print-flg (fms "***NOTE***: Starting TOOL2.~%" nil *standard-co* state nil)) (t state)) (er-let* ((x (tool2-fn-lst term (car runes-hyps-assns) (cadr runes-hyps-assns) (cddr runes-hyps-assns) g?equiv state hints prove-assumptions inhibit-output print-flg must-rewrite-flg ctx))) (cond ((not (= (length x) (length (cadr runes-hyps-assns)))) (er soft ctx "Unable to successfully simplify term~% ~x0~%and ~ hypotheses~% ~x1 in every case generated." (untranslate term nil (w state)) (untranslate-lst hyps t (w state)))) (x (value x)) (t (er soft ctx "No theorems were suggested for term~% ~x0~%and ~ hypotheses~% ~x1." (untranslate term nil (w state)) (untranslate-lst hyps t (w state)))))))))))
other
(defxdoc defthm? :parents (expander) :short "Generate a theorem." :long "<p>Example:</p> @({ (defthm? app-simplify (implies (true-listp x) (equal (append x y) ?)) :hints (("Goal" :expand ((true-listp x) (true-listp (cdr x)) (append x y)))) ; show some output :print-flg t) }) <p>General Forms:</p> @({ (DEFTHM? name (IMPLIES hyps (equiv term ?)) :hints hints :prove-assumptions prove-flg ; t or nil, default t :print-flg print-flg ; t or nil, default nil :simplify-hyps-p flg ; t, nil, or :no-split; default t ) (DEFTHM? name (equiv term ?) :hints hints :prove-assumptions prove-flg ; t or nil, default t :print-flg print-flg ; t or nil, default nil :simplify-hyps-p flg ; t, nil, or :no-split; default t ) }) <p>where @('name') is a new symbolic name (see @(see name)), @('term') is a term to be simplified assuming @('hyps') is true, and @(see hints) is as described in its @(see documentation). The four keyword arguments above are all optional, and behave as you might expect. In particular, set @(':simplify-hyps-p') to @('nil') if you do not want the @('hyps') to be simplified; otherwise, case splitting may occur in the course of their simplification.</p> <p>If the given @('term') cannot be simplified, then the event fails. Otherwise, the result is an @(see encapsulate) event with one or more @(see defthm) events of the form of the theorem, except with @('hyps') simplified (and even omitted if simplified to @('t')) and @('term') simplified under the assumption that @('hyps') is true. The reason that there can be more than one @(see defthm) event is that @('hyps') may simplify to an expression that generates a case split, for example if it simplifies to an @(see if) expression that does not represent a conjunction.</p> <p>In general, simplification may generate assumptions because of @(see force). By default, an attempt is made to prove these assumptions, which must succeed or else this event fails. However, if @(':prove-assumptions') is @('nil'), then roughly speaking, no proof of forced hypotheses is attempted until after simplification is complete. The documentation of :prove-assumptions is admittedly weak here; feel free to experiment.</p> <p>See @(see rewrite$) for a flexible, convenient interface to the ACL2 rewriter that can be called programmatically. Also see @(see symsim).</p> <p>Here are some examples, including the one above. Try them out and see what happens.</p> @({ ; Doesn't simplify, so fails: (defthm? app-simplify (implies (true-listp x) (equal (append x y) ?)) :hints (("Goal" :expand (true-listp x)))) :pbt 0 ; The following creates one event, but maybe we'd prefer cases to be ; broken out into separate events. That comes next. (defthm? app-simplify (implies (true-listp x) (equal (append x y) ?)) :hints (("Goal" :expand (append x y)))) :pbt 0 :pe :here :pe APP-SIMPLIFY :u (defthm? app-simplify (implies (true-listp x) (equal (append x y) ?)) :hints (("Goal" :expand ((true-listp x) (true-listp (cdr x)) (append x y)))) ; show some extra output; this is optional :print-flg t) :pe :here :u })")
defthm?macro
(defmacro defthm? (name term &key hints (prove-assumptions 't) (simplify-hyps-p 't) print-flg) (let* ((form0 `(defthm?-fn ',NAME ',TERM ',SIMPLIFY-HYPS-P ',HINTS ',PROVE-ASSUMPTIONS ',PRINT-FLG (w state) state)) (form `(er-let* ((val ,FORM0)) (pprogn (f-put-global 'defthm?-result val state) (value :invisible))))) `(state-global-let* ((defthm?-result nil)) (er-progn (ld '(,FORM) :ld-pre-eval-print nil :ld-prompt nil) (value (f-get-global 'defthm?-result state))))))
*adjust-hints-exec-theory*constant
(defconst *adjust-hints-exec-theory* '(definition-runes (union-eq '(iff) *expandable-boot-strap-non-rec-fns*) t world))
adjust-hints-with-runes1function
(defun adjust-hints-with-runes1 (hint runes) (cond ((null hint) (list :in-theory (list 'union-theories *adjust-hints-exec-theory* (list 'quote runes)))) ((eq (car hint) :in-theory) (list* :in-theory (list 'union-theories *adjust-hints-exec-theory* `(intersection-theories ',RUNES ,(CADR HINT))) (cddr hint))) (t (list* (car hint) (cadr hint) (adjust-hints-with-runes1 (cddr hint) runes)))))
adjust-hints-with-runesfunction
(defun adjust-hints-with-runes (hints runes top-goal-seen-p) (cond ((null hints) (if top-goal-seen-p nil `(("Goal" :in-theory (union-theories ,*ADJUST-HINTS-EXEC-THEORY* ',RUNES))))) (t (cons (cons (caar hints) (adjust-hints-with-runes1 (cdar hints) runes)) (adjust-hints-with-runes (cdr hints) runes (or top-goal-seen-p (equal (caar hints) "Goal")))))))
*fake-runes*constant
(defconst *fake-runes* (list *fake-rune-for-anonymous-enabled-rule* *fake-rune-for-type-set* *fake-rune-for-linear*))
defthm-?-fn-forms1-lstfunction
(defun defthm-?-fn-forms1-lst (name index x equiv lhs hints wrld) (cond ((null x) nil) (t (let ((runes (set-difference-equal (car (car x)) *fake-runes*)) (hyps (cadr (car x))) (rhs (caddr (car x))) (assumptions (cdddr (car x)))) (cons `(defthm ,(IF (AND (ZEROP INDEX) (NULL (CDR X))) NAME (PACKN (LIST NAME '$ INDEX))) ,(UNTRANSLATE (IMPLICATE (CONJOIN (APPEND ASSUMPTIONS HYPS)) (FCONS-TERM* EQUIV LHS RHS)) T WRLD) :hints ,(ADJUST-HINTS-WITH-RUNES HINTS RUNES NIL)) (defthm-?-fn-forms1-lst name (1+ index) (cdr x) equiv lhs hints wrld))))))
defthm?-fn-formsfunction
(defun defthm?-fn-forms (name form simplify-hyps-p hints prove-assumptions inhibit-output print-flg wrld state) (with-ctx-summarized (cons 'defthm? name) (er-let* ((tform (translate form t t t ctx wrld state))) (let* ((x (unprettyify tform)) (hyps (car (car x))) (concl (cdr (car x)))) (cond ((and (null (cdr x)) (not (variablep concl)) (not (fquotep concl)) (variablep (fargn concl 2))) (cond ((equivalence-relationp (ffn-symb concl) wrld) (er-let* ((x (tool-fn (fargn concl 1) hyps simplify-hyps-p (ffn-symb concl) state hints prove-assumptions inhibit-output print-flg t ctx))) (value (defthm-?-fn-forms1-lst name 0 x (ffn-symb concl) (fargn concl 1) hints wrld)))) (t (er soft ctx "The form supplied to DEFTHM? must be of the form ~x0 or ~x1, ~ where equiv is an equivalence relation. However, ~x2 is not ~ an equivalence relation in the current world." '(implies hyps (equiv lhs var)) '(equiv lhs var) (ffn-symb concl))))) (t (er soft ctx "The form supplied to DEFTHM? must be of the form ~x0 or ~x1,~ where var is a variable. But ~x2 is not of this form." '(implies hyps (equiv lhs var)) '(equiv lhs var) form)))))))
defthm?-fnfunction
(defun defthm?-fn (name term simplify-hyps-p hints prove-assumptions print-flg wrld state) (state-global-let* ((inhibit-output-lst (if (boundp-global 'defthm?-inhibit-output-lst state) (f-get-global 'defthm?-inhibit-output-lst state) (@ inhibit-output-lst)))) (er-let* ((forms (defthm?-fn-forms name term simplify-hyps-p hints prove-assumptions nil print-flg wrld state))) (er-progn (encapsulate-fn nil (cons '(logic) forms) state nil) (value (list* 'encapsulate nil forms))))))
other
(defxdoc symsim :parents (expander) :short "Simplify given term and hypotheses." :long "<p>Example:</p> @({ (symsim (append x y) ((not (atom x)) (not (cdr x))) :hints (("Goal" :expand ((true-listp x) (true-listp (cdr x)) (append x y))))) }) <p>yields</p> @({ Simplified term: (CONS (CAR X) Y) Simplified hyps: ((CONSP X) (NOT (CDR X)))~/ General Form: (symsim term hyps :hints hints :inhibit-output inhibit-flg ; t, :prove, :all, or nil, default t :prove-assumptions prove-flg ; t, nil, or (default) any other value :print-flg print-flg ; t or nil, default nil :simplify-hyps-p flg ; t, nil, or :no-split; default t ) }) <p>where @('term') is a term to be simplified assuming that each @('hyp') in the list @('hyps') is true, and @(see hints) is as described in its @(see documentation). The keyword arguments above are all optional, and behave as you might expect. In particular, set @(':simplify-hyps-p') to @('nil') if you do not want the @('hyps') to be simplified; otherwise, case splitting may occur in the course of their simplification.</p> <p>Prover output is inhibited if @(':inhibit-output') is @('t') (the default). Only proof output is inhibited if @(':inhibit-output') is @(':prove') (so for example, summaries and warnings are printed), and all prover output is shown or inhibited if @(':inhibit-output') is @('nil') or @(':all'), respectively.</p> <p>See @(see rewrite$) for a flexible, convenient interface to the ACL2 rewriter that can be called programmatically. Also see @(see defthm?), which is related to @('symsim') and is a bit more thoroughly documented. Here are some examples that should help give an idea of how @('symsim') works. (The name, by the way, is short for "symbolically simulate".) Try these, as well as the examples shown above.</p> @({ (symsim (append x y) nil :hints (("Goal" :expand ((true-listp x) (append x y) (append (cdr x) y))))) ; Generates three cases: (symsim (append x y) ((true-listp x)) :hints (("Goal" :expand ((true-listp x) (true-listp (cdr x)) (append x y) (append (cdr x) y))))) ; Let's illustrate the role of FORCE. The following rule ; forces append to open up, and comes into play below. (defthm true-listp-expand-append (implies (and (force (true-listp x)) x) (equal (append x y) (cons (car x) (append (cdr x) y))))) ; Generates assumption forced by preceding rule. (symsim (append x y) ((not (atom x)))) ; But now we fail; but why? See next form. (symsim (append x y) ((consp x)) :prove-assumptions t) ; Let's not inhibit output. Then we can see the failed forcing round. (symsim (append x y) ((consp x)) :prove-assumptions t :inhibit-output nil) ; As above, but doesn't deal with generated forced assumptions at all (just ; drops them on the floor). (symsim (append x y) ((consp x)) :prove-assumptions nil) })")
symsimmacro
(defmacro symsim (term hyps &key hints (prove-assumptions 'try) (inhibit-output 't) (simplify-hyps-p 't) print-flg) `(symsim-fn ',TERM ',HYPS ',SIMPLIFY-HYPS-P ',HINTS ',PROVE-ASSUMPTIONS ',INHIBIT-OUTPUT ',PRINT-FLG (w state) state))
symsim-fn-print-lstfunction
(defun symsim-fn-print-lst (tuples n total wrld state) (cond ((null tuples) (fms "========================================~%~%" nil *standard-co* state nil)) (t (let ((tuple (car tuples))) (pprogn (fms "========== Generated case #~x0 of ~x1 ==========~%" (list (cons #\0 n) (cons #\1 total)) *standard-co* state nil) (fms "Runes:~% ~x0~%Simplified hyps:~% ~x1~%Simplified term:~% ~ ~x2~%Simplified assumptions:~% ~x3~%" (list (cons #\0 (car tuple)) (cons #\1 (untranslate-lst (cadr tuple) t wrld)) (cons #\2 (untranslate (caddr tuple) nil wrld)) (cons #\3 (prettyify-clause-lst (cdddr tuple) (let*-abstractionp state) wrld))) *standard-co* state nil) (symsim-fn-print-lst (cdr tuples) (1+ n) total wrld state))))))
symsim-fnfunction
(defun symsim-fn (term hyps simplify-hyps-p hints prove-assumptions inhibit-output print-flg wrld state) (er-let* ((tterm (translate term t t t 'top-level wrld state)) (thyps (translate-term-lst hyps t t t 'top-level wrld state)) (tuples-lst (tool-fn tterm thyps simplify-hyps-p 'equal state hints prove-assumptions inhibit-output print-flg t (cons 'symsim-fn term)))) (pprogn (if print-flg (symsim-fn-print-lst tuples-lst 1 (length tuples-lst) wrld state) state) (value tuples-lst))))
normalize-no-ttreefunction
(defun normalize-no-ttree (term iff-flg type-alist ens wrld) (mv-let (x ttree) (normalize term iff-flg type-alist ens wrld nil (backchain-limit wrld :ts)) (declare (ignore ttree)) x))
simp-hyps-auxfunction
(defun simp-hyps-aux (hyps-remaining hyps-init hyps-res ctx ens wrld state hints inhibit-output print-flg simp-flg) (cond ((null hyps-remaining) (value (reverse hyps-res))) (t (let* ((hyp0 (car hyps-remaining)) (hyp (normalize-no-ttree hyp0 t nil ens wrld)) (other-hyps (remove1-equal hyp0 hyps-init))) (mv-let (erp x state) (tool2-fn0 hyp other-hyps 'iff ctx ens wrld state hints nil inhibit-output nil print-flg nil) (let* ((res (if erp hyp (normalize-no-ttree (cadr x) t nil ens wrld))) (simplified-to-t? (equal res ''t)) (simplified-to-nil? (equal res ''nil)) (simplified? (term-order res hyp)) (always-simp? (and (not (equal simp-flg :t)) (not (equal simp-flg :term-order)))) (nhyps-init (cond (simplified-to-t? other-hyps) ((or always-simp? (and simplified? (not (equal simp-flg :t)))) (append (flatten-ands-in-lit res) other-hyps)) (t (append (flatten-ands-in-lit hyp) other-hyps)))) (nhyps-res (cond (simplified-to-t? hyps-res) ((or always-simp? (and simplified? (not (equal simp-flg :t)))) (append (flatten-ands-in-lit res) hyps-res)) (t (append (flatten-ands-in-lit hyp) hyps-res))))) (if simplified-to-nil? (value nil) (simp-hyps-aux (cdr hyps-remaining) nhyps-init nhyps-res ctx ens wrld state hints inhibit-output print-flg simp-flg))))))))
simp-hyps0function
(defun simp-hyps0 (hyps ctx ens wrld state hints inhibit-output print-flg simp-flg) "See the documentation for simp-hyps. This function has the same functionality, but requires the user to provide the ctx, ens, and wrld." (let ((nd-hyps (remove-duplicates hyps))) (er-let* ((t-nd-hyps (simp-hyps-aux nd-hyps nd-hyps nil ctx ens wrld state hints inhibit-output print-flg :t))) (if (equal simp-flg :t) (value t-nd-hyps) (simp-hyps-aux t-nd-hyps t-nd-hyps nil ctx ens wrld state hints inhibit-output print-flg simp-flg)))))
simp-hypsfunction
(defun simp-hyps (hyps state hints inhibit-output print-flg simp-flg) "Given a list of terms (hyps), return a list that is a subset of hyps. The conjunction of hyps should be equal to the conjuction of the returned list. If simp-flg is :t, all we do is to remove elements of hyps that can be proven to simplify to t, assuming the rest of the elements in hyps hold. If simp-flg is :term-order, then we replace elements of hyps with what they simplify to (again, assuming the rest of the elements in hyps hold) if we wind up with a smaller term (as determined by the function term-order). Otherwise, we replace elements of hyps with whatever they simplify to (again, assuming the rest of the elements in hyps hold). Some care is taken to deal with duplicates, and the like. For example, we always try with simp-flg set to :t first since this tends to return results that depend less on the order of arguments. To see this, note that if you give ((natp x) (integerp x)) as input, you would get different results when you change the order of the hyps (if you didn't try :t first). " (simp-hyps0 hyps 'simp-hyps (ens state) (w state) state hints inhibit-output print-flg simp-flg))
defsimp-fnfunction
(defun defsimp-fn (term hyps equiv state in-theory expand translate-flg must-rewrite-flg defthm-name rule-classes print) (let ((ctx 'defsimp) (wrld (w state)) (ens (ens state)) (hints `(,@(AND (NOT (EQ IN-THEORY :NONE)) `((:IN-THEORY ,IN-THEORY))) ,@(AND EXPAND `((:EXPAND ,EXPAND)))))) (er-let* ((runes/new-term/assumptions (tool2-fn0 term hyps equiv ctx ens wrld state hints t t translate-flg nil must-rewrite-flg))) (let ((runes (car runes/new-term/assumptions)) (new-term (cadr runes/new-term/assumptions)) (assumptions (cddr runes/new-term/assumptions))) (cond (assumptions (er soft ctx "Implementation error: assumptions were unexpectedly forced. ~ Please contact the maintainers of books/misc/expander.lisp")) ((not (true-listp hyps)) (er soft ctx "The given hypotheses must be a true list, but ~x0 is not." hyps)) (t (let* ((formula (if hyps (list 'implies (if (cdr hyps) (cons 'and hyps) (car hyps)) (list (or equiv 'equal) term new-term)) (list (or equiv 'equal) term new-term))) (runes+ `(union-theories (theory 'minimal-theory) ',RUNES)) (event-form `(defthm ,DEFTHM-NAME ,FORMULA :instructions ((:in-theory ,RUNES+) ,@(AND HYPS '(:PROMOTE)) (:dive 1) (:then (:s :backchain-limit 500) (:prove ,@(AND EXPAND `(:HINTS (("Goal" :EXPAND ,EXPAND)))))) :up :s-prop) ,@(AND (NOT (EQ RULE-CLASSES :REWRITE)) `(:RULE-CLASSES ,RULE-CLASSES))))) (pprogn (cond ((eq print t) (fms "New term:~|~x0~|~%" (list (cons #\0 new-term)) (standard-co state) state nil)) ((eq print :all) (fms "~x0~|~%" (list (cons #\0 event-form)) (standard-co state) state nil)) (t state)) (value event-form)))))))))
defsimpmacro
(defmacro defsimp (term hyps defthm-name &key (rule-classes ':rewrite) (in-theory ':none) expand equiv (translate-flg 't) (must-rewrite-flg 't) (print ':all)) (let ((form `(defsimp-fn ',TERM ',HYPS ',EQUIV state ',IN-THEORY ',EXPAND ',TRANSLATE-FLG ,MUST-REWRITE-FLG ',DEFTHM-NAME ',RULE-CLASSES ',PRINT))) `(with-output :off :all :on error ,(IF (EQ PRINT :ONLY) `(MAKE-EVENT (ER-LET* ((FORM ,FORM)) (VALUE (LIST 'VALUE-TRIPLE (LIST 'QUOTE FORM))))) `(MAKE-EVENT ,FORM)))))