X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=a1353b2f021aac59be2fe0896c2fbd827ab2795d;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=ab26aae4872f133d42ef74fcb32f3e389f9b32eb;hpb=ce3086647682ebfa15e9e8abaacd6e817449cea2;p=helm.git diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index ab26aae48..a1353b2f0 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -26,6 +26,18 @@ Terms & co. Lexical conventions + + qstring + + + + &qstring; + ::= + "〈〈any sequence of characters excluded "〉〉" + + + +
id @@ -86,6 +98,30 @@
+ + csymbol + + + + &csymbol; + ::= + '&id; + + + +
+ + symbol + + + + &symbol; + ::= + 〈〈None of the above〉〉 + + + +
Terms @@ -104,7 +140,7 @@ --> - +
Terms @@ -186,17 +222,19 @@ &rec_def;::= - &id; [&id;|(&id;[,&term;]… :&term;)]… + &id; [&id;|_|(&id;[,&id;]… :&term;)]… + - [on &nat;] + [on &id;] [: &term;] ≝ &term;] + @@ -240,6 +278,12 @@ Setthe impredicate sort of datatypes + + + | + CProp + one fixed predicative sort of constructive propositions + | @@ -265,7 +309,7 @@ | match &term; - [ in &term; ] + [ in &id; ] [ return &term; ] with @@ -353,6 +397,7 @@ &match_branch; ::= &match_pattern; ⇒ &term; + &match_pattern; @@ -366,6 +411,18 @@ (&id; &id; [&id;]…) n-ary constructor (binds the n arguments) + + + | + &id; &id; [&id;]… + n-ary constructor (binds the n arguments) + + + + | + _ + any remaining constructor (ignoring its arguments) +
@@ -396,6 +453,11 @@ f must be defined by means of tactics. Notice that the command is equivalent to theorem f: T ≝ t. + + <emphasis role="bold">letrec</emphasis> &TODO; + &TODO; + &TODO; + [<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]… [<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]… @@ -470,7 +532,7 @@ <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para> </sect2> <sect2 id="variant"> - <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] + <emphasis role="bold">variant</emphasis> &id;<emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> &term; variant variant f: T ≝ t Same as theorem f: T ≝ t, but it does not @@ -528,12 +590,118 @@ &pattern; ::= - &TODO; + in + [&id;[: &path;]]… + [⊢ &path;]] + simple pattern + + + + | + in match &path; + [in + [&id;[: &path;]]… + [⊢ &path;]] + full pattern + + + + + + path + + + + &path; + ::= + 〈〈any &sterm; without occurrences of Set, Prop, CProp, Type, &id;, &uri; and user provided notation; however, % is now an additional production for &sterm;〉〉
- &TODO; + A path locates zero or more subterms of a given term by mimicking the term structure up to: + + Occurrences of the subterms to locate that are + represented by %. + Subterms without any occurrence of subterms to locate + that can be represented by ?. + + + Warning: the format for a path for a match … with + expression is restricted to: match &path; + with + [ + _ + ⇒ + &path; + | … + | + _ + ⇒ + &path; + ] + Its semantics is the following: the n-th + "_ + ⇒ + &path;" branch is matched against the n-th constructor of the + inductive data type. The head λ-abstractions of &path; are matched + against the corresponding constructor arguments. + + For instance, the path + ∀_,_:?.(? ? % ?)→(? ? ? %) + locates at once the subterms + x+y and x*y in the + term ∀x,y:nat.x+y=1→0=x*y + (where the notation A=B hides the term + (eq T A B) for some type T). + + 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 + located by the pattern r in the conclusion of the + sequent and by the patterns p and + q in the hypotheses H + and K of the sequent. + + If no list of hypotheses is provided in a simple pattern, no subterm + is selected in the hypothesis. If the ⊢ p + part of the pattern is not provided, no subterm will be matched in the + conclusion if at least one hypothesis is provided; otherwise the whole + conclusion is selected. + + Finally, a full pattern is interpreted in three + steps. In the first step the match T in + part is ignored and a set S of subterms is + located as for the case of + simple patterns. In the second step the term T + is parsed and interpreted in the context of each subterm + s ∈ S. In the last term for each + s ∈ S the interpreted term T + computed in the previous step is looked for. The final set of subterms + located by the full pattern is the set of occurrences of + the interpreted T in the subterms s. + + 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 ∀_,_:?.(? ? % ?) + 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 ⊢ ∀_,_:?.(? ? (? % ?) ?). + + Every tactic that acts on subterms of the selected sequents have + a pattern argument for uniformity. To automatically generate a simple + pattern: + + Select in the current goal the subterms to pass to the + tactic by using the mouse. In order to perform a multiple selection of + subterms, hold the Ctrl key while selecting every subterm after the + first one. + From the contextual menu select "Copy". + From the "Edit" or the contextual menu select + "Paste as pattern" + @@ -548,20 +716,9 @@ &reduction-kind; ::= - demodulate - - - - | normalize Computes the βδιζ-normal form - - - | - reduce - Computes the βδιζ-normal form - | @@ -585,6 +742,101 @@ + + + auto-params + + auto-params + + + + &autoparams; + ::= + [&simpleautoparam;]… + [by + &term; [,&term;]…] + + + + +
+ + simple-auto-param + + + + &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) + + + + | + type + Try to close also goals of sort Type, otherwise only goals + living in sort Prop are attacked. + + + + + | + paramodulation + Try to close the goal performing unit-equality paramodulation + + + + + | + size=&nat; + The maximal number of nodes in the proof + + + + | + timeout=&nat; + Timeout in seconds + + + + +
+ + + + justification + + justification + + + + &justification; + ::= + using &term; + Proof term manually provided + + + + | + &autoparams; + Call automation + + + +
+