X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fhelp%2FC%2Fsec_terms.xml;h=fbf8dd4ef9cb614c7dfb52eb4c2fa80e1ab210b2;hb=8d2887c7a3e452302bf976b6303c65c3a7f7961e;hp=93dd12bef734e4fde0d5920a913935b6850529c6;hpb=9c67c1566df112f5c35d752361bd02b6a3742993;p=helm.git diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index 93dd12bef..fbf8dd4ef 100644 --- a/matita/help/C/sec_terms.xml +++ b/matita/help/C/sec_terms.xml @@ -2,115 +2,211 @@ - Terms, axioms, definitions, declarations and proofs - - + 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;]… + + + Terms & co. + + Lexical conventions + + + id + + + + &id; + ::= + 〈〈&TODO;〉〉 + + + +
+ + nat + + + + &nat; + ::= + 〈〈&TODO;〉〉 + + + +
+ + uri + + + + &uri; + ::= + 〈〈&TODO;〉〉 + + + +
+ + + Terms - - - + +
+ Terms + - &id; + &term; ::= - 〈〈&TODO;〉〉 + &sterm; + simple or delimited term - - -
- - - - - &nat; - ::= - 〈〈&TODO;〉〉 + + | + &term; &term; + application - - -
- - - - - &uri; - ::= - 〈〈&TODO;〉〉 + + | + λ&args;.&term; + λ-abstraction - - -
- - - - - &term; - ::= - &id; - identifier + + | + Π&args;.&term; + dependent product meant to define a datatype | - &uri; - a qualified reference + ∀&args;.&term; + dependent product meant to define a proposition | - Prop - the impredicative sort of propositions + &term; → &term; + non-dependent product (logical implication or function space) | - Set - the impredicate sort of datatypes + let [&id;|(&id;: &term;)] ≝ &term; in &term; + local definition | - Type - one predicatie sort of datatypes + let + [co]rec + &id; [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] + [: &term;] + ≝ &term; + + (co)recursive definitions + + + + + + [and + [&id;|(&id;[,&term;]… :&term;)]… [on &nat;] + [: &term;] + ≝ &term;]… + + + + + + + + in &term; + + | - &term; &term; - application + … + user provided notation + + + +
+ + + Simple terms + + + + &sterm; + ::= + (&term;) + | - λ&id;[: &term;].&term; - λ-abstraction + &id;[\subst[ + &id;≔&term; + [;&id;≔&term;]… + ]] + + identifier with optional explicit named substitution | - Π&id;[: &term;].&term; - dependent product meant to define a datatype + &uri; + a qualified reference | - ∀&id;[: &term;].&term; - dependent product meant to define a proposition + Prop + the impredicative sort of propositions | - &term; → &term; - non-dependent product (logical implication or function space) + Set + the impredicate sort of datatypes | - let [&id;|(&id;: &term;)] ≝ &term; in &term; - local definition + Type + one predicative sort of datatypes + + + + | + ? + implicit argument + + + + | + ?n + [[ + [_|&term;]… + ]] + metavariable @@ -127,53 +223,91 @@ [ - &term_pattern; ⇒ &term; + &match_pattern; ⇒ &term; [ | - &term_pattern; ⇒ &term; + &match_pattern; ⇒ &term; ]…] | - let - [co]rec - &id; [&id;]… [on &nat;] - [: &term;] - ≝ &term; - - (co)recursive definitions + (&term;:&term;) + cast + | + … + user provided notation at precedence 90 + + + +
+ + + Arguments + + + + &args; + ::= + + _[: &term;] + + ignored argument + + + | - [and - &id; [&id;]… [on &nat;] - [: &term;] - ≝ &term;]… + (_[: &term;]) + ignored argument + + + | + &id;[,&id;]…[: &term;] + + | + (&id;[,&id;]…[: &term;]) - - in &term; - + + + +
+ + + Miscellaneous arguments + + + + &args2; + ::= + &id; + + + + + | + (&id;[,&id;]…: &term;)
- - - +
+ Pattern matching + - &term_pattern; + &match_pattern; ::= &id; 0-ary constructor @@ -187,17 +321,21 @@
+ + + - - axiom &id;: &term; + + Definitions and declarations + + <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; @@ -209,18 +347,65 @@ given. In this case Matita enters in interactive mode and f must be defined by means of tactics. 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 @@ -237,7 +422,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 @@ -245,19 +430,19 @@ 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