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).
axiom hypname.
... 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}...}
.
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.3This 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.
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).
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).
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)
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.elim.
by_absurd.
Equivalent to elim absurd. intro.
by_contradiction.
Equivalent to elim contradiction. 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.prove command, but keeps the current goal, only adding
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.
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.
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.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.lock). Recall that instance unlock automatically the existential variable if
necessary.
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}.
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.numth goal becomes the current goal.
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)
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). Proof error: All ready proving. >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)
tactic1 ;; tactic2tactic1 for all goals generated by tactic1.
Try tactictactic 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 ;;.