X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_declarative_tactics.xml;fp=matita%2Fhelp%2FC%2Fsec_declarative_tactics.xml;h=cc6aeb61de2ae497fff42a6b7ad44909d693baf2;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/help/C/sec_declarative_tactics.xml b/matita/help/C/sec_declarative_tactics.xml new file mode 100644 index 000000000..cc6aeb61d --- /dev/null +++ b/matita/help/C/sec_declarative_tactics.xml @@ -0,0 +1,471 @@ + + + Declarative Tactics + + + Quick reference card + + &declarativetacticref; + + + + + + assume + assume + assume x : t + + + + Synopsis: + + 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). + + + + 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. + + + + + + + + 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 t (id) + + + + Synopsis: + + by induction hypothesis we know &term; ( &id; ) + + + + Pre-condition: + + &TODO; + + + + Action: + + &TODO; + + + + New sequents to prove: + + None. + + + + + + + + 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 + + + + Synopsis: + + case &id; ( &id; : &term; ) + + + + Pre-condition: + + &TODO; + + + + Action: + + &TODO; + + + + New sequents to prove: + + &TODO; + + + + + + + + obtain/conclude + obtain/conclude + obtain H t=t [auto_params | exact t| proof | using t] done + + + + Synopsis: + + [obtain &id; | conclude &term;] = &term; [&autoparams; | exact &term; | using &term; | proof] [done] + + + + Pre-condition: + + &TODO; + + + + Action: + + &TODO; + + + + New sequence to prove: + + &TODO; + + + + + + + + by term we proved + by term we proved + by th we proved t [""|(id)] + + + + Synopsis: + + by &term; we proved &term; + ( &id; ) + + + + Pre-condition: + + thmust have type Prop. + idcan to be omitted with null + + + + Action: + + It closes the current sequent by applyingth to t. + + + + New sequence to prove: + + &TODO; + + + + + + + + exits elim + exits elim + by t let id:t such that t (id) + + + + 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 + + + + New sequence to prove: + + It opens one new sequent. The names of the new hypotheses are picked byt (id) + + + + + + + + and elim + and elim + by t we have t (id) and t (id) + + + + Synopsis: + + by &term; we have &term; + ( &id; ) and &term; + ( &id; ) + + + + Pre-condition: + + t must be an logical type,type and + + + + Action: + + It proceeds on the values of t, according to the elimination principle + + + + New sequence to prove: + + It opens one new sequent, the names of the new hypotheses are picked by t(id) and t(id) + + + + + + +