X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=082a5bb75f47b79d26820ac30506c11ceeb7abdd;hb=275a432d33c455d75725d5991e82b62e7d01f68d;hp=e9402f2371d3757eaa4e479e269bb7d351e17882;hpb=c25f685f27ea3b902fce0a87fe6d9b80c9a69bc5;p=helm.git diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index e9402f237..082a5bb75 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -2,92 +2,433 @@ - 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.: [<|>] + 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 + + qstring + + + + &qstring; + ::= + "〈〈any sequence of characters excluded "〉〉" + + + +
+ + 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;]…)] + + + +
+ + csymbol + + + + &csymbol; + ::= + '&id; + + + +
+ + + Terms - + + - - - - - - <term> - ::= - <id> - identifier - - - - | - <term> <term> - application - - - - | - λ<id>[: <term>].<term> - λ-abstraction - - - - | - Π<id>[: <term>].<term> - dependent product meant to define a datatype - - - - | - ∀<id>[: <term>].<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> ≝ <term> in <term> - local definition - - - - | - ... - &TODO; - - - -
+ + &term; + &sterm; + + + + --> + + + + 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 + &rec_def; + + (co)recursive definitions + + + + + + [and &rec_def;]… + + + + + + + + in &term; + + + + + + | + … + user provided notation + + + &rec_def; + ::= + + &id; [&id;|_|(&id;[,&id;]… :&term;)]… + + + + + + + + [on &id;] + [: &term;] + ≝ &term;] + + + + + +
+ + + Simple terms + + + + &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 + + + + | + CProp + one fixed predicative sort of constructive propositions + + + + | + Type + one predicative sort of datatypes + + + + | + ? + implicit argument + + + + | + ?n + [[ + [_|&term;]… + ]] + metavariable + + + + | + match &term; + [ in &id; ] + [ return &term; ] + with + + case analysis + + + + + + [ + &match_branch;[|&match_branch;]… + ] + + + + + + | + (&term;:&term;) + cast + + + + | + … + user provided notation at precedence 90 + + + +
+ + + Arguments + + + + &args; + ::= + + _[: &term;] + + ignored argument + + + + | + + (_[: &term;]) + + ignored argument + + + + | + &id;[,&id;]…[: &term;] + + + + + | + (&id;[,&id;]…[: &term;]) + + + + &args2; + ::= + &id; + + + + + | + (&id;[,&id;]…: &term;) + + + + +
+ + + Pattern matching + + + + &match_branch; + ::= + &match_pattern; ⇒ &term; + + + + &match_pattern; + ::= + &id; + 0-ary constructor + + + + | + (&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) + + + +
+ + + - - 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; @@ -99,18 +440,70 @@ 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">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;]…]… + (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 @@ -127,7 +520,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 @@ -135,24 +528,298 @@ 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; + ::= + 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;〉〉 + + + +
+ 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" + + + + + 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 + + + + | + 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 + + 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 + + + + + | + timeout=&nat; + Timeout in seconds + + + + +
+ + + + justification + + justification + + + + &justification; + ::= + using &term; + Proof term manually provided + + + + | + &autoparams; + Call automation + + + +
+ + +