X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=812c8ed970a2044472bcfd78653955ce29654fb0;hb=5381c04b3298d905239dd0cb0550025a674b433a;hp=2c1afb0cfc8ebbe9b5b0a036ae10affb22760621;hpb=dba1193e19fc88a1e71ab548efc867aae8d150da;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 2c1afb0cf..812c8ed97 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -1,41 +1,62 @@
-
- Tactics
+
+ Tactics
-
- absurd <term>
- absurd P
+
+ Quick reference card
+ &tacticref;
+
+
+
+
+ absurd
+ absurd
+ absurd P
+
+
+
+ Synopsis:
+
+ absurd &sterm;
+
+ Pre-conditions:P must have type Prop.
- Action:
- it closes the current sequent by eliminating an
+ It closes the current sequent by eliminating an
absurd term.New sequents to prove:
- it opens two new sequents of conclusion P
+ It opens two new sequents of conclusion P
and ¬P.
-
-
-
- apply <term>
+
+
+
+ apply
+ applyapply t
+
+ Synopsis:
+
+ apply &sterm;
+
+ Pre-conditions:
@@ -49,13 +70,68 @@
Action:
- it closes the current sequent by applying t to n implicit arguments (that become new sequents).
+ It closes the current sequent by applying t to n implicit arguments (that become new sequents).
+
+
+
+ New sequents to prove:
+
+ It opens a new sequent for each premise
+ Ti that is not
+ instantiated by unification. Ti is
+ the conclusion of the i-th new sequent to
+ prove.
+
+
+
+
+
+
+ applyS
+ applyS
+ applyS t auto_params
+
+
+
+ Synopsis:
+
+ applyS &sterm; &autoparams;
+
+
+
+ Pre-conditions:
+
+ t must have type
+ T1 â ... â
+ Tn â G.
+
+
+
+ Action:
+
+ applyS is useful when
+ apply fails because the current goal
+ and the conclusion of the applied theorems are extensionally
+ equivalent up to instantiation of metavariables, but cannot
+ be unified. E.g. the goal is P(n*O+m) and
+ the theorem to be applied proves âm.P(m+O).
+
+
+ It tries to automatically rewrite the current goal using
+ auto paramodulation
+ to make it unifiable with G.
+ Then it closes the current sequent by applying
+ t to n
+ implicit arguments (that become new sequents).
+ The auto_params parameters are passed
+ directly to auto paramodulation.
+ New sequents to prove:
- it opens a new sequent for each premise
+ It opens a new sequent for each premise
Ti that is not
instantiated by unification. Ti is
the conclusion of the i-th new sequent to
@@ -64,54 +140,70 @@
-
-
+
+ assumption
- assumption
+ assumption
+ assumption
+
+ Synopsis:
+
+ assumption
+
+ Pre-conditions:
- there must exist an hypothesis whose type can be unified with
+ There must exist an hypothesis whose type can be unified with
the conclusion of the current sequent.Action:
- it closes the current sequent exploiting an hypothesis.
+ It closes the current sequent exploiting an hypothesis.New sequents to prove:
- none
+ None
-
-
- auto [depth=<int>] [width=<int>] [paramodulation] [full]
- auto depth=d width=w paramodulation full
+
+
+ auto
+ auto
+ auto params
+
+ Synopsis:
+
+ auto &autoparams;.
+ autobatch &autoparams;
+
+ Pre-conditions:
- none, but the tactic may fail finding a proof if every
+ None, but the tactic may fail finding a proof if every
proof is in the search space that is pruned away. Pruning is
- controlled by d and w.
+ controlled by the optional params.
Moreover, only lemmas whose type signature is a subset of the
signature of the current sequent are considered. The signature of
- a sequent is ...TODO
+ a sequent is essentially the set of constats appearing in it.
+ Action:
- it closes the current sequent by repeated application of
+ It closes the current sequent by repeated application of
rewriting steps (unless paramodulation is
omitted), hypothesis and lemmas in the library.
@@ -119,45 +211,118 @@
New sequents to prove:
- none
+ None
-
-
- clear <id>
- clear H
+
+
+ cases
+ cases
+
+ cases t hyps
+
+
+ Synopsis:
+
+
+ cases
+ &term; [([&id;]â¦)]
+
+
+ Pre-conditions:
- H must be an hypothesis of the
- current sequent to prove.
+
+ t must inhabit an inductive type
+
+
+
+
+ Action:
+
+
+ It proceed by cases on t. The new generated
+ hypothesis in each branch are named according to
+ hyps.
+
+
+
+
+ New sequents to prove:
+
+ One new sequent for each constructor of the type of
+ t. Each sequent has a new hypothesis for
+ each argument of the constructor.
+
+
+
+
+
+
+ clear
+ clear
+
+ clear H1 ... Hm
+
+
+
+
+ Synopsis:
+
+
+ clear
+ &id; [&id;â¦]
+
+
+
+
+ Pre-conditions:
+
+
+
+ H1 ... Hm
+ must be hypotheses of the
+ current sequent to prove.
+ Action:
- it hides the hypothesis H from the
- current sequent.
+
+ It hides the hypotheses
+
+ H1 ... Hm
+ from the current sequent.
+ New sequents to prove:
- none
+ None
-
-
- clearbody <id>
+
+
+ clearbody
+ clearbodyclearbody H
+
+ Synopsis:
+
+ clearbody &id;
+
+ Pre-conditions:
@@ -168,28 +333,87 @@
Action:
- it hides the definiens of a definition in the current
+ It hides the definiens of a definition in the current
sequent context. Thus the definition becomes an hypothesis.New sequents to prove:
- none.
+ None.
+
+
+
+
+
+
+ compose
+ compose
+ compose n t1 with t2 hyps
+
+
+
+ Synopsis:
+
+ compose [&nat;] &sterm; [with &sterm;] [&intros-spec;]
+
+
+
+ Pre-conditions:
+
+
+
+
+
+ Action:
+
+ Composes t1 with t2 in every possible way
+ n times introducing generated terms
+ as if intros hyps was issued.
+ If t1:âx:A.B[x] and
+ t2:âx,y:A.B[x]âB[y]âC[x,y] it generates:
+
+
+ λx,y:A.t2 x y (t1 x) : âx,y:A.B[y]âC[x,y]
+
+
+ λx,y:A.λH:B[x].t2 x y H (t1 y) : âx,y:A.B[x]âC[x,y]
+
+
+
+
+ If t2 is omitted it composes
+ t1
+ with every hypothesis that can be introduced.
+ n iterates the process.
+
+
+
+ New sequents to prove:
+
+ The same, but with more hypothesis eventually introduced
+ by the &intros-spec;.
-
-
- change <pattern> with <term>
+
+
+ change
+ changechange patt with t
+
+ Synopsis:
+
+ change &pattern; with &sterm;
+
+ Pre-conditions:
- each subterm matched by the pattern must be convertible
+ Each subterm matched by the pattern must be convertible
with the term t disambiguated in the context
of the matched subterm.
@@ -197,7 +421,7 @@
Action:
- it replaces the subterms of the current sequent matched by
+ It replaces the subterms of the current sequent matched by
patt with the new term t.
For each subterm matched by the pattern, t is
disambiguated in the context of the subterm.
@@ -206,75 +430,97 @@
New sequents to prove:
- none.
+ None.
-
-
- constructor <int>
+
+
+ constructor
+ constructorconstructor n
+
+ Synopsis:
+
+ constructor &nat;
+
+ Pre-conditions:
- the conclusion of the current sequent must be
- an inductive type or the application of an inductive type.
+ The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least n constructors.Action:
- it applies the n-th constructor of the
+ It applies the n-th constructor of the
inductive type of the conclusion of the current sequent.New sequents to prove:
- it opens a new sequent for each premise of the constructor
+ It opens a new sequent for each premise of the constructor
that can not be inferred by unification. For more details,
see the apply tactic.
-
-
+
+ contradiction
- contradiction
+ contradiction
+ contradiction
+
+ Synopsis:
+
+ contradiction
+
+ Pre-conditions:
- there must be in the current context an hypothesis of type
+ There must be in the current context an hypothesis of type
False.Action:
- it closes the current sequent by applying an hypothesis of
+ It closes the current sequent by applying an hypothesis of
type False.New sequents to prove:
- none
+ None
-
-
- cut <term> [as <id>]
+
+
+ cut
+ cutcut P as H
+
+ Synopsis:
+
+ cut &sterm; [as &id;]
+
+ Pre-conditions:
@@ -284,13 +530,13 @@
Action:
- it closes the current sequent.
+ It closes the current sequent.New sequents to prove:
- it opens two new sequents. The first one has an extra
+ It opens two new sequents. The first one has an extra
hypothesis H:P. If H is
omitted, the name of the hypothesis is automatically generated.
The second sequent has conclusion P and
@@ -299,66 +545,142 @@
-
-
- decompose [<ident list>] <ident> [<intros_spec>]
- decompose ???
+
+
+ decompose
+ decompose
+
+ decompose as H1 ... Hm
+
+
+
+
+ Synopsis:
+
+
+ decompose
+ [as &id;â¦]
+
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+
+ For each each premise H of type
+ T in the current context where
+ T is a non-recursive inductive type without
+ right parameters and of sort Prop or CProp, the tactic runs
+
+ elim H as H1 ... Hm
+ , clears H and runs itself
+ recursively on each new premise introduced by
+ elim in the opened sequents.
+
+
+
+
+ New sequents to prove:
+
+
+ The ones generated by all the elim tactics run.
+
+
+
+
+
+
+
+ demodulate
+ demodulate
+ demodulate auto_params
+
+ Synopsis:
+
+ demodulate &autoparams;
+
+ Pre-conditions:
- TODO.
+ None.Action:
- TODO.
+ &TODO;New sequents to prove:
- TODO.
+ None.
-
-
- discriminate <term>
- discriminate p
+
+
+ destruct
+ destruct
+ destruct p
+
+ Synopsis:
+
+ destruct &sterm;
+
+ Pre-conditions:
- p must have type K1 t1 ... tn = K'1 t'1 ... t'm where K and K' must be different constructors of the same inductive type and each argument list can be empty if
-its constructor takes no arguments.
+ p must have type E1 = E2 where the two sides of the equality are possibly applied constructors of an inductive type.Action:
- it closes the current sequent by proving the absurdity of
- p.
+ The tactic recursively compare the two sides of the equality
+ looking for different constructors in corresponding position.
+ If two of them are found, the tactic closes the current sequent
+ by proving the absurdity of p. Otherwise
+ it adds a new hypothesis for each leaf of the formula that
+ states the equality of the subformulae in the corresponding
+ positions on the two sides of the equality.
+ New sequents to prove:
- none.
+ None.
-
-
- elim <term> [using <term>] [<intros_spec>]
+
+
+ elim
+ elimelim t using th hyps
+
+ Synopsis:
+
+ elim &sterm; [using &sterm;] &intros-spec;
+
+ Pre-conditions:
@@ -371,7 +693,7 @@ its constructor takes no arguments.Action:
- it proceeds by cases on the values of t,
+ It proceeds by cases on the values of t,
according to the elimination principle th.
@@ -379,19 +701,29 @@ its constructor takes no arguments.
New sequents to prove:
- it opens one new sequent for each case. The names of
+ It opens one new sequent for each case. The names of
the new hypotheses are picked by hyps, if
- provided.
+ provided. If hyps specifies also a number of hypotheses that
+ is less than the number of new hypotheses for a new sequent,
+ then the exceeding hypothesis will be kept as implications in
+ the conclusion of the sequent.
-
-
- elimType <term> [using <term>]
- elimType T using th
+
+
+ elimType
+ elimType
+ elimType T using th hyps
+
+ Synopsis:
+
+ elimType &sterm; [using &sterm;] &intros-spec;
+
+ Pre-conditions:
@@ -412,78 +744,100 @@ its constructor takes no arguments.
-
-
- exact <term>
+
+
+ exact
+ exactexact p
+
+ Synopsis:
+
+ exact &sterm;
+
+ Pre-conditions:
- the type of p must be convertible
+ The type of p must be convertible
with the conclusion of the current sequent.Action:
- it closes the current sequent using p.
+ It closes the current sequent using p.New sequents to prove:
- none.
+ None.
-
-
+
+ exists
- exists
+ exists
+ exists
+
+ Synopsis:
+
+ exists
+
+ Pre-conditions:
- the conclusion of the current sequent must be
- an inductive type or the application of an inductive type.
+ The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type
+ with at least one constructor.Action:
- equivalent to constructor 1.
+ Equivalent to constructor 1.New sequents to prove:
- it opens a new sequent for each premise of the first
+ It opens a new sequent for each premise of the first
constructor of the inductive type that is the conclusion of the
current sequent. For more details, see the constructor tactic.
-
-
+
+ fail
+ failfail
+
+ Synopsis:
+
+ fail
+
+ Pre-conditions:
- none.
+ None.Action:
- this tactic always fail.
+ This tactic always fail.
@@ -494,111 +848,945 @@ its constructor takes no arguments.
-
-
- fold <reduction_kind> <term> <pattern>
- The tactic fold
-
-
+
+
+ fold
+ fold
+ fold red t patt
+
+
+
+ Synopsis:
+
+ fold &reduction-kind; &sterm; &pattern;
+
+
+
+ Pre-conditions:
+
+ The pattern must not specify the wanted term.
+
+
+
+ Action:
+
+ First of all it locates all the subterms matched by
+ patt. In the context of each matched subterm
+ it disambiguates the term t and reduces it
+ to its red normal form; then it replaces with
+ t every occurrence of the normal form in the
+ matched subterm.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+ fourier
- The tactic fourier
-
-
- fwd <ident> [<ident list>]
- The tactic fwd
-
-
- generalize <pattern> [as <id>]
- The tactic generalize
-
-
+ fourier
+ fourier
+
+
+
+ Synopsis:
+
+ fourier
+
+
+
+ Pre-conditions:
+
+ The conclusion of the current sequent must be a linear
+ inequation over real numbers taken from standard library of
+ Coq. Moreover the inequations in the hypotheses must imply the
+ inequation in the conclusion of the current sequent.
+
+
+
+ Action:
+
+ It closes the current sequent by applying the Fourier method.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ fwd
+ fwd
+ fwd H as H0 ... Hn
+
+
+
+ Synopsis:
+
+ fwd &id; [as &id; [&id;]â¦]
+
+
+
+ Pre-conditions:
+
+
+ The type of H must be the premise of a
+ forward simplification theorem.
+
+
+
+
+ Action:
+
+
+ This tactic is under development.
+ It simplifies the current context by removing
+ H using the following methods:
+ forward application (by lapply) of a suitable
+ simplification theorem, chosen automatically, of which the type
+ of H is a premise,
+ decomposition (by decompose),
+ rewriting (by rewrite).
+ H0 ... Hn
+ are passed to the tactics fwd invokes, as
+ names for the premise they introduce.
+
+
+
+
+ New sequents to prove:
+
+
+ The ones opened by the tactics fwd invokes.
+
+
+
+
+
+
+
+ generalize
+ generalize
+ generalize patt as H
+
+
+
+ Synopsis:
+
+ generalize &pattern; [as &id;]
+
+
+
+ Pre-conditions:
+
+ All the terms matched by patt must be
+ convertible and close in the context of the current sequent.
+
+
+
+ Action:
+
+ It closes the current sequent by applying a stronger
+ lemma that is proved using the new generated sequent.
+
+
+
+ New sequents to prove:
+
+ It opens a new sequent where the current sequent conclusion
+ G is generalized to
+ âx.G{x/t} where {x/t}
+ is a notation for the replacement with x of all
+ the occurrences of the term t matched by
+ patt. If patt matches no
+ subterm then t is defined as the
+ wanted part of the pattern.
+
+
+
+
+
+ id
- The tactic id
-
-
- injection <term>
- The tactic injection
-
-
- intro [<ident>]
- The tactic intro
-
-
- intros <intros_spec>
- The tactic intros
-
-
- intros <term>
- The tactic intros
-
-
- lapply [depth=<int>] <term> [to <term list] [using <ident>]
- The tactic lapply
-
-
- left
- The tactic left
-
-
- letin <ident> â <term>
- The tactic letin
-
-
- normalize <pattern>
- The tactic normalize
-
-
- paramodulation <pattern>
- The tactic paramodulation
-
-
- reduce <pattern>
- The tactic reduce
-
-
- reflexivity
- The tactic reflexivity
-
-
- replace <pattern> with <term>
- The tactic replace
-
-
- rewrite {<|>} <term> <pattern>
- The tactic rewrite
-
-
- right
- The tactic right
-
-
- ring
- The tactic ring
-
-
- simplify <pattern>
- The tactic simplify
-
-
- split
- The tactic split
-
-
- symmetry
- The tactic symmetry
-
-
- transitivity <term>
- The tactic transitivity
-
-
- unfold [<term>] <pattern>
- The tactic unfold
-
-
- whd <pattern>
- The tactic whd
-
+ id
+ id
+
+
+
+ Synopsis:
+
+ id
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ This identity tactic does nothing without failing.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ intro
+ intro
+ intro H
+
+
+
+ Synopsis:
+
+ intro [&id;]
+
+
+
+ Pre-conditions:
+
+ The conclusion of the sequent to prove must be an implication
+ or a universal quantification.
+
+
+
+ Action:
+
+ It applies the right introduction rule for implication,
+ closing the current sequent.
+
+
+
+ New sequents to prove:
+
+ It opens a new sequent to prove adding to the hypothesis
+ the antecedent of the implication and setting the conclusion
+ to the consequent of the implicaiton. The name of the new
+ hypothesis is H if provided; otherwise it
+ is automatically generated.
+
+
+
+
+
+
+ intros
+ intros
+ intros hyps
+
+
+
+ Synopsis:
+
+ intros &intros-spec;
+
+
+
+ Pre-conditions:
+
+ If hyps specifies a number of hypotheses
+ to introduce, then the conclusion of the current sequent must
+ be formed by at least that number of imbricated implications
+ or universal quantifications.
+
+
+
+ Action:
+
+ It applies several times the right introduction rule for
+ implication, closing the current sequent.
+
+
+
+ New sequents to prove:
+
+ It opens a new sequent to prove adding a number of new
+ hypotheses equal to the number of new hypotheses requested.
+ If the user does not request a precise number of new hypotheses,
+ it adds as many hypotheses as possible.
+ The name of each new hypothesis is either popped from the
+ user provided list of names, or it is automatically generated when
+ the list is (or becomes) empty.
+
+
+
+
+
+
+ inversion
+ inversion
+ inversion t
+
+
+
+ Synopsis:
+
+ inversion &sterm;
+
+
+
+ Pre-conditions:
+
+ The type of the term t must be an inductive
+ type or the application of an inductive type.
+
+
+
+ Action:
+
+ It proceeds by cases on t paying attention
+ to the constraints imposed by the actual "right arguments"
+ of the inductive type.
+
+
+
+ New sequents to prove:
+
+ It opens one new sequent to prove for each case in the
+ definition of the type of t. With respect to
+ a simple elimination, each new sequent has additional hypotheses
+ that states the equalities of the "right parameters"
+ of the inductive type with terms originally present in the
+ sequent to prove.
+
+
+
+
+
+
+ lapply
+ lapply
+
+ lapply linear depth=d t
+ to t1, ..., tn as H
+
+
+
+
+ Synopsis:
+
+
+ lapply
+ [linear]
+ [depth=&nat;]
+ &sterm;
+ [to
+ &sterm;
+ [,&sterm;â¦]
+ ]
+ [as &id;]
+
+
+
+
+ Pre-conditions:
+
+
+ t must have at least d
+ independent premises and n must not be
+ greater than d.
+
+
+
+
+ Action:
+
+
+ Invokes letin H â (t ? ... ?)
+ with enough ?'s to reach the
+ d-th independent premise of
+ t
+ (d is maximum if unspecified).
+ Then istantiates (by apply) with
+ t1, ..., tn
+ the ?'s corresponding to the first
+ n independent premises of
+ t.
+ Usually the other ?'s preceding the
+ n-th independent premise of
+ t are istantiated as a consequence.
+ If the linear flag is specified and if
+ t, t1, ..., tn
+ are (applications of) premises in the current context, they are
+ cleared.
+
+
+
+
+ New sequents to prove:
+
+
+ The ones opened by the tactics lapply invokes.
+
+
+
+
+
+
+
+ left
+ left
+ left
+
+
+
+ Synopsis:
+
+ left
+
+
+
+ Pre-conditions:
+
+ The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type
+ with at least one constructor.
+
+
+
+ Action:
+
+ Equivalent to constructor 1.
+
+
+
+ New sequents to prove:
+
+ It opens a new sequent for each premise of the first
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the constructor tactic.
+
+
+
+
+
+
+ letin
+ letin
+ letin x â t
+
+
+
+ Synopsis:
+
+ letin &id; â &sterm;
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ It adds to the context of the current sequent to prove a new
+ definition x â t.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ normalize
+ normalize
+ normalize patt
+
+
+
+ Synopsis:
+
+ normalize &pattern;
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ It replaces all the terms matched by patt
+ with their βδιζ-normal form.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ reflexivity
+ reflexivity
+ reflexivity
+
+
+
+ Synopsis:
+
+ reflexivity
+
+
+
+ Pre-conditions:
+
+ The conclusion of the current sequent must be
+ t=t for some term t
+
+
+
+ Action:
+
+ It closes the current sequent by reflexivity
+ of equality.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ replace
+ change
+ change patt with t
+
+
+
+ Synopsis:
+
+ replace &pattern; with &sterm;
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ It replaces the subterms of the current sequent matched by
+ patt with the new term t.
+ For each subterm matched by the pattern, t is
+ disambiguated in the context of the subterm.
+
+
+
+ New sequents to prove:
+
+ For each matched term t' it opens
+ a new sequent to prove whose conclusion is
+ t'=t.
+
+
+
+
+
+
+ rewrite
+ rewrite
+ rewrite dir p patt
+
+
+
+ Synopsis:
+
+ rewrite [<|>] &sterm; &pattern;
+
+
+
+ Pre-conditions:
+
+ p must be the proof of an equality,
+ possibly under some hypotheses.
+
+
+
+ Action:
+
+ It looks in every term matched by patt
+ for all the occurrences of the
+ left hand side of the equality that p proves
+ (resp. the right hand side if dir is
+ <). Every occurence found is replaced with
+ the opposite side of the equality.
+
+
+
+ New sequents to prove:
+
+ It opens one new sequent for each hypothesis of the
+ equality proved by p that is not closed
+ by unification.
+
+
+
+
+
+
+ right
+ right
+ right
+
+
+
+ Synopsis:
+
+ right
+
+
+
+ Pre-conditions:
+
+ The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least two constructors.
+
+
+
+ Action:
+
+ Equivalent to constructor 2.
+
+
+
+ New sequents to prove:
+
+ It opens a new sequent for each premise of the second
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the constructor tactic.
+
+
+
+
+
+
+ ring
+ ring
+ ring
+
+
+
+ Synopsis:
+
+ ring
+
+
+
+ Pre-conditions:
+
+ The conclusion of the current sequent must be an
+ equality over Coq's real numbers that can be proved using
+ the ring properties of the real numbers only.
+
+
+
+ Action:
+
+ It closes the current sequent veryfying the equality by
+ means of computation (i.e. this is a reflexive tactic, implemented
+ exploiting the "two level reasoning" technique).
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ simplify
+ simplify
+ simplify patt
+
+
+
+ Synopsis:
+
+ simplify &pattern;
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ It replaces all the terms matched by patt
+ with other convertible terms that are supposed to be simpler.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ split
+ split
+ split
+
+
+
+ Synopsis:
+
+ split
+
+
+
+ Pre-conditions:
+
+ The conclusion of the current sequent must be
+ an inductive type or the application of an inductive type with
+ at least one constructor.
+
+
+
+ Action:
+
+ Equivalent to constructor 1.
+
+
+
+ New sequents to prove:
+
+ It opens a new sequent for each premise of the first
+ constructor of the inductive type that is the conclusion of the
+ current sequent. For more details, see the constructor tactic.
+
+
+
+
+
+
+
+ subst
+ subst
+ subst
+
+
+
+ Synopsis:
+
+ subst
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ For each premise of the form
+ H: x = t or H: t = x
+ where x is a local variable and
+ t does not depend on x,
+ the tactic rewrites H wherever
+ x appears clearing H and
+ x afterwards.
+
+
+
+ New sequents to prove:
+
+ The one opened by the applied tactics.
+
+
+
+
+
+
+ symmetry
+ symmetry
+ The tactic symmetry
+ symmetry
+
+
+
+ Synopsis:
+
+ symmetry
+
+
+
+ Pre-conditions:
+
+ The conclusion of the current proof must be an equality.
+
+
+
+ Action:
+
+ It swaps the two sides of the equalityusing the symmetric
+ property.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ transitivity
+ transitivity
+ transitivity t
+
+
+
+ Synopsis:
+
+ transitivity &sterm;
+
+
+
+ Pre-conditions:
+
+ The conclusion of the current proof must be an equality.
+
+
+
+ Action:
+
+ It closes the current sequent by transitivity of the equality.
+
+
+
+ New sequents to prove:
+
+ It opens two new sequents l=t and
+ t=r where l and r are the left and right hand side of the equality in the conclusion of
+the current sequent to prove.
+
+
+
+
+
+
+ unfold
+ unfold
+ unfold t patt
+
+
+
+ Synopsis:
+
+ unfold [&sterm;] &pattern;
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ It finds all the occurrences of t
+ (possibly applied to arguments) in the subterms matched by
+ patt. Then it δ-expands each occurrence,
+ also performing β-reduction of the obtained term. If
+ t is omitted it defaults to each
+ subterm matched by patt.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+ whd
+ whd
+ whd patt
+
+
+
+ Synopsis:
+
+ whd &pattern;
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ It replaces all the terms matched by patt
+ with their βδιζ-weak-head normal form.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
-
+