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).
... 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
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.
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.
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)
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
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)
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 ...
Equivalent to elim absurd. intro.
Equivalent to elim contradiction. intro.
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
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
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))
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
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.
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.
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.
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 ...
Similar to rewrite except that it rewrites the hypothesis named hyp_name. The dots (...) stands for the rewrite arguments.
A synonymous to rewrite, use it when you only do expansion of definitions.
A synonymous to rewrite_hyp, use it when you only do expansion of definitions.
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
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
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
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.
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).
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) ...
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 a constant or an hypothesis local to this goal (can not be used to rename local definitions).
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
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)
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). Proof error: All ready proving. >phox> abort. >phox> goal /\X (X -> X). |- /\ X (X -> X)
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 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)