From: Claudio Sacerdoti Coen Date: Fri, 18 Nov 2011 14:31:39 +0000 (+0000) Subject: For release 0.99.1. X-Git-Tag: make_still_working~2091 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=8f699ab265e380a2d1ab7dba0ee5e8ba5556a84a For release 0.99.1. --- diff --git a/matita/matita/help/C/declarative_tactics_quickref.xml b/matita/matita/help/C/declarative_tactics_quickref.xml index 002a7a376..1f16a4725 100644 --- a/matita/matita/help/C/declarative_tactics_quickref.xml +++ b/matita/matita/help/C/declarative_tactics_quickref.xml @@ -1,75 +1,6 @@ tactics - - - &tactic; - ::= - assume id : sterm - - - - | - by induction hypothesis we know term ( id ) - - - - | - case id [( id : term )] … - - - - | - justification done - - - - | - justification let id - : term such that term - ( id ) - - - - | - [obtain id | conclude term] = term [auto_params | using term | using once term | proof] [done] - - - - | - suppose term ( id - ) [ that is equivalent to term ] - - - - | - the thesis becomes term - - - - | - we need to prove term - [(id - )] - [ or equivalently term] - - - - | - we proceed by cases on term to prove term - - - - | - we proceed by induction on term to prove term - - - - | - justification we proved term - ( id - ) - - +
diff --git a/matita/matita/help/C/sec_commands.xml b/matita/matita/help/C/sec_commands.xml index 7e22f3304..3deaf4b51 100644 --- a/matita/matita/help/C/sec_commands.xml +++ b/matita/matita/help/C/sec_commands.xml @@ -60,7 +60,7 @@ Synopsis: - check &term; + check &sterm; @@ -74,6 +74,7 @@ + + coercion + TODO + + + include include "s" @@ -323,6 +334,7 @@ + + qed qed @@ -401,7 +416,33 @@ + + qed- + qed- + + + + Synopsis: + + qed- + + + + + Action: + + Saves the current interactive theorem or + definition without indexing. Therefore automation will ignore + it. + In order to do this, the set of sequents still to be proved + must be empty. + + + + + + diff --git a/matita/matita/help/C/sec_declarative_tactics.xml b/matita/matita/help/C/sec_declarative_tactics.xml index bc0b424e0..d77c276c4 100644 --- a/matita/matita/help/C/sec_declarative_tactics.xml +++ b/matita/matita/help/C/sec_declarative_tactics.xml @@ -1,4 +1,5 @@ + diff --git a/matita/matita/help/C/sec_gettingstarted.xml b/matita/matita/help/C/sec_gettingstarted.xml index e18f3a067..9679dcfd2 100644 --- a/matita/matita/help/C/sec_gettingstarted.xml +++ b/matita/matita/help/C/sec_gettingstarted.xml @@ -76,6 +76,7 @@ "about:proof". + Authoring diff --git a/matita/matita/help/C/sec_install.xml b/matita/matita/help/C/sec_install.xml index 92e9d62cc..23c690081 100644 --- a/matita/matita/help/C/sec_install.xml +++ b/matita/matita/help/C/sec_install.xml @@ -288,6 +288,7 @@ + + @@ -325,6 +329,7 @@ + @@ -360,6 +366,7 @@ + @@ -429,6 +437,7 @@ + Compiling and installing @@ -499,9 +509,10 @@ + @@ -551,6 +563,7 @@ installs &appname; related tools, standard library and the needed runtime stuff in the proper places on the filesystem. + @@ -569,6 +582,7 @@ + diff --git a/matita/matita/help/C/sec_intro.xml b/matita/matita/help/C/sec_intro.xml index 6c22f4664..19a504c2d 100644 --- a/matita/matita/help/C/sec_intro.xml +++ b/matita/matita/help/C/sec_intro.xml @@ -26,28 +26,33 @@ of the art. In particular: An on-line help can be browsed via the Gnome documentation browser. - Mathematical formulae are rendered in two dimensional notation via MathML and Unicode. + + Mathematical formulae are rendered via Unicode. + It allows the use of the typical ambiguous mathematical notation by means of a disambiguating parser. + Matita vs Coq The system shares a common look&feel with the Coq proof assistant - and its graphical user interface. The two systems have the same logic, - very close proof languages and similar sets of tactics. Moreover, - Matita is compatible with the library of Coq. + and its graphical user interface. The two systems have variants + of the same logic, + close proof languages and similar sets of tactics. From the user point of view the main lacking features with respect to Coq are: @@ -68,7 +73,7 @@ of the art. In particular: several rarely used variants for most of the tactics; - sections and local variables. To maintain compatibility with the library of Coq, theorems defined inside sections are abstracted by name over the section variables; their instances are explicitly applied to actual arguments by means of explicit named substitutions. + sections and local variables. diff --git a/matita/matita/help/C/sec_tactics.xml b/matita/matita/help/C/sec_tactics.xml index ebd100a26..4687868ad 100644 --- a/matita/matita/help/C/sec_tactics.xml +++ b/matita/matita/help/C/sec_tactics.xml @@ -10,51 +10,16 @@ - - absurd - absurd - absurd P - - - - Synopsis: - - absurd &sterm; - - - - Pre-conditions: - - P must have type Prop. - - - - Action: - - It closes the current sequent by eliminating an - absurd term. - - - - New sequents to prove: - - It opens two new sequents of conclusion P - and ¬P. - - - - - - apply - apply - apply t + @ + @ + @t Synopsis: - apply &sterm; + @ &sterm; @@ -86,203 +51,163 @@ - - applyS - applyS - applyS t auto_params + + // + // + /params/ Synopsis: - applyS &sterm; &autoparams; + /&autoparams;/. + Pre-conditions: - t must have type - T1 → ... → - Tn → G. + None, but the tactic may fail finding a proof if every + proof is in the search space that is pruned away. Pruning is + controlled by the optional params. + Moreover, only lemmas whose type signature is a subset of the + signature of the current sequent are considered. The signature of + a sequent is essentially the set of constats appearing in it. + 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). - The auto_params parameters are passed - directly to auto paramodulation. - + It closes the current sequent by repeated application of + rewriting steps (unless paramodulation is + omitted), hypothesis and lemmas in the library. 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. + None - - assumption - assumption - assumption + + # + # + #H Synopsis: - assumption + #&id; Pre-conditions: - There must exist an hypothesis whose type can be unified with - the conclusion of the current sequent. + The conclusion of the sequent to prove must be an implication + or a universal quantification. Action: - It closes the current sequent exploiting an hypothesis. + It applies the right introduction rule for implication, + closing the current sequent. New sequents to prove: - None + It opens a new sequent to prove adding to the hypothesis + the antecedent of the implication and setting the conclusion + to the consequent of the implicaiton. The name of the new + hypothesis is H. - - auto - auto - auto params + + #_ + #_ + #_ Synopsis: - auto &autoparams;. - autobatch &autoparams; + #_ Pre-conditions: - None, but the tactic may fail finding a proof if every - proof is in the search space that is pruned away. Pruning is - controlled by the optional params. - Moreover, only lemmas whose type signature is a subset of the - signature of the current sequent are considered. The signature of - a sequent is essentially the set of constats appearing in it. - + The conclusion of the sequent to prove must be an implication. + Action: - It closes the current sequent by repeated application of - rewriting steps (unless paramodulation is - omitted), hypothesis and lemmas in the library. + It applies the ``a fortiori'' rule for implication, + closing the current sequent. New sequents to prove: - None + It opens a new sequent whose conclusion is the conclusion + of the implication of the original sequent. - - cases - cases - - cases t pattern hyps - + + ## + ## + ## Synopsis: - - cases - &term; &pattern; [([&id;]…)] - + ## Pre-conditions: - - t must inhabit an inductive type - + None. Action: - - It proceed by cases on t. The new generated - hypothesis in each branch are named according to - hyps. - The elimintation predicate is restricted by - pattern. In particular, if some hypothesis - is listed in pattern, the hypothesis is - generalized and cleared before proceeding by cases on - t. Currently, we only support patterns of the - form H1 … Hn ⊢ %. This limitation will be lifted in the future. - - - - - New sequents to prove: - - One new sequent for each constructor of the type of - t. Each sequent has a new hypothesis for - each argument of the constructor. + This macro expands to the longest possible list of + #Hi tactics. The + names of the introduced hypotheses are automatically + generated. - clear - clear - - clear H1 ... Hm - + - + - + -H Synopsis: - clear - &id; [&id;…] + -&id; @@ -290,9 +215,7 @@ Pre-conditions: - - H1 ... Hm - must be hypotheses of the + H must be an hypothesis of the current sequent to prove. @@ -301,10 +224,8 @@ Action: - It hides the hypotheses - - H1 ... Hm - from the current sequent. + It hides the hypothesis H + from the current sequent. @@ -317,876 +238,228 @@ - - clearbody - clearbody - clearbody H + + % + % + %n {args} Synopsis: - clearbody &id; + % [&nat;] [{&sterm;…}] Pre-conditions: - H must be an hypothesis of the - current sequent to prove. + The conclusion of the current sequent must be + an inductive type or the application of an inductive type with + at least n constructors. Action: - It hides the definiens of a definition in the current - sequent context. Thus the definition becomes an hypothesis. + It applies the n-th constructor of the + inductive type of the conclusion of the current sequent to + the arguments args. + If n is omitted, it defaults to 1. New sequents to prove: - None. + It opens a new sequent for each premise of the constructor + that can not be inferred by unification. For more details, + see the apply tactic. - - compose - compose - compose n t1 with t2 hyps + + * + * + + * as H + Synopsis: - compose [&nat;] &sterm; [with &sterm;] [&intros-spec;] + + * + [as &id;] + Pre-conditions: - + The current conclusion must be of the form + T → G where I is + an inductive type applied to its arguments, if any. Action: - Composes t1 with t2 in every possible way - n times introducing generated terms - as if intros hyps was issued. - If t1:∀x:A.B[x] and - t2:∀x,y:A.B[x]→B[y]→C[x,y] it generates: - - - λx,y:A.t2 x y (t1 x) : ∀x,y:A.B[y]→C[x,y] - - - λx,y:A.λH:B[x].t2 x y H (t1 y) : ∀x,y:A.B[x]→C[x,y] - - - - - If t2 is omitted it composes - t1 - with every hypothesis that can be introduced. - n iterates the process. + + It introduces a new hypothesis H of type + T. Then it proceeds by cases over + H. Finally, if the name H + is not specified, it clears the new hypothesis from all contexts. + New sequents to prove: - The same, but with more hypothesis eventually introduced - by the &intros-spec;. + + The ones generated by case analysis. + - - change - change - change patt with t + + > + > + > p patt Synopsis: - change &pattern; with &sterm; + [<|>] &sterm; &pattern; Pre-conditions: - Each subterm matched by the pattern must be convertible - with the term t disambiguated in the context - of the matched subterm. + p must be the proof of an equality, + possibly under some hypotheses. Action: - It replaces the subterms of the current sequent matched by - patt with the new term t. - For each subterm matched by the pattern, t is - disambiguated in the context of the subterm. + It looks in every term matched by patt + for all the occurrences of the + left hand side of the equality that p proves + (resp. the right hand side if < is used). + Every occurence found is replaced with + the opposite side of the equality. New sequents to prove: - None. + It opens one new sequent for each hypothesis of the + equality proved by p that is not closed + by unification. - - constructor - constructor - constructor n + + applyS + applyS + applyS t auto_params Synopsis: - constructor &nat; + applyS &sterm; &autoparams; Pre-conditions: - The conclusion of the current sequent must be - an inductive type or the application of an inductive type with - at least n constructors. + t must have type + T1 → ... → + Tn → G. Action: - It applies the n-th constructor of the - inductive type of the conclusion of the current sequent. + 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). + The auto_params parameters are passed + directly to auto paramodulation. + New sequents to prove: - It opens a new sequent for each premise of the constructor - that can not be inferred by unification. For more details, - see the apply tactic. - - - - - - - contradiction - contradiction - contradiction - - - - Synopsis: - - contradiction - - - - Pre-conditions: - - There must be in the current context an hypothesis of type - False. - - - - Action: - - It closes the current sequent by applying an hypothesis of - type False. - - - - New sequents to prove: - - None - - - - - - - cut - cut - cut P as H - - - - Synopsis: - - cut &sterm; [as &id;] - - - - Pre-conditions: - - P must have type Prop. - - - - Action: - - It closes the current sequent. - - - - New sequents to prove: - - It opens two new sequents. The first one has an extra - hypothesis H:P. If H is - omitted, the name of the hypothesis is automatically generated. - The second sequent has conclusion P and - hypotheses the hypotheses of the current sequent to prove. - - - - - - - decompose - decompose - - decompose as H1 ... Hm - - - - - Synopsis: - - - decompose - [as &id;…] - - - - - Pre-conditions: - - None. - - - - Action: - - - For each each premise H of type - T in the current context where - T is a non-recursive inductive type without - right parameters and of sort Prop or CProp, the tactic runs - - elim H as H1 ... Hm - , clears H and runs itself - recursively on each new premise introduced by - elim in the opened sequents. - - - - - New sequents to prove: - - - The ones generated by all the elim tactics run. - - - - - - - - demodulate - demodulate - demodulate auto_params - - - - Synopsis: - - demodulate &autoparams; - - - - Pre-conditions: - - None. - - - - Action: - - &TODO; - - - - New sequents to prove: - - None. - - - - - - - destruct - destruct - destruct p - - - - Synopsis: - - destruct &sterm; - - - - Pre-conditions: - - p must have type E1 = E2 where the two sides of the equality are possibly applied constructors of an inductive type. - - - - Action: - - 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. - - - - - New sequents to prove: - - None. - - - - - - - elim - elim - elim t pattern using th hyps - - - - Synopsis: - - elim &sterm; &pattern; [using &sterm;] &intros-spec; - - - - Pre-conditions: - - t must inhabit an inductive type and - th must be an elimination principle for that - inductive type. If th is omitted the appropriate - standard elimination principle is chosen. - - - - Action: - - It proceeds by cases on the values of t, - according to the elimination principle th. - The induction predicate is restricted by - pattern. In particular, if some hypothesis - is listed in pattern, the hypothesis is - generalized and cleared before eliminating t - - - - - New sequents to prove: - - It opens one new sequent for each case. The names of - the new hypotheses are picked by hyps, if - provided. If hyps specifies also a number of hypotheses that - is less than the number of new hypotheses for a new sequent, - then the exceeding hypothesis will be kept as implications in - the conclusion of the sequent. - - - - - - - elimType - elimType - elimType T using th hyps - - - - Synopsis: - - elimType &sterm; [using &sterm;] &intros-spec; - - - - Pre-conditions: - - T must be an inductive type. - - - - Action: - - TODO (severely bugged now). - - - - New sequents to prove: - - TODO - - - - - - - exact - exact - exact p - - - - Synopsis: - - exact &sterm; - - - - Pre-conditions: - - The type of p must be convertible - with the conclusion of the current sequent. - - - - Action: - - It closes the current sequent using p. - - - - New sequents to prove: - - None. - - - - - - - exists - exists - exists - - - - Synopsis: - - exists - - - - Pre-conditions: - - The conclusion of the current sequent must be - an inductive type or the application of an inductive type - with at least one constructor. - - - - Action: - - Equivalent to constructor 1. - - - - New sequents to prove: - - It opens a new sequent for each premise of the first - constructor of the inductive type that is the conclusion of the - current sequent. For more details, see the constructor tactic. - - - - - - - fail - fail - fail - - - - Synopsis: - - fail - - - - Pre-conditions: - - None. - - - - Action: - - This tactic always fail. - - - - New sequents to prove: - - N.A. - - - - - - - fold - fold - fold red t patt - - - - Synopsis: - - fold &reduction-kind; &sterm; &pattern; - - - - Pre-conditions: - - The pattern must not specify the wanted term. - - - - Action: - - First of all it locates all the subterms matched by - patt. In the context of each matched subterm - it disambiguates the term t and reduces it - to its red normal form; then it replaces with - t every occurrence of the normal form in the - matched subterm. - - - - New sequents to prove: - - None. - - - - - - - fourier - fourier - fourier - - - - Synopsis: - - fourier - - - - Pre-conditions: - - The conclusion of the current sequent must be a linear - inequation over real numbers taken from standard library of - Coq. Moreover the inequations in the hypotheses must imply the - inequation in the conclusion of the current sequent. - - - - Action: - - It closes the current sequent by applying the Fourier method. - - - - New sequents to prove: - - None. - - - - - - - fwd - fwd - fwd H as H0 ... Hn - - - - Synopsis: - - fwd &id; [as &id; [&id;]…] - - - - Pre-conditions: - - - The type of H must be the premise of a - forward simplification theorem. - - - - - Action: - - - This tactic is under development. - It simplifies the current context by removing - H using the following methods: - forward application (by lapply) of a suitable - simplification theorem, chosen automatically, of which the type - of H is a premise, - decomposition (by decompose), - rewriting (by rewrite). - H0 ... Hn - are passed to the tactics fwd invokes, as - names for the premise they introduce. - - - - - New sequents to prove: - - - The ones opened by the tactics fwd invokes. - - - - - - - - generalize - generalize - generalize patt as H - - - - Synopsis: - - generalize &pattern; [as &id;] - - - - Pre-conditions: - - All the terms matched by patt must be - convertible and close in the context of the current sequent. - - - - Action: - - It closes the current sequent by applying a stronger - lemma that is proved using the new generated sequent. - - - - New sequents to prove: - - It opens a new sequent where the current sequent conclusion - G is generalized to - ∀x.G{x/t} where {x/t} - is a notation for the replacement with x of all - the occurrences of the term t matched by - patt. If patt matches no - subterm then t is defined as the - wanted part of the pattern. - - - - - - - id - id - id - - - - Synopsis: - - id - - - - Pre-conditions: - - None. - - - - Action: - - This identity tactic does nothing without failing. - - - - New sequents to prove: - - None. - - - - - - - intro - intro - intro H - - - - Synopsis: - - intro [&id;] - - - - Pre-conditions: - - The conclusion of the sequent to prove must be an implication - or a universal quantification. - - - - Action: - - It applies the right introduction rule for implication, - closing the current sequent. - - - - New sequents to prove: - - It opens a new sequent to prove adding to the hypothesis - the antecedent of the implication and setting the conclusion - to the consequent of the implicaiton. The name of the new - hypothesis is H if provided; otherwise it - is automatically generated. - - - - - - - intros - intros - intros hyps - - - - Synopsis: - - intros &intros-spec; - - - - Pre-conditions: - - If hyps specifies a number of hypotheses - to introduce, then the conclusion of the current sequent must - be formed by at least that number of imbricated implications - or universal quantifications. - - - - Action: - - It applies several times the right introduction rule for - implication, closing the current sequent. - - - - New sequents to prove: - - It opens a new sequent to prove adding a number of new - hypotheses equal to the number of new hypotheses requested. - If the user does not request a precise number of new hypotheses, - it adds as many hypotheses as possible. - The name of each new hypothesis is either popped from the - user provided list of names, or it is automatically generated when - the list is (or becomes) empty. + 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. - - inversion - inversion - inversion t + + assumption + assumption + assumption Synopsis: - inversion &sterm; + assumption Pre-conditions: - The type of the term t must be an inductive - type or the application of an inductive type. + There must exist an hypothesis whose type can be unified with + the conclusion of the current sequent. Action: - It proceeds by cases on t paying attention - to the constraints imposed by the actual "right arguments" - of the inductive type. + It closes the current sequent exploiting an hypothesis. New sequents to prove: - It opens one new sequent to prove for each case in the - definition of the type of t. With respect to - a simple elimination, each new sequent has additional hypotheses - that states the equalities of the "right parameters" - of the inductive type with terms originally present in the - sequent to prove. + None - - lapply - lapply + + cases + cases - lapply linear depth=d t - to t1, ..., tn as H + cases t pattern @@ -1194,15 +467,8 @@ Synopsis: - lapply - [linear] - [depth=&nat;] - &sterm; - [to - &sterm; - [,&sterm;…] - ] - [as &id;] + cases + &term; &pattern; @@ -1210,9 +476,7 @@ Pre-conditions: - t must have at least d - independent premises and n must not be - greater than d. + t must inhabit an inductive type @@ -1220,131 +484,147 @@ Action: - Invokes letin H ≝ (t ? ... ?) - with enough ?'s to reach the - d-th independent premise of - t - (d is maximum if unspecified). - Then istantiates (by apply) with - t1, ..., tn - the ?'s corresponding to the first - n independent premises of - t. - 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. + It proceed by cases on t. The new generated + hypothesis in each branch are named according to + hyps. + The elimintation predicate is restricted by + pattern. In particular, if some hypothesis + is listed in pattern, the hypothesis is + generalized and cleared before proceeding by cases on + t. Currently, we only support patterns of the + form H1 … Hn ⊢ %. This limitation will be lifted in the future. New sequents to prove: - - The ones opened by the tactics lapply invokes. - + One new sequent for each constructor of the type of + t. Each sequent has a new hypothesis for + each argument of the constructor. - - left - left - left + + + + change + change + change patt with t Synopsis: - normalize &pattern; + change &pattern; with &sterm; Pre-conditions: - None. + Each subterm matched by the pattern must be convertible + with the term t disambiguated in the context + of the matched subterm. Action: - It replaces all the terms matched by patt - with their βδιζ-normal form. + It replaces the subterms of the current sequent matched by + patt with the new term t. + For each subterm matched by the pattern, t is + disambiguated in the context of the subterm. @@ -1356,51 +636,54 @@ - - reflexivity - reflexivity - reflexivity + + cut + cut + cut P Synopsis: - reflexivity + cut &sterm; Pre-conditions: - The conclusion of the current sequent must be - t=t for some term t + P must be a type. Action: - It closes the current sequent by reflexivity - of equality. + It closes the current sequent. New sequents to prove: - None. + It opens two new sequents. The first one has conclusion + P → G where G is the + old conclusion. + The second sequent has conclusion P and + hypotheses the hypotheses of the current sequent to prove. - - replace - change - change patt with t + + + destruct + destruct + destruct (H0 ... Hn) skip (K0 ... Km) Synopsis: - rewrite [<|>] &sterm; &pattern; + destruct + [(&id;…)] [skip (&id;…)] Pre-conditions: - p must be the proof of an equality, - possibly under some hypotheses. + Each hypothesis Hi must be either a Leibniz or a John Major equality where the two sides of the equality are possibly applied constructors of an inductive type. Action: - It looks in every term matched by patt - for all the occurrences of the - left hand side of the equality that p proves - (resp. the right hand side if dir is - <). Every occurence found is replaced with - the opposite side of the equality. + The tactic recursively compare the two sides of each 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. If the newly + added hypothesis is an equality between a variable and a term, + the variable is substituted for the term everywhere in the + sequent, except for the hypotheses Kj, and it is then cleared from the list of hypotheses. + New sequents to prove: - It opens one new sequent for each hypothesis of the - equality proved by p that is not closed - by unification. + None. - - right - right - right + + elim + elim + elim t pattern Synopsis: - right + elim &sterm; &pattern; Pre-conditions: - The conclusion of the current sequent must be - an inductive type or the application of an inductive type with - at least two constructors. + t must inhabit an inductive type. + Action: - Equivalent to constructor 2. + It proceeds by cases on the values of t, + according to the most appropriate elimination principle for + the current goal. + The induction predicate is restricted by + pattern. In particular, if some hypothesis + is listed in pattern, the hypothesis is + generalized and cleared before eliminating t + New sequents to prove: - It opens a new sequent for each premise of the second - constructor of the inductive type that is the conclusion of the - current sequent. For more details, see the constructor tactic. + It opens one new sequent for each case. - - ring - ring - ring + + + generalize + generalize + generalize patt Synopsis: - simplify &pattern; + generalize &pattern; Pre-conditions: - None. + All the terms matched by patt must be + convertible and close in the context of the current sequent. Action: - It replaces all the terms matched by patt - with other convertible terms that are supposed to be simpler. + It closes the current sequent by applying a stronger + lemma that is proved using the new generated sequent. New sequents to prove: - None. + It opens a new sequent where the current sequent conclusion + G is generalized to + ∀x.G{x/t} where {x/t} + is a notation for the replacement with x of all + the occurrences of the term t matched by + patt. If patt matches no + subterm then t is defined as the + wanted part of the pattern. - - split - split - split + + + inversion + inversion + inversion t Synopsis: - subst + inversion &sterm; Pre-conditions: - - None. - + + The type of the term t must be an inductive + type or the application of an inductive type. + 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. - + + It proceeds by cases on t paying attention + to the constraints imposed by the actual "right arguments" + of the inductive type. + New sequents to prove: - - The one opened by the applied tactics. - + + It opens one new sequent to prove for each case in the + definition of the type of t. With respect to + a simple elimination, each new sequent has additional hypotheses + that states the equalities of the "right parameters" + of the inductive type with terms originally present in the + sequent to prove. It uses either Leibniz or John Major equality + for the new hypotheses, according to the included files. + - - symmetry - symmetry - The tactic symmetry - symmetry + + lapply + lapply + + lapply t + Synopsis: - symmetry + + lapply + &sterm; + Pre-conditions: - The conclusion of the current proof must be an equality. + None. Action: - It swaps the two sides of the equalityusing the symmetric - property. + + It generalizes the conclusion of the current goal + adding as a premise the type of t, + closing the current goal. + New sequents to prove: - None. + + The new sequent has conclusion T → G where + T is the type of t + and G the old conclusion. + - - transitivity - transitivity - transitivity t + + letin + letin + letin x ≝ t Synopsis: - transitivity &sterm; + letin &id; ≝ &sterm; Pre-conditions: - The conclusion of the current proof must be an equality. + None. Action: - It closes the current sequent by transitivity of the equality. + It adds to the context of the current sequent to prove a new + definition x ≝ t. New sequents to prove: - It opens two new sequents l=t and - t=r where l and r are the left and right hand side of the equality in the conclusion of -the current sequent to prove. + None. - - unfold - unfold - unfold t patt + + normalize + normalize + normalize patt nodelta Synopsis: - unfold [&sterm;] &pattern; + normalize &pattern; + [nodelta] @@ -1746,12 +1049,9 @@ the current sequent to prove. Action: - It finds all the occurrences of t - (possibly applied to arguments) in the subterms matched by - patt. Then it δ-expands each occurrence, - also performing β-reduction of the obtained term. If - t is omitted it defaults to each - subterm matched by patt. + It replaces all the terms matched by patt + with their βδιζ-normal form. If nodelta is + specified, δ-expansions are not performed. @@ -1766,13 +1066,13 @@ the current sequent to prove. whd whd - whd patt + whd patt nodelta Synopsis: - whd &pattern; + whd &pattern; [nodelta] @@ -1785,7 +1085,7 @@ the current sequent to prove. Action: It replaces all the terms matched by patt - with their βδιζ-weak-head normal form. + with their βδιζ-weak-head normal form. If nodelta is specified, δ-expansions are not performed. diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml index a1353b2f0..8e680bb7c 100644 --- a/matita/matita/help/C/sec_terms.xml +++ b/matita/matita/help/C/sec_terms.xml @@ -524,13 +524,15 @@ P. Otherwise an interactive proof is started. P can be omitted only if the proof is not interactive. + A warning is raised if the name of the theorem cannot be obtained by mangling the name of the constants in its thesis. Notice that the command is equivalent to definition f: T ≝ t. + + + <emphasis role="bold">corollary</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] + corollary + corollary f: T ≝ t + Same as theorem f: T ≝ t <emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] @@ -551,11 +559,12 @@ fact f: T ≝ t Same as theorem f: T ≝ t - - <emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] - remark - remark f: T ≝ t - Same as theorem f: T ≝ t + + <emphasis role="bold">example</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] + example + example f: T ≝ t + Same as theorem f: T ≝ t, but the example + is not indexed nor used by automation. @@ -564,6 +573,7 @@ This section documents the syntax of some recurring arguments for tactics. + pattern @@ -590,18 +601,18 @@ &pattern; ::= - in + { [&id;[: &path;]]… - [⊢ &path;]] + [⊢ &path;]]} simple pattern | - in match &path; + {match &path; [in [&id;[: &path;]]… - [⊢ &path;]] + [⊢ &path;]]} full pattern @@ -657,7 +668,7 @@ A simple pattern extends paths to locate subterms in a whole sequent. In particular, the pattern - in H: p K: q ⊢ r locates at once all the subterms + { H: p K: q ⊢ r } locates at once all the subterms located by the pattern r in the conclusion of the sequent and by the patterns p and q in the hypotheses H @@ -684,11 +695,11 @@ A full pattern can always be replaced by a simple pattern, often at the cost of increased verbosity or decreased readability. Example: the pattern - ⊢ in match x+y in ∀_,_:?.(? ? % ?) + { match x+y in ⊢ ∀_,_:?.(? ? % ?) } locates only the first occurrence of x+y in the sequent x,y: nat ⊢ ∀z,w:nat. (x+y) * (z+w) = z * (x+y) + w * (x+y). The corresponding simple pattern - is ⊢ ∀_,_:?.(? ? (? % ?) ?). + is { ⊢ ∀_,_:?.(? ? (? % ?) ?) }. Every tactic that acts on subterms of the selected sequents have a pattern argument for uniformity. To automatically generate a simple @@ -716,27 +727,16 @@ &reduction-kind; ::= - normalize - Computes the βδιζ-normal form - - - - | - simplify - Computes a form supposed to be simpler - - - - | - unfold [&sterm;] - δ-reduces the constant or variable if specified, or that - in head position + normalize [nodelta] + Computes the βδιζ-normal form. If nodelta + is specified, δ-expansions are not performed. | - whd - Computes the βδιζ-weak-head normal form + whd [nodelta] + Computes the βδιζ-weak-head normal form. If nodelta + is specified, δ-expansions are not performed. @@ -815,6 +815,7 @@ +