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=bc0b424e0d3b0bb75ed6613a456fa904315136c8;hb=784f0d4d7cff3700363affe647f7b8b218726fcb;hpb=dd627e471392375ca7b6dad78a931a8682e06dbe
diff --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml
index bc0b424e0..76acf5e0a 100644
--- a/matita/matita/help/C/sec_declarative_tactics.xml
+++ b/matita/matita/help/C/sec_declarative_tactics.xml
@@ -14,277 +14,167 @@
assume
assume
- assume x : t
+ assume x : T
Synopsis:
- assume &id; : &sterm;
+ assume &id; :
+ &sterm;
Pre-conditions:
- The conclusion of the current proof must be
- âx:T.P or
- TâP where T is
- a data type (i.e. T has type
- Set or Type).
+
+ The conclusion of the sequent to prove must be a universal quantification.
+
Action:
- It adds to the context of the current sequent to prove a new
- declaration x : T . The new conclusion becomes
- P.
+
+ It applies the right introduction rule for the universal quantifier, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the quantifier).
+
New sequents to prove:
- None.
+
+ It opens a new sequent to prove the quantified subformula adding x : T to the hypotheses.
+
-
- by induction hypothesis we know
- by induction hypothesis we know
- by induction hypothesis we know t (id)
-
-
-
- Synopsis:
- by induction hypothesis we know &term; ( &id; )
-
-
-
- Pre-condition:
-
- To be used in a proof by induction to state the inductive
- hypothesis.
-
-
-
- Action:
-
- Introduces the inductive hypothesis.
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
-
- case
- case
- case id (id1:t1) ⦠(idn:tn)
-
-
-
- Synopsis:
-
- case &id; [( &id; : &term; )] â¦
-
-
-
- Pre-condition:
-
- To be used in a proof by induction or by cases to start
- a new case
-
-
-
- Action:
-
- Starts the new case id declaring
- the local parameters (id1:t1) ⦠(idn:tn)
-
-
-
- New sequents to prove:
-
- None
-
-
-
-
-
-
-
- done
- done
- justification done
-
+
+ suppose
+ suppose
+ suppose A (H)
+
Synopsis:
- &justification; done
+ suppose &term; ( &id;
+ )
-
+
Pre-condition:
-
-
-
-
-
+
+
+ The conclusion of the sequent to prove must be an implication.
+
+
+
+
Action:
-
- It closes the current sequent given the justification.
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
+
+
+ It applies the right introduction rule for the implication, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the implication).
+
+
+
+
+ New sequents to prove:
+
+
+ It opens a new sequent to prove the consequent of the implication adding the antecedent A to the hypotheses. The name of the new hypothesis is H.
+
+
+
+
+
-
-
- let such that
- let such that
- justification let x:t such that p (id)
-
-
-
-
- Synopsis:
-
- &justification; let &id;
- : &term; such that &term;
- ( &id; )
-
-
-
- Pre-condition:
-
-
-
-
-
-
- Action:
-
- It derives âx:t.p using the
- justification and then it introduces in the context
- x and the hypothesis
- p labelled with
- id.
-
-
-
-
- New sequent to prove:
-
- None.
-
-
-
-
+
+ letin
+ letin
+ let x := T
+
+
+
+ Synopsis:
+
+ let &id; = &term;
+
+
+
+ Pre-condition:
+
+ None
+
+
+
+ Action:
+
+ It adds a new local definition x := T to the context of the sequent to prove.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
-
- obtain
- obtain
- obtain H t1 = t2 justification
+
+ that is equivalent to
+ that is equivalent to
+ that is equivalent to t
Synopsis:
- [obtain &id; | conclude &term;] = &term; [&autoparams; | using &term; | using once &term; | proof] [done]
+
+ that is equivalent to &term;
+
Pre-condition:
- conclude can be used only if the current
- sequent is stating an equality. The left hand side must be omitted
- in an equality chain.
+
+ The user must have applied one of the following tactics immediately before applying this tactic: assume, suppose, we need to prove, by just we proved,the thesis becomes, that is equivalent to.
+
Action:
- Starts or continues an equality chain. If the chain starts
- with obtain H a new subproof named
- H is started.
+
+ If the tactic that was applied before this introduced a new hypothesis in the context, this tactic works on this hypothesis; otherwise, it works on the conclusion. Either way, if the term t is beta-equivalent to the term t1 on which this tactic is working (i.e. they can be reduced to a common term), t1 is changed with t.
+
+ If the tactic that was applied before this tactic was that is equivalent to, and that tactic was working on a term t1, this tactic keeps working on t1.
+
New sequent to prove:
- If the chain starts
- with obtain H a nre sequent for
- t2 = ? is opened.
-
+
+ If this tactic is working on the conclusion, a new sequent with the same hypotheses and the conclusion changed to t is opened. If this tactic is working on the last introduced hypotesis, a new sequent with the same conclusion is opened. The hypotheses of this sequent are the same, except for the one on which the tactic is working on, which is changed with t.
+
-
- suppose
- suppose
- suppose t1 (x)Â that is equivalent to t2
-
-
-
- Synopsis:
-
- suppose &term; ( &id;
- ) [ that is equivalent to &term; ]
-
-
-
- Pre-condition:
-
- The conclusion of the current proof must be
- âx:T.P or
- TâP where T is
- a proposition (i.e. T has type
- Prop or CProp).
-
-
-
- Action:
-
- It adds to the context of the current sequent to prove a new
- declaration x : T . The new conclusion becomes
- P.
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
the thesis becomes
the thesis becomes
- the thesis becomes t
+ the thesis becomes P
@@ -296,14 +186,13 @@
Pre-condition:
- The provided term t must be convertible with
- current sequent.
+ The provided term P must be identical to the current conclusion.
Action:
- It changes the current goal to the one provided.
+ It allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to, after stating the current conclusion.
@@ -315,11 +204,11 @@
-
+
we need to prove
we need to prove
- we need to prove t1 (id) or equivalently t2
+ we need to prove T [(H)]
@@ -328,41 +217,122 @@
we need to prove &term;
[(&id;
)]
- [ or equivalently &term;]
+
Pre-condition:
-
+ None.
Action:
- If id is provided, starts a subproof that once concluded
- will be named id. Otherwise states what needs to be proved.
- If t2Â is provided, the new goal is
- immediately changed to t2 wich must
- be equivalent to t1.
+ If id is provided, it applies a logical cut on T. Otherwise, it allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to.
New sequents to prove:
- The stated one if id is provided
+ If id is supplied, a new sequent with T as the conclusion is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with H:T added to the hypotheses.
+
+ we proved
+ we proved
+ justification we proved T [(id)]
+
+
+
+ Synopsis:
+
+ &justification; we proved &term;
+ [( &id;
+ )]
+
+
+
+
+ Pre-condition:
+
+
+ None.
+
+
+
+
+ Action:
+
+
+ If id is supplied, a logical cut on T is made. Otherwise, if T is identical to the current conclusion, it allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to.
+
+
+
+
+ New sequent to prove:
+
+
+ If id is supplied, a new sequent with T as the conclusion is opened and then immediately closed using the supplied justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and a new hypotesis T is added to the context, with name id.
+ If id is not supplied, no new sequents are opened.
+
+
+
+
+
+
+
+
+
+ let such that
+ let such that
+ justification let x:T such that P (H)
+
+
+
+
+ Synopsis:
+
+ &justification; let &id;
+ : &term; such that &term;
+ ( &id; )
+
+
+
+ Pre-condition:
+
+
+ None.
+
+
+
+
+ Action:
+
+
+ It applies the left introduction rule of the existential quantifier on the formula â x. P(x) (in Natural Deduction this corresponds to the elimination rule for the quantifier).
+
+
+
+
+ New sequent to prove:
+
+ A new sequent with â x. P(x) as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses x : T and H : P are added to the context.
+
+
+
+
+
we have
we have
- justification we have t1 (id1) and t2 (id2)
+ justification we have A (H1) and B (H2)
@@ -377,33 +347,69 @@
Pre-condition:
-
+
+ None.
+
Action:
- It derives t1â§t2 using the
- justification then it introduces in the context
- t1 labelled with id1 and
- t2 labelled with id2.
-
+
+ It applies the left multiplicative introduction rule for the conjunction on the formula A ⧠B (in Natural Deduction this corresponds to the elimination rule for the conjunction).
+
New sequent to prove:
- None.
+ A new sequent with A ⧠B as the conclusion is opened and then immediately closed using the given justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and two new hypotheses H1 : A and H2 : B are added to the context.
+
+
+ we proceed by induction on
+ we proceed by induction on
+ we proceed by induction on t to prove P
+
+
+
+ Synopsis:
+
+ we proceed by induction on &term; to prove &term;
+
+
+
+ Pre-condition:
+
+ The type of t must be an inductive type and P must be identical to the current conclusion.
+
+
+
+
+ Action:
+
+ It applies the induction principle on t to prove P.
+
+
+
+ New sequents to prove:
+
+ It opens a new sequent for each constructor of the type of t, each with the conclusion P instantiated for the constructor. For the inductive constructors (i.e. if the inductive type is T, constructors with an argument of type T), the conclusion is a logical implication, where the antecedent is the inductive hypothesis for the constructor, and the consequent is P.
+
+
+
+
+
+
we proceed by cases on
we proceed by cases on
- we proceed by cases on t to prove th
+ we proceed by cases on t to prove P
@@ -415,104 +421,241 @@
Pre-condition:
- t must inhabitant of an inductive type and
+ The type of t must be an inductive type and P must be identical to the current conclusion.
+
+
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.
+
+
+
+
+