X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=468a27695c6e64495fd5450cc66b0eed395de912;hb=2bd3b029f7f67d9c616b7756278573cc9e96510c;hp=56c2a66167b4e47c17f14cecb6ec5a7cde65a809;hpb=cc3ab906b631ef0edb4402cb622fc3fa96682717;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 56c2a6616..468a27695 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/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
@@ -450,16 +503,16 @@
-
- demodulation
- demodulation
- demodulation patt
+
+ demodulate
+ demodulate
+ demodulateSynopsis:
- demodulation &pattern;
+ demodulate
@@ -483,30 +536,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.
+
@@ -897,43 +955,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
@@ -1061,7 +1082,7 @@ its constructor takes no arguments.
lapplylapply
- lapply depth=d t
+ lapply linear depth=d t
to t1, ..., tn as H
@@ -1071,6 +1092,7 @@ its constructor takes no arguments.lapply
+ [linear]
[depth=&nat;]
&sterm;
[to
@@ -1108,6 +1130,10 @@ its constructor takes no arguments.
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.
@@ -1227,39 +1253,6 @@ its constructor takes no arguments.
-
- paramodulation
- paramodulation
- paramodulation patt
-
-
-
- Synopsis:
-
- paramodulation &pattern;
-
-
-
- Pre-conditions:
-
- TODO.
-
-
-
- Action:
-
- TODO.
-
-
-
- New sequents to prove:
-
- TODO.
-
-
-
-
- reducereduce
@@ -1553,6 +1546,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