next up previous contents
Next: 19. The Primitive Inference Up: 3. Reference Manual Previous: 17. The IMPS Special

Subsections

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:

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:
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:

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:

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

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:

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:

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:

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:

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:

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+y2 | = | y2+x |, then applying the macete commutative-law-for-addition to the 0-th occurrence of x+y2 yields a new sequent with assertion |y2+x | = | y2+x |. If the macete had been applied globally, the resulting assertion would have been |y2+x | = | x+y2|.

  
apply-macete-locally-with-minor-premises

Script usage:

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

Interactive argument retrieval:

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:

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:

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:

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:

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:

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:

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:

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:

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 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:

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:

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:

  
case-split-on-conditionals

Script usage:

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

Interactive argument retrieval:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

Remarks:

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

\begin{displaymath}\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) .\end{displaymath}

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:

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:

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:

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:

  
incorporate-antecedent

Script usage:

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

Interactive argument retrieval:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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:

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 l1-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

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

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:

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:

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 t0 and t1 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:

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:

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:

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:

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:

Key binding:

w
next up previous contents
Next: 19. The Primitive Inference Up: 3. Reference Manual Previous: 17. The IMPS Special
System Administrator
2000-07-23