X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_terms.xml;h=05385f666b3a41ad4267a1977c0e8c8dac9aa4d5;hb=a3f4c0a8b4328cb9a9fe3b4c2e577be2a258675c;hp=f7991374cbb754a8ff0b0cfe3f7ae673c1946938;hpb=5fbdf01e49ca301b3dbf1ddb3c4e358d8189e45c;p=helm.git diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index f7991374c..05385f666 100644 --- a/matita/help/C/sec_terms.xml +++ b/matita/help/C/sec_terms.xml @@ -17,83 +17,111 @@ sequence in square brackets, that are followed by three dots. The empty sequence is a valid repetition. E.g.: [and &term;]… + Characters belonging to a set of characters are given + by listing the set elements in square brackets. Hyphens are used to + specify ranges of characters in the set. + E.g.: [a-zA-Z0-9_-] Terms & co. Lexical conventions - - +
+ qstring + + + + &qstring; + ::= + "〈〈any sequence of characters excluded "〉〉" + + + +
+ id - &id; + &id; ::= - 〈〈any sequence of letters, underscores or valid XML digits prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉 + 〈〈any sequence of letters, underscores or valid XML digits prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉
- +
nat - &nat; + &nat; ::= - 〈〈any sequence of valid XML digits + 〈〈any sequence of valid XML digits〉〉
- +
char - &char; + &char; ::= [a-zA-Z0-9_-]
- +
uri-step - &uri-step; + &uri-step; ::= &char;[&char;]…
- +
uri - &uri; + &uri; ::= [cic:/|theory:/]&uri-step;[/&uri-step;]….&id;[.&id;]…[#xpointer(&nat;/&nat;[/&nat;]…)]
- Terms + + + + - +
Terms - &term; + &term; ::= &sterm; simple or delimited term @@ -137,11 +165,10 @@ | - let - [co]rec - &id; [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] - [: &term;] - ≝ &term; + + let + [co]rec + &rec_def; (co)recursive definitions @@ -149,10 +176,7 @@ - [and - [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] - [: &term;] - ≝ &term;]… + [and &rec_def;]… @@ -170,16 +194,34 @@ …user provided notation + + &rec_def; + ::= + + &id; [&id;|_|(&id;[,&id;]… :&term;)]… + + + + + + + + [on &id;] + [: &term;] + ≝ &term;] + + +
- +
Simple terms - &sterm; + &sterm; ::= (&term;) @@ -212,6 +254,12 @@ Set the impredicate sort of datatypes + + + | + CProp + one fixed predicative sort of constructive propositions + | @@ -237,7 +285,7 @@ | match &term; - [ in &term; ] + [ in &id; ] [ return &term; ] with @@ -248,11 +296,9 @@ [ - &match_pattern; ⇒ &term; - [ - | - &match_pattern; ⇒ &term; - ]…] + &match_branch;[|&match_branch;]… + ] + @@ -271,12 +317,12 @@
- +
Arguments - &args; + &args; ::= _[: &term;] @@ -303,16 +349,8 @@ (&id;[,&id;]…[: &term;]) - - -
- - - Miscellaneous arguments - - - &args2; + &args2; ::= &id; @@ -327,12 +365,18 @@
- +
Pattern matching + + &match_branch; + ::= + &match_pattern; ⇒ &term; + + - &match_pattern; + &match_pattern; ::= &id; 0-ary constructor @@ -343,6 +387,12 @@ (&id; &id; [&id;]…) n-ary constructor (binds the n arguments) + + + | + &id; &id; [&id;]… + n-ary constructor (binds the n arguments) +
@@ -373,6 +423,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;]…]… @@ -447,7 +502,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 @@ -474,5 +529,206 @@ + + Tactic arguments + This section documents the syntax of some recurring arguments for + tactics. + + + intros-spec + + intros-spec + + + + &intros-spec; + ::= + [&nat;] [([&id;]…)] + + + +
+ The natural number is the number of new hypotheses to be introduced. The list of identifiers gives the name for the first hypotheses. + + + + pattern + + pattern + + + + &pattern; + ::= + in + [&id;[: &path;]]… + [⊢ &path;]] + simple pattern + + + + | + in match &term; + [in + [&id;[: &path;]]… + [⊢ &path;]] + full pattern + + + +
+ + path + + + + &path; + ::= + 〈〈any &sterm; whithout occurrences of Set, Prop, CProp, Type, &id;, &uri; and user provided notation; however, % is now an additional production for &sterm;〉〉 + + + +
+ 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 ?. + + + 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" + + + + + reduction-kind + Reduction kinds are normalization functions that transform a term + to a convertible but simpler one. Each reduction kind can be used both + as a tactic argument and as a stand-alone tactic. + + reduction-kind + + + + &reduction-kind; + ::= + normalize + Computes the βδιζ-normal form + + + + | + reduce + 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 + + + + | + whd + Computes the βδιζ-weak-head normal form + + + +
+ + + + auto-params + &TODO; + + reduction-kind + + + + &autoparams; + ::= + depth=&nat; + &TODO; + + + + | + width=&nat; + &TODO; + + + + | + &TODO; + &TODO; + + + +
+ + +