X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=779f95eb81153022a73692038f7a2a2137d5b539;hb=1b9dcf31051dfcf1e80991954ecbcb6aa9744388;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..779f95eb8 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -1,19 +1,20 @@
-
+
Tactics
-
+
absurd <term>
+ absurd
absurd P
-
+
+
Pre-conditions:
P must have type Prop.
-
Action:
@@ -29,10 +30,11 @@
-
-
-
+
+
+
apply <term>
+ apply
apply t
@@ -64,10 +66,11 @@
-
-
+
+
assumption
- assumption
+ assumption
+ assumption
@@ -91,9 +94,10 @@
-
-
+
+
auto [depth=<int>] [width=<int>] [paramodulation] [full]
+ auto
auto depth=d width=w paramodulation full
@@ -124,9 +128,10 @@
-
-
+
+
clear <id>
+ clear
clear H
@@ -152,9 +157,10 @@
-
-
+
+
clearbody <id>
+ clearbody
clearbody H
@@ -180,9 +186,10 @@
-
-
+
+
change <pattern> with <term>
+ change
change patt with t
@@ -211,9 +218,10 @@
-
-
+
+
constructor <int>
+ constructor
constructor n
@@ -221,7 +229,8 @@
Pre-conditions:
the conclusion of the current sequent must be
- an inductive type or the application of an inductive type.
+ an inductive type or the application of an inductive type with
+ at least n constructors.
@@ -241,10 +250,11 @@
-
-
+
+
contradiction
- contradiction
+ contradiction
+ contradiction
@@ -269,9 +279,10 @@
-
-
+
+
cut <term> [as <id>]
+ cut
cut P as H
@@ -299,9 +310,10 @@
-
-
+
+
decompose [<ident list>] <ident> [<intros_spec>]
+ decompose
decompose ???
@@ -325,16 +337,17 @@
-
-
+
+
discriminate <term>
+ discriminate
discriminate p
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
+ p must have type K t1 ... tn = K' 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.
@@ -353,9 +366,10 @@ its constructor takes no arguments.
-
-
+
+
elim <term> [using <term>] [<intros_spec>]
+ elim
elim t using th hyps
@@ -386,9 +400,10 @@ its constructor takes no arguments.
-
-
+
+
elimType <term> [using <term>]
+ elimType
elimType T using th
@@ -412,9 +427,10 @@ its constructor takes no arguments.
-
-
+
+
exact <term>
+ exact
exact p
@@ -439,17 +455,19 @@ its constructor takes no arguments.
-
-
+
+
exists
- exists
+ exists
+ exists
Pre-conditions:
the conclusion of the current sequent must be
- an inductive type or the application of an inductive type.
+ an inductive type or the application of an inductive type
+ with at least one constructor.
@@ -468,9 +486,10 @@ its constructor takes no arguments.
-
-
- fail
+
+
+ fail
+ failt
fail
@@ -494,111 +513,799 @@ its constructor takes no arguments.
-
-
+
+
fold <reduction_kind> <term> <pattern>
- The tactic fold
-
-
+ fold
+ fold red t patt
+
+
+
+ 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
-
-
+ fourier
+ 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 <ident> [<ident list>]
- The tactic fwd
-
-
+ fwd
+ fwd ...TODO
+
+
+
+ Pre-conditions:
+
+ TODO.
+
+
+
+ Action:
+
+ TODO.
+
+
+
+ New sequents to prove:
+
+ TODO.
+
+
+
+
+
+
generalize <pattern> [as <id>]
- The tactic generalize
-
-
+ generalize
+ generalize patt as H
+
+
+
+ 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
-
-
+ id
+ absurd P
+
+
+
+ Pre-conditions:
+
+ none.
+
+
+
+ Action:
+
+ this identity tactic does nothing without failing.
+
+
+
+ New sequents to prove:
+
+ none.
+
+
+
+
+
+
injection <term>
- The tactic injection
-
-
+ injection
+ injection p
+
+
+
+ Pre-conditions:
+
+ p must have type K t1 ... tn = K t'1 ... t'n where both argument lists are empty if
+K takes no arguments.
+
+
+
+ Action:
+
+ it derives new hypotheses by injectivity of
+ K.
+
+
+
+ New sequents to prove:
+
+ the new sequent to prove is equal to the current sequent
+ with the additional hypotheses
+ t1=t'1 ... tn=t'n.
+
+
+
+
+
+
intro [<ident>]
- The tactic intro
-
-
+ intro
+ intro H
+
+
+
+ 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_spec>
- The tactic intros
-
-
- intros <term>
- The tactic intros
-
-
+ intros
+ intros hyps
+
+
+
+ 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 <term>
+ inversion
+ inversion t
+
+
+
+ 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 [depth=<int>] <term> [to <term list] [using <ident>]
- The tactic lapply
-
-
+ lapply
+ lapply ???
+
+
+
+ Pre-conditions:
+
+ TODO.
+
+
+
+ Action:
+
+ TODO.
+
+
+
+ New sequents to prove:
+
+ TODO.
+
+
+
+
+
+
left
- The tactic left
-
-
+ left
+ 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 <ident> â <term>
- The tactic letin
-
-
+ letin
+ letin x â t
+
+
+
+ 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 <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
-
-
+ normalize
+ normalize patt
+
+
+
+ Pre-conditions:
+
+ none.
+
+
+
+ Action:
+
+ it replaces all the terms matched by patt
+ with their βδιζ-normal form.
+
+
+
+ New sequents to prove:
+
+ none.
+
+
+
+
+
+
+ paramodulation <pattern>
+ paramodulation
+ paramodulation patt
+
+
+
+ Pre-conditions:
+
+ TODO.
+
+
+
+ Action:
+
+ TODO.
+
+
+
+ New sequents to prove:
+
+ TODO.
+
+
+
+
+
+
+ reduce <pattern>
+ reduce
+ reduce patt
+
+
+
+ Pre-conditions:
+
+ none.
+
+
+
+ Action:
+
+ it replaces all the terms matched by patt
+ with their βδιζ-normal form.
+
+
+
+ New sequents to prove:
+
+ none.
+
+
+
+
+
+
+ reflexivity
+ reflexivity
+ 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 <pattern> with <term>
+ change
+ change patt with t
+
+
+
+ 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 {<|>} <term> <pattern>
+ rewrite
+ rewrite dir p patt
+
+
+
+ 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
+
+
+
+ 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
- The tactic ring
-
-
+ ring
+ 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 <pattern>
- The tactic simplify
-
-
+ simplify
+ simplify patt
+
+
+
+ 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
- The tactic split
-
-
+ split
+ 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.
+
+
+
+
+
+
symmetry
+ symmetry
The tactic symmetry
-
-
+ 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 <term>
- The tactic transitivity
-
-
+ transitivity
+ transitivity t
+
+
+
+ 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 [<term>] <pattern>
- The tactic unfold
-
-
+ unfold
+ unfold t patt
+
+
+
+ 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 <pattern>
- The tactic whd
-
+ whd
+ whd patt
+
+
+
+ Pre-conditions:
+
+ none.
+
+
+
+ Action:
+
+ it replaces all the terms matched by patt
+ with their βδιζ-weak-head normal form.
+
+
+
+ New sequents to prove:
+
+ none.
+
+
+
+
+
-
+