X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_declarative_tactics.xml;h=76acf5e0ad78a1bbfe3d6bb5333dd3b84ba2c9d2;hp=d77c276c4904db43fa894b2da9a3e29fa94da536;hb=784f0d4d7cff3700363affe647f7b8b218726fcb;hpb=8f699ab265e380a2d1ab7dba0ee5e8ba5556a84a
diff --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml
index d77c276c4..76acf5e0a 100644
--- a/matita/matita/help/C/sec_declarative_tactics.xml
+++ b/matita/matita/help/C/sec_declarative_tactics.xml
@@ -1,5 +1,4 @@
-
Action:
- It proceeds by cases on t
+ It proceeds by case-analysis on t
New sequents to prove:
It opens one new sequent for each constructor of the
- type of t.
+ type of t, each with the conclusion P instantiated for the constructor.
-
-
- we proceed by induction on
- we proceed by induction on
- we proceed by induction on t to prove th
-
-
-
- Synopsis:
-
- we proceed by induction on &term; to prove &term;
-
-
-
- Pre-condition:
-
- t must inhabitant of an inductive type and
- th must be the conclusion to be proved by induction.
-
-
-
-
- Action:
+
+
+ case
+ case
+ case id (id1:T1) ⦠(idn:Tn)
+
+
+
+ Synopsis:
+
+ case &id; [( &id; : &term; )] ⦠[( &id; : &term; )]
+
+
+
+ Pre-condition:
- It proceed by induction on t.
+ The user must have started a proof by induction/cases that has not been concluded yet, id must be a constructor for the inductive type of the term under induction/case-analysis, and the case must not have already been proved.
-
-
- New sequents to prove:
+
+
+ Action:
- It opens one new sequent for each constructor of the
- type of t.
+ It starts the proof for the case id, where id1:T1,â¦,idn:Tn are the arguments of the constructor, each declared with its type.
-
-
-
-
+
+
+ New sequents to prove:
+
+ The sequent for the case id.
+
+
+
+
+
+
+ by induction hypothesis we know
+ by induction hypothesis we know
+ by induction hypothesis we know P (id)
+
+
+
+ Synopsis:
+ by induction hypothesis we know &term; ( &id; )
+
+
+
+ Pre-condition:
+
+ The user must have started proving a case for a proof by induction/case-analysis.
+
+
+
+ Action:
+
+ It introduces the inductive hypothesis.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
-
- we proved
- we proved
- justification we proved t (id)
-
-
+
+ conclude
+ conclude
+ conclude t1
+
+
Synopsis:
- &justification; we proved &term;
- ( &id;
- )
+ conclude &term;
+
+
+
+ Pre-condition:
+
+
+ The current conclusion must be an equality t1 = tk
+
+
+
+
+ Action:
+
+ It starts an equality chain on the conclusion. It allows the user to apply the tactic = to continue the chain.
-
-
- Pre-condition:
+
+
+ New sequent to prove:
- tmust have type Prop.
-
+ None.
-
-
- Action:
+
+
+
+
+
+ obtain
+ obtain
+ obtain H t1
+
+
+
+ Synopsis:
+
+ obtain &id; &term;
+
+
+
+ Pre-condition:
- It derives t
- using the justification and labels the conclusion with
- id.
-
+
+ None.
+
+
+
+
+ Action:
+
+ It starts an equality chain t1 = ?, which, when concluded, will be added to hypoteses of the current sequent. It allows the user to apply the tactic = to continue the chain.
+
+
+
+ New sequent to prove:
+
+ A new sequent for t1 = ? is opened, a new sequent for ? is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with H: t1 = ? added to its hypotheses. This hypotesis will be changed when the equality chain is concluded with H: t1 = tk, where tk is the last term of the equality chain. The goal for ? can be safely ignored, as it will be automatically closed when the equality chain is concluded.
-
-
- New sequent to prove:
+
+
+
+
+
+ =
+ =
+ = t2 justification
+
+
+
+ Synopsis:
+
+
+ = &term; [&autoparams; | using &term; | using once &term; | proof] [done]
+
+
+
+
+ Pre-condition:
- None.
+
+ The user must have started an equality chain with conclude or obtain that has not been concluded yet.
+
+
+
+
+ Action:
+
+
+ It applies the transitivity of = on the left-hand-side of the current conclusion, t2, and the right-hand-side of the current conclusion, using the given justification. If done is supplied, this represents the last step in the equality chain.
+
+
+
+
+ New sequent to prove:
+
+
+ A new sequent for lhs = t2 is opened and then immediately closed using the given justification. A new sequent with the conclusion t2 = rhs is opened.
+
-
-
-
-
+
+
+
+
+
+
+ done
+ done
+ justification done
+
+
+
+ Synopsis:
+
+ &justification; done
+
+
+
+ Pre-condition:
+
+ The user is proving a sequent which was opened with the tactic we need to prove, or the user is proving a sequent which was opened with the tactic we proceed by induction/cases on, or the user is proving a chain of equalities that was started with either the tactic conclude or obtain.
+
+
+
+ Action:
+
+ It closes the current sequent with the given justification.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
--->