X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_declarative_tactics.xml;h=bc0b424e0d3b0bb75ed6613a456fa904315136c8;hb=f63e9358746f82de0dd07d60bdf82fdc0fae2101;hp=cc6aeb61de2ae497fff42a6b7ad44909d693baf2;hpb=c78a913e4e45c1128b59ca8be9d53fc0c36fc9e0;p=helm.git
diff --git a/helm/software/matita/help/C/sec_declarative_tactics.xml b/helm/software/matita/help/C/sec_declarative_tactics.xml
index cc6aeb61d..bc0b424e0 100644
--- a/helm/software/matita/help/C/sec_declarative_tactics.xml
+++ b/helm/software/matita/help/C/sec_declarative_tactics.xml
@@ -51,199 +51,28 @@
-
- suppose
- suppose
- suppose t(x)
-
-
-
- Synopsis:
-
- suppose &term; ( &id;
- ) [ that is equivalent to &term; ]
-
-
-
- Pre-condition:
-
- &TODO;
-
-
-
- Action:
-
- &TODO;
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
-
- by done
- by done
- by [ t | _ ] done
-
-
-
- Synopsis:
-
- by &term; done
-
-
-
- Pre-condition:
-
- The term can be omitted with a "_", the running term will come found automatically.
-
-
-
- Action:
-
- It closes the current sequent by applying t, taht it can be one under proof or the main proof.
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
-
- we need to prove
- we need to prove
- we need to prove t [(id)] [or equivalent t]
-
-
-
- Synopsis:
-
- we need to prove &term;
-
-
-
- Pre-condition:
-
- &TODO;
-
-
-
- Action:
-
- &TODO;
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
-
- we proceed by induction
- we proceed by induction
- we proceed by induction on t to prove th
-
-
-
- Synopsis:
-
- we proceed by induction on &term; to prove &term;
-
-
-
- Pre-condition:
-
- t must inhabit an inductive type and th must be an elimination principle for that inductive type.
-
-
-
- Action:
-
- It proceed on the values of t.
-
-
-
- New sequents to prove:
-
- It opens one new sequent to demonstrate.
-
-
-
-
-
-
-
- we proceed by cases
- we proceed by cases
- we proceed by cases on t to prove t
-
-
-
- Synopsis:
-
- we proceed by cases on &term; to prove &term;
-
-
-
- Pre-condition:
-
- &TODO;
-
-
-
- Action:
-
- &TODO;
-
-
-
- New sequents to prove:
-
- None.
-
-
-
-
-
-
- by induction
- by induction
+ 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; )
+ by induction hypothesis we know &term; ( &id; )
Pre-condition:
- &TODO;
+ To be used in a proof by induction to state the inductive
+ hypothesis.
Action:
- &TODO;
+ Introduces the inductive hypothesis.
@@ -256,192 +85,291 @@
-
- thesis becomes
- thesis becomes
- the thesis becomes t
-
-
-
- Synopsis:
-
- the thesis becomes &sterm;
-
-
-
- Pre-condition:
-
- Each subterm must be convertible with the term t disambiguate in the context of the matched subterm.
-
-
-
- Action:
-
- It replaces the subterm of the current sequent with the new term
-
-
-
- New sequence to prove:
-
- None.
-
-
-
-
-
-
case
case
- case id (id:t)list
+ case id (id1:t1) ⦠(idn:tn)
Synopsis:
- case &id; ( &id; : &term; )
+ case &id; [( &id; : &term; )] â¦
Pre-condition:
- &TODO;
+ To be used in a proof by induction or by cases to start
+ a new case
Action:
- &TODO;
+ Starts the new case id declaring
+ the local parameters (id1:t1) ⦠(idn:tn)
New sequents to prove:
- &TODO;
+ None
+
+ done
+ done
+ justification done
+
+
+
+ Synopsis:
+
+ &justification; done
+
+
+
+ Pre-condition:
+
+
+
+
+
+ Action:
+
+ It closes the current sequent given the justification.
+
+
+
+ New sequents to prove:
+
+ None.
+
+
+
+
+
+
+
+
+ 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.
+
+
+
+
+
+
- obtain/conclude
- obtain/conclude
- obtain H t=t [auto_params | exact t| proof | using t] done
+ obtain
+ obtain
+ obtain H t1 = t2 justification
Synopsis:
- [obtain &id; | conclude &term;] = &term; [&autoparams; | exact &term; | using &term; | proof] [done]
+ [obtain &id; | conclude &term;] = &term; [&autoparams; | using &term; | using once &term; | proof] [done]
Pre-condition:
- &TODO;
-
+ conclude can be used only if the current
+ sequent is stating an equality. The left hand side must be omitted
+ in an equality chain.
+
Action:
- &TODO;
+ Starts or continues an equality chain. If the chain starts
+ with obtain H a new subproof named
+ H is started.
- New sequence to prove:
+ New sequent to prove:
- &TODO;
+ If the chain starts
+ with obtain H a nre sequent for
+ t2 = ? is opened.
+
-
- by term we proved
- by term we proved
- by th we proved t [""|(id)]
+
+ 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
-
-
- Synopsis:
-
- by &term; we proved &term;
- ( &id; )
-
+
+
+ Synopsis:
+
+ the thesis becomes &term;
+
Pre-condition:
- thmust have type Prop.
- idcan to be omitted with null
+ The provided term t must be convertible with
+ current sequent.
Action:
- It closes the current sequent by applyingth to t.
+ It changes the current goal to the one provided.
- New sequence to prove:
+ New sequent to prove:
- &TODO;
+ None.
-
-
-
- exits elim
- exits elim
- by t let id:t such that t (id)
+
+
+
+ we need to prove
+ we need to prove
+ we need to prove t1 (id) or equivalently t2
Synopsis:
- by &term; let &id;
- : &term; such that &term;
- ( &id; )
-
-
-
- Pre-condition:
-
- t must be an inductive type,existential and
- t (id) must be an elimanation priciple for that inductive type.
-
-
-
-
- Action:
-
- it proceeds on t to the elimination of the existential one
+ we need to prove &term;
+ [(&id;
+ )]
+ [ or equivalently &term;]
-
- New sequence to prove:
+
+ Pre-condition:
- It opens one new sequent. The names of the new hypotheses are picked byt (id)
+
-
+
+
+ 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.
+
+
+
+
+ New sequents to prove:
+
+ The stated one if id is provided
+
+
+
- and elim
- and elim
- by t we have t (id) and t (id)
+ we have
+ we have
+ justification we have t1 (id1) and t2 (id2)
+
Synopsis:
- by &term; we have &term;
+ &justification; we have &term;
( &id; ) and &term;
( &id; )
@@ -449,23 +377,142 @@
Pre-condition:
- t must be an logical type,type and
+
Action:
- It proceeds on the values of t, according to the elimination principle
+ It derives t1â§t2 using the
+ justification then it introduces in the context
+ t1 labelled with id1 and
+ t2 labelled with id2.
+
- New sequence to prove:
+ New sequent to prove:
- It opens one new sequent, the names of the new hypotheses are picked by t(id) and t(id)
+ None.
+
+ we proceed by cases on
+ we proceed by cases on
+ we proceed by cases on t to prove th
+
+
+
+ Synopsis:
+
+ we proceed by cases on &term; to prove &term;
+
+
+
+ Pre-condition:
+
+ t must inhabitant of an inductive type and
+ th must be the conclusion to be proved by
+ cases.
+
+
+
+ Action:
+
+ It proceeds by cases on t
+
+
+
+ New sequents to prove:
+
+ It opens one new sequent for each constructor of the
+ type of t.
+
+
+
+
+
+
+
+ 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:
+
+ It proceed by induction on t.
+
+
+
+ New sequents to prove:
+
+ It opens one new sequent for each constructor of the
+ type of t.
+
+
+
+
+
+
+
+
+ we proved
+ we proved
+ justification we proved t (id)
+
+
+
+ Synopsis:
+
+ &justification; we proved &term;
+ ( &id;
+ )
+
+
+
+ Pre-condition:
+
+ tmust have type Prop.
+
+
+
+
+ Action:
+
+ It derives t
+ using the justification and labels the conclusion with
+ id.
+
+
+
+
+ New sequent to prove:
+
+ None.
+
+
+
+
+
+