19. The Primitive Inference Procedures

In this chapter we list and document each of the primitive inference procedures. We will use the following format to describe them.

Parameters.

A list of the arguments (other than the sequent node) required by procedure. These arguments can be of the following types:

• A formula.
• A list of formulas.
• A path represented as a list of nonnegative integers.
• A list of paths.
• A constant.
• A macete.
• Another sequent node (usually referred to as the major premise).

Description.

A brief description of the primitive inference. Some of primitive inference procedures have descriptions which are identical to the description of the corresponding interactive proof command.

  
antecedent-inference

Parameters:

A sequent node assumption.

Description:

The effect of applying this primitive inference procedure is given by the following table.

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$, where $\{\varphi\}$ is the parameter to the primitive inference procedure.
• $\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.

  
backchain-inference

Parameters:

A sequent node assumption.

Description

This primitive inference procedure attempts to use the assumption given as argument 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-inference 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 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.
• 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.

  
backchain-backwards-inference

Parameters:

A sequent node assumption.

Description:

This primitive inference procedure works the same way as backchain, except that subformulas of the assumption of the forms s=t, $s\simeq t$, $s\equiv t$ are used from right to left.

  
backchain-through-formula-inference

Parameters:

A sequent node assumption.

Description:

Similar to backchain, except that it does not backchain through equivalences, i.e., formulas of the form s=t, $s\simeq t$, or $s\equiv t.$

  
choice

Parameters:

None.

Description:

This primitive inference procedure 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)$.

  
contraposition

Parameters:

A sequent node assumption $\varphi.$

Description:

This primitive inference procedure interchanges the given sequent's assertion and the assumption $\varphi.$

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

  
cut

Parameters:

A sequent node to be the major premise.

Description:

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$

Notes:

• The major premise is the sequent $\Gamma \cup \{\psi_1,\ldots,\psi_n\} \Rightarrow \varphi.$

  
definedness

Parameters:

None.

Description:

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

  
defined-constant-unfolding

Parameters:

• A list of paths $(p_1, \ldots, p_n)$ to occurrences of a defined constant c.
• The constant c itself.

Description:

This primitive inference procedure replaces occurrences of the defined constant c at the paths p_i by its unfolding e.

  
direct-inference

Parameters:

None.

Description:

This primitive inference procedure applies an analogue of an introduction rule of Gentzen's sequent calculus (in reverse), based on the lead 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.$

  
disjunction-elimination

Parameters:

A sequent node.

Description:

NO DESCRIPTION.

  
eliminate-iota

Parameters:

A path p to an iota-expression occurrence in the assertion.

Description:

This primitive inference procedure 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.''

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 expression located at the path p in $\psi$.
• $\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.

  
existential-generalization

Parameters:

A sequent node $\Gamma \Rightarrow \varphi$.

Description:

This primitive inference procedure proves an existential assertion by exhibiting witnesses.

Conclusion	$\Gamma \Rightarrow \exists x_1\mbox{:}\sigma_1, \dots ,x_n \mbox{:}\sigma_n, \varphi$
Premise	$\Gamma \Rightarrow \varphi$

Notes:

• The command will fail unless the parameter sequent node is of the form $\Gamma \Rightarrow \varphi.$

  
extensionality

Parameters:

None.

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 primitive inference 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.

  
force-substitution

Parameters:

• Paths. A list of paths $p_1, \ldots , p_n.$
• Replacements. A list of expressions $r_1, \ldots , r_n.$

Description:

This primitive inference procedure changes part of the sequent assertion. It yields two or more new subgoals. One subgoal is obtained from the original sequent assertion by replacing the subexpression e_i at the path p_i with r_i. The other subgoals assert that the replacements are sound.

Conclusion	$\Gamma \Rightarrow \varphi$
Major Premise	$\Gamma \Rightarrow \varphi[r_i/e_i]$
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 path p_i.
• $\varphi_i$ is:
  • $e_i \equiv r_i$ if e_i is a formula and the parity of the path p_i is 0.
  • $r_i \supset e_i$ if e_i is a formula and the parity of the path p_i is 1.
  • $e_i \supset r_i$ if e_i is a formula and the parity of the path p_i is -1.
  • $e_i \simeq r_i$ in all other cases.

  
incorporate-antecedent

Parameters:

A sequent node assumption $\varphi.$

Description:

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

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

  
insistent-direct-inference

Parameters:

None.

Description:

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

  
insistent-simplification

Parameters:

None.

Description:

This primitive inference procedure is equivalent to disabling all quasi-constructors and then calling simplification.

  
macete-application-at-paths

Parameters:

• A list of paths $(p_1, \ldots, p_n).$
• A macete.

Description:

This primitive inference procedure applies the argument macete to the sequent node assertion at those occurrences specified by the paths $p_1, \ldots, p_n$.

  
macete-application-with-minor-premises-at-paths

Parameters:

• A list of paths $(p_1, \ldots, p_n).$
• A macete

Description:

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

  
raise-conditional-inference

Parameters:

A list of paths $(p_1, \ldots, p_n)$ to conditional subexpressions.

Description:

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

For the moment, let us assume that n=1. Suppose the conditional expression in $\varphi$ located at p₁ 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 primitive inference procedure 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 primitive inference procedure fails.

Now assume n > 1. The primitive inference procedure 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.

  
simplification

Parameters:

None.

Description:

This primitive inference procedure 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.

  
simplification-with-minor-premises

Parameters:

None.

Description:

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

  
sort-definedness

Parameters:

None.

Description:

This primitive inference procedure applies to a sequent whose assertion is a definedness statement of the form $(t\downarrow\sigma)$. The primitive inference procedure first tests whether the context entails the definedness of t in $\sigma$. If the test fails, the primitive inference procedure 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.

  
theorem-assumption

Parameters:

A formula which must be a theorem of the context theory.

Description:

This primitive inference procedure adds the argument theorem to the context of the given sequent.

  
universal-instantiation

Parameters:

A sequent node $\Gamma \Rightarrow \forall x_1\mbox{:}\sigma_1, \dots ,x_n \mbox{:}\sigma_n, \varphi$.

Description:

This primitive inference procedure proves a formula by proving a universal.

Conclusion	$\Gamma \Rightarrow \varphi$
Premise	$\Gamma \Rightarrow \forall x_1\mbox{:}\sigma_1, \dots ,x_n \mbox{:}\sigma_n, \varphi$

Notes:

• The command will fail unless the parameter sequent node is of the form $\Gamma \Rightarrow \forall x_1\mbox{:}\sigma_1, \dots ,x_n \mbox{:}\sigma_n, \varphi.$

  
unordered-conjunction-direct-inference

Parameters:

None.

Description:

If the sequent node assertion is a conjunction, this primitive inference procedure 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$

  
weakening

Parameters:

A set of formulas $\Delta.$

Description:

This primitive inference procedure removes one or more assumptions you specify from the context of the given sequent.

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