X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=cc0043724f57c33fa32f0e7bec60dfff326c8098;hb=cc16727f34114cee287e6a81b80f68657c656725;hp=b4e3cb3a9a20d8e7a890fcff67813e95e2d6ce8b;hpb=4041b420beef86580438e1f021d4bd674f16bb71;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index b4e3cb3a9..cc0043724 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -4,7 +4,7 @@
Tactics
- absurd <term>
+ absurd &sterm;
absurd
absurd P
@@ -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.
@@ -33,7 +33,7 @@
- apply <term>
+ apply &sterm;
apply
apply t
@@ -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
@@ -68,7 +68,7 @@
- assumption
+ assumption
assumption
assumption
@@ -76,27 +76,27 @@
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=&nat;] [width=&nat;] [paramodulation] [full]
auto
auto depth=d width=w paramodulation full
@@ -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,14 +123,14 @@
New sequents to prove:
- none
+ None
- clear <id>
+ clear &id;
clear
clear H
@@ -145,21 +145,21 @@
Action:
- it hides the hypothesis H from the
+ It hides the hypothesis H from the
current sequent.
New sequents to prove:
- none
+ None
- clearbody <id>
+ clearbody &id;
clearbody
clearbody H
@@ -174,21 +174,21 @@
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.
- change <pattern> with <term>
+ change &pattern; with &sterm;
change
change patt with t
@@ -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,14 +213,14 @@
New sequents to prove:
- none.
+ None.
- constructor <int>
+ constructor &nat;
constructor
constructor n
@@ -228,7 +228,7 @@
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 n constructors.
@@ -236,14 +236,14 @@
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.
@@ -252,7 +252,7 @@
- contradiction
+ contradiction
contradiction
contradiction
@@ -260,28 +260,28 @@
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 &sterm; [as &id;]
cut
cut P as H
@@ -295,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
@@ -312,34 +312,75 @@
- decompose [<ident list>] <ident> [<intros_spec>]
+ decompose &id; [&id;]⦠&intros-spec;
decompose
- decompose ???
+
+ decompose (T1 ... Tn) H hips
+
Pre-conditions:
- TODO.
+
+ H must inhabit one inductive type among
+
+ T1 ... Tn
+
+ and the types of a predefined list.
+
Action:
- TODO.
+
+ Runs elim H hyps, clears H and tries to run
+ itself recursively on each new identifier introduced by
+ elim in the opened sequents.
+
New sequents to prove:
- TODO.
+
+ The ones generated by all the elim tactics run.
+
+
+
+
+
+
+
+ demodulation &pattern;
+ demodulation
+ demodulation patt
+
+
+
+ Pre-conditions:
+
+ None.
+
+
+
+ Action:
+
+ &TODO;
+
+
+
+ New sequents to prove:
+
+ None.
- discriminate <term>
+ discriminate &sterm;
discriminate
discriminate p
@@ -354,21 +395,21 @@ 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.
- elim <term> [using <term>] [<intros_spec>]
+ elim &sterm; [using &sterm;] &intros-spec;
elim
elim t using th hyps
@@ -385,7 +426,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.
@@ -393,18 +434,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 &sterm; [using &sterm;] &intros-spec;
elimType
- elimType T using th
+ elimType T using th hyps
@@ -429,7 +473,7 @@ its constructor takes no arguments.
- exact <term>
+ exact &sterm;
exact
exact p
@@ -437,27 +481,27 @@ 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.
- exists
+ exists
exists
exists
@@ -465,7 +509,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 one constructor.
@@ -473,13 +517,13 @@ its constructor takes no arguments.
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.
@@ -488,21 +532,21 @@ its constructor takes no arguments.
- fail
- failt
+ fail
+ fail
fail
Pre-conditions:
- none.
+ None.
Action:
- this tactic always fail.
+ This tactic always fail.
@@ -515,7 +559,7 @@ its constructor takes no arguments.
- fold <reduction_kind> <term> <pattern>
+ fold &reduction-kind; &sterm; &pattern;
fold
fold red t patt
@@ -523,13 +567,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
@@ -540,14 +584,14 @@ its constructor takes no arguments.
New sequents to prove:
- none.
+ None.
- fourier
+ fourier
fourier
fourier
@@ -555,7 +599,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.
@@ -564,20 +608,20 @@ 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.
- fwd <ident> [<ident list>]
+ fwd &id; [([&id;]â¦)]
fwd
fwd ...TODO
@@ -604,7 +648,7 @@ its constructor takes no arguments.
- generalize <pattern> [as <id>]
+ generalize &pattern; [as &id;]
generalize
generalize patt as H
@@ -612,21 +656,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,7 +684,7 @@ its constructor takes no arguments.
- id
+ id
id
id
@@ -648,27 +692,27 @@ its constructor takes no arguments.
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.
- injection <term>
- injection
+ injection &sterm;
+ injection
injection p
@@ -682,14 +726,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.
@@ -698,7 +742,7 @@ its constructor takes no arguments.
- intro [<ident>]
+ intro [&id;]
intro
intro H
@@ -706,21 +750,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
@@ -731,7 +775,7 @@ its constructor takes no arguments.
- intros <intros_spec>
+ intros &intros-spec;
intros
intros hyps
@@ -748,14 +792,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.
@@ -768,7 +812,7 @@ its constructor takes no arguments.
- inversion <term>
+ inversion &sterm;
inversion
inversion t
@@ -776,14 +820,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.
@@ -791,7 +835,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"
@@ -803,9 +847,12 @@ its constructor takes no arguments.
- lapply [depth=<int>] <term> [to <term list] [using <ident>]
+ lapply [depth=&nat;] &sterm; [to &sterm; [&sterm;]â¦] [as &id;]
lapply
- lapply ???
+
+ lapply depth=d t
+ to t1, ..., tn as H
+
@@ -830,7 +877,7 @@ its constructor takes no arguments.
- left
+ left
left
left
@@ -838,7 +885,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 one constructor.
@@ -846,13 +893,13 @@ its constructor takes no arguments.
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.
@@ -861,7 +908,7 @@ its constructor takes no arguments.
- letin <ident> â <term>
+ letin &id; â &sterm;
letin
letin x â t
@@ -869,27 +916,27 @@ its constructor takes no arguments.
Pre-conditions:
- none.
+ None.
Action:
- it adds to the context of the current sequent to prove a new
+ It adds to the context of the current sequent to prove a new
definition x â t.
New sequents to prove:
- none.
+ None.
- normalize <pattern>
+ normalize &pattern;
normalize
normalize patt
@@ -897,27 +944,27 @@ its constructor takes no arguments.
Pre-conditions:
- none.
+ None.
Action:
- it replaces all the terms matched by patt
+ It replaces all the terms matched by patt
with their βδιζ-normal form.
New sequents to prove:
- none.
+ None.
- paramodulation <pattern>
+ paramodulation &pattern;
paramodulation
paramodulation patt
@@ -944,7 +991,7 @@ its constructor takes no arguments.
- reduce <pattern>
+ reduce &pattern;
reduce
reduce patt
@@ -952,27 +999,27 @@ its constructor takes no arguments.
Pre-conditions:
- none.
+ None.
Action:
- it replaces all the terms matched by patt
+ It replaces all the terms matched by patt
with their βδιζ-normal form.
New sequents to prove:
- none.
+ None.
- reflexivity
+ reflexivity
reflexivity
reflexivity
@@ -980,28 +1027,28 @@ its constructor takes no arguments.
Pre-conditions:
- the conclusion of the current sequent must be
+ The conclusion of the current sequent must be
t=t for some term t
Action:
- it closes the current sequent by reflexivity
+ It closes the current sequent by reflexivity
of equality.
New sequents to prove:
- none.
+ None.
- replace <pattern> with <term>
+ replace &pattern; with &sterm;
change
change patt with t
@@ -1009,13 +1056,13 @@ its constructor takes no arguments.
Pre-conditions:
- none.
+ None.
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.
@@ -1024,7 +1071,7 @@ its constructor takes no arguments.
New sequents to prove:
- for each matched term t' it opens
+ For each matched term t' it opens
a new sequent to prove whose conclusion is
t'=t.
@@ -1033,7 +1080,7 @@ its constructor takes no arguments.
- rewrite {<|>} <term> <pattern>
+ rewrite [<|>] &sterm; &pattern;
rewrite
rewrite dir p patt
@@ -1048,7 +1095,7 @@ its constructor takes no arguments.
Action:
- it looks in every term matched by patt
+ 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
@@ -1059,7 +1106,7 @@ its constructor takes no arguments.
New sequents to prove:
- it opens one new sequent for each hypothesis of the
+ It opens one new sequent for each hypothesis of the
equality proved by p that is not closed
by unification.
@@ -1068,7 +1115,7 @@ its constructor takes no arguments.
- right
+ right
right
right
@@ -1076,7 +1123,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.
@@ -1084,13 +1131,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.
@@ -1099,7 +1146,7 @@ its constructor takes no arguments.
- ring
+ ring
ring
ring
@@ -1107,7 +1154,7 @@ its constructor takes no arguments.
Pre-conditions:
- the conclusion of the current sequent must be an
+ 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.
@@ -1115,7 +1162,7 @@ its constructor takes no arguments.
Action:
- it closes the current sequent veryfying the equality by
+ 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).
@@ -1123,14 +1170,14 @@ its constructor takes no arguments.
New sequents to prove:
- none.
+ None.
- simplify <pattern>
+ simplify &pattern;
simplify
simplify patt
@@ -1138,27 +1185,27 @@ its constructor takes no arguments.
Pre-conditions:
- none.
+ None.
Action:
- it replaces all the terms matched by patt
+ It replaces all the terms matched by patt
with other convertible terms that are supposed to be simpler.
New sequents to prove:
- none.
+ None.
- split
+ split
split
split
@@ -1166,7 +1213,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 one constructor.
@@ -1174,13 +1221,13 @@ its constructor takes no arguments.
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.
@@ -1189,7 +1236,7 @@ its constructor takes no arguments.
- symmetry
+ symmetry
symmetry
The tactic symmetry
symmetry
@@ -1198,27 +1245,27 @@ its constructor takes no arguments.
Pre-conditions:
- the conclusion of the current proof must be an equality.
+ The conclusion of the current proof must be an equality.
Action:
- it swaps the two sides of the equalityusing the symmetric
+ It swaps the two sides of the equalityusing the symmetric
property.
New sequents to prove:
- none.
+ None.
- transitivity <term>
+ transitivity &sterm;
transitivity
transitivity t
@@ -1226,19 +1273,19 @@ its constructor takes no arguments.
Pre-conditions:
- the conclusion of the current proof must be an equality.
+ The conclusion of the current proof must be an equality.
Action:
- it closes the current sequent by transitivity of the equality.
+ It closes the current sequent by transitivity of the equality.
New sequents to prove:
- it opens two new sequents l=t and
+ 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.
@@ -1247,7 +1294,7 @@ the current sequent to prove.
- unfold [<term>] <pattern>
+ unfold [&sterm;] &pattern;
unfold
unfold t patt
@@ -1255,13 +1302,13 @@ the current sequent to prove.
Pre-conditions:
- none.
+ None.
Action:
- it finds all the occurrences of t
+ 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
@@ -1272,14 +1319,14 @@ the current sequent to prove.
New sequents to prove:
- none.
+ None.
- whd <pattern>
+ whd &pattern;
whd
whd patt
@@ -1287,20 +1334,20 @@ the current sequent to prove.
Pre-conditions:
- none.
+ None.
Action:
- it replaces all the terms matched by patt
+ It replaces all the terms matched by patt
with their βδιζ-weak-head normal form.
New sequents to prove:
- none.
+ None.