X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_tactics.xml;h=53a20ac6a78e3c07404d442cb8b7a0de17c7b661;hb=f27b26f3f3d2300b11aa4d68dbe823e15ffbdf1c;hp=2e1f6f36565e8a32f32c921e63badaf964e26a36;hpb=935a53fb77f36e5d90a2a59fa500744001e9d780;p=helm.git
diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index 2e1f6f365..53a20ac6a 100644
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -86,6 +86,59 @@
+
+ applyS
+ applyS
+ applyS t
+
+
+
+ Synopsis:
+
+ applyS &sterm;
+
+
+
+ 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).
+
+
+
+
+ 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
@@ -163,27 +216,40 @@
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.
+
@@ -382,14 +448,22 @@
decomposedecompose
- decompose (T1 ... Tn) H hips
+ decompose (T1 ... Tn)
+ H as H1 ... HmSynopsis:
- decompose &id; [&id;]⦠&intros-spec;
+
+ decompose
+ [(
+ &id;â¦
+ )]
+ [&id;]
+ [as &id;â¦]
+
@@ -408,9 +482,13 @@
Action:
- Runs elim H hyps, clears H and tries to run
- itself recursively on each new identifier introduced by
- elim in the opened sequents.
+ Runs
+ elim H H1 ... Hm
+ , clears H and tries to run itself
+ recursively on each new identifier introduced by
+ elim in the opened sequents.
+ If H is not provided tries this operation on
+ each premise in the current context.
@@ -425,16 +503,16 @@
-
- demodulation
- demodulation
- demodulation patt
+
+ demodulate
+ demodulate
+ demodulateSynopsis:
- demodulation &pattern;
+ demodulate
@@ -750,31 +828,48 @@ its constructor takes no arguments.fwdfwd
- fwd ...TODO
+ fwd H as H0 ... HnSynopsis:
- fwd &id; [([&id;]â¦)]
+ fwd &id; [as &id; [&id;]â¦]Pre-conditions:
- TODO.
+
+ The type of H must be the premise of a
+ forward simplification theorem.
+ Action:
- TODO.
+
+ This tactic is under development.
+ It simplifies the current context by removing
+ H using the following methods:
+ 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:
- TODO.
+
+ The ones opened by the tactics fwd invokes.
+
@@ -857,7 +952,7 @@ its constructor takes no arguments.injection
- injection
+ injectioninjection p
@@ -1019,7 +1114,7 @@ its constructor takes no arguments.lapplylapply
- lapply depth=d t
+ lapply linear depth=d t
to t1, ..., tn as H
@@ -1027,25 +1122,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.
+
@@ -1156,39 +1285,6 @@ its constructor takes no arguments.
-
- paramodulation
- paramodulation
- paramodulation patt
-
-
-
- Synopsis:
-
- paramodulation &pattern;
-
-
-
- Pre-conditions:
-
- TODO.
-
-
-
- Action:
-
- TODO.
-
-
-
- New sequents to prove:
-
- TODO.
-
-
-
-
- reducereduce