ACL2-PC::RUN-INSTR-ON-NEW-GOALS

(macro) auxiliary to then


Parent topic:  PROOF-CHECKER
Home

See documentation for then.

ACL2-PC::S

(primitive) simplify the current subterm


Parent topic:  PROOF-CHECKER
Home

Examples: S -- simplify the current subterm (S :backchain-limit 2 :normalize t :expand (append x z)) -- simplify the current subterm, but during the rewriting process first ``normalize'' it by pushing IFs to the top-level, and also force the term (append x z) to be expanded during the rewriting process

General Form: (s &key rewrite normalize backchain-limit repeat in-theory hands-off expand)

Simplify the current subterm according to the keyword parameters supplied. First if-normalization is applied (unless the normalize argument is nil), i.e., each subterm of the form (f ... (if test x y) ...) is replaced by the term (if test (f ... x ...) (f ... y ...)) except, of course, when f is if and the indicated if subterm is in the second or third argument position. Then rewriting is applied (unless the rewrite argument is nil). Finally this pair of actions is repeated -- until the rewriting step causes no change in the term. A description of each parameter follows.

:rewrite -- default t

When non-nil, instructs the system to use ACL2's rewriter (or, something close to it) during simplification.

:normalize -- default t

When non-nil, instructs the system to use if-normalization (as described above) during simplification.

:backchain-limit -- default 0

Sets the number of recursive calls to the rewriter that are allowed for backchaining. Even with the default of 0, some reasoning is allowed (technically speaking, type-set reasoning is allowed) in the relieving of hypotheses.

:repeat -- default 0

Sets the number of times the current term is to be rewritten. If this value is t, then the default is used (as specified by the constant *default-s-repeat-limit*).

:in-theory, :hands-off, :expand

These have their usual meaning; see hints.

Note: if conditional rewrite rules are used that cause case splits because of the use of force, then appropriate new subgoals will be created, i.e., with the same current subterm (and address) but with each new (forced) hypothesis being negated and then used to create a corresponding new subgoal. In that case, the current goal will have all such new hypotheses added to the list of top-level hypotheses.

ACL2-PC::S-PROP

(atomic macro) simplify propositionally


Parent topic:  PROOF-CHECKER
Home

Example:
s-prop

General Form:
(s-prop &rest names)

Simplify, using the default settings for s (which include if-normalization and rewriting without real backchaining), but with respect to a theory in which only basic functions and rules (the ones in *s-prop-theory*), together with the names (or parenthesized names) in the &rest argument names, are enabled.

ACL2-PC::SAVE

(macro) save the proof-checker state (state-stack)


Parent topic:  PROOF-CHECKER
Home

Example:
(save lemma3-attempt

General Form:
(save &optional name do-it-flg)

Saves the current proof-checker state by ``associating'' it with the given name. Submit (retrieve name) to Lisp to get back to this proof-checker state. If verify was originally supplied with an event name, then the argument can be omitted in favor of that name as the default.

Note that if a save has already been done with the indicated name (or the default event name), then the user will be queried regarding whether to go ahead with the save -- except, if do-it-flg is supplied and not nil, then there will be no query and the save will be effected.

See also the documentation for retrieve and unsave.

ACL2-PC::SEQUENCE

(meta) run the given list of instructions according to a multitude of options


Parent topic:  PROOF-CHECKER
Home

Example:
(sequence (induct p prove) t)

See also the definitions of commands do-all, do-strict, protect, and succeed.

General Form:
(sequence instruction-list
          &optional
          strict-flg protect-flg success-expr no-prompt-flg)

Each instruction in the list instruction-list is run, and the instruction ``succeeds'' if every instruction in instruction-list ``succeeds''. However, it might ``succeed'' even if some instructions in the list ``fail''; more generally, the various arguments control a number of aspects of the running of the instructions. All this is explained in the paragraphs below. First we embark on a general discussion of the instruction interpreter, including the notions of ``succeed'' and ``fail''.

Note: The arguments are not evaluated, except (in a sense) for success-expr, as described below.

Each primitive and meta instruction can be thought of as returning an error triple (in the standard ACL2 sense), say (erp val state). An instruction (primitive or meta) ``succeeds'' if erp is nil and val is not nil; otherwise it ``fails''. (When we use the words ``succeed'' or ``fail'' in this technical sense, we'll always include them in double quotes.) If an instruction ``fails,'' we say that that the failure is ``soft'' if erp is nil; otherwise the failure is ``hard''. The sequence command gives the user control over how to treat ``success'' and ``failure'' when sequencing instructions, though we have created a number of handy macro commands for this purpose, notably do-all, do-strict and protect.

Here is precisely what happens when a sequence instruction is run. The instruction interpreter is run on the instructions supplied in the argument instruction-list (in order). The interpreter halts the first time there is a hard ``failure.'' except that if strict-flg is supplied and not nil, then the interpreter halts the first time there is any ``failure.'' The error triple (erp val state) returned by the sequence instruction is the triple returned by the last instruction executed (or, the triple (nil t state) if instruction-list is nil), except for the following provision. If success-expr is supplied and not nil, then it is evaluated with the state global variables erp and val (in ACL2 package) bound to the corresponding components of the error triple returned (as described above). At least two values should be returned, and the first two of these will be substituted for erp and val in the triple finally returned by sequence. For example, if success-expr is (mv erp val), then no change will be made to the error triple, and if instead it is (mv nil t), then the sequence instruction will ``succeed''.

That concludes the description of the error triple returned by a sequence instruction, but it remains to explain the effects of the arguments protect-flg and no-prompt-flg.

If protect-flg is supplied and not nil and if also the instruction ``fails'' (i.e., the error component of the triple is not nil or the value component is nil), then the state is reverted so that the proof-checker's state (including the behavior of restore) is set back to what it was before the sequence instruction was executed. Otherwise, unless no-restore-flg is set, the state is changed so that the restore command will now undo the effect of this sequence instruction (even if there were nested calls to sequence).

Finally, as each instruction in instruction-list is executed, the prompt and that instruction will be printed, unless the global state variable print-prompt-and-instr-flg is unbound or nil and the parameter no-prompt-flg is supplied and not nil.

ACL2-PC::SHOW-ABBREVIATIONS

(macro) display the current abbreviations


Parent topic:  PROOF-CHECKER
Home

Examples:
(show-abbreviations v w)
   -- assuming that v and w currently abbreviate terms,
      then this instruction displays them together with
      the terms they abbreviate
show-abbreviations
   -- display all abbreviations

See also add-abbreviation and remove-abbreviations. In particular, the documentation for add-abbreviation contains a general discussion of abbreviations.

General Form:
(show-abbreviations &rest vars)

Display each argument in vars together with the term it abbreviates (if any). If there are no arguments, i.e. the instruction is simply show-abbreviations, then display all abbreviations together with the terms they abbreviate.

If the term abbreviated by a variable, say v, contains a proper subterm that is also abbreviate by (another) variable, then both the unabbreviated term and the abbreviated term (but not using (? v) to abbreviate the term) are displayed with together with v.

ACL2-PC::SHOW-REWRITES

(macro) display the applicable rewrite rules


Parent topic:  PROOF-CHECKER
Home

Example: show-rewrites

General Form: (show-rewrites &optional rule-id enabled-only-flg)

Display rewrite rules whose left-hand side matches the current subterm. This command is useful in conjunction with rewrite. If rule-id is supplied and is a name (non-nil symbol) or a rune, then only the corresponding rewrite rule(s) will be displayed, while if rule-id is a positive integer n, then only the nth rule that would be in the list is displayed. In each case, the display will point out when a rule is currently disabled (in the interactive environment), except that if enabled-only-flg is supplied and not nil, then disabled rules will not be displayed at all. Finally, the free variables of any rule (those occurring in the rule that do not occur in the left-hand side of its conclusion) will be displayed. See also the documentation for rewrite.

ACL2-PC::SKIP

(macro) ``succeed'' without doing anything


Parent topic:  PROOF-CHECKER
Home

Example and General Form:
skip

Make no change in the state-stack, but ``succeed''. Same as (sequence nil).

ACL2-PC::SL

(atomic macro) simplify with lemmas


Parent topic:  PROOF-CHECKER
Home

Examples:
sl
(sl 3)

General Form:
(sl &optional backchain-limit)

Simplify, but with all function definitions disabled (see function-theory in the top-level ACL2 loop), except for a few basic functions (the ones in *s-prop-theory*). If backchain-limit is supplied and not nil, then it should be a nonnegative integer; see (help s).

ACL2-PC::SPLIT

(atomic macro) split the current goal into cases


Parent topic:  PROOF-CHECKER
Home

Example:
split

For example, if the current goal has one hypothesis (or x y) and a conclusion of (and a b), then split will create four new goals:

one with hypothesis X and conclusion A one with hypothesis X and conclusion B one with hypothesis Y and conclusion A one with hypothesis Y and conclusion B.

General Form: SPLIT

Replace the current goal by subgoals whose conjunction is equivalent (primarily by propositional reasoning) to the original goal, where each such goal cannot be similarly split.

Note: The new goals will all have their hypotheses promoted; in particular, no conclusion will have a top function symbol of implies. Also note that split will fail if there is exactly one new goal created and it is the same as the existing current goal.

The way split really works is to call the ACL2 theorem prover with only simplification (and preprocessing) turned on, and with only a few built-in functions (especially, propositional ones) enabled, namely, the ones in the list *s-prop-theory*. However, because the prover is called, type-set reasoning can be used to eliminate some cases. For example, if (true-listp x) is in the hypotheses, then probably (true-listp (cdr x)) will be reduced to t.

ACL2-PC::SR

(macro) same as SHOW-REWRITES


Parent topic:  PROOF-CHECKER
Home

Example:
sr

General Form:
(sr &optional rule-id)

See the documentation for show-rewrites, as sr and show-rewrites are identical.

ACL2-PC::SUCCEED

(macro) run the given instructions, and ``succeed''


Parent topic:  PROOF-CHECKER
Home

Example:
(succeed induct p prove)

General Form:
(succeed &rest instruction-list)

Run the indicated instructions until there is a hard ``failure'', and ``succeed''. (See the documentation for sequence for an explanation of ``success'' and ``failure''.)

ACL2-PC::TH

(macro) print the top-level hypotheses and the current subterm


Parent topic:  PROOF-CHECKER
Home

Examples:
th               -- print all (top-level) hypotheses and the current
                    subterm
(th (1 3) (2 4)) -- print hypotheses 1 and 3 and governors 2 and 4,
                    and the current subterm
(th (1 3) t)     -- print hypotheses 1 and 3 and all governors, and
                    the current subterm

General Form:
(th &optional hyps-indices govs-indices)

Print hypotheses and the current subterm. The printing of hypotheses (and perhaps governors) are controlled as in the hyps command; see its documentation.

Historical note: The name th is adapted from the Gypsy Verification Environment, where th abbreviates the command theorem, which says to print information on the current goal.

ACL2-PC::THEN

(macro) apply one instruction to current goal and another to new subgoals


Parent topic:  PROOF-CHECKER
Home

Example:
(then induct prove)

General Form:
(then first-instruction &optional completion must-succeed-flg)

Run first-instruction, and then run completion (another instruction) on each subgoal created by first-instruction. If must-succeed-flg is supplied and not nil, then immediately remove the effects of each invocation of completion that ``fails''.

ACL2-PC::TOP

(atomic macro) move to the top of the goal


Parent topic:  PROOF-CHECKER
Home

Example and General Form:
top

For example, if the conclusion is (= x (* (- y) z)) and the current subterm is y, then after executing top, the current subterm will be the same as the conclusion, i.e., (= x (* (- y) z)).

Top is the same as (up n), where n is the number of times one needs to execute up in order to get to the top of the conclusion. The top command fails if one is already at the top of the conclusion.

ACL2-PC::TYPE-ALIST

(macro) display the type-alist from the current context


Parent topic:  PROOF-CHECKER
Home

Example and General Form:
type-alist

Display the current assumptions as a type-alist. Note that this display includes the result of forward chaining.

ACL2-PC::UNDO

(meta) undo some instructions


Parent topic:  PROOF-CHECKER
Home

Examples:
(undo 7)
undo

General Forms:


(undo n) -- Undo the last n instructions.  The argument n should be
            a positive integer.


undo     -- Same as (undo 1).

Note: To remove the effect of an undo command, use restore. See the documentation for details.

Note: If the argument n is greater than the total number of interactive instructions in the current session, then (undo n) will simply take you back to the start of the session.

The undo meta command always ``succeeds''; it returns (mv nil t state) unless its optional argument is supplied and of the wrong type (i.e. not a positive integer) or there are no instructions to undo.

ACL2-PC::UNSAVE

(macro) remove a proof-checker state


Parent topic:  PROOF-CHECKER
Home

Example:
(unsave assoc-of-append)

General Form:
(unsave &optional name)

Eliminates the association of a proof-checker state with name, if name is supplied and not nil. The name may be nil or not supplied, in which case it defaults to the event name supplied with the original call to verify (if there is one -- otherwise, the instruction ``fails'' and there is no change). The ACL2 function unsave may also be executed outside the interactive loop, with the same syntax.

See also documentation for save and retrieve.

ACL2-PC::UP

(primitive) move to the parent (or some ancestor) of the current subterm


Parent topic:  PROOF-CHECKER
Home

Examples:  if the conclusion is (= x (* (- y) z)) and the
           current subterm is y, then we have:
up or (up 1) -- the current subterm becomes (- y)
(up 2)       -- the current subterm becomes (* (- y) z)
(up 3)       -- the current subterm becomes the entire conclusion
(up 4)       -- no change; can't go up that many levels

General Form:
(up &optional n)

Move up n levels in the conclusion from the current subterm, where n is a positive integer. If n is not supplied or is nil, then move up 1 level, i.e., treat the instruction as (up 1).

ACL2-PC::USE

(atomic macro) use a lemma instance


Parent topic:  PROOF-CHECKER
Home

Example:
(USE true-listp-append
     (:instance assoc-of-append (x a) (y b) (z c)))
-- Add two top-level hypotheses, one the lemma called
   true-listp-append, and the other an instance of the lemma called
   assoc-of-append by the substitution in which x is assigned a, y
   is assigned b, and z is assigned c.

General Form:
(use &rest args)

Add the given lemma instances to the list of top-level hypotheses. See hints for the syntax of :use hints in defthm, which is essentially the same as the syntax here (see the example above).

This command calls the prove command, and hence should only be used at the top of the conclusion.

ACL2-PC::X

(atomic macro) expand and (maybe) simplify function call at the current subterm


Parent topic:  PROOF-CHECKER
Home

Examples:
x --  expand and simplify.

For example, if the current subterm is (append a b), then after x the current subterm will probably be (cons (car a) (append (cdr a) b)) if (consp a) and (true-listp a) are among the top-level hypotheses and governors. If there are no top-level hypotheses and governors, then after x the current subterm will probably be:

(if (true-listp x)
    (if x
        (cons (car x) (append (cdr x) y))
      y)
  (apply 'binary-append (list x y))).

General Form:
(X &key
   rewrite normalize backchain-limit in-theory hands-off expand)

Expand the function call at the current subterm, and simplify using the same conventions as with the s command (see documentation for s).

Unlike s, it is permitted to set both :rewrite and :normalize to nil, which will result in no simplification; see x-dumb.

Note (obscure): On rare occasions the current address may be affected by the use of x. For example, suppose we have the definition

(defun g (x) (if (consp x) x 3))

and then we enter the proof-checker with

(verify (if (integerp x) (equal (g x) 3) t)) .

Then after invoking the instruction (dive 2 1), so that the current subterm is (g x), followed by the instruction x, we would expect the conclusion to be (if (integerp x) (equal 3 3) t). However, the system actually replaces (equal 3 3) with t (because we use the ACL2 term-forming primitives), and hence the conclusion is actually (if (integerp x) (equal 3 3) t). Therefore, the current address is put at (2) rather than (2 1). In such cases, a warning ``NOTE'' will be printed to the terminal.

The other primitive commands to which the above ``truncation'' note applies are equiv, rewrite, and s.

ACL2-PC::X-DUMB

(atomic macro) expand function call at the current subterm, without simplifying


Parent topic:  PROOF-CHECKER
Home

Example: x-dumb: expand without simplification.

General Form: (x-dumb &optional new-goals-flg keep-all-guards-flg)

Same as (expand t new-goals-flg keep-all-guards-flg). See documentation for expand.

See also x, which allows simplification.

DEFINE-PC-HELP

define a macro command whose purpose is to print something


Parent topic:  PROOF-CHECKER
Home

Example:
(define-pc-help pp () 
  (if (goals t)
      (fms0 "~|~q0~|"
            (list (cons #0 
                        (fetch-term (conc t)
                                    (current-addr t)))))
    (print-all-goals-proved-message state)))

General Form:
(define-pc-help name args &rest body)

This defines a macro command named name, as explained further below. The body should (after removing optional declarations) have multiplicity 1 and state-out t, i.e. it should return a single value of state. Typically, it will just print something.

What (define-pc-help name args &rest body) really does is to create a call of define-pc-macro that defines name to take arguments args, to have the declarations indicated by all but the last form in body, and to have a body that (via pprogn) first executes the form in the last element of body and then returns a call to the command skip (which will return (mv nil t state)).

INSTRUCTIONS

instructions to the proof checker


Parent topic:  PROOF-CHECKER
Home

Example:
:instructions (induct prove promote (dive 1) x
                      (dive 2) = top (drop 2) prove)

See defthm for the role of :instructions in place of :hints. As illustrated by the example above, the value associated with :instructions is a list of proof-checker commands. At the moment the best way to understand the idea of the interactive proof-checker (see proof-checker and see verify) is probably to read the first 11 pages of CLI Technical Report 19, which describes the corresponding facility for Nqthm.

When inside the interactive loop (i.e., after executing verify), use help to get a list of legal instructions and (help instr) to get help for the instruction instr.

MACRO-COMMAND

compound command for the proof-checker


Parent topic:  PROOF-CHECKER
Home

The proof-checker (see proof-checker) allows the user to supply interactive commands. Compound commands, called macro commands, may be defined; these expand into zero or more other commands. Some of these are ``atomic'' macro commands; these are viewed as a single command step when completed successfully.

More documentation will be written on the proof-checker. For now, we simply point out that there are lots of examples of the use of define-pc-macro and define-pc-atomic-macro in the ACL2 source file "proof-checker-b.lisp". The former is used to create macro commands, which can be submitted to the interactive loop (see verify) and will ``expand'' into zero or more commands. The latter is similar, except that the undoing mechanism (see acl2-pc::undo) understands atomic macro commands to represent single interactive commands. Also see acl2-pc::comm and see acl2-pc::commands for a discussion of the display of interactive commands.

Also see toggle-pc-macro for how to change a macro command to an atomic macro command, and vice versa.

RETRIEVE

re-enter a (specified) proof-checker state


Parent topic:  PROOF-CHECKER
Home

Examples:
(retrieve associativity-of-permutationp)
retrieve

General Form:
(retrieve &optional name)

See acl2-pc::retrieve, or use (help retrieve) inside the interactive proof-checker loop. Also see unsave.

TOGGLE-PC-MACRO

change an ordinary macro command to an atomic macro, or vice-versa


Parent topic:  PROOF-CHECKER
Home

Example:
(toggle-pc-macro pro)

Change pro from an atomic macro command to an ordinary one (or vice-versa, if pro happens to be an ordinary macro command)

General Form:
(toggle-pc-macro name &optional new-tp)

If name is an atomic macro command then this turns it into an ordinary one, and vice-versa. However, if new-tp is supplied and not nil, then it should be the new type, or else there is no change.

UNSAVE

remove a proof-checker state


Parent topic:  PROOF-CHECKER
Home

Example:
(unsave assoc-of-append)

General Form:
(unsave name)

Eliminates the association of a proof-checker state with name. See unsave or see acl2-pc::unsave.

Also see acl2-pc::save and see retrieve.

VERIFY

enter the interactive proof checker


Parent topic:  PROOF-CHECKER
Home

For proof-checker command summaries, see proof-checker.

Examples:
(VERIFY (implies (and (true-listp x) (true-listp y))
                      (equal (append (append x y) z)
                             (append x (append y z)))))
   -- Attempt to prove the given term interactively.

(VERIFY (p x)
        :event-name p-always-holds
        :rule-classes (:rewrite :generalize)
        :instructions ((rewrite p-always-holds-lemma)
                       change-goal))
   -- Attempt to prove (p x), where the intention is to call the
      resulting DEFTHM event by the name p-always-holds, with
      rule-classes as indicated.  The two indicated instructions
      will be run immediately to start the proof.


(VERIFY)
   -- Re-enter the proof-checker in the state at which is was last
      left.


General Form:
(VERIFY &OPTIONAL raw-term
        &KEY
        event-name
        rule-classes
        instructions)

Verify is the function used for entering the proof-checker's interactive loop.