X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=caee727a4ab52835465a31ce12574a0086a42b98;hb=224c374eb4460b577aa3e89cf65d42563b6dace6;hp=fda93f0b38a8dee552ca3270520a4043c981f188;hpb=90903c3a5f562b908190d746b36a4417e1e984ba;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index fda93f0b3..caee727a4 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -346,7 +346,7 @@
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.
@@ -604,42 +604,258 @@ its constructor takes no arguments.
generalize <pattern> [as <id>]
generalize
- The tactic 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
id
- The tactic id
+ absurd P
+
+
+
+ Pre-conditions:
+
+ none.
+
+
+
+ Action:
+
+ this identity tactic does nothing without failing.
+
+
+
+ New sequents to prove:
+
+ none.
+
+
+
+
injection <term>
injection
- The tactic 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>]
intro
- The tactic 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>
intros
- The tactic 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
- The tactic 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>]
lapply
- The tactic lapply
+ lapply ???
+
+
+
+ Pre-conditions:
+
+ TODO.
+
+
+
+ Action:
+
+ TODO.
+
+
+
+ New sequents to prove:
+
+ TODO.
+
+
+
+
left
left
- The tactic left
+ left
+
+
+
+ Pre-conditions:
+
+ the conclusion of the current sequent must be
+ an inductive type or the application of an inductive type.
+
+
+
+ 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>
@@ -679,7 +895,33 @@ its constructor takes no arguments.
right
right
- The tactic 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