X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=dbb6900d98f9d92d17184070315b0e7adf6d42f9;hb=94188b0cbaff6340464d90cc13ee246ea7ec3284;hp=a1353b2f021aac59be2fe0896c2fbd827ab2795d;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml index a1353b2f0..dbb6900d9 100644 --- a/matita/matita/help/C/sec_terms.xml +++ b/matita/matita/help/C/sec_terms.xml @@ -453,6 +453,41 @@ f must be defined by means of tactics. Notice that the command is equivalent to theorem f: T ≝ t. + + <emphasis role="bold">discriminator</emphasis> &id; + discriminator + discriminator i + Defines a new discrimination (injectivity+conflict) principle à la + McBride for the inductive type i. + The principle will use John + Major's equality if such equality is defined, otherwise it will use + Leibniz equality; in the former case, it will be called + i_jmdiscr, in the latter, i_discr. + The command will fail if neither equality is available. + Discrimination principles are used by the destruct tactic and are + usually automatically generated by Matita during the definition of the + corresponding inductive type. This command is thus especially useful + when the correct equality was not loaded at the time of that + definition. + + + <emphasis role="bold">inverter</emphasis> &id; <emphasis role="bold">for</emphasis> &id; (&path;) [&term;] + inverter + inverter n for i (path) : s + Defines a new induction/inversion principle for the inductive type + i, called n. + (path) must be in the form (# # # ... #), + where each # can be either ? or + %, and the number of symbols is equal to the number of + right parameters (indices) of i. Parentheses are + mandatory. If the j-th symbol is + %, Matita will generate a principle providing + equations for reasoning on the j-th index of i. If the + symbol is a ?, no corresponding equation will be + provided. + s, which must be a sort, is the target sort of the + induction/inversion principle and defaults to Prop. + <emphasis role="bold">letrec</emphasis> &TODO; &TODO; @@ -524,13 +559,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 +594,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 +608,7 @@ This section documents the syntax of some recurring arguments for tactics. + pattern @@ -592,16 +638,16 @@ ::= in [&id;[: &path;]]… - [⊢ &path;]] + [⊢ &path;]]; simple pattern | - in match &path; + in match &path; [in [&id;[: &path;]]… - [⊢ &path;]] + [⊢ &path;]]; full pattern @@ -609,7 +655,7 @@ path - + &path; @@ -657,7 +703,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 +730,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 +762,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. @@ -752,9 +787,20 @@ &autoparams; ::= - [&simpleautoparam;]… + [&nat;] [&simpleautoparam;]… [by - &term; [,&term;]…] + [&sterm;… | _]] + + The natural number, which defaults to 1, gives a bound to + the depth of the search tree. The terms listed is the only + knowledge base used by automation together with all indexed factual + and equational theorems in the included library. If the list of terms + is empty, only equational theorems and facts in the library are + used. If the list is omitted, it defaults to all indexed theorems + in the library. Finally, if the list is _, + the automation command becomes a macro that is expanded in a new + automation command where _ is replaced with the + list of theorems required to prove the sequent. @@ -767,47 +813,35 @@ &simpleautoparam; ::= - depth=&nat; - Give a bound to the depth of the search tree - - - - | width=&nat; The maximal width of the search tree | - library - Search everywhere (not only in included files) + size=&nat; + The maximal number of nodes in the proof | - type - Try to close also goals of sort Type, otherwise only goals - living in sort Prop are attacked. + demod + Simplifies the current sequent using the current set of + equations known to automation | - paramodulation + paramod Try to close the goal performing unit-equality paramodulation | - size=&nat; - The maximal number of nodes in the proof - - - - | - timeout=&nat; - Timeout in seconds + fast_paramod + A bounded version of paramod that is granted to terminate quickly @@ -815,6 +849,7 @@
+