X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=5e29eb41eec2fce914c6d8b73119753482f63198;hb=24b8b9f80e0754f40a4a7cc773b49cc0401831ae;hp=5fafcd0ac5b3b90af1ba2b43a965ea6c0b4d7004;hpb=ddc473c05167ab7aafafcc13425a154b9b0fd57f;p=helm.git diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 5fafcd0ac..5e29eb41e 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -2,27 +2,378 @@ - Terms, 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; + ::= + 〈〈&TODO;〉〉 + + + +
+ + + + + + &nat; + ::= + 〈〈&TODO;〉〉 + + + +
+ + + + + + &uri; + ::= + 〈〈&TODO;〉〉 + + + +
+ + + Terms + + + + + + &term; + ::= + &sterm; + simple or delimited term + + + + | + &term; &term; + application + + + + | + λ&args;.&term; + λ-abstraction + + + + | + Π&args;.&term; + dependent product meant to define a datatype + + + + | + ∀&args;.&term; + dependent product meant to define a proposition + + + + | + &term; → &term; + non-dependent product (logical implication or function space) + + + + | + let [&id;|(&id;: &term;)] ≝ &term; in &term; + local definition + + + + | + 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; + + + + + + | + … + user provided notation + + + +
- - Terms - &TODO; - + + + + + + &sterm; + ::= + (&term;) + + + + + | + &id;[\subst[ + &id;≔&term; + [;&id;≔&term;]… + ]] + + identifier with optional explicit named substitution + + + + | + &uri; + a qualified reference + + + + | + Prop + the impredicative sort of propositions + + + + | + Set + the impredicate sort of datatypes + + + + | + Type + one predicative sort of datatypes + + + + | + ? + implicit argument + + + + | + ?n + [[ + [_|&term;]… + ]] + metavariable + + + + | + match &term; + [ in &term; ] + [ return &term; ] + with + + case analysis + + + + + + [ + &match_pattern; ⇒ &term; + [ + | + &match_pattern; ⇒ &term; + ]…] + + + + + | + (&term;:&term;) + cast + + + + | + … + user provided notation at precedence 90 + + + +
- - Definitions - &TODO; + + + + + + &args; + ::= + + _[: &term;] + + ignored argument + + + + | + + (_[: &term;]) + + ignored argument + + + + | + &id;[,&id;]…[: &term;] + + + + + | + (&id;[,&id;]…[: &term;]) + + + + +
+ + + + + + + &match_pattern; + ::= + &id; + 0-ary constructor + + + + | + (&id; &id; [&id;]…) + n-ary constructor (binds the n arguments) + + + +
+ + - - Declarations (of inductive types) - Declarations + + Definitions and declarations + + axiom &id;: &term; + axiom + axiom H: P + H is declared as an axiom that states P + + + definition &id;[: &term;] [≝ &term;] + definition + definition f: T ≝ t + f is defined as t; + T is its type. An error is raised if the type of + t is not convertible to T. + T is inferred from t if + omitted. + t can be omitted only if T is + 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) + (co)inductive types declaration &TODO; + - Proofs - &TODO; + Proofs + + theorem &id;[: &term;] [≝ &term;] + theorem + theorem f: P ≝ p + Proves a new theorem f whose thesis is + P. + If p is provided, it must be a proof term for + P. Otherwise an interactive proof is started. + P can be omitted only if the proof is not + interactive. + Proving a theorem already proved in the library is an error. + To provide an alternative name and proof for the same theorem, use + variant f: P ≝ p. + 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. + + + variant &id;[: &term;] [≝ &term;] + variant + variant f: T ≝ t + Same as theorem f: T ≝ t, but it does not + complain if the theorem has already been proved. To be used to give + an alternative name or proof to a theorem. + + + lemma &id;[: &term;] [≝ &term;] + lemma + lemma f: T ≝ t + Same as theorem f: T ≝ t + + + fact &id;[: &term;] [≝ &term;] + fact + fact f: T ≝ t + Same as theorem f: T ≝ t + + + remark &id;[: &term;] [≝ &term;] + remark + remark f: T ≝ t + Same as theorem f: T ≝ t +