18. The Proof Commands

 

This chapter is intended to provide users with documentation for IMPS proof commands. However, it is not suggested that users read this chapter before using IMPS.

Commands can be used in two modes:

• Interactive mode. In this mode an individual command is invoked by supplying the command's name. The system will then prompt you for additional arguments.
• Script mode. In this mode a command is invoked by a command form. Command forms are s-expressions
  
  $$\mbox{\tt (} \mbox{\it command-name} \ \mbox{\it a}_1 \dots\ \mbox{\it a}_n\mbox{\tt ) }$$
  
  
  To use commands in this way, you must know the possible command arguments. Commands in script mode can be invoked line by line, by region, or in batch mode. Moreover, if the command requires no arguments, then the name of the command by itself is a command form.

We will use the following template to describe use of individual commands. (The last three entries are optional.)

Script usage

Describes the use of the command in scripts. Arguments such as theories, macetes, and theorems are specified by name. Some arguments can be specified in various ways. When an argument is an assumption, it can be specified as follows:

• A nonnegative integer i. This denotes the i-th assumption.
• A string $\sigma.$ If $\sigma$ denotes an expression which is alpha-equivalent to an assumption, then it denotes that assumption. If $\sigma$ matches one or more assumptions, then it refers to the first of those assumptions. Matching here is done in a way that does not preserve scopes of binding constructors and places only type constraints on the matching of variables.

Interactive argument retrieval.

This tells you how arguments are requested in the minibuffer when used interactively, with a brief description of each argument. In cases where IMPS can determine that there is only one possible choice for an argument, for example, if the argument is an index number for an assumption when there is exactly one assumption, then IMPS will make this choice and not return for additional input.

Command Kind.

Null-inference, single-inference, or multi-inference. A null-inference command never adds any inference nodes to the deduction graph. A single-inference commands adds exactly one inference node to the deduction graph, when it is successful. A multi-inference command adds more than one inference node to the deduction graph in some cases.

Description.

A brief description of the command. Some commands can be described as rules of inference in a logical calculus. For each such command we use a table composed of the following units:

Conclusion	TEMPLATE
Premise	TEMPLATE

where the item TEMPLATE for the conclusion refers to the form for the given goal (sequent), while the TEMPLATE item for the premise indicates the form for the resulting subgoal. In general, there will be more than one premise; moreover, in some cases we distinguish one particular premise as a major premise. In so doing, we regard the remaining premises as minor premises.

Related commands.

These are other commands you might consider applying because, for example, they are quicker or more effective for your task at hand.

Remarks.

Hints or observations that we think you should find useful.

Key binding.

A single key to invoke the command.

Command Application in Interactive Mode

To apply a command in interactive mode to the current sequent node (that is, the one visible in the sequent node buffer), hit !. You can also apply a command by selecting it from the command menu as follows:

• For Emacs version 19, click on the entry Extend-DG in the menubar and select the option Commands.
• For Emacs version 18, click right on the Command menu item in the Extending the Deduction Graph pane. You can also invoke the command menu directly by pressing the key F3.

You will be presented with a well-pruned menu of those commands which are applicable to the given sequent node. Once you select a command, the system will request the additional arguments it needs to apply the command. You will notice that for a given command, the system will sometimes request additional arguments and at other times not do so. In the cases where the system fails to make a request for arguments, the system determines what these additional arguments should be on its own.

Command Application in Script Mode

For the precise definition of what a script is, see the section on the proof script language in Chapter 12. Essentially a proof script is a sequence of forms of the following kinds:

• $\mbox{\tt (} \mbox{\it keyword} \ \mbox{\it a}_1 \dots\ \mbox{\it a}_n\mbox{\tt )}$
• $\mbox{\tt (} \mbox{\it command-name} \ \mbox{\it a}_1 \dots\ \mbox{\it a}_n\mbox{\tt )}$

Each command form (that is, a form which begins with a command name) instructs IMPS to do the following two things:

• Apply the command with name command-name to the current sequent node with the arguments $\mbox{\it a}_1 \dots \mbox{\it a}_n.$
• Reset the current sequent node to be the first ungrounded relative.

To apply a single command in script mode to the current sequent node, place the cursor on the first line of the command form and type C-c l. In order for the interface software to recognize the form to execute, there cannot be more than one command form per line. However, a single command form can occupy more than one line.

To apply in sequence the command forms within a region, type C-c r.

  
antecedent-inference

Script usage:

(antecedent-inference assumption). assumption can be given as an integer i or a string $\sigma.$

Interactive argument retrieval:

• 0-based index of antecedent formula - $\mbox{\tt (}i_1 \; i_2 \; \cdots \;i_n \mbox{\tt ):}$ i.
  The $i_1,i_2,\ldots,i_n$ are the indices of the assumptions of sequent node on which antecedent inferences can be done, that is an implication, conjunction, disjunction, biconditional, conditional-formula, or an existential formula. In case there is only one such formula, this argument request is omitted.

Command kind:

Single-inference.

Description:

Conclusion	$\Gamma \cup \{ \varphi \supset \psi\} \Rightarrow \theta$
Premises	$\Gamma \cup \{\neg \varphi\} \Rightarrow \theta$
	$\Gamma \cup \{\psi \} \Rightarrow \theta$
Conclusion	$\Gamma \cup \{\varphi_1 \wedge \cdots \wedge \varphi_n \} \Rightarrow \psi$
Premise	$\Gamma \cup \{\varphi_1, \ldots ,\varphi_n \} \Rightarrow \psi$
Conclusion	$\Gamma \cup \{\varphi_1 \vee \cdots \vee \varphi_n \} \Rightarrow \psi$
Premises $(1\leq i \leq n)$	$\Gamma \cup \{\varphi_i \} \Rightarrow \psi$
Conclusion	$\Gamma \cup \{\varphi \equiv \psi\} \Rightarrow \theta$
Premises	$\Gamma \cup \{\varphi,\psi\} \Rightarrow \theta$
	$\Gamma \cup \{\neg \varphi,\neg \psi\}\Rightarrow \theta$
Conclusion	$\Gamma \cup \{\mbox{if-form}(\varphi,\psi,\theta)\} \Rightarrow \xi$
Premises	$\Gamma \cup \{\varphi,\psi\} \Rightarrow \xi$
	$\Gamma \cup \{\neg\varphi,\theta\} \Rightarrow \xi$
Conclusion	$\Gamma \cup \{\exists x_1\mbox{:}\sigma_1, \ldots, x_n\mbox{:}\sigma_n, \varphi\} \Rightarrow \psi$
Premise	$\Gamma \cup \{\varphi^\prime\} \Rightarrow \psi$

Notes:

• Each sequent in the preceding table is of the form $\Gamma \cup \{\varphi\} \Rightarrow \psi$.
• The index of the assumption $\varphi$ in context $\Gamma \cup \{\varphi\}$ is i.
• $\varphi^\prime$ is obtained from $\varphi$ by renaming the variables among $x_1,\ldots,x_n$ which are free in both $\varphi$ and the original sequent.

Related commands

:
antecedent-inference-strategy
direct-and-antecedent-inference-strategy
direct-inference

Remarks:

Keep in mind that any antecedent inference produces subgoals which together are equivalent to the original goal. Thus, it is always safe to do antecedent inferences, in the sense that they do not produce false subgoals from true ones.

Key binding:

a

  
antecedent-inference-strategy

Script usage:

(antecedent-inference-strategy assumption-list).
assumption-list can be given as a list of numbers, a list of strings, or an assumption-list form.

Interactive argument retrieval:

• List of formula indices for antecedent inferences -
  $\mbox{\tt (} i_1 \;i_2 \; \cdots \;i_m \mbox{\tt ):} j_1 \;j_2 \; \cdots \;j_n$. The $i_1,i_2,\ldots,i_m$ are the indices of the assumptions of sequent node on which antecedent inferences can be done, that is an implication, conjunction, disjunction, biconditional, conditional-formula, or an existential formula. In case there is only one such formula, this argument request is omitted.

Command kind:

Multi-inference.

Description:

Call an assumption of the goal sequent node fixed if its index is not among $j_1, \ldots ,j_n.$ This command repeatedly applies the antecedent-inference command to the goal node and resulting subgoal nodes until the only possible antecedent inferences are on fixed assumptions.

Related commands

:
antecedent-inference
direct-and-antecedent-inference-strategy

Remarks:

This command is called as a subroutine by a number of other commands including instantiate-theorem and instantiate-universal-antecedent.

Key binding:

A

  
apply-macete

Script usage:

(apply-macete macete).

Interactive argument retrieval:

• Macete name: The name of a macete. Formally, a macete is a function which takes as arguments a context and an expression and returns an expression. Macetes are used to apply a theorem or a collection of theorems to a sequent in a deduction graph. In order to use them effectively, read the section on macetes in the manual.

Command kind:

Single-inference.

Description:

This command applies the argument macete to the given sequent node.

Related commands

:
apply-macete-locally
apply-macete-locally-with-minor-premises
apply-macete-with-minor-premises

Remarks:

Macetes are an easy and very effective way of applying lemmas in a proof. In fact, in the course of developing a theory, we suggest that some effort be expended in formulating lemmas with a view to applying them as macetes.

Key binding:

m

  
apply-macete-locally

Script usage:

(apply-macete-locally macete expression occurrences).

Interactive argument retrieval:

• Macete name: The name of a macete.

• Expression to apply macete: A subexpression of the sequent assertion to which you want to apply the macete.

• Occurrences of expression (0-based): The list occurrences of the expression you want to apply the macete to.

Command kind:

Single-inference.

Description:

This command applies the argument macete to the given sequent node at those occurrences of the expression supplied in response to the minibuffer prompt.

Related commands

:
apply-macete
apply-macete-locally-with-minor-premises
apply-macete-with-minor-premises

Remarks:

This command is useful when you need to control where a macete is applied, in cases where it applies at several locations. For example, if the sequent assertion is | x+y² | = | y²+x |, then applying the macete commutative-law-for-addition to the 0-th occurrence of x+y² yields a new sequent with assertion |y²+x | = | y²+x |. If the macete had been applied globally, the resulting assertion would have been |y²+x | = | x+y²|.

  
apply-macete-locally-with-minor-premises

Script usage:

(apply-macete-locally-with-minor-premises macete expression occurrences).

Interactive argument retrieval:

• Macete name: The name of a macete.

• Expression to apply macete: A subexpression of the sequent assertion to which you want to apply the macete.

• Occurrences of expression (0-based): The list occurrences of the expression you want to apply the macete to.

Command kind:

Single-inference.

Description:

This command applies the argument macete to the given sequent node, in the same way as apply-macete-locally, but with the following important difference: whenever the truth or falsehood of a definedness or sort-definedness assertion cannot be settled by the simplifier, the assertion is posted as a additional subgoal to be proved.

Related commands

:
apply-macete
apply-macete-locally
apply-macete-with-minor-premises

  
apply-macete-with-minor-premises

Script usage:

(apply-macete-with-minor-premises macete).

Interactive argument retrieval:

• Macete name: The name of a macete.

Command kind:

Single-inference.

Description:

This command applies the argument macete to the given sequent node, in the same way as apply-macete, but with the following important difference: whenever the truth or falsehood of a convergence requirement cannot be settled by the simplifier, the assertion is posted as a additional subgoal to be proved.

Related commands

:
apply-macete
apply-macete-locally
apply-macete-locally-with-minor-premises

Remarks:

The convergence requirements which are posted as additional subgoals arise from two different sources:

1.

Convergence requirements are generated by the simplifier in the course of certain reductions, including algebraic simplification and beta-reduction.

2.

Convergence requirements are also generated by checks that instantiations of universally valid formulas used by the macete are sound.

You should never assume that subgoals generated by this command are always true. As always for nonreversible commands, you should inspect the new subgoals to insure IMPS is not misdirecting your proof.

  
assume-theorem

Script usage:

(assume-theorem theorem).

Interactive argument retrieval:

• Theorem name: The name of a theorem in the deduction graph theory.

Command kind:

Single-inference.

Description:

This command adds the argument theorem to the context of the given sequent.

Related commands

:
apply-macete
assume-transported-theorem
instantiate-theorem

Remarks:

To apply a theorem to a sequent, you will usually want to use apply-macete or instantiate-theorem instead of assume-theorem.

  
assume-transported-theorem

Script usage:

(assume-transported-theorem theorem interpretation).

Interactive argument retrieval:

• Theorem name: The name of a theorem in T.

• Theory interpretation: The name of a theory interpretation of T in the deduction graph's theory.

Command kind:

Single-inference.

Description:

This command transports the argument theorem to the deduction graph's theory via the argument theory interpretation. Then the transported theorem is added to the context of the given sequent using assume-theorem.

Related commands

:
apply-macete
assume-theorem
instantiate-transported-theorem

Remarks:

To apply a theorem to a sequent from outside the deduction graph's theory, you will usually want to use apply-macete or instantiate-transported-theorem instead of assume-transported-theorem.

  
auto-instantiate-existential

Script usage:

auto-instantiate-existential.

Interactive argument retrieval:

None.

Command Kind:

Multi-inference.

Description:

This command tries to instantiate an existential assertion with terms from the context of the given sequent.

Related commands

:
auto-instantiate-universal-antecedent
instantiate-existential

  
auto-instantiate-universal-antecedent

Script usage:

(auto-instantiate-universal-antecedent
assumption). assumption can be given as an integer i or a string $\sigma.$

Interactive argument retrieval:

• 0-based index of universal antecedent formula -
  $(i_1 \; i_2 \; \cdots \;i_n$): i. The $i_1,i_2,\ldots,i_n$ are the indices of the universal assumptions of the sequent node. In case there is only one universal antecedent formula, this argument request is omitted.

Command Kind:

Multi-inference.

Description:

This command tries to instantiate the i-th assumption of the context of the given sequent with terms from the context.

Related commands

:
auto-instantiate-existential
instantiate-universal-antecedent

  
backchain

Script usage:

(backchain assumption). assumption can be given as an integer i or a string $\sigma.$

Interactive argument retrieval:

• 0-based index of antecedent formula: If there is only one assumption, this argument request is omitted.

Command Kind:

Single-inference.

Description:

This command includes the behavior described under backchain-through-formula. However, for a part of the assumption of one of the forms s=t, $s\simeq t$, $s\equiv t$, if a subexpression of the assertion matches s, then it is replaced by the corresponding instance of t.

Related commands

:
backchain-backwards
backchain-repeatedly
backchain-through-formula

Key Binding:

b

  
backchain-backwards

Script usage:

(backchain-backwards assumption). assumption can be given as an integer i or a string $\sigma.$

Interactive argument retrieval:

• 0-based index of antecedent formula:

Command Kind:

Single-inference.

Description:

Backchain-backwards differs from backchain in that subformulas of the assumption of the forms s=t, $s\simeq t$, $s\equiv t$ are used from right to left.

Related commands

:
backchain
backchain-repeatedly
backchain-through-formula

  
backchain-repeatedly

Script usage:

(backchain-repeatedly assumption-list). assumption-list can be given as a list of numbers, of strings or an assumption-list form.

Interactive argument retrieval:

• List of 0-based indices of antecedent formulas: If there is only one assumption, this argument request is omitted.

Command Kind:

Multi-inference.

Description:

A succession of backchains are performed using the indicated assumptions. Execution terminates when every backchaining opportunity against those assumptions has been used up.

Related commands

:
backchain
backchain-backwards
backchain-through-formula

  
backchain-through-formula

Script usage:

(backchain-through-formula assumption). assumption can be given as an integer i or a string $\sigma.$

Interactive argument retrieval:

• 0-based index of antecedent formula: If there is only one assumption, this argument request is omitted.

Command kind:

Single-inference.

Description:

This command attempts to use the assumption with the given index to replace the assertion to be proved. In the simplest case, if the given assumption is $\varphi\supset \psi$ and the assertion is $\psi$, then backchain-through-formula replaces the assertion with $\varphi$. Similarly, if the assertion is $\lnot \varphi$, it is replaced with $\lnot \psi$. The command extends this simplest case in four ways:

• If the assumption is universally quantified, then matching is used to select a relevant instance.
• If the assumption is a disjunction
  
  $$\bigvee_{i\in i} \varphi_i,$$
  
  
  then, for any $j\in i$, it may be treated as
  
  $$(\bigwedge_{i\in i, i\not=j} \lnot \varphi_i) \;\supset\; \varphi_j.$$
  
  

• If the assumption is a conjunction, each conjunct is tried separately, in turn.
• These rules are used iteratively to descend through the structure of the assumption as deeply as necessary.

If IMPS cannot recognize that the terms returned by a match are defined in the appropriate sorts, then these assertions are returned as additional minor premises that must later be grounded to complete the derivation.

Related commands

:
backchain
backchain-backwards
backchain-repeatedly

  
beta-reduce

Script usage:

beta-reduce.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command attempts to beta-reduce each lambda-application in the assertion of the given sequent.

Related commands

:
beta-reduce-antecedent
beta-reduce-insistently
beta-reduce-repeatedly
beta-reduce-with-minor-premises
simplify

Remarks:

Since beta-reduction can often be applied several times in a row, the command beta-reduce-repeatedly is usually preferable to this command. Beta-reduction is also performed by simplify.

  
beta-reduce-antecedent

Script usage:

(beta-reduce-antecedent assumption). assumption can be given as an integer i or a string $\sigma.$

Interactive argument retrieval:

• 0-based index of antecedent-formula: i. If there is only one assumption, this argument request is omitted.

Command kind:

Multi-inference.

Description:

This command is used for beta-reducing an assumption in the context of the given sequent. It is equivalent to the following sequence of commands: incorporate-antecedent applied to the given sequent with argument i; beta-reduce-repeatedly applied to the sequent yielded by the previous command; and direct-inference applied to the sequent yielded by the previous command. The commands halts if beta-reduce-repeatedly grounds the first produced sequent.

Related commands:

:
beta-reduce-repeatedly
simplify-antecedent

Remarks:

The implementation of this command has the side effect that the assertion is beta-reduced as well as the antecedent formula.

  
beta-reduce-insistently

Script usage:

beta-reduce-insistently.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command is equivalent to disabling all quasi-constructors and then calling beta-reduce.

Related commands

:
beta-reduce
insistent-direct-inference
simplify-insistently

Remarks:

There is rarely any need to use this command. It has the disagreeable effect of exploding quasi-constructors.

  
beta-reduce-repeatedly

Script usage:

beta-reduce-repeatedly.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command attempts to beta-reduce each lambda-application in the assertion of the given sequent repeatedly until there are no longer any lambda-applications that beta-reduce.

Related commands

:
beta-reduce
beta-reduce-antecedent

Remarks:

Since beta-reduction can often be applied several times in a row, this command is usually preferable to the command beta-reduce.

Key binding:

C-c b

  
beta-reduce-with-minor-premises

Script usage:

beta-reduce-with-minor-premises.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command is the same as beta-reduce except that, instead of failing when convergence requirements are not verified, it posts the unverified convergence requirements as additional subgoals to be proved.

Related commands

:
beta-reduce
simplify-with-minor-premises

Remarks:

This command is useful for determining why a lambda-application does not beta-reduce.

  
case-split

Script usage:

(case-split list-of-formulas).

Interactive argument retrieval:

• First formula: $\varphi_1$.
• Next formula (<RET> if done): $\varphi_1$.
  
• Next formula (<RET> if done): $\varphi_n\ \ (n \geq 1)$.

Description:

This command considers all the different possible cases for $\varphi_1, \ldots ,\varphi_n.$

Conclusion	$\Gamma \Rightarrow \psi$
Premises $(A \subseteq \{1,\ldots,n\})$	$\Gamma \cup \{\varphi^A_1 \wedge \cdots \wedge \varphi^A_n\} \Rightarrow \psi$

Notes:

• For each $A \subseteq \{1,\ldots,n\},$ $\varphi^A_i$ is $\varphi_i$if $i \in A,$ and $\neg \varphi_i$ otherwise.

  
case-split-on-conditionals

Script usage:

(case-split-on-conditionals occurrences). occurrences is a list of integers.

Interactive argument retrieval:

• Occurrences of conditionals to be raised (0-based): A list l given in the form $l_1 \cdots l_n$.

Command kind:

Multi-inference.

Description:

This command applies case-split to the first components of the conditional expressions in the given sequent specified by l. The command simplify is then applied to each of the newly created sequents.

Related commands:

:
case-split
raise-conditional

Remarks:

Avoid using this command with more than two occurrences of conditionals.

  
choice-principle

Script usage:

choice-principle.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command implements a version of the axiom of choice.

Conclusion	$\Gamma \Rightarrow \exists f\mbox{:}[\sigma_1,\ldots,\sigma_n,\tau], \forall x_1\mbox{:}\sigma^{\prime}_{1},\ldots, x_n\mbox{:}\sigma^{\prime}_{n}, \varphi$
Premise	$\Gamma \Rightarrow \forall x_1\mbox{:}\sigma^{\prime}_{1},\ldots, x_n\mbox{:... ..._{n}, \exists y_f\mbox{:}\tau, \varphi[{y_f}/{f(x_1,\ldots,x_n)}]_{\rm all}$

Notes:

• $\sigma_i$ and $\sigma^{\prime}_{i}$ have the same type for all i with $1 \leq i \leq n$.
• The command fails if there is any occurrence of f in $\varphi$ which is not in an application of the form $f(x_1, \ldots ,x_n)$.

Remarks:

The existential sequence is often introduced into the deduction graph using cut-with-single-formula.

  
contrapose

Script usage:

(contrapose assumption). assumption can be given as an integer i or a string $\sigma.$

Interactive argument retrieval:

• 0-based index of antecedent-formula: i. If there is only one assumption, this argument request is omitted.

Command kind:

Single-inference.

Description:

This command interchanges the given sequent's assertion and its assumption given by i.

Conclusion	$\Gamma \cup \{\varphi\} \Rightarrow \psi$
Premise	$\Gamma \cup \{\neg\psi \} \Rightarrow \neg \varphi$

Notes:

• The index of $\varphi$ in context $\Gamma \cup \{\varphi\}$ is i.

Remarks:

Use contrapose if you want to do ``proof by contradiction.'' However, if there is nothing to contrapose with (because the sequent has no assumptions), you will have to add an assumption by using cut-with-single-formula or instantiate-theorem.

Key binding:

c

  
cut-using-sequent

Script usage:

(cut-using-sequent sequent-node). sequent-node can be given as an integer (referring to the sequent node with that number) or as a list (context-string assertion-string).

Interactive argument retrieval:

• Major premise number: The number of a sequent node.

Command kind:

Single-inference.

Description:

This command allows you to add some new assumptions to the context of the given sequent. Of course, you are required to show separately that the new assumptions are consequences of the context. The node containing the major premise sequent must exist before the command can be called. Usually you create this sequent node with edit-and-post-sequent-node.

Conclusion	$\Gamma \Rightarrow \varphi$
Major Premise	$\Gamma \cup \{\psi_1,\ldots,\psi_n\} \Rightarrow \varphi$
Minor Premises $(1\leq i \leq n)$	$\Gamma \Rightarrow \psi_i$

Related commands:

cut-with-single-formula.

Remarks:

To cut with one formula, you should usually use cut-with-single-formula.

  
cut-with-single-formula

Script usage:

(cut-with-single-formula formula).

Interactive argument retrieval:

• Formula to cut: String specifying a formula $\psi$.

Command kind:

Single-inference.

Description:

This command allows you to add a new assumption to the context of the given sequent. Of course, you are required to show separately that the new assumption is a consequence of the context.

Conclusion	$\Gamma \Rightarrow \varphi$
Major Premise	$\Gamma \cup \{\psi\} \Rightarrow \varphi$
Minor Premise	$\Gamma \Rightarrow \psi$

Related commands:

cut-using-sequent.

Remarks:

To cut with several formulas at the same time, use cut-using-sequent.

Key binding:

&

  
definedness

Script usage:

definedness.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command applies to a sequent whose assertion is a definedness statement of the form $t\!\!\downarrow$. The command first tests whether the context entails the definedness of t. If the test fails, the command then tries to reduce the sequent to a set of simpler sequents.

Related commands:

sort-definedness.

Remarks:

This command is mainly useful when t is an application or a conditional.

  
direct-and-antecedent-inference-strategy

Script usage:

direct-and-antecedent-inference-strategy.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command repeatedly applies (1) direct-inference to the given sequent and resulting sequents and (2) antecedent-inference to newly created antecedents of the given sequent and resulting sequents until no more such direct and antecedent inferences are possible.

Related commands

:
antecedent-inference-strategy
direct-and-antecedent-inference-strategy-with-simplification
direct-inference-strategy

Key binding:

D

direct-and-antecedent-inference-strategy-with-
simplification

Script usage

:
direct-and-antecedent-inference-strategy-with-simplification.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command first applies direct-and-antecedent-inference-strategy to the given sequent, and then applies simplify to all resulting sequents.

Related commands

:
antecedent-inference-strategy
direct-and-antecedent-inference-strategy
direct-inference-strategy

  
direct-inference

Script usage:

direct-inference.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command applies an analogue of an introduction rule of Gentzen's sequent calculus (in reverse), based on the leading constructor of the assertion of the given sequent.

Conclusion	$\Gamma \Rightarrow \varphi \supset \psi$
Premise	$\Gamma \cup \{\varphi\} \Rightarrow \psi$
Conclusion	$\Gamma \Rightarrow \varphi_1 \wedge \cdots \wedge \varphi_n$
Premises $(1\leq i \leq n)$	$\Gamma \cup \{\varphi_1, \ldots ,\varphi_{i-1}\} \Rightarrow \varphi_i$
Conclusion	$\Gamma \Rightarrow \varphi_1 \vee \cdots \vee \varphi_n$
Premise	$\Gamma \cup \{ \neg \varphi_1 , \ldots , \neg \varphi_{n-1}\} \Rightarrow \varphi_n$
Conclusion	$\Gamma \Rightarrow \varphi \equiv \psi$
Premises	$\Gamma \cup \{\varphi\} \Rightarrow \psi$
	$\Gamma \cup \{\psi\} \Rightarrow \varphi$
Conclusion	$\Gamma \Rightarrow \mbox{if-form}(\varphi,\psi,\theta)$
Premises	$\Gamma \cup \{\varphi\} \Rightarrow \psi$
	$\Gamma \cup \{\neg \psi\} \Rightarrow \theta$
Conclusion	$\Gamma \Rightarrow \forall x_1\mbox{:}\sigma_1, \ldots, x_n\mbox{:}\sigma_n, \varphi$
Premise	$\Gamma \Rightarrow \varphi^\prime$

Notes:

• $\varphi^\prime$ is obtained from $\varphi$ by renaming the variables among $x_1,\ldots,x_n$ which are free in both $\varphi$ and the context $\Gamma.$

Related commands

:
antecedent-inference
direct-inference-strategy
unordered-direct-inference

Remarks:

Keep in mind that any direct inference produces subgoals which together are equivalent to the original goal. Thus it is always safe to do direct inferences, in the sense that they do not produce false subgoals from true goals.

Key binding:

d

  
direct-inference-strategy

Script usage:

direct-inference-strategy.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command repeatedly applies direct-inference to the given sequent and resulting sequents until no more direct inferences are possible. In other words, it adds to the deduction graph the smallest set of sequents containing the given sequent and closed under direct inferences.

Related commands

:
antecedent-inference-strategy
direct-inference
direct-and-antecedent-inference-strategy

  
disable-quasi-constructor

Script usage:

(disable-quasi-constructor quasi-constructor).

Interactive argument retrieval:

• Quasi-constructor name: The name of a quasi-constructor in the expression.

Command kind:

Null-inference.

Description:

This command disables the quasi-constructor given as argument.

  
edit-and-post-sequent-node

Script usage:

(edit-and-post-sequent-node context-string assertion-string).

Interactive argument retrieval:

• Edit sequent and C-c C-c when finished. A sequent presented as a string of formulas using => to separate the sequent assumptions from the sequent assertion.

Command kind:

Null-inference.

Description:

This commands adds the sequent given as an argument to the deduction graph.

Key binding:

e

  
eliminate-defined-iota-expression

Script usage:

(eliminate-iota index symbol).

Interactive argument retrieval:

• 0-based index of iota-expression occurrence: i.
• Name of replacement variable: y

Command kind:

Multi-inference.

Description:

This command replaces the i-th occurrence of an iota-expression in the given sequent's assertion with the variable y. The command is predicated upon the iota-expression being defined with respect to the sequent's context. (An iota-expression is an expression whose lead constructor is iota or a quasi-constructor that builds an iota-expression.)

Conclusion	$\Gamma \Rightarrow \psi$
Major Premise	$\Gamma \cup \{\varphi[{y}/{x}]_{\rm free}, \forall z\mbox{:}\sigma, (\varphi[{z}/{x}]_{\rm free} \supset z=y)\} \Rightarrow \psi'$
Minor Premise	$\Gamma \Rightarrow (\iota x\mbox{:}\sigma, \varphi)\!\!\downarrow$

Notes:

• $\iota x\mbox{:}\sigma, \varphi$ is the i-th iota-expression occurrence in $\psi$.
• $\psi'$ is the result of replacing the i-th iota expression occurrence in $\psi$ with y.

Related commands:

eliminate-iota.

Remarks:

This command is very useful for dealing with iota-expressions that are known to be defined with respect to the sequent's context. The minor premise is grounded automatically if the sequent's context contains $(\iota x\mbox{:}\sigma, \varphi)\!\!\downarrow$.

  
eliminate-iota

Script usage:

(eliminate-iota index).

Interactive argument retrieval:

• 0-based index of iota-expression occurrence: i.

Command kind:

Single-inference.

Description:

This command applies to a sequent whose assertion is an atomic formula or negated atomic formula containing a specified occurrence of an iota-expression. The command reduces the sequent to an equivalent sequent in which the specified iota-expression occurrence is ``eliminated.'' (An iota-expression is an expression whose lead constructor is iota or a quasi-constructor that builds an iota-expression.)

Conclusion	$\Gamma \Rightarrow \psi$
Major Premise	$\Gamma \Rightarrow \exists y\mbox{:}\sigma, (\varphi[{y}/{x}]_{\rm free} \wed... ...rall z\mbox{:}\sigma, (\varphi[{z}/{x}]_{\rm free} \supset z=y) \wedge \psi')$
Conclusion	$\Gamma \Rightarrow \neg \psi$
Major Premise	$\Gamma \Rightarrow \exists y\mbox{:}\sigma, (\varphi[{y}/{x}]_{\rm free} \wedge \forall z\mbox{:}\sigma, (\varphi[{z}/{x}]_{\rm free} \supset z=y)) \supset$
	$\exists y\mbox{:}\sigma, (\varphi[{y}/{x}]_{\rm free} \supset \neg\psi')$

Notes:

• $\psi$ is an atomic formula.
• $\iota x\mbox{:}\sigma, \varphi$ is the i-th iota-expression occurrence in $\psi$, an atomic formula.
• $\psi'$ is the result of replacing the i-th iota-expression occurrence in $\psi$ with y.
• The occurrence of $\iota x\mbox{:}\sigma, \varphi$ in $\psi$ is within some argument component s of $\psi$. Moreover, the occurrence is an extended application component of s, where a is an extended application component of b if either a is bor b is an application of kind $\iota$ and a is an extended application component of a component of b.

Related commands:

eliminate-defined-iota-expression.

Remarks:

If $\psi$ is an equation or a definedness expression, the macete eliminate-iota-macete is more direct than eliminate-iota.

  
enable-quasi-constructor

Script usage:

(enable-quasi-constructor quasi-constructor).

Interactive argument retrieval:

• Quasi-constructor name: The name of a quasi-constructor in the expression.

Command kind:

Null-inference.

Description:

This command enables the quasi-constructor given as argument.

  
extensionality

Script usage:

extensionality.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

If the sequent node assertion is an equality or quasi-equality or the negation of an equality or quasi-equality of n-ary functions, this command applies the extensionality principle.

Conclusion	$\Gamma \Rightarrow f=g$
Major Premise	$\Gamma \Rightarrow \forall x_1\mbox{:}\sigma_1, \dots ,x_n\mbox{:}\sigma_n, f(x_1, \cdots ,x_n) \simeq g(x_1, \cdots ,x_n)$
Minor Premise	$\Gamma \Rightarrow f\!\!\downarrow$
Minor Premise	$\Gamma \Rightarrow g\!\!\downarrow$
Conclusion	$\Gamma \Rightarrow f \simeq g$
Major Premise	$\Gamma \Rightarrow \forall x_1\mbox{:}\sigma_1, \dots ,x_n\mbox{:}\sigma_n, f(x_1, \cdots ,x_n) \simeq g(x_1, \cdots ,x_n)$
Minor Premise	$\Gamma \cup \{g\!\!\downarrow\} \Rightarrow f\!\!\downarrow$
Minor Premise	$\Gamma \cup \{f\!\!\downarrow\} \Rightarrow g\!\!\downarrow$
Conclusion	$\Gamma \Rightarrow \neg f=g$
Premise	$\Gamma \Rightarrow \exists x_1\mbox{:}\sigma_1, \dots ,x_n\mbox{:}\sigma_n, \neg f(x_1, \cdots ,x_n) \simeq g(x_1, \cdots ,x_n)$
Conclusion	$\Gamma \Rightarrow \neg f \simeq g$
Premise	$\Gamma \Rightarrow \exists x_1\mbox{:}\sigma_1, \dots ,x_n\mbox{:}\sigma_n, \neg f(x_1, \cdots ,x_n) \simeq g(x_1, \cdots ,x_n)$

Notes:

• If the sorts of f and g are $[\alpha_1,\ldots,\alpha_n,\alpha_{n+1}]$ and $[\beta_1,\ldots,\beta_n,\beta_{n+1}]$, respectively, then $\sigma_i= \alpha_i \sqcup \beta_i$ for all i with $1 \leq i \leq n$.
• A sequent node corresponding to a minor premise is not created if the truth of the minor premise is immediately apparent to IMPS.
• If f and g are of kind $\ast$, then ``='' is used in place of ``$\simeq$'' in the premise.

Remarks:

By substitution of quasi-equals for quasi-equals, both f=g and $f \simeq g$ imply

$$\forall x_1\mbox{:}\sigma_1, \dots ,x_n\mbox{:}\sigma_n, f(x_1, \cdots ,x_n) \simeq g(x_1, \cdots ,x_n) .$$

So in this direction extensionality is nothing new.

Key binding:

~

  
force-substitution

Script usage:

(force-substitution expression replacement occurrences). expression and replacement are denoted by strings, and occurrences is a list of integers.

Interactive argument retrieval:

• Expression to replace: The subexpression e of the sequent node assertion you want to replace.
• Replace it with: The new expression r you want to replace it with.
• 0-based indices of occurrences to change: A list lgiven in the form $l_1 \cdots l_n$.

Command kind:

Single-inference.

Description:

This command allows you to change part of the sequent assertion. It yields two or more new subgoals. One subgoal is obtained from the original sequent assertion by making the requested replacements. The other subgoals assert that the replacements are sound.

Conclusion	$\Gamma \Rightarrow \varphi$
Major Premise	$\Gamma \Rightarrow \varphi[{r}/{e}]_{l}$
Minor Premises $(1\leq i \leq n)$	$\Gamma_i \Rightarrow \varphi_i$

Notes:

• $\Gamma_i$ is the local context of $\Gamma \Rightarrow \varphi$ at the location of the l_i-th occurrence of e in $\varphi$.
• $\varphi_i$ is
  • $e \equiv r$ if e is a formula and the parity of the path l_i is 0.
  • $r \supset e$ if e is a formula and the parity of the path l_i is 1.
  • $e \supset r$ if e is a formula and the parity of the path l_i is -1.
  • $e \simeq r$ in all other cases.

Key binding:

f

  
generalize-using-sequent

Script usage:

(generalize-using-sequent major-premise). major-premise can be given as an integer (referring to the sequent node with that number) or as a list (context-string assertion-string).

Interactive argument retrieval:

• Major premise number: The number of a sequent node.

Command kind:

Single-inference.

Description:

This command generalizes the assertion of the given sequent. The node containing the major premise sequent must exist before the command can be called. Usually you create this sequent node with edit-and-post-sequent-node.

Conclusion	$\Gamma \Rightarrow \varphi$
Major Premise	$\Gamma \Rightarrow \forall x_1\mbox{:}\sigma_1,\ldots,x_n\mbox{:}\sigma_n, \varphi'$
Minor Premises $(1\leq i \leq n)$	$\Gamma \Rightarrow t_i \downarrow \sigma_i$

Notes:

• $\varphi$ is the result of simultaneously replacing each free occurrence of x_i in $\varphi'$ with t_i for all i with $1 \leq i \leq n$.
• t_i is free for x_i in $\varphi'$ for each i with $1 \leq i \leq n$.

  
incorporate-antecedent

Script usage:

(incorporate-antecedent assumption). assumption can be given as an integer i or a string $\sigma.$

Interactive argument retrieval:

• 0-based index of antecedent-formula: i. If there is only one assumption, this argument request is omitted.

Command kind:

Single-inference.

Description:

This commands does the reverse of direct-inference on an implication.

Conclusion	$\Gamma \cup \{\varphi\} \Rightarrow \psi$
Premise	$\Gamma \Rightarrow \varphi \supset \psi$

Notes:

• The index of $\varphi$ in the context $\Gamma \cup \{\varphi\}$is i.

Related commands:

direct-inference.

Remarks:

This command is used for incorporating an assumption of a sequent's context into the sequent's assertion. It is particularly useful as a preparation for applying such commands as apply-macete, beta-reduce, and simplify.

Key binding:

@

  
induction

Script usage:

(induction inductor variable). inductor is a symbol naming an inductor, and variable is a string or (). If () is supplied as argument, IMPS will choose the variable of induction itself.

Interactive argument retrieval:

• Inductor: An inductor is an IMPS structure which has an associated induction principle together with heuristics (in the form of macetes and commands) to handle separately the base and induction cases.

• Variable to induct on (<RET> to use IMPS default): IMPS will choose a variable of the appropriate sort to induct on. Thus, in general, there is no danger that it will attempt to induct on a variable for which induction makes no sense. However, if various choices for an induction variable are possible, the choice is more or less arbitrary. In these cases, you should be prepared to suggest the variable.

Command kind:

Multi-inference.

Description:

This command attempts to apply a formula called an induction principle to a sequent and applies some auxiliary inferences as well. The induction principle used by IMPS is determined by the inductor you give as an argument. When using the induction command, the system will attempt to reformulate the sequent in a form which matches the induction principle. In particular, you can use the induction command directly in cases where the goal sequent does not exactly match the induction principle.

Remarks:

In a formal sense ``induction'' refers to an axiom or theorem in a particular theory (for example, the formula of weak induction below), and in this sense, ``applying induction,'' means applying this formula to a sequent. However, induction alone rarely gets the job done. Other tricks, such as algebraic simplification, beta-reduction, and unfolding of definitions, especially recursive ones, are usually needed. In this broader sense, induction can be thought of as a proof technique incorporating a large number of fairly standard inferences.

Despite its simplicity, induction is one of the most powerful proof techniques in mathematics, especially in proofs for formulas involving the integers. Moreover, forms of induction are also used in theories of syntax or theories of lists. An induction principle in one of these theories is usually referred to as structural induction.

The induction principle for the inductor integer-inductor is the formula

$$\begin{eqnarray*}\lefteqn{\forall s\mbox{:}[{ \bf z },\ast] ,m\mbox{:}{ \bf z },... ... t \mbox{:}{ \bf z }, m \leq t \supset (s(t) \supset s(t+1)))). \end{eqnarray*}$$

This formula is usually referred to as the principle of weak induction. You might also be familiar with the principle of strong induction; in fact, both induction principles are equivalent. However, some formulas cannot be proved directly with the principle of weak induction, because the induction hypothesis is not sufficiently strong to prove the induction conclusion. In such cases, instead of using a different induction principle, you first prove a stronger formula by using the same weak induction principle.

You can build inductors using the form def-inductor. See Section 17.1.

Key binding:

i

  
insistent-direct-inference

Script usage:

insistent-direct-inference.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command is equivalent to disabling all quasi-constructors and then calling direct-inference.

Related commands

:
direct-inference
insistent-direct-inference-strategy.

Remarks:

There is rarely any need to use this command. It has the disagreeable effect of exploding quasi-constructors.

  
insistent-direct-inference-strategy

Script usage:

insistent-direct-inference-strategy.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command repeatedly applies the insistent-direct-inference command to the goal node and resulting subgoal nodes until no more insistent direct inferences are possible. In other words, it adds to the deduction graph the smallest set of sequents containing the goal sequent and closed under insistent direct inferences. This command is equivalent to disabling all quasi-constructors and then calling direct-inference-strategy.

Related commands

:
direct-inference-strategy
insistent-direct-inference

Remarks:

Like insistent-direct-inference, this command has the disagreeable effect of exploding quasi-constructors.

  
instantiate-existential

Script usage:

(instantiate-existential instantiations). instantiations is a list of strings denoting expressions.

Interactive argument retrieval:

• Instance for variable x₁ of sort $\sigma_1$: t₁.
  
• Instance for variable x_n of sort $\sigma_n$: t_n $(n \geq 1)$.

Command kind:

Multi-inference.

Description:

This command instantiates an existential assertion with the specified terms.

Conclusion	$\Gamma \Rightarrow \exists x_1\mbox{:}\sigma_1,\ldots,x_n\mbox{:}\sigma_n, \varphi$
Major Premise	$\Gamma \Rightarrow \varphi'$
Minor Premises $(1\leq i \leq n)$	$\Gamma \Rightarrow t_i \downarrow \sigma_i$

Notes:

• $\varphi'$ is the result of simultaneously replacing each free occurrence of x₁ in $\varphi$ with t_i, for each i with $1 \leq i \leq n$, if necessary renaming bound variables in $\varphi$ to avoid variable captures.

Related commands:

auto-instantiate-existential.

  
instantiate-theorem

Script usage

(instantiate-theorem theorem instantiations). theorem is the name of a theorem, and instantiations is a list of strings denoting expressions.

Interactive argument retrieval:

• Theorem name: The name of a theorem $\forall x_1\mbox{:}\sigma_1,\ldots,x_n\mbox{:}\sigma_n, \psi$ in the deduction graph's theory.
• Instance for variable x₁ of sort $\sigma_1$: t₁.
  
• Instance for variable x_n of sort $\sigma_n$: t_n $(n \geq 1)$.

Command kind:

Multi-inference.

Description:

This command instantiates the argument theorem with the specified terms $t_1,\ldots,t_n$ and then adds the resulting formula to the context of the given sequent.

Conclusion	$\Gamma \Rightarrow \varphi$
Major Premise	$\Gamma \cup \{\psi'\}\Rightarrow \varphi$
Minor Premises $(1\leq i \leq n)$	$\Gamma \Rightarrow t_i \downarrow \sigma_i$

Notes:

• $\psi'$ is the result of simultaneously replacing each free occurrence of x_i in $\psi$ with t_i, for each i with $1 \leq i \leq n$, if necessary renaming bound variables in $\psi$ to avoid variable captures.

Related commands

:
assume-theorem
instantiate-transported-theorem

  
instantiate-transported-theorem

Script usage:

(instantiate-transported-theorem theorem interpretation instantiations). theorem is the name of a theorem, interpretation is the name of a theory interpretation, and instantiations is a list of strings denoting expressions.

Interactive argument retrieval:

• Theorem name: The name of a theorem $\forall x_1\mbox{:}\sigma_1,\ldots,x_n\mbox{:}\sigma_n, \psi$ in T.
• Theory interpretation (<RET> to let IMPS find one): The
  name of a theory interpretation i of T in the deduction graph's theory.
• Instance for variable x₁ of sort $\sigma_1$: t₁.
  
• Instance for variable x_n of sort $\sigma_n$: t_n $(n \geq 1)$.

Command kind:

Multi-inference.

Description:

This command transports the argument theorem to the deduction graph's theory via i. Then, the transported theorem is instantiated with the specified terms $t_1,\ldots,t_n$. And, finally, the resulting formula is added to the context of the given sequent.

If no theory interpretation name is given, IMPS will try to find a theory interpretation to play the role of i using the sort information contained in the terms $t_1,\ldots,t_n$.

Related commands

:
assume-transported-theorem
instantiate-theorem

Remarks:

IMPS can often find an appropriate theory interpretation automatically when the home theory of the theorem is a generic theory, i.e., a theory which contains neither constants nor axioms.

  
instantiate-universal-antecedent

Script usage:

(instantiate-universal-antecedent assumption instantiations). assumption can be given as an integer i or a string $\sigma$, and instantiations is a list of strings denoting expressions.

Interactive argument retrieval:

• 0-based index of universal antecedent formula
  $\mbox{\tt (}i_1 \; i_2 \; \cdots \;i_n \mbox{\tt ):}$ i. The $i_1,i_2,\ldots,i_n$ are the indices of the universal assumptions of the sequent node. In case there is only one universal antecedent formula, this argument request is omitted.
• Instance for variable x₁ of sort $\sigma_1$: t₁.
  
• Instance for variable x_n of sort $\sigma_n$: t_n $(n \geq 1)$.

Command kind:

Multi-inference.

Description:

This command instantiates the i-th assumption of the context of the given sequent (provided the assumption is a universal statement).

Conclusion	$\Gamma \cup \{\forall x_1\mbox{:}\sigma_1,\ldots,x_n\mbox{:}\sigma_n, \psi\}\Rightarrow \varphi$
Major Premise	$\Gamma \cup \{\psi'\}\Rightarrow \varphi$
Minor Premises $(1\leq i \leq n)$	$\Gamma \Rightarrow t_i \downarrow \sigma_i$

Notes:

• The index of the assumption $\forall x_1\mbox{:}\sigma_1,\ldots,x_n\mbox{:}\sigma_n, \psi$ in the context $\Gamma \cup \{\forall x_1\mbox{:}\sigma_1,\ldots,x_n\mbox{:}\sigma_n,\psi\}$ is i.
• $\psi'$ is the result of simultaneously replacing each free occurrence of x₁ in $\psi$ with t_i, for each i with $1 \leq i \leq n$, if necessary renaming bound variables in $\psi$ to avoid variable captures.

Related commands

:
auto-instantiate-universal-antecedent
instantiate-universal-antecedent-multiply

  
instantiate-universal-antecedent-multiply

Script usage:

(instantiate-universal-antecedent-multiply assumption lists-of-instantiations). assumption can be given as an integer i or a string $\sigma$, and lists-of-instantiations is a list of lists of strings which specify the expressions that instantiate the universally quantified assumption.

Interactive argument retrieval:

• 0-based index of antecedent-formula: i. If there is only one assumption, this argument request is omitted.
• First instance term: t₁.
• Next instance term (<RET> if done): t₂.
  
• Next instance term (<RET> if done): $t_n\ \ (n \geq 1)$.
• Input terms for another instance? (y or n)
  

Command kind:

Multi-inference.

Description:

This command produces one or more instances of the i-th assumption of the context of the given sequent (provided the assumption is a universal statement) in the same way that instantiate-universal-antecedent produces one instance of the assumption.

Related commands

:
auto-instantiate-universal-antecedent
instantiate-universal-antecedent

  
prove-by-logic-and-simplification

Script usage:

(prove-by-logic-and-simplification persistence).

Interactive argument retrieval:

• Backchaining persistence: An integer, which is 3 by default.

Command kind:

Multi-inference.

Description

This command tries to ground a sequent by applying a list inference procedures (some of which have a sequent assumption as an additional argument) to the goal node and recursively to the generated subgoal nodes. See Table 18.1. When an inference procedure is applied to the goal sequent or to a subgoal sequent, two possibilities can occur:

1.

The inference procedure fails. In this case, prove-by-logic-and-simplification tries the same inference procedure with the next assumption as argument (if this makes sense), the next inference procedure on the list, if one exists, or otherwise backtracks.

2.

The inference procedure succeeds, either grounding the node or generating one or more new subgoals to prove. In this case we attempt to prove each new subgoal by applying the primitive inferences in order.

 

Table 18.1: Search Order for prove-by-logic-and-simplification

Condition	Procedure	Action
do-simplify?	simplify	lower do-simplify?
0< persist	backchain-through-formula	lower persist
		raise do-simplify?
	antecedent-inference for
	existentials and conjunctions
	direct-inference
	antecedent-inference for
	other assumptions	raise do-simplify?
0< persist	backchain-inference
	sort-definedness
	definedness
	extensionality	raise do-simplify?
	conditional-inference followed	raise do-simplify?
	by direct-inference

Notes:

1.

The variable persist is the backchaining persistence supplied as an argument to the command. lower persist means reduce backchaining persistence by 1.

2.

do-simplify? is a boolean flag which starts off as true when the command is called.

Remarks:

This command is an example of an ending strategy, that is, a proof construction procedure to be used when all that remains to be done is completely straightforward reasoning. It should be used with great caution since in the cases in which it fails to ground a node it may generate a large number of irrelevant subgoals.

Key binding:

None, lest you accidently hit it.

  
raise-conditional

Script usage:

(raise-conditional occurrences). occurrences is given by a list of integers.

Interactive argument retrieval:

• Occurrences of conditionals to be raised (0-based): A list l given in the form $l_1 \cdots l_n$.

Command kind:

Single-inference.

Description:

This command will ``raise'' a subset of the conditional expressions (i.e., expressions whose lead constructor is if), specified by l, in the assertion of the given sequent $\Gamma \Rightarrow \varphi$.

For the moment, let us assume that n=1. Suppose the l₁-th occurrence of a conditional expression in $\varphi$ is the a-th occurrence of $s=\mbox{if}(\theta,t_1,t_2)$ in $\varphi$; the smallest formula containing the a-th occurrence of s in $\varphi$ is the b-th occurrence of $\psi$ in $\varphi$; and the a-th occurrence of s in $\varphi$ is the c-th occurrence of s in $\psi$. If every free occurrence of a variable in s is also a free occurrence in $\psi$, the command reduces the sequent to

$$\Gamma \Rightarrow \varphi[{\mbox{if-form}(\theta, \psi[{t_1}/{s}]_{c}, \psi[{t_2}/{s}]_{c})}/{\psi}]_{b},$$

and otherwise the command fails.

Now assume n > 1. The command will then simultaneously raise each specified occurrence of a conditional expression in $\varphi$, in the manner of the previous paragraph, if there are no conflicts between the occurrences. The kinds of conflicts that can arise and how they are resolved are listed below:

• If two or more specified occurrences of a conditional expression s in $\varphi$ are contained in same smallest formula, they are raised together.
• If two or more specified occurrences of distinct conditional expressions in $\varphi$ are contained in same smallest formula, at most one of the occurrences is raised.
• If $\psi_1$ and $\psi_2$ are the smallest formulas respectively containing two specified occurrences of a conditional expression in $\varphi$ and $\psi_1$ is a proper subexpression of $\psi_2$, then the first specified conditional expression is not raised.

Related commands:

case-split-on-conditionals.

Remarks:

This command can be used to change a conditional expression $\mbox{if}(\theta,\varphi_1,\varphi_2)$ in a sequent's assertion, where $\varphi_1$ and $\varphi_2$ are formulas, to the conditional formula $\mbox{if-form}(\theta,\varphi_1,\varphi_2)$.

Key binding:

r

  
simplify

Script usage:

simplify.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command simplifies the assertion of the given sequent with respect to the context of the sequent. It uses both theory-specific and general logical methods to reduce the sequent to a logically equivalent sequent. The theory-specific methods include algebraic simplification, deciding rational linear inequalities, and applying rewrite rules.

Related commands

:
beta-reduce
simplify-antecedent
simplify-insistently
simplify-with-minor-premises

Remarks:

This is a very powerful command that can be computationally expensive. Computation can often be saved by using the weaker command beta-reduce.

Key binding:

C-c s

  
simplify-antecedent

Script usage:

(simplify-antecedent assumption). assumption can be given as an integer i or a string $\sigma.$

Interactive argument retrieval:

• 0-based index of antecedent-formula: i. If there is only one assumption, this argument request is omitted.

Command kind:

Multi-inference.

Description:

This command is used for simplifying an assumption in the context of the given sequent with respect to this context. It is equivalent to the following sequence of commands: contrapose applied to the given sequent with argument i; simplify applied to the sequent yielded by the previous command; and contrapose applied to the sequent yielded by the previous command with the index of the negated assertion of the original sequent. The commands halts if simplify grounds the first produced sequent.

Related commands:

:
beta-reduce-antecedent
simplify

  
simplify-insistently

Script usage:

simplify-insistently.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command is equivalent to disabling all quasi-constructors and then calling simplify.

Related commands

:
beta-reduce-insistently
insistent-direct-inference
simplify

Remarks:

There is rarely any need to use this command. It has the disagreeable effect of exploding quasi-constructors.

  
simplify-with-minor-premises

Script usage:

simplify-with-minor-premises.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command is the same as simplify except that, instead of failing when convergence requirements are not verified, it posts the unverified convergence requirements as additional subgoals to be proved.

Related commands:

:
beta-reduce-with-minor-premises
simplify

Remarks:

This command is useful for identifying convergence requirements that the simplifier cannot verify.

  
sort-definedness

Script usage:

sort-definedness.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

This command applies to a sequent whose assertion is a definedness statement of the form $(t\downarrow\sigma)$. The command first tests whether the context entails the definedness of t in $\sigma$. If the test fails, the command then tries to reduce the sequent to a set of simpler sequents. In particular, when t is a conditional term if $(\varphi, t_0, t_1)$, it distributes the sort definedness assertion into the consequent and alternative. If t₀ and t₁ are not themselves conditional terms, the new subgoal has the assertion if-form $(\varphi, (t_0\downarrow\sigma), (t_1\downarrow\sigma))$. If one or both of them is a conditional term, then the sort definedness assertion is recursively distributed into the consequents and alternatives.

Related commands:

definedness.

Remarks:

This command is mainly useful when t is an application, a function, or a conditional term.

  
sort-definedness-and-conditionals

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This strategy invokes sort-definedness. Insistent direct inference and repeated beta reduction are then invoked, followed by case-split-on-conditionals, applied to the first conditional term.

Related commands:

sort-definedness.

Remarks:

This command is useful for a goal $(t\downarrow\sigma)$ when the definition of $\sigma$ involves a conditional term.

  
unfold-defined-constants

Script usage:

unfold-defined-constants.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command replaces every occurrence of a defined constant by its respective unfolding. The command beta-reduce-repeatedly is called after all the unfoldings are performed.

Related commands

:
unfold-defined-constants-repeatedly
unfold-directly-defined-constants
unfold-recursively-defined-constants
unfold-single-defined-constant

Key binding:

C-c u

  
unfold-defined-constants-repeatedly

Script usage:

unfold-defined-constants-repeatedly.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command replaces every occurrence of a defined constant by its respective unfolding, repeatedly, until there are no occurrences of defined constants. The command beta-reduce-repeatedly is called after all the unfoldings are performed.

Related commands

:
unfold-defined-constants
unfold-directly-defined-constants-repeatedly
unfold-recursively-defined-constants-repeatedly
unfold-single-defined-constant

Remarks:

If there are occurrences of recursively defined constants, this command can run forever.

  
unfold-directly-defined-constants

Script usage:

unfold-directly-defined-constants.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command replaces every occurrence of a directly defined constant by its respective unfolding. (A directly defined constant is a constant defined nonrecursively.) The command beta-reduce-repeatedly is called after all the unfoldings are performed.

Related commands

:
unfold-defined-constants
unfold-directly-defined-constants-repeatedly
unfold-recursively-defined-constants
unfold-single-defined-constant

  
unfold-directly-defined-constants-repeatedly

Script usage:

unfold-directly-defined-constants-repeatedly.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command replaces every occurrence of a directly defined constant by its respective unfolding, repeatedly, until there are no occurrences of directly defined constants. (A directly defined constant is a constant defined nonrecursively.) The command beta-reduce-repeatedly is called after all the unfoldings are performed.

Related commands

:
unfold-defined-constants-repeatedly
unfold-directly-defined-constants
unfold-recursively-defined-constants-repeatedly
unfold-single-defined-constant

Remarks:

This command will always terminate, unlike
unfold-defined-constants-repeatedly and
unfold-recursively-defined-constants-repeatedly.

  
unfold-recursively-defined-constants

Script usage:

unfold-recursively-defined-constants.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command replaces every occurrence of a recursively defined constant by its respective unfolding. The command beta-reduce-repeatedly is called after all the unfoldings are performed.

Related commands

:
unfold-defined-constants
unfold-directly-defined-constants
unfold-recursively-defined-constants-repeatedly
unfold-single-defined-constant

  
unfold-recursively-defined-constants-repeatedly

Script usage:

unfold-recursively-defined-constants-repeatedly.

Interactive argument retrieval:

None.

Command kind:

Multi-inference.

Description:

This command replaces every occurrence of a recursively defined constant by its respective unfolding, repeatedly, until there are no occurrences of recursively defined constants. The command beta-reduce-repeatedly is called after all the unfoldings are performed.

Related commands

:
unfold-defined-constants-repeatedly
unfold-directly-defined-constants-repeatedly
unfold-recursively-defined-constants
unfold-single-defined-constant

Remarks:

This command may run forever.

  
unfold-single-defined-constant

Script usage:

(unfold-single-defined-constant occurrences constant). occurrences is a list of integers, and constant is denoted by the constant name.

Interactive argument retrieval:

• Constant name: c.
• Occurrences to unfold (0-based): A list l given in the form
  $l_1 \cdots l_n$.

Notice that the order in which arguments are requested is different than the order for script usage.

Command kind:

Multi-inference.

Description:

This command replaces each specified occurrence of the defined constant c by its unfolding e:

Conclusion	$\Gamma \Rightarrow \varphi$
Premise	$\Gamma \Rightarrow \varphi[{e}/{c}]_{l}$

The command beta-reduce-repeatedly is called after all the unfoldings are performed.

Related commands

:
unfold-defined-constants
unfold-defined-constants-repeatedly
unfold-directly-defined-constants
unfold-directly-defined-constants-repeatedly
unfold-recursively-defined-constants
unfold-recursively-defined-constants-repeatedly
unfold-single-defined-constant-globally

Remarks:

The related commands are all elaborations of this command.

Key binding:

u

  
unfold-single-defined-constant-globally

Script usage:

(unfold-single-defined-constant-globally constant).

Interactive argument retrieval:

• Constant name: c.

Command kind:

Multi-inference.

Description:

This command replaces every occurrence of the defined constant c by its unfolding e:

Conclusion	$\Gamma \Rightarrow \varphi$
Premise	$\Gamma \Rightarrow \varphi[{e}/{c}]_{\rm all}$

The command beta-reduce-repeatedly is called after all the unfoldings are performed.

Related commands:

unfold-single-defined-constant.

Key binding:

U

  
unordered-direct-inference

Script usage:

unordered-direct-inference.

Interactive argument retrieval:

None.

Command kind:

Single-inference.

Description:

If the sequent node assertion is a conjunction, this command does a direct inference without strengthening the context.

Conclusion	$\Gamma \Rightarrow \varphi_1 \wedge \cdots \wedge \varphi_n$
Premises $(1\leq i \leq n)$	$\Gamma \Rightarrow \varphi_i$

Related commands:

direct-inference.

  
weaken

Script usage:

(weaken assumption-list). assumption-list can be given as a list of numbers, a list of strings, or an assumption-list form.

Interactive argument retrieval:

• List of formula indices to omit (0-based): A list l given in the form $l_1 \cdots l_n$.

Command Kind:

Single-inference.

Description:

This command removes one or more assumptions you specify from the context of the given sequent.

Conclusion	$\Gamma \cup \Delta \Rightarrow \varphi$
Premise	$\Gamma \Rightarrow \varphi$

Notes:

• The indices of the members of $\Delta$ in the context $\Gamma \cup \Delta$ are given by l.

Remarks:

You might wonder why you would ever want to remove an assumption, but in fact, in many cases this is a natural step to take:

• If an assumption is irrelevant, then removing it will do no harm and will make the job of the simplifier a lot easier,
• It is often the case that sequent nodes are identical except for the addition of ``irrelevant'' assumptions. In this case, removing the irrelevant assumptions allows you to ground both sequents by just grounding one.

Key binding:

w