X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=11b06b21cab7269c8bd3bd2867ed8bc48b31f1c5;hb=21f2ca1e83578359d9ab6926d466a4645049ee76;hp=dd2af7f5fe09596c922865c7f25e456cefb29de2;hpb=26778a467329055d706f9b8d9d6869f17186e453;p=helm.git diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index dd2af7f5f..11b06b21c 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -5,65 +5,111 @@ Syntax To describe syntax in this manual we use the following conventions: - Non terminal symbols are emphasized and have a link to their definition. E.g.: &term; - Terminal symbols are in bold. E.g.: theorem - Optional sequences of elements are put in square brackets. - E.g.: [in &term;] - Alternatives are put in square brakets and they are separated - by vertical bars. E.g.: [<|>] - Repetition of sequences of elements are given by putting the - first sequence in square brackets, that are followed by three dots. - E.g.: [and &term;]… + Non terminal symbols are emphasized and have a link to their + definition. E.g.: &term; + Terminal symbols are in bold. E.g.: + theorem + Optional sequences of elements are put in square brackets. + E.g.: [in &term;] + Alternatives are put in square brakets and they are + separated by vertical bars. E.g.: [<|>] + Repetitions of a sequence of elements are given by putting the + 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 - - - - - - &id; - ::= - 〈〈&TODO;〉〉 - - - -
- - - - - - &nat; - ::= - 〈〈&TODO;〉〉 - - - -
- - - - - - &uri; - ::= - 〈〈&TODO;〉〉 - - - -
+ + 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 ([?'`])〉〉 + + + +
+ + nat + + + + &nat; + ::= + 〈〈any sequence of valid XML digits〉〉 + + + +
+ + char + + + + &char; + ::= + [a-zA-Z0-9_-] + + + +
+ + uri-step + + + + &uri-step; + ::= + &char;[&char;]… + + + +
+ + uri + + + + &uri; + ::= + [cic:/|theory:/]&uri-step;[/&uri-step;]….&id;[.&id;]…[#xpointer(&nat;/&nat;[/&nat;]…)] + + + +
Terms - - - + + + + + +
+ Terms + - &term; + &term; ::= &sterm; simple or delimited term @@ -107,11 +153,10 @@ | - let - [co]rec - &id; [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] - [: &term;] - ≝ &term; + + let + [co]rec + &rec_def; (co)recursive definitions @@ -119,10 +164,7 @@ - [and - [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] - [: &term;] - ≝ &term;]… + [and &rec_def;]… @@ -140,16 +182,34 @@ …user provided notation + + &rec_def; + ::= + + &id; [&id;|(&id;[,&term;]… :&term;)]… + + + + + + + + [on &nat;] + [: &term;] + ≝ &term;] + + +
- - - +
+ Simple terms + - &sterm; + &sterm; ::= (&term;) @@ -218,11 +278,9 @@ [ - &match_pattern; ⇒ &term; - [ - | - &match_pattern; ⇒ &term; - ]…] + &match_branch;[|&match_branch;]… + ] + @@ -241,12 +299,12 @@
- - - +
+ Arguments + - &args; + &args; ::= _[: &term;] @@ -273,16 +331,34 @@ (&id;[,&id;]…[: &term;]) + + &args2; + ::= + &id; + + + + + | + (&id;[,&id;]…: &term;) + +
- - - +
+ Pattern matching + - - &match_pattern; + + &match_branch; + ::= + &match_pattern; ⇒ &term; + + + + &match_pattern; ::= &id; 0-ary constructor @@ -296,6 +372,7 @@
+ @@ -303,13 +380,13 @@ Definitions and declarations - axiom &id;: &term; + <emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term; axiom axiom H: P H is declared as an axiom that states P - definition &id;[: &term;] [≝ &term;] + <emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] definition definition f: T ≝ t f is defined as t; @@ -323,16 +400,63 @@ Notice that the command is equivalent to theorem f: T ≝ t. - [co]inductive &id; (of inductive types) + [<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;]…]… + (co)inductive types declaration - &TODO; + inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm' + Declares a family of two mutually inductive types + i and i' whose types are + S and S', which must be convertible + to sorts. + The constructors ki of type Ti + and ki' of type Ti' are also + simultaneously declared. The declared types i and + i' may occur in the types of the constructors, but + only in strongly positive positions according to the rules of the + calculus. + The whole family is parameterized over the arguments x,y,z. + If the keyword coinductive is used, the declared + types are considered mutually coinductive. + Elimination principles for the record are automatically generated + by Matita, if allowed by the typing rules of the calculus according to + the sort S. If generated, + they are named i_ind, i_rec and + i_rect according to the sort of their induction + predicate. + + + <emphasis role="bold">record</emphasis> &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis><emphasis role="bold">{</emphasis>[&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:></emphasis>] &term;]…<emphasis role="bold">}</emphasis> + record + record id x y z: S ≝ { f1: T1; …; fn:Tn } + Declares a new record family id parameterized over + x,y,z. + S is the type of the record + and it must be convertible to a sort. + Each field fi is declared by giving its type + Ti. A record without any field is admitted. + Elimination principles for the record are automatically generated + by Matita, if allowed by the typing rules of the calculus according to + the sort S. If generated, + they are named i_ind, i_rec and + i_rect according to the sort of their induction + predicate. + For each field fi a record projection + fi is also automatically generated if projection + is allowed by the typing rules of the calculus according to the + sort S, the type T1 and + the definability of depending record projections. + If the type of a field is declared with :>, + the corresponding record projection becomes an implicit coercion. + This is just syntactic sugar and it has the same effect of declaring the + record projection as a coercion later on. Proofs - theorem &id;[: &term;] [≝ &term;] + <emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] theorem theorem f: P ≝ p Proves a new theorem f whose thesis is @@ -349,7 +473,7 @@ Notice that the command is equivalent to definition f: T ≝ t. - variant &id;[: &term;] [≝ &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 @@ -357,24 +481,114 @@ an alternative name or proof to a theorem. - lemma &id;[: &term;] [≝ &term;] + <emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] lemma lemma f: T ≝ t Same as theorem f: T ≝ t - fact &id;[: &term;] [≝ &term;] + <emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;] fact fact f: T ≝ t Same as theorem f: T ≝ t - remark &id;[: &term;] [≝ &term;] + <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 + + 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; + ::= + &TODO; + + + +
+ &TODO; + + + + 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; + ::= + demodulate + + + + | + 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 + + + +
+ + +