X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=4bba23eb6e22c887d99171a63f6776f76dfdf4b5;hb=bfcb2bf3391de8f0c4de9b8d35ea44ddc71a4291;hp=caee727a4ab52835465a31ce12574a0086a42b98;hpb=224c374eb4460b577aa3e89cf65d42563b6dace6;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index caee727a4..4bba23eb6 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -18,14 +18,14 @@
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.
@@ -51,13 +51,13 @@
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
+ 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
@@ -76,20 +76,20 @@
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
@@ -104,7 +104,7 @@
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.
Moreover, only lemmas whose type signature is a subset of the
@@ -115,7 +115,7 @@
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.
@@ -123,7 +123,7 @@
New sequents to prove:
- none
+ None
@@ -145,14 +145,14 @@
Action:
- it hides the hypothesis H from the
+ It hides the hypothesis H from the
current sequent.
New sequents to prove:
- none
+ None
@@ -174,14 +174,14 @@
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.
@@ -196,7 +196,7 @@
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.
@@ -204,7 +204,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.
@@ -213,7 +213,7 @@
New sequents to prove:
- none.
+ None.
@@ -228,21 +228,22 @@
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.
@@ -259,21 +260,21 @@
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
@@ -294,13 +295,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
@@ -353,14 +354,14 @@ its constructor takes no arguments.
Action:
- it closes the current sequent by proving the absurdity of
+ It closes the current sequent by proving the absurdity of
p.
New sequents to prove:
- none.
+ None.
@@ -384,7 +385,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.
@@ -392,18 +393,21 @@ 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 <term> [using <term>] [<intros_spec>]
elimType
- elimType T using th
+ elimType T using th hyps
@@ -436,20 +440,20 @@ its constructor takes no arguments.
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.
@@ -464,20 +468,21 @@ its constructor takes no arguments.
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.
@@ -494,13 +499,13 @@ its constructor takes no arguments.
Pre-conditions:
- none.
+ None.
Action:
- this tactic always fail.
+ This tactic always fail.
@@ -521,13 +526,13 @@ its constructor takes no arguments.
Pre-conditions:
- the pattern must not specify the wanted term.
+ The pattern must not specify the wanted term.
Action:
- first of all it locates all the subterms matched by
+ 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
@@ -538,7 +543,7 @@ its constructor takes no arguments.
New sequents to prove:
- none.
+ None.
@@ -553,7 +558,7 @@ its constructor takes no arguments.
Pre-conditions:
- the conclusion of the current sequent must be a linear
+ 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.
@@ -562,13 +567,13 @@ its constructor takes no arguments.
Action:
- it closes the current sequent by applying the Fourier method.
+ It closes the current sequent by applying the Fourier method.
New sequents to prove:
- none.
+ None.
@@ -610,21 +615,21 @@ its constructor takes no arguments.
Pre-conditions:
- all the terms matched by patt must be
+ 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
+ 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
+ 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
@@ -640,25 +645,25 @@ its constructor takes no arguments.
id
id
- absurd P
+ id
Pre-conditions:
- none.
+ None.
Action:
- this identity tactic does nothing without failing.
+ This identity tactic does nothing without failing.
New sequents to prove:
- none.
+ None.
@@ -680,14 +685,14 @@ its constructor takes no arguments.
Action:
- it derives new hypotheses by injectivity of
+ It derives new hypotheses by injectivity of
K.
New sequents to prove:
- the new sequent to prove is equal to the current sequent
+ The new sequent to prove is equal to the current sequent
with the additional hypotheses
t1=t'1 ... tn=t'n.
@@ -704,21 +709,21 @@ its constructor takes no arguments.
Pre-conditions:
- the conclusion of the sequent to prove must be an implication
+ The conclusion of the sequent to prove must be an implication
or a universal quantification.
Action:
- it applies the right introduction rule for implication,
+ 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
+ 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
@@ -746,14 +751,14 @@ its constructor takes no arguments.
Action:
- it applies several times the right introduction rule for
+ 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
+ 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.
@@ -774,14 +779,14 @@ its constructor takes no arguments.
Pre-conditions:
- the type of the term t must be an inductive
+ 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
+ It proceeds by cases on t paying attention
to the constraints imposed by the actual "right arguments"
of the inductive type.
@@ -789,7 +794,7 @@ its constructor takes no arguments.
New sequents to prove:
- it opens one new sequent to prove for each case in the
+ 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"
@@ -836,20 +841,21 @@ its constructor takes no arguments.
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.
@@ -860,37 +866,209 @@ its constructor takes no arguments.
letin <ident> â <term>
letin
- The tactic 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>
normalize
- The tactic 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
- The tactic paramodulation
+ paramodulation patt
+
+
+
+ Pre-conditions:
+
+ TODO.
+
+
+
+ Action:
+
+ TODO.
+
+
+
+ New sequents to prove:
+
+ TODO.
+
+
+
+
reduce <pattern>
reduce
- The tactic 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
- The tactic 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>
- replace
- The tactic replace
+ 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
- The tactic 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
@@ -901,7 +1079,7 @@ its constructor takes no arguments.
Pre-conditions:
- the conclusion of the current sequent must be
+ The conclusion of the current sequent must be
an inductive type or the application of an inductive type with
at least two constructors.
@@ -909,13 +1087,13 @@ its constructor takes no arguments.
Action:
- equivalent to constructor 2.
+ Equivalent to constructor 2.
New sequents to prove:
- it opens a new sequent for each premise of the second
+ 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.
@@ -926,37 +1104,210 @@ its constructor takes no arguments.
ring
ring
- The tactic 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>
simplify
- The tactic 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
split
- The tactic 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>
transitivity
- The tactic 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>
unfold
- The tactic 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>
whd
- The tactic 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.
+
+
+
+