Next: Flags index. Up: Commands. Previous: Top-level commands.   Contents

Subsections

# Proof commands.

The command described in this section are available only after starting a new proof using the goal command. Moreover, except save and undo they can't be use after you finished the proof (when the message proved has been printed).

## Basic proof commands.

All proof commands are complex commands, using unification and equational rewriting. The following ones are extensions of the basic commands of natural deduction, but much more powerful.
axiom hypname.
Tries to prove the current goal by identifying it with hypothesis hypname, using unification and equational reasoning.

```...
G := X (?1 + N0)
|- X (N0 + ?2)
%PhoX% axiom G.
0 goal created.
proved
%
```

```...
H := N x
H0 := N y
H1 := X (x + S N0)
|- X (S x)
%PhoX% axiom H1.
0 goal created.
proved
```

elim {num0} expr0 { with opt1 {and/then ... {and/then optn}...} .
A.2]

This command corresponds to the following usual tool in natural proof : prove the current goal by applying hypothesis or theorem expr0. More formally this command tries to prove the current goal by applying some elimination rules on the formula or theorem expr0 (modulo unification and equational reasoning). Elimination rules are built in as the ordinary ones for forall quantifier and implication. For other symbols, elimination rules can be defined with the new_elim) commands.

After this tactic succeeds, all the new goals (Hypothesis of expr0 adapted to this particular case) are printed, the first one becoming the new current goal.

```New goal is:
goal 1/1
H := N x
H0 := N y
H1 := N z
|- x + y + z = (x + y) + z

%PhoX% elim H.  (* the default elimination rule for predicate N
is induction *)
2 goals created.

New goals are:
goal 1/2
H := N x
H0 := N y
H1 := N z
|- N0 + y + z = (N0 + y) + z

goal 2/2
H := N x
H0 := N y
H1 := N z
H2 := N y0
H3 := y0 + y + z = (y0 + y) + z
|- S y0 + y + z = (S y0 + y) + z
```

The following example use equational rewriting :

```H := N x
H0 := N y
H1 := N z
|- x + y + z = (x + y) + z

%PhoX% elim equal.reflexive.
(* associativity equations are in library nat *)
0 goal created.
```

You have the option to give some more informations opti, that can be expressions (individual terms or propositions), or abbreviated name of elimination rules.

Expressions has to be given between parenthesis if they are not variables. They indicate that a for-all quantifier (individual term) or an implication (proposition) occuring (strictly positively) in expr0 has to be eliminated with this expression. In case there is only one such option, the first usable occurence form left to right is used (regardless the goal).

```def lInfix[5] R "Transitive" =
/\x,y,z ( R x y -> R y z -> R x z).
...

H := R Transitive
H0 := R a b
H1 := R b c
|- R a c
%PhoX% elim H with H0.
1 goal created, with 1 automatically solved.
```

but

```H := R Transitive
H0 := R a b
H1 := R b c
|- R a c

%PhoX% elim H with H1.
Error: Proof error: Tactic elim failed.
```

You can pass several options separated by and or then. In case opti is introduced by an and, the tactic search the first unused occurrence in expr0 of forall quantifier, implication or connective usable with opti.

```H := R Transitive
H0 := R a b
H1 := R b c
|- R a c

%PhoX% elim H with a and b and c.
0 goal created.
```

to skip a variable or hypothesis you can use unification variables (think that ? match any variable or hypothesis) :

```H := R Transitive
H0 := R a b
H1 := R b c
|- R a c

%PhoX% elim H with ? and b.  (* ? will match a *)
0 goal created.
```

In case opti is introduced by a then : ... opti then opti' ..., the tactic search the first unused occurrence of forall quantifier, implication or connective usable with opti' after the occurrence used for opti.

```H := R Transitive
H0 := R a b
H1 := R b c
|- R a c

%PhoX% elim H with H0 and a.
0 goal created.
```

but

```H := R Transitive
H0 := R a b
H1 := R b c
|- R a c

%PhoX% elim H with H0 then a.
Error: Proof error: Tactic elim failed.
```

Abbreviated name of elimination rules have to be given between square brackets. The tactic try to uses this elimination rule for the first connective in expr0 using it.

```H := N x
|- x = N0 or \/y:N  x = S y

%PhoX% elim H with [case].
2 goals created.

New goals are:
goal 1/2
H := N x
H0 := x = N0
|- N0 = N0 or \/y:N  N0 = S y

goal 2/2
H := N x
H0 := N y
H1 := x = S y
|- S y = N0 or \/y0:N  S y = S y0
```

You can use abbreviated names and expression, and and then together. All occurrences matched after a then opti have to be after the one matched by opti. The and matches the first unused occurrence with respect to the previous constraint on a possible then placed before.

```H := /\x:N  ((x = N0 -> C) & ((x = N1 -> C) & (x = N2 -> C)))
|- C

%PhoX% elim H with N1 and [r] then [l].
2 goals created.

New goals are:
goal 1/2
H := /\x:N  ((x = N0 -> C) & ((x = N1 -> C) & (x = N2 -> C)))
|- N N1

goal 2/2
H := /\x:N  ((x = N0 -> C) & ((x = N1 -> C) & (x = N2 -> C)))
|- N1 = N1
```

The first option num0 is not very used. It allows to precise the number of elimination rules to apply.

elim {num0} {-num1 opt1} ... {-numn optn} expr0.A.3

This syntax is now deprecated but still used in libraries and examples. Use the syntax above!

Tries to prove the current goal by applying some elimination rules on the formula or theorem expr0. You have the option to precise a minimum number of elimination rules (num0) or/and give some information opti to help in finding the numi-th elimination.

• If the numi-th elimination acts on a for-all quantifier, opti must be an expression which can be substituted to this variable (this expression has to be given between parenthesis if it is not a variable).
• If the numi-th elimination acts on an implication, opti must be an expression which can be unified with the left formula in the implication (this expression has to be given between parenthesis if it is not a variable).
• If the numi-th elimination acts on a connective for which you introduced new elimination rules (using new_elim), opti has to be the abbreviated name of one of these rules, between square bracket.

Moreover, this tactic expands the definition of a symbol if and only if this symbol has no elimination rules.

After this tactic succeeded, all the new goals are printed, the last one to be printed is the new current goal.

```>phox> goal /\x/\y/\z (N x -> N y -> N z ->
x + (y + z) = (x + y) + z).

|- /\ x /\ y /\ z (N x -> N y -> N z ->
x + y + z = (x + y) + z)
>phox> intro 6.

H := N x
H0 := N y
H1 := N z
|- x + y + z = (x + y) + z
>phox> elim -4 x nat_rec.

H := N x
H0 := N y
H1 := N z
|- /\ y0 (N y0 -> y0 + y + z = (y0 + y) + z ->
S y0 + y + z = (S y0 + y) + z)

H := N x
H0 := N y
H1 := N z
|- O + y + z = (O + y) + z

>phox> elim equal_refl.

H := N x
H0 := N y
H1 := N z
|- /\ y0 (N y0 -> y0 + y + z = (y0 + y) + z ->
S y0 + y + z = (S y0 + y) + z)
```

intro num. or intro name1 .... nameN.

In the first form, apply num introduction rules on the goal formula. New names are automatically generated for hypothesis and universal variables. In this form, the intro command only uses the last intro rule specified for a given connective by the new_intro command.

In the second form, for each name an intro rule is applied on the goal formula. If the outermost connective is an implication, the name is used as a new name for the hypothesis. If it is an universal quantification, the name is used for the new variable. If it is a connective with introduction rules defined by the new_intro command, name should be the name of one of these rules and this rule will be applied. Moreover, this tactic expands definition of a symbol if and only if this symbol has no introduction rules.

```>phox> goal /\x /\y (N x -> N y -> N (x + y)).

|- /\ x /\ y (N x -> N y -> N (x + y))
>phox> intro 7.

H := N x
H0 := N y
H1 := X O
H2 := /\ y0 (X y0 -> X (S y0))
|- X (x + y)
>phox> abort.
>phox> goal /\X /\Y (X & Y -> X or Y).

|- /\ X /\ Y (X & Y -> X or Y)
>phox>  intro A B H l.

H := A & B
|- A
```

intros {symbol_list}.

Apply as many introductions as possible without expanding a definition. If a symbol_list is given only rules for these symbols are applied and only defined symbols in this list are expanded. If no list is given, Definitions are expanded until the head is a symbol with some introduction rules and then only those rules will be applied and those definition will be expanded (if this head symbol is an implication or a universal quantification, introduction rules for both implication and universal quantification will be applied, as showed by the following example).

```>phox> goal /\x /\y (N x -> N y -> N (x + y)).

|- /\ x,y (N x -> N y -> N (x + y))
>phox> intros.

H0 := N y
H := N x
|- N (x + y)
```

## More proof commands.

apply { with opt1 {and/then ... { and/then optn}...} .

Equivalent to use ?. elim ... . Usage is similar to elim (see this entry above for details). The command apply adds to the current goal a new hypothesis obtained by applying expr0 (an hypothesis or a theorem) to one or many hypothesis of the current goal. as for elim, if there are unproved hypothesis of expr0 they are added as new goals. The difference with elim, is that apply has not to prove the current goal.

```H0 := /\a0,b (R a0 b -> R b a0)
H1 := /\x \/y R x y
H := /\a0,b,c (R a0 b -> R b c -> R a0 c)
|- R a a

%PhoX% apply H1 with a.

...
G := \/y R a y
|- R a a

%PhoX% left G.
...
H2 := R a y
|- R a a

%PhoX% apply H0 with H2.
...
G := R y a
|- R a a

[%PhoX% elim H with ? and y and ?. (* concludes *)]
[%Phox% elim H with H2 and G. (* concludes *)]
[%Phox% apply H with H2 and G. (* concludes if auto_lvl=1. *)]

%Phox% apply H with a and y and a. (* does not conclude. *)
...
G0 := R a y -> R y a -> R a a
|- R a a
...
```

apply {num0} {-num1 opt1} ... {-numn optn} expr0.
Old syntax for apply, don't use it ! See elim.

by_absurd.

Equivalent to elim absurd. intro.

from expr.

Try to unify expr (which can be a formula or a theorem) with the current goal. If it succeeds, expr replace the current goal.

```>phox> goal /\x/\y/\z (N x -> N y -> N z ->
x + (y + z) = (x + y) + z).

|- /\ x /\ y /\ z (N x -> N y -> N z ->
x + y + z = (x + y) + z)
>phox> intro 6.
....

....

H := N x
H0 := N y
H1 := N z
H2 := N y0
H3 := y0 + y + z = (y0 + y) + z
|- S y0 + y + z = (S y0 + y) + z
>phox> from S (y0 + y + z) = S (y0 + y) + z.

H := N x
H0 := N y
H1 := N z
H2 := N y0
H3 := y0 + y + z = (y0 + y) + z
|- S (y0 + y + z) = S (y0 + y) + z
>phox> from S (y0 + y + z) = S ((y0 + y) + z).

H := N x
H0 := N y
H1 := N z
H2 := N y0
H3 := y0 + y + z = (y0 + y) + z
|- S (y0 + y + z) = S ((y0 + y) + z)
>phox> trivial.
proved
```

left hypname {num | ident_list}.

An elimination rule whose conclusion can be any formula is called a left rule. The left command applies left rules to the hypothesis of name hypname. If an integer num is given, then num left rule are applied. If a list of identifier is given, they are used when the left rule needs to generate new names (like the standard left rule for the existential quantifier) or when there is a choice of left rules, in this case you give the abbreviated name of the rule (see intro).

```>phox> goal /\X,Y (\/x (X x or Y) -> Y or \/x X x).

|- /\X /\Y (\/x (X x or Y) -> Y or \/x X x)

%phox% intros.
1 goal created.
New goal is:

H := \/x (X x or Y)
|- Y or \/x X x

%phox% left H z.
1 goal created.
New goal is:

H0 := X z or Y
|- Y or \/x X x

%phox% left H0.
2 goals created.
New goals are:

H1 := X z
|- Y or \/x X x

H1 := Y
|- Y or \/x X x

%phox% trivial.
0 goal created.
Current goal now is:

H1 := X z
|- Y or \/x X x

%phox% trivial.
0 goal created.
proved
```

lefts hypname {symbol_list}.

Applies ``many'' left rules on the hypothesis of name hypname. If a symbol_list is given only rules for these symbols are applied and only defined symbols in this list are expanded. If no list is given, Definitions are expanded until the head is a symbol with some left rules and then only those rules will be applied and those definitions will be expanded.

```>phox> goal /\X,Y (\/x (X x or Y) -> Y or \/x X x).

|- /\X /\Y (\/x (X x or Y) -> Y or \/x X x)

%phox% intros.
1 goal created.
New goal is:

H := \/x (X x or Y)
|- Y or \/x X x

%phox% lefts H \$\/ \$or.
2 goals created.
New goals are:

H1 := X x
|- Y or \/x0 X x0

H1 := Y
|- Y or \/x0 X x0

%phox% trivial.
0 goal created.
Current goal now is:

H1 := X x
|- Y or \/x0 X x0

%phox% trivial.
0 goal created.
proved
```

```...
H := N x
H0 := N y
H1 := N y0
H2 := S y0 <= S y
|- S y0 <= y or S y0 = S y
%PhoX% print lesseq.S_inj.N.
lesseq.S_inj.N = /\x0,y1:N  (S x0 <= S y1 -> x0 <= y1) : theorem
%PhoX% apply -5 H2 lesseq.S_inj.N.
3 goals created, with 2 automatically solved.

New goal is:
H := N x
H0 := N y
H1 := N y0
H2 := S y0 <= S y
G := y0 <= y
|- S y0 <= y or S y0 = S y
```

Another example (in combination with rmh) :

```...
H := List D0 l
H0 := D0 a
H1 := List D0 l'
H2 := /\n0:N  (n0 <= length l' -> List D0 (nthl l' n0))
H4 := N y
G := y <= length l'
|- List D0 (nthl (a :: l') (S y))

%PhoX% apply -3 G H2 ;; rmh H2.
2 goals created, with 1 automatically solved.
New goal is:

H := List D0 l
H0 := D0 a
H1 := List D0 l'
H4 := N y
G := y <= length l'
G0 := List D0 (nthl l' y)
|- List D0 (nthl (a :: l') (S y))
```

prove expr.

Adds expr to the current hypothesis and adds a new goal with expr as conclusion, keeping the hypothesis of the current goal (cut rule). expr may be a theorem, then no new goal is created. The current goal becomes the new statment.

```>phox> goal /\x1/\y1/\x2/\y2 (pair x1 y1 = pair x2 y2
-> x1 = x2 or y1 = x2).

|- /\ x1 /\ y1 /\ x2 /\ y2 (pair x1 y1 = pair x2 y2
-> x1 = x2 or y1 = x2)
>phox> intro 5.

H := pair x1 y1 = pair x2 y2
|- x1 = x2 or y1 = x2
>phox> prove pair x2 y2 = pair x1 y1.

H := pair x1 y1 = pair x2 y2
G := pair x2 y2 = pair x1 y1
|- x1 = x2 or y1 = x2

H := pair x1 y1 = pair x2 y2
|- pair x2 y2 = pair x1 y1
```

use expr.
Same as prove command, but keeps the current goal, only adding
ttexpr to hypothesis.

## Automatic proving.

Almost all proof commands use some kind of automatic proving. The following ones try to prove the formula with no indications on the rules to apply.

auto ...

Tries trivial with bigger and bigger value for the depth limit. It only stops when it succeed or when not enough memory is available. This command uses the same option as trivial does.

trivial {num} {-|= name1 ... namen} {+ theo1 ... theop}.A.4

Try a simple trivial tactic to prove the current goal. The option num give a limit to the number of elimination performed by the search. Each elimination cost (1 + number of created goals).

The option {- name1 ... namen} tells trivial not to use the hypothesis name1 ... namen. The option {= name1 ... namen} tells trivial to only use the hypothesis name1 ... namen. The option + theo1 ... theop tells trivial to use the given theorem.

```>phox> goal /\x/\y (y E pair x y).

|- /\x/\y (y E pair x y)
>phox> trivial + pair_ax.
proved.
```

## Rewriting.

rewrite {-l lim | -p pos} {{-r|-nc} eqn1} {{-r|-nc} eqn2} ...

If eqn1, eqn2, ... are equations (or conditional equations) or list of equations (defined using def_thlist), the current goal is rewritten using these equations as long as possible. For each equation, the option -r indicates to use it from right to left (the default is left to right) and the option -nc forces the system not to try to prove automatically the conditions necessary to apply the equation (the default is to try).

```...
H0 := N y
H1 := N z
H2 := N y0
H3 := y0 * (y + z) = y0 * y + y0 * z
|- S y0 * (y + z) = S y0 * y + S y0 * z

%PhoX% print mul.lS.N.
mul.lS.N = /\x0,y1:N  S x0 * y1 = y1 + x0 * y1 : theorem
%PhoX% rewrite mul.lS.N.
1 goal created.
New goal is:

H0 := N y
H1 := N z
H2 := N y0
H3 := y0 * (y + z) = y0 * y + y0 * z
|- (y + z) + y0 * (y + z) = (y + y0 * y) + z + y0 * z

%PhoX% rewrite H3.
1 goal created.
New goal is:

H0 := N y
H1 := N z
H2 := N y0
H3 := y0 * (y + z) = y0 * y + y0 * z
|- (y + z) + y0 * y + y0 * z = (y + y0 * y) + z + y0 * z
...
```

If sym1, sym2, are defined symbol, their definition will be expanded. Do not use rewrite just for expansion of definitions, use unfold instead.

Note: by default, rewrite will unfold a definition if and only if it is needed to do rewriting, while unfold will not (this mean you can use unfold to do rewriting if you do not want to perform rewriting under some definitions).

The global option -l lim limits to lim steps of rewriting. The option -p pos indicates to perform only one rewrite step at the pos-th possible occurrence (occurrences are numbered from 0). These options allows to use for instance commutativity equations.

```...
H := N x
H0 := N y
H1 := N z
|- (y + z) * x = y * x + z * x

%PhoX% rewrite -p 0 mul.commutative.N.
1 goal created.
New goal is:

H := N x
H0 := N y
H1 := N z
|- x * (y + z) = y * x + z * x

%PhoX% rewrite -p 1 mul.commutative.N.
1 goal created.
New goal is:

H := N x
H0 := N y
H1 := N z
|- x * (y + z) = x * y + z * x
...
```

rewrite_hyp hyp_name ...

Similar to rewrite except that it rewrites the hypothesis named hyp_name. The dots (...) stands for the rewrite arguments.

unfold ...

A synonymous to rewrite, use it when you only do expansion of definitions.

unfold_hyp hyp_name ...

A synonymous to rewrite_hyp, use it when you only do expansion of definitions.

## Managing existential variables.

Existential variables are usually designed in phox by ?x where x is a natural number. They are introduced for instance by applying an intro command to an existential formula, or sometimes by applying an elim H command where H is an universal formula.

You can use existential variables in goals, for instance :

```>PhoX> goal N3^N2=?1.

Goals left to prove:

|- N3 ^ N2 = ?1

%PhoX% rewrite calcul.N.
1 goal created.
New goal is:

Goals left to prove:

|- S S S S S S S S S N0 = ?1

%PhoX% intro.
0 goal created.
proved
%PhoX% save essai.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
essai = N3 ^ N2 = S S S S S S S S S N0 : theorem
```

constraints.

Print the constraints which should be fulfilled by unification variables.

```>phox> goal /\X (/\x\/y X x y -> \/y/\x X x y).

|- /\ X (/\ x \/ y X x y -> \/ y /\ x X x y)
%phox% intro 4.

H := /\ x0 \/ y X x0 y
|- X x ?32
%phox% constraints.
Unification variable ?32 should not use x
```

instance expr0 expr1.
:

Unify expr0 and expr1. This is useful to instantiate some unification variables. expr0 must be a variable or an expression between parenthesis.

```H := N x
H0 := N y
H3 := y = N2 * X + N1
|- S y = N2 * ?792
>phox> instance ?792 S X.

H := N x
H0 := N y
H3 := y = N2 * X + N1
|- S y = N2 * S X
```

lock var.
: This command locks the existential variable (or meta-variable, or unification variable) var for unification. That is for all succeeding commands var is seen as a constant, except the command instance that makes the existential variable disappear, and the command unlock that explicitely unlocks the existential variable. When introduced in a proof, it is possible that you still donnot know the value to replace an existential variable by. As there is no more general unifier in presence of high order logic and equational reasoning, somme commands could instanciate an unlocked existential variable in an unexpected way.

For instance in the following case :

```%PhoX% local y = x - k.
...
%PhoX% prove N y.
2 goals created.
New goals are:

Goals left to prove:

H := N k
H0 := N n
G := N ?1
H1 := N x
H2 := x >= ?1
G0 := k <= ?1
|- N y
...
%PhoX% trivial.
```

if ?1 is not locked, ?1 will be instanciated by y, which is not the expected behaviour.

unlock var.
: This command unlocks the existential variable (or existential variable) var for unification, in case this variable is locked (see above lock). Recall that instance unlock automatically the existential variable if necessary.

## Managing goals.

goals.

Prints all the remaining goals, the current goal being the last to be printed, being the first with option -pg used for Proof General (cf next for an example).

after {em num}.
Change the current goal. If no num is given then the current goal become the last goal. If num is given, then the current goal is sent after the numth.

next {em num}.

Change the current goal. If no num is given then the current goal becomes the last goal. If a positive num is given, then the current goal becomes the numth (the 0th being the current goal). If a negative num is given, the numth goal become the current one (next -4 is the ``inverse'' command of next 4).

```>phox> goals.

H := N x
H0 := N y
H1 := N z
|- /\ y0 (N y0 -> y0 + y + z = (y0 + y) + z ->
S y0 + y + z = (S y0 + y) + z)

H := N x
H0 := N y
H1 := N z
|- /\ y0 (N y0 -> O + y0 + z = y0 + z ->
O + S y0 + z = S y0 + z)

H := N x
H0 := N y
H1 := N z
|- O + O + z = O + z
>phox> next.

H := N x
H0 := N y
H1 := N z
|- /\ y0 (N y0 -> O + y0 + z = y0 + z ->
O + S y0 + z = S y0 + z)
...
```

select num.
The numth goal becomes the current goal.

## Managing context.

local .....

The same syntax as the def command but to define symbols local to the current proof (see the def (section A.1.2) command for the syntax).

rename oldname newname.

Rename a constant or an hypothesis local to this goal (can not be used to rename local definitions).

rmh name1 ... namen.

Deletes the hypothesis name1, ...,namen from the current goal.

```>phox>  goal /\X /\Y (Y -> X -> X).

|- /\ X /\ Y (Y -> X -> X)
>phox> intro 3.

H := Y
|- X -> X
>phox> rmh H.

|- X -> X
```

slh name1 ... namen.

Keeps only the hypothesis name1, ...,namen in the current goal.

```>phox> goal /\x,y : N N (x + y).

|- /\ x,y : N N (x + y)
>phox> intros.

H0 := N y
H := N x
|- N (x + y)
>phox> slh H.

H := N x
|- N (x + y)
```

## Managing state of the proof.

abort.

Abort the current proof, so you can start another one !

```>phox> goal /\X /\Y (X -> Y).

|- /\ X /\ Y (X -> Y)
>phox> intro 3.

H := H
|- Y
>phox> goal /\X (X -> X).
>phox> abort.
>phox> goal /\X (X -> X).

|- /\ X (X -> X)
```

{Local} save {name}.

When a proof is finished (the message proved has been printed), save the new theorem with the given name in the data base. Note: the proof is verified at this step, if an error occurs, please report the bug !

You do not have to give the name if the proof was started with the theorem command or a similar one instead of goal : the name from the declaration of theorem is choosen.

The prefix Local tells that this theorem should not be exported. This means that if you use the Import or Use command, only the exported theorems will be added.

```>phox>  goal /\x (N x -> N S x).

|- /\ x (N x -> N (S x))
>phox> trivial.
proved
>phox> save succ_total.
Building proof .... Done.
Typing proof .... Done.
Verifying proof .... Done.
```

undo {num}.

Undo the last action (or the last num actions).

```>phox> goal /\X (X -> X).

|- /\ X (X -> X)
>phox> intro.

|- X -> X
>phox> undo.

|- /\ X (X -> X)
```

## Tacticals.

This feature is new and has limitations.

tactic1 ;; tactic2
Use tactic1 for all goals generated by tactic1.

Try tactic
If tactic is successful, Try tactic is the same as tactic. If tactic fails, Try tactic succeeds and does not modify the current goal. This is useful after a ;;.

Next: Flags index. Up: Commands. Previous: Top-level commands.   Contents
Christophe Raffalli 2005-03-02