X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=0fabbbf7ca5f8a68167a62bcaa68334f59363eb3;hb=9376f52b7f5890d924ae7d93bcae2af9e516126d;hp=c10d2bd337aabc49384f3c7984677369e751fce8;hpb=0fe1347ecafd65a4be26f85595032653f81d1ab3;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index c10d2bd33..0fabbbf7c 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -86,6 +86,61 @@
+
+ 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
+ Ti that is not
+ instantiated by unification. Ti is
+ the conclusion of the i-th new sequent to
+ prove.
+
+
+
+
+ assumptionassumption
@@ -123,13 +178,13 @@
autoauto
- auto depth=d width=w paramodulation full
+ auto paramsSynopsis:
- auto [depth=&nat;] [width=&nat;] [paramodulation] [full]
+ auto &autoparams;
@@ -137,10 +192,10 @@
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 ...&TODO;
@@ -160,30 +215,89 @@
+
+ cases
+ cases
+
+ cases t hyps
+
+
+
+
+ Synopsis:
+
+
+ cases
+ &term; [([&id;]â¦)]
+
+
+
+
+ Pre-conditions:
+
+
+ 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.
+
+
+
+
+ clearclear
- clear H
+
+ clear H1 ... Hm
+ Synopsis:
- clear &id;
+
+ clear
+ &id; [&id;â¦]
+ Pre-conditions:
- H must be an hypothesis of the
- current sequent to prove.
+
+
+ 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.
+
@@ -230,6 +344,58 @@
+
+ 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;.
+
+
+
+
+ changechange
@@ -382,35 +548,38 @@
decomposedecompose
- decompose (T1 ... Tn) H hips
+ decompose as H1 ... HmSynopsis:
- decompose &id; [&id;]⦠&intros-spec;
+
+ decompose
+ [as &id;â¦]
+ Pre-conditions:
-
- H must inhabit one inductive type among
-
- T1 ... Tn
-
- and the types of a predefined list.
-
+ None.Action:
- Runs elim H hyps, clears H and tries to run
- itself recursively on each new identifier introduced by
- elim in the opened sequents.
+ 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.
@@ -425,16 +594,16 @@
-
- demodulation
- demodulation
- demodulation patt
+
+ demodulate
+ demodulate
+ demodulateSynopsis:
- demodulation &pattern;
+ demodulate
@@ -458,30 +627,35 @@
-
- discriminate
- discriminate
- discriminate p
+
+ destruct
+ destruct
+ destruct pSynopsis:
- discriminate &sterm;
+ destruct &sterm;Pre-conditions:
- 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.
+ 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.
+
@@ -750,13 +924,13 @@ its constructor takes no arguments.fwdfwd
- fwd H
+ fwd H as H0 ... HnSynopsis:
- fwd &id; [([&id;]â¦)]
+ fwd &id; [as &id; [&id;]â¦]
@@ -775,16 +949,23 @@ its constructor takes no arguments.
This tactic is under development.
It simplifies the current context by removing
H using the following methods:
- forward application of a suitable simplification theorem (chosen
- automatically) of which the type of H is a
- premise, decomposition, rewriting.
+ 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:
- None.
+
+ The ones opened by the tactics fwd invokes.
+
@@ -865,43 +1046,6 @@ its constructor takes no arguments.
-
- injection
- injection
- injection p
-
-
-
- Synopsis:
-
- injection &sterm;
-
-
-
- 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.
-
-
-
-
- introintro
@@ -1029,7 +1173,7 @@ its constructor takes no arguments.
lapplylapply
- lapply depth=d t
+ lapply linear depth=d t
to t1, ..., tn as H
@@ -1037,25 +1181,59 @@ its constructor takes no arguments.Synopsis:
- lapply [depth=&nat;] &sterm; [to &sterm; [&sterm;]â¦] [as &id;]
+
+ lapply
+ [linear]
+ [depth=&nat;]
+ &sterm;
+ [to
+ &sterm;
+ [,&sterm;â¦]
+ ]
+ [as &id;]
+ Pre-conditions:
- TODO.
+
+ t must have at least d
+ independent premises and n must not be
+ greater than d.
+ Action:
- TODO.
+
+ 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:
- TODO.
+
+ The ones opened by the tactics lapply invokes.
+
@@ -1166,39 +1344,6 @@ its constructor takes no arguments.
-
- paramodulation
- paramodulation
- paramodulation patt
-
-
-
- Synopsis:
-
- paramodulation &pattern;
-
-
-
- Pre-conditions:
-
- TODO.
-
-
-
- Action:
-
- TODO.
-
-
-
- New sequents to prove:
-
- TODO.
-
-
-
-
- reducereduce
@@ -1492,6 +1637,46 @@ its constructor takes no arguments.
+
+
+ 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.
+
+
+
+
+ symmetrysymmetry