diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 522 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 71 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 726 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 293 |
4 files changed, 922 insertions, 690 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 381f8bb661..ef183174d7 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -20,9 +20,9 @@ There are types for functions (or programs), there are atomic types (especially datatypes)... but also types for proofs and types for the types themselves. Especially, any object handled in the formalism must belong to a type. For instance, universal quantification is relative -to a type and takes the form "*for all x of type T, P* ". The expression -“x of type T” is written :g:`x:T`. Informally, :g:`x:T` can be thought as -“x belongs to T”. +to a type and takes the form “*for all x of type* :math:`T`, :math:`P`”. The expression +“:math:`x` *of type* :math:`T`” is written “:math:`x:T`”. Informally, “:math:`x:T`” can be thought as +“:math:`x` *belongs to* :math:`T`”. The types of types are *sorts*. Types and sorts are themselves terms so that terms, types and sorts are all components of a common @@ -36,22 +36,30 @@ Sorts ~~~~~~~~~~~ All sorts have a type and there is an infinite well-founded typing -hierarchy of sorts whose base sorts are :math:`\Prop` and :math:`\Set`. +hierarchy of sorts whose base sorts are :math:`\SProp`, :math:`\Prop` +and :math:`\Set`. The sort :math:`\Prop` intends to be the type of logical propositions. If :math:`M` is a logical proposition then it denotes the class of terms representing proofs of :math:`M`. An object :math:`m` belonging to :math:`M` witnesses the fact that :math:`M` is provable. An object of type :math:`\Prop` is called a proposition. +The sort :math:`\SProp` is like :math:`\Prop` but the propositions in +:math:`\SProp` are known to have irrelevant proofs (all proofs are +equal). Objects of type :math:`\SProp` are called strict propositions. +:math:`\SProp` is rejected except when using the compiler option +``-allow-sprop``. See :ref:`sprop` for information about using +:math:`\SProp`. + The sort :math:`\Set` intends to be the type of small sets. This includes data types such as booleans and naturals, but also products, subsets, and function types over these data types. -:math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms. +:math:`\SProp`, :math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms. Consequently they also have a type. Because assuming simply that :math:`\Set` has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of -|Cic| has infinitely many sorts. There are, in addition to :math:`\Set` and :math:`\Prop` -a hierarchy of universes :math:`\Type(i)` for any integer :math:`i`. +|Cic| has infinitely many sorts. There are, in addition to the base sorts, +a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`. Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as booleans, natural numbers, as well as products, subsets and function @@ -63,7 +71,7 @@ Formally, we call :math:`\Sort` the set of sorts which is defined by: .. math:: - \Sort \equiv \{\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} + \Sort \equiv \{\SProp,\Prop,\Set,\Type(i)\;|\; i~∈ ℕ\} Their properties, such as: :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and :math:`\Type(i):\Type(i+1)`, are defined in Section :ref:`subtyping-rules`. @@ -84,7 +92,7 @@ implemented using *algebraic universes*. An algebraic universe :math:`u` is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression :math:`u+1`), or an upper bound of algebraic universes (an -expression :math:`\max(u 1 ,...,u n )`), or the base universe (the expression +expression :math:`\max(u_1 ,...,u_n )`), or the base universe (the expression :math:`0`) which corresponds, in the arity of template polymorphic inductive types (see Section :ref:`well-formed-inductive-definitions`), @@ -113,28 +121,28 @@ language of the *Calculus of Inductive Constructions* is built from the following rules. -#. the sorts :math:`\Set`, :math:`\Prop`, :math:`\Type(i)` are terms. +#. the sorts :math:`\SProp`, :math:`\Prop`, :math:`\Set`, :math:`\Type(i)` are terms. #. variables, hereafter ranged over by letters :math:`x`, :math:`y`, etc., are terms #. constants, hereafter ranged over by letters :math:`c`, :math:`d`, etc., are terms. #. if :math:`x` is a variable and :math:`T`, :math:`U` are terms then - :math:`∀ x:T,U` (:g:`forall x:T, U` in |Coq| concrete syntax) is a term. - If :math:`x` occurs in :math:`U`, :math:`∀ x:T,U` reads as + :math:`∀ x:T,~U` (:g:`forall x:T, U` in |Coq| concrete syntax) is a term. + If :math:`x` occurs in :math:`U`, :math:`∀ x:T,~U` reads as “for all :math:`x` of type :math:`T`, :math:`U`”. - As :math:`U` depends on :math:`x`, one says that :math:`∀ x:T,U` is + As :math:`U` depends on :math:`x`, one says that :math:`∀ x:T,~U` is a *dependent product*. If :math:`x` does not occur in :math:`U` then - :math:`∀ x:T,U` reads as + :math:`∀ x:T,~U` reads as “if :math:`T` then :math:`U`”. A *non dependent product* can be written: :math:`T \rightarrow U`. #. if :math:`x` is a variable and :math:`T`, :math:`u` are terms then - :math:`λ x:T . u` (:g:`fun x:T => u` + :math:`λ x:T .~u` (:g:`fun x:T => u` in |Coq| concrete syntax) is a term. This is a notation for the - λ-abstraction of λ-calculus :cite:`Bar81`. The term :math:`λ x:T . u` is a function + λ-abstraction of λ-calculus :cite:`Bar81`. The term :math:`λ x:T .~u` is a function which maps elements of :math:`T` to the expression :math:`u`. #. if :math:`t` and :math:`u` are terms then :math:`(t~u)` is a term (:g:`t u` in |Coq| concrete - syntax). The term :math:`(t~u)` reads as “t applied to u”. -#. if :g:`x` is a variable, and :math:`t`, :math:`T` and :math:`u` are - terms then :g:`let x:=t:T in u` is + syntax). The term :math:`(t~u)` reads as “:math:`t` applied to :math:`u`”. +#. if :math:`x` is a variable, and :math:`t`, :math:`T` and :math:`u` are + terms then :math:`\letin{x}{t:T}{u}` is a term which denotes the term :math:`u` where the variable :math:`x` is locally bound to :math:`t` of type :math:`T`. This stands for the common “let-in” construction of functional programs such as ML or Scheme. @@ -145,7 +153,7 @@ the following rules. **Free variables.** The notion of free variables is defined as usual. In the expressions -:g:`λx:T. U` and :g:`∀ x:T, U` the occurrences of :math:`x` in :math:`U` are bound. +:math:`λx:T.~U` and :math:`∀ x:T,~U` the occurrences of :math:`x` in :math:`U` are bound. .. _Substitution: @@ -172,11 +180,11 @@ implicative proposition, to denote :math:`\nat →\Prop` which is the type of unary predicates over the natural numbers, etc. Let us assume that ``mult`` is a function of type :math:`\nat→\nat→\nat` and ``eqnat`` a -predicate of type \nat→\nat→ \Prop. The λ-abstraction can serve to build -“ordinary” functions as in :math:`λ x:\nat.(\kw{mult}~x~x)` (i.e. +predicate of type :math:`\nat→\nat→ \Prop`. The λ-abstraction can serve to build +“ordinary” functions as in :math:`λ x:\nat.~(\kw{mult}~x~x)` (i.e. :g:`fun x:nat => mult x x` in |Coq| notation) but may build also predicates over the natural -numbers. For instance :math:`λ x:\nat.(\kw{eqnat}~x~0)` +numbers. For instance :math:`λ x:\nat.~(\kw{eqnat}~x~0)` (i.e. :g:`fun x:nat => eqnat x 0` in |Coq| notation) will represent the predicate of one variable :math:`x` which asserts the equality of :math:`x` with :math:`0`. This predicate has type @@ -186,7 +194,7 @@ object :math:`P~t` of type :math:`\Prop`, namely a proposition. Furthermore :g:`forall x:nat, P x` will represent the type of functions which associate to each natural number :math:`n` an object of type :math:`(P~n)` and -consequently represent the type of proofs of the formula “:math:`∀ x. P(x`)”. +consequently represent the type of proofs of the formula “:math:`∀ x.~P(x)`”. .. _Typing-rules: @@ -206,7 +214,7 @@ A *local context* is an ordered list of *local declarations* of names which we call *variables*. The declaration of some variable :math:`x` is either a *local assumption*, written :math:`x:T` (:math:`T` is a type) or a *local definition*, written :math:`x:=t:T`. We use brackets to write local contexts. -A typical example is :math:`[x:T;y:=u:U;z:V]`. Notice that the variables +A typical example is :math:`[x:T;~y:=u:U;~z:V]`. Notice that the variables declared in a local context must be distinct. If :math:`Γ` is a local context that declares some :math:`x`, we write :math:`x ∈ Γ`. By writing :math:`(x:T) ∈ Γ` we mean that either :math:`x:T` is an @@ -216,7 +224,7 @@ For the rest of the chapter, :math:`Γ::(y:T)` denotes the local context :math:` enriched with the local assumption :math:`y:T`. Similarly, :math:`Γ::(y:=t:T)` denotes the local context :math:`Γ` enriched with the local definition :math:`(y:=t:T)`. The notation :math:`[]` denotes the empty local context. By :math:`Γ_1 ; Γ_2` we mean -concatenation of the local context :math:`Γ_1` and the local context :math:`Γ_2` . +concatenation of the local context :math:`Γ_1` and the local context :math:`Γ_2`. .. _Global-environment: @@ -232,9 +240,9 @@ A *global assumption* will be represented in the global environment as :math:`(c:T)` which assumes the name :math:`c` to be of some type :math:`T`. A *global definition* will be represented in the global environment as :math:`c:=t:T` which defines the name :math:`c` to have value :math:`t` and type :math:`T`. We shall call -such names *constants*. For the rest of the chapter, the :math:`E;c:T` denotes +such names *constants*. For the rest of the chapter, the :math:`E;~c:T` denotes the global environment :math:`E` enriched with the global assumption :math:`c:T`. -Similarly, :math:`E;c:=t:T` denotes the global environment :math:`E` enriched with the +Similarly, :math:`E;~c:=t:T` denotes the global environment :math:`E` enriched with the global definition :math:`(c:=t:T)`. The rules for inductive definitions (see Section @@ -284,14 +292,20 @@ following rules. s \in \Sort c \notin E ------------ - \WF{E;c:T}{} + \WF{E;~c:T}{} .. inference:: W-Global-Def \WTE{}{t}{T} c \notin E --------------- - \WF{E;c:=t:T}{} + \WF{E;~c:=t:T}{} + +.. inference:: Ax-SProp + + \WFE{\Gamma} + ---------------------- + \WTEG{\SProp}{\Type(1)} .. inference:: Ax-Prop @@ -325,39 +339,48 @@ following rules. ---------------------------------------------------------- \WTEG{c}{T} -.. inference:: Prod-Prop +.. inference:: Prod-SProp \WTEG{T}{s} s \in {\Sort} + \WTE{\Gamma::(x:T)}{U}{\SProp} + ----------------------------- + \WTEG{\forall~x:T,U}{\SProp} + +.. inference:: Prod-Prop + + \WTEG{T}{s} + s \in \Sort \WTE{\Gamma::(x:T)}{U}{\Prop} ----------------------------- - \WTEG{\forall~x:T,U}{\Prop} + \WTEG{∀ x:T,~U}{\Prop} .. inference:: Prod-Set \WTEG{T}{s} - s \in \{\Prop, \Set\} + s \in \{\SProp, \Prop, \Set\} \WTE{\Gamma::(x:T)}{U}{\Set} ---------------------------- - \WTEG{\forall~x:T,U}{\Set} + \WTEG{∀ x:T,~U}{\Set} .. inference:: Prod-Type - \WTEG{T}{\Type(i)} + \WTEG{T}{s} + s \in \{\SProp, \Type{i}\} \WTE{\Gamma::(x:T)}{U}{\Type(i)} -------------------------------- - \WTEG{\forall~x:T,U}{\Type(i)} + \WTEG{∀ x:T,~U}{\Type(i)} .. inference:: Lam - \WTEG{\forall~x:T,U}{s} + \WTEG{∀ x:T,~U}{s} \WTE{\Gamma::(x:T)}{t}{U} ------------------------------------ - \WTEG{\lb x:T\mto t}{\forall x:T, U} + \WTEG{λ x:T\mto t}{∀ x:T,~U} .. inference:: App - \WTEG{t}{\forall~x:U,T} + \WTEG{t}{∀ x:U,~T} \WTEG{u}{U} ------------------------------ \WTEG{(t\ u)}{\subst{T}{x}{u}} @@ -383,7 +406,7 @@ following rules. .. note:: We may have :math:`\letin{x}{t:T}{u}` well-typed without having - :math:`((λ x:T.u) t)` well-typed (where :math:`T` is a type of + :math:`((λ x:T.~u)~t)` well-typed (where :math:`T` is a type of :math:`t`). This is because the value :math:`t` associated to :math:`x` may be used in a conversion rule (see Section :ref:`Conversion-rules`). @@ -406,18 +429,18 @@ can decide if two programs are *intentionally* equal (one says We want to be able to identify some terms as we can identify the application of a function to a given argument with its result. For -instance the identity function over a given type T can be written -:math:`λx:T. x`. In any global environment :math:`E` and local context +instance the identity function over a given type :math:`T` can be written +:math:`λx:T.~x`. In any global environment :math:`E` and local context :math:`Γ`, we want to identify any object :math:`a` (of type -:math:`T`) with the application :math:`((λ x:T. x) a)`. We define for +:math:`T`) with the application :math:`((λ x:T.~x)~a)`. We define for this a *reduction* (or a *conversion*) rule we call :math:`β`: .. math:: - E[Γ] ⊢ ((λx:T. t) u)~\triangleright_β~\subst{t}{x}{u} + E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u} We say that :math:`\subst{t}{x}{u}` is the *β-contraction* of -:math:`((λx:T. t) u)` and, conversely, that :math:`((λ x:T. t) u)` is the +:math:`((λx:T.~t)~u)` and, conversely, that :math:`((λ x:T.~t)~u)` is the *β-expansion* of :math:`\subst{t}{x}{u}`. According to β-reduction, terms of the *Calculus of Inductive @@ -481,7 +504,7 @@ destroyed, this reduction differs from δ-reduction. It is called \WTEG{u}{U} \WTE{\Gamma::(x:=u:U)}{t}{T} -------------- - E[Γ] ⊢ \letin{x}{u}{t}~\triangleright_ζ~\subst{t}{x}{u} + E[Γ] ⊢ \letin{x}{u:U}{t}~\triangleright_ζ~\subst{t}{x}{u} .. _eta-expansion: @@ -490,10 +513,10 @@ destroyed, this reduction differs from δ-reduction. It is called ~~~~~~~~~~~ Another important concept is η-expansion. It is legal to identify any -term :math:`t` of functional type :math:`∀ x:T, U` with its so-called η-expansion +term :math:`t` of functional type :math:`∀ x:T,~U` with its so-called η-expansion .. math:: - λx:T. (t~x) + λx:T.~(t~x) for :math:`x` an arbitrary variable name fresh in :math:`t`. @@ -503,27 +526,35 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. We deliberately do not define η-reduction: .. math:: - λ x:T. (t~x) \not\triangleright_η t + λ x:T.~(t~x)~\not\triangleright_η~t This is because, in general, the type of :math:`t` need not to be convertible - to the type of :math:`λ x:T. (t~x)`. E.g., if we take :math:`f` such that: + to the type of :math:`λ x:T.~(t~x)`. E.g., if we take :math:`f` such that: .. math:: - f : ∀ x:\Type(2),\Type(1) + f ~:~ ∀ x:\Type(2),~\Type(1) then .. math:: - λ x:\Type(1),(f~x) : ∀ x:\Type(1),\Type(1) + λ x:\Type(1).~(f~x) ~:~ ∀ x:\Type(1),~\Type(1) We could not allow .. math:: - λ x:Type(1),(f x) \triangleright_η f + λ x:\Type(1).~(f~x) ~\triangleright_η~ f - because the type of the reduced term :math:`∀ x:\Type(2),\Type(1)` would not be - convertible to the type of the original term :math:`∀ x:\Type(1),\Type(1).` + because the type of the reduced term :math:`∀ x:\Type(2),~\Type(1)` would not be + convertible to the type of the original term :math:`∀ x:\Type(1),~\Type(1)`. + +.. _proof-irrelevance: +Proof Irrelevance +~~~~~~~~~~~~~~~~~ + +It is legal to identify any two terms whose common type is a strict +proposition :math:`A : \SProp`. Terms in a strict propositions are +therefore called *irrelevant*. .. _convertibility: @@ -533,19 +564,19 @@ Convertibility Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the relation :math:`t` reduces to :math:`u` in the global environment :math:`E` and local context :math:`Γ` with one of the previous -reductions β, ι, δ or ζ. +reductions β, δ, ι or ζ. We say that two terms :math:`t_1` and :math:`t_2` are -*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the +*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and -:math:`u_2` are identical, or they are convertible up to η-expansion, -i.e. :math:`u_1` is :math:`λ x:T. u_1'` and :math:`u_2 x` is -recursively convertible to :math:`u_1'` , or, symmetrically, -:math:`u_2` is :math:`λx:T. u_2'` -and :math:`u_1 x` is recursively convertible to u_2′ . We then write -:math:`E[Γ] ⊢ t_1 =_{βδιζη} t_2` . +:math:`u_2` are identical up to irrelevant subterms, or they are convertible up to η-expansion, +i.e. :math:`u_1` is :math:`λ x:T.~u_1'` and :math:`u_2 x` is +recursively convertible to :math:`u_1'`, or, symmetrically, +:math:`u_2` is :math:`λx:T.~u_2'` +and :math:`u_1 x` is recursively convertible to :math:`u_2'`. We then write +:math:`E[Γ] ⊢ t_1 =_{βδιζη} t_2`. Apart from this we consider two instances of polymorphic and cumulative (see Chapter :ref:`polymorphicuniverses`) inductive types @@ -601,8 +632,8 @@ Subtyping rules ------------------- At the moment, we did not take into account one rule between universes -which says that any term in a universe of index i is also a term in -the universe of index i+1 (this is the *cumulativity* rule of |Cic|). +which says that any term in a universe of index :math:`i` is also a term in +the universe of index :math:`i+1` (this is the *cumulativity* rule of |Cic|). This property extends the equivalence relation of convertibility into a *subtyping* relation inductively defined by: @@ -612,27 +643,28 @@ a *subtyping* relation inductively defined by: #. for any :math:`i`, :math:`E[Γ] ⊢ \Set ≤_{βδιζη} \Type(i)`, #. :math:`E[Γ] ⊢ \Prop ≤_{βδιζη} \Set`, hence, by transitivity, :math:`E[Γ] ⊢ \Prop ≤_{βδιζη} \Type(i)`, for any :math:`i` + (note: :math:`\SProp` is not related by cumulativity to any other term) #. if :math:`E[Γ] ⊢ T =_{βδιζη} U` and :math:`E[Γ::(x:T)] ⊢ T' ≤_{βδιζη} U'` then - :math:`E[Γ] ⊢ ∀x:T, T′ ≤_{βδιζη} ∀ x:U, U′`. + :math:`E[Γ] ⊢ ∀x:T,~T′ ≤_{βδιζη} ∀ x:U,~U′`. #. if :math:`\ind{p}{Γ_I}{Γ_C}` is a universe polymorphic and cumulative (see Chapter :ref:`polymorphicuniverses`) inductive type (see below) and - :math:`(t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort)∈Γ_I` + :math:`(t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S)∈Γ_I` and - :math:`(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', \Sort')∈Γ_I` + :math:`(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', S')∈Γ_I` are two different instances of *the same* inductive type (differing only in universe levels) with constructors .. math:: - [c_1 : ∀Γ_P ,∀ T_{1,1} … T_{1,n_1} , t~v_{1,1} … v_{1,m} ;…; - c_k : ∀Γ_P ,∀ T_{k,1} … T_{k,n_k} ,t~v_{n,1} … v_{n,m} ] + [c_1 : ∀Γ_P ,∀ T_{1,1} … T_{1,n_1} ,~t~v_{1,1} … v_{1,m} ;~…;~ + c_k : ∀Γ_P ,∀ T_{k,1} … T_{k,n_k} ,~t~v_{k,1} … v_{k,m} ] and .. math:: - [c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' , t'~v_{1,1}' … v_{1,m}' ;…; - c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,t'~v_{n,1}' … v_{n,m}' ] + [c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' ,~t'~v_{1,1}' … v_{1,m}' ;~…;~ + c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,~t'~v_{k,1}' … v_{k,m}' ] respectively then @@ -656,8 +688,8 @@ a *subtyping* relation inductively defined by: .. math:: E[Γ] ⊢ A_i ≤_{βδιζη} A_i' - where :math:`Γ_{\mathit{Arr}(t)} = [a_1 : A_1 ; … ; a_l : A_l ]` and - :math:`Γ_{\mathit{Arr}(t)}' = [a_1 : A_1'; … ; a_l : A_l']`. + where :math:`Γ_{\mathit{Arr}(t)} = [a_1 : A_1 ;~ … ;~a_l : A_l ]` and + :math:`Γ_{\mathit{Arr}(t)}' = [a_1 : A_1';~ … ;~a_l : A_l']`. The conversion rule up to subtyping is now exactly: @@ -677,19 +709,19 @@ The conversion rule up to subtyping is now exactly: form*. There are several ways (or strategies) to apply the reduction rules. Among them, we have to mention the *head reduction* which will play an important role (see Chapter :ref:`tactics`). Any term :math:`t` can be written as -:math:`λ x_1 :T_1 . … λ x_k :T_k . (t_0~t_1 … t_n )` where :math:`t_0` is not an -application. We say then that :math:`t~0` is the *head of* :math:`t`. If we assume -that :math:`t_0` is :math:`λ x:T. u_0` then one step of β-head reduction of :math:`t` is: +:math:`λ x_1 :T_1 .~… λ x_k :T_k .~(t_0~t_1 … t_n )` where :math:`t_0` is not an +application. We say then that :math:`t_0` is the *head of* :math:`t`. If we assume +that :math:`t_0` is :math:`λ x:T.~u_0` then one step of β-head reduction of :math:`t` is: .. math:: - λ x_1 :T_1 . … λ x_k :T_k . (λ x:T. u_0~t_1 … t_n ) \triangleright - λ (x_1 :T_1 )…(x_k :T_k ). (\subst{u_0}{x}{t_1}~t_2 … t_n ) + λ x_1 :T_1 .~… λ x_k :T_k .~(λ x:T.~u_0~t_1 … t_n ) ~\triangleright~ + λ (x_1 :T_1 )…(x_k :T_k ).~(\subst{u_0}{x}{t_1}~t_2 … t_n ) Iterating the process of head reduction until the head of the reduced term is no more an abstraction leads to the *β-head normal form* of :math:`t`: .. math:: - t \triangleright … \triangleright λ x_1 :T_1 . …λ x_k :T_k . (v~u_1 … u_m ) + t \triangleright … \triangleright λ x_1 :T_1 .~…λ x_k :T_k .~(v~u_1 … u_m ) where :math:`v` is not an abstraction (nor an application). Note that the head normal form must not be confused with the normal form since some :math:`u_i` @@ -713,12 +745,12 @@ Formally, we can represent any *inductive definition* as These inductive definitions, together with global assumptions and global definitions, then form the global environment. Additionally, -for any :math:`p` there always exists :math:`Γ_P =[a_1 :A_1 ;…;a_p :A_p ]` such that +for any :math:`p` there always exists :math:`Γ_P =[a_1 :A_1 ;~…;~a_p :A_p ]` such that each :math:`T` in :math:`(t:T)∈Γ_I \cup Γ_C` can be written as: :math:`∀Γ_P , T'` where :math:`Γ_P` is called the *context of parameters*. Furthermore, we must have that each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{\mathit{Arr}(t)}, S` where -:math:`Γ_{\mathit{Arr}(t)}` is called the *Arity* of the inductive type t and :math:`S` is called -the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts). +:math:`Γ_{\mathit{Arr}(t)}` is called the *Arity* of the inductive type :math:`t` and :math:`S` is called +the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` which is the set of sorts). .. example:: @@ -726,8 +758,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is .. math:: \ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl} - \Nil & : & \forall A:\Set,\List~A \\ - \cons & : & \forall A:\Set, A→ \List~A→ \List~A + \Nil & : & ∀ A:\Set,~\List~A \\ + \cons & : & ∀ A:\Set,~A→ \List~A→ \List~A \end{array} \right]} @@ -771,8 +803,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) + \evenS &:& ∀ n,~\odd~n → \even~(\nS~n)\\ + \oddS &:& ∀ n,~\even~n → \odd~(\nS~n) \end{array}\right]} which corresponds to the result of the |Coq| declaration: @@ -782,7 +814,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) - with odd : nat -> prop := + with odd : nat -> Prop := | odd_S : forall n, even n -> odd (S n). @@ -792,8 +824,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is Types of inductive objects ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We have to give the type of constants in a global environment E which -contains an inductive declaration. +We have to give the type of constants in a global environment :math:`E` which +contains an inductive definition. .. inference:: Ind @@ -820,9 +852,9 @@ contains an inductive declaration. \begin{array}{l} E[Γ] ⊢ \even : \nat→\Prop\\ E[Γ] ⊢ \odd : \nat→\Prop\\ - E[Γ] ⊢ \even\_O : \even~O\\ - E[Γ] ⊢ \even\_S : \forall~n:\nat, \odd~n → \even~(S~n)\\ - E[Γ] ⊢ \odd\_S : \forall~n:\nat, \even~n → \odd~(S~n) + E[Γ] ⊢ \evenO : \even~\nO\\ + E[Γ] ⊢ \evenS : ∀ n:\nat,~\odd~n → \even~(\nS~n)\\ + E[Γ] ⊢ \oddS : ∀ n:\nat,~\even~n → \odd~(\nS~n) \end{array} @@ -833,7 +865,7 @@ contains an inductive declaration. Well-formed inductive definitions ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We cannot accept any inductive declaration because some of them lead +We cannot accept any inductive definition because some of them lead to inconsistent systems. We restrict ourselves to definitions which satisfy a syntactic criterion of positivity. Before giving the formal rules, we need a few definitions: @@ -842,11 +874,11 @@ Arity of a given sort +++++++++++++++++++++ A type :math:`T` is an *arity of sort* :math:`s` if it converts to the sort :math:`s` or to a -product :math:`∀ x:T,U` with :math:`U` an arity of sort :math:`s`. +product :math:`∀ x:T,~U` with :math:`U` an arity of sort :math:`s`. .. example:: - :math:`A→\Set` is an arity of sort :math:`\Set`. :math:`∀ A:\Prop,A→ \Prop` is an arity of sort + :math:`A→\Set` is an arity of sort :math:`\Set`. :math:`∀ A:\Prop,~A→ \Prop` is an arity of sort :math:`\Prop`. @@ -858,21 +890,21 @@ sort :math:`s`. .. example:: - :math:`A→ Set` and :math:`∀ A:\Prop,A→ \Prop` are arities. + :math:`A→ \Set` and :math:`∀ A:\Prop,~A→ \Prop` are arities. -Type constructor -++++++++++++++++ -We say that T is a *type of constructor of I* in one of the following +Type of constructor ++++++++++++++++++++ +We say that :math:`T` is a *type of constructor of* :math:`I` in one of the following two cases: + :math:`T` is :math:`(I~t_1 … t_n )` -+ :math:`T` is :math:`∀ x:U,T'` where :math:`T'` is also a type of constructor of :math:`I` ++ :math:`T` is :math:`∀ x:U,~T'` where :math:`T'` is also a type of constructor of :math:`I` .. example:: :math:`\nat` and :math:`\nat→\nat` are types of constructor of :math:`\nat`. - :math:`∀ A:Type,\List~A` and :math:`∀ A:Type,A→\List~A→\List~A` are types of constructor of :math:`\List`. + :math:`∀ A:\Type,~\List~A` and :math:`∀ A:\Type,~A→\List~A→\List~A` are types of constructor of :math:`\List`. .. _positivity: @@ -883,7 +915,7 @@ The type of constructor :math:`T` will be said to *satisfy the positivity condition* for a constant :math:`X` in the following cases: + :math:`T=(X~t_1 … t_n )` and :math:`X` does not occur free in any :math:`t_i` -+ :math:`T=∀ x:U,V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` ++ :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` satisfies the positivity condition for :math:`X`. Strict positivity @@ -895,13 +927,13 @@ cases: + :math:`X` does not occur in :math:`T` + :math:`T` converts to :math:`(X~t_1 … t_n )` and :math:`X` does not occur in any of :math:`t_i` -+ :math:`T` converts to :math:`∀ x:U,V` and :math:`X` does not occur in type :math:`U` but occurs ++ :math:`T` converts to :math:`∀ x:U,~V` and :math:`X` does not occur in type :math:`U` but occurs strictly positively in type :math:`V` + :math:`T` converts to :math:`(I~a_1 … a_m~t_1 … t_p )` where :math:`I` is the name of an - inductive declaration of the form + inductive definition of the form .. math:: - \ind{m}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_m :P_m ,C_1 ;…;c_n :∀ p_1 :P_1 ,… ∀p_m :P_m ,C_n} + \ind{m}{I:A}{c_1 :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_1 ;~…;~c_n :∀ p_1 :P_1 ,… ∀p_m :P_m ,~C_n} (in particular, it is not mutually defined and it has :math:`m` parameters) and :math:`X` does not occur in @@ -914,9 +946,9 @@ Nested Positivity The type of constructor :math:`T` of :math:`I` *satisfies the nested positivity condition* for a constant :math:`X` in the following cases: -+ :math:`T=(I~b_1 … b_m~u_1 … u_p)`, :math:`I` is an inductive definition with :math:`m` ++ :math:`T=(I~b_1 … b_m~u_1 … u_p)`, :math:`I` is an inductive type with :math:`m` parameters and :math:`X` does not occur in any :math:`u_i` -+ :math:`T=∀ x:U,V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` ++ :math:`T=∀ x:U,~V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` satisfies the nested positivity condition for :math:`X` @@ -929,8 +961,7 @@ condition* for a constant :math:`X` in the following cases: Inductive nattree (A:Type) : Type := | leaf : nattree A - | node : A -> (nat -> nattree A) -> nattree A. - End TreeExample. + | natnode : A -> (nat -> nattree A) -> nattree A. Then every instantiated constructor of ``nattree A`` satisfies the nested positivity condition for ``nattree``: @@ -940,10 +971,10 @@ condition* for a constant :math:`X` in the following cases: type of that constructor (primarily because ``nattree`` does not have any (real) arguments) ... (bullet 1) - + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the + + Type ``A → (nat → nattree A) → nattree A`` of constructor ``natnode`` satisfies the positivity condition for ``nattree`` because: - - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3) + - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 1) - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2) @@ -958,16 +989,15 @@ We shall now describe the rules allowing the introduction of a new inductive definition. Let :math:`E` be a global environment and :math:`Γ_P`, :math:`Γ_I`, :math:`Γ_C` be contexts -such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k]`, and -:math:`Γ_C` is :math:`[c_1:∀ Γ_P ,C_1 ;…;c_n :∀ Γ_P ,C_n ]`. Then +such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]`, and +:math:`Γ_C` is :math:`[c_1:∀ Γ_P ,C_1 ;~…;~c_n :∀ Γ_P ,C_n ]`. Then .. inference:: W-Ind \WFE{Γ_P} - (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k} (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ - \WF{E;\ind{p}{Γ_I}{Γ_C}}{Γ} + \WF{E;~\ind{p}{Γ_I}{Γ_C}}{} provided that the following side conditions hold: @@ -977,21 +1007,21 @@ provided that the following side conditions hold: context of parameters, + for :math:`j=1… k` we have that :math:`A_j` is an arity of sort :math:`s_j` and :math:`I_j ∉ E`, + for :math:`i=1… n` we have that :math:`C_i` is a type of constructor of :math:`I_{q_i}` which - satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ Γ ∪ E`. + satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ E`. One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative -sort :math:`\Prop` but may fail to define inductive definition on sort :math:`\Set` and -generate constraints between universes for inductive definitions in -the Type hierarchy. +sorts :math:`\SProp` and :math:`\Prop` but may fail to define +inductive type on sort :math:`\Set` and generate constraints +between universes for inductive types in the Type hierarchy. .. example:: It is well known that the existential quantifier can be encoded as an - inductive definition. The following declaration introduces the second- - order existential quantifier :math:`∃ X.P(X)`. + inductive definition. The following declaration introduces the + second-order existential quantifier :math:`∃ X.P(X)`. .. coqtop:: in @@ -1028,7 +1058,7 @@ in :math:`\Type`. .. flag:: Auto Template Polymorphism This option, enabled by default, makes every inductive type declared - at level :math:`Type` (without annotations or hiding it behind a + at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic. This can be prevented using the ``notemplate`` attribute. @@ -1041,6 +1071,12 @@ in :math:`\Type`. enabled it will prevail over automatic template polymorphism and cause an error when using the ``template`` attribute. +.. warn:: Automatically declaring @ident as template polymorphic. + + Warning ``auto-template`` can be used to find which types are + implicitly declared template polymorphic by :flag:`Auto Template + Polymorphism`. + If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local @@ -1049,17 +1085,17 @@ Calculus of Inductive Constructions. The following typing rule is added to the theory. Let :math:`\ind{p}{Γ_I}{Γ_C}` be an inductive definition. Let -:math:`Γ_P = [p_1 :P_1 ;…;p_p :P_p ]` be its context of parameters, -:math:`Γ_I = [I_1:∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k ]` its context of definitions and -:math:`Γ_C = [c_1 :∀ Γ_P ,C_1 ;…;c_n :∀ Γ_P ,C_n]` its context of constructors, +:math:`Γ_P = [p_1 :P_1 ;~…;~p_p :P_p ]` be its context of parameters, +:math:`Γ_I = [I_1:∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k ]` its context of definitions and +:math:`Γ_C = [c_1 :∀ Γ_P ,C_1 ;~…;~c_n :∀ Γ_P ,C_n]` its context of constructors, with :math:`c_i` a constructor of :math:`I_{q_i}`. Let :math:`m ≤ p` be the length of the longest prefix of parameters such that the :math:`m` first arguments of all occurrences of all :math:`I_j` in all :math:`C_k` (even the occurrences in the hypotheses of :math:`C_k`) are exactly applied to :math:`p_1 … p_m` (:math:`m` is the number of *recursively uniform parameters* and the :math:`p−m` remaining parameters -are the *recursively non-uniform parameters*). Let :math:`q_1 , …, q_r` , with +are the *recursively non-uniform parameters*). Let :math:`q_1 , …, q_r`, with :math:`0≤ r≤ m`, be a (possibly) partial instantiation of the recursively -uniform parameters of :math:`Γ_P` . We have: +uniform parameters of :math:`Γ_P`. We have: .. inference:: Ind-Family @@ -1071,15 +1107,15 @@ uniform parameters of :math:`Γ_P` . We have: \end{array} \right. ----------------------------- - E[] ⊢ I_j~q_1 … q_r :∀ [p_{r+1} :P_{r+1} ;…;p_p :P_p], (A_j)_{/s_j} + E[] ⊢ I_j~q_1 … q_r :∀ [p_{r+1} :P_{r+1} ;~…;~p_p :P_p], (A_j)_{/s_j} provided that the following side conditions hold: + :math:`Γ_{P′}` is the context obtained from :math:`Γ_P` by replacing each :math:`P_l` that is an arity with :math:`P_l'` for :math:`1≤ l ≤ r` (notice that :math:`P_l` arity implies :math:`P_l'` - arity since :math:`(E[] ⊢ P_l' ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1} )`; - + there are sorts :math:`s_i` , for :math:`1 ≤ i ≤ k` such that, for - :math:`Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;…;I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]` + arity since :math:`E[] ⊢ P_l' ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}`); + + there are sorts :math:`s_i`, for :math:`1 ≤ i ≤ k` such that, for + :math:`Γ_{I'} = [I_1 :∀ Γ_{P'} ,(A_1)_{/s_1} ;~…;~I_k :∀ Γ_{P'} ,(A_k)_{/s_k}]` we have :math:`(E[Γ_{I′} ;Γ_{P′}] ⊢ C_i : s_{q_i})_{i=1… n}` ; + the sorts :math:`s_i` are such that all eliminations, to :math:`\Prop`, :math:`\Set` and :math:`\Type(j)`, are allowed @@ -1097,7 +1133,7 @@ replacements of sorts, needed for this derivation, in the parameters that are arities (this is possible because :math:`\ind{p}{Γ_I}{Γ_C}` well-formed implies that :math:`\ind{p}{Γ_{I'}}{Γ_{C'}}` is well-formed and has the same allowed eliminations, where :math:`Γ_{I′}` is defined as above and -:math:`Γ_{C′} = [c_1 :∀ Γ_{P′} ,C_1 ;…;c_n :∀ Γ_{P′} ,C_n ]`). That is, the changes in the +:math:`Γ_{C′} = [c_1 :∀ Γ_{P′} ,C_1 ;~…;~c_n :∀ Γ_{P′} ,C_n ]`). That is, the changes in the types of each partial instance :math:`q_1 … q_r` can be characterized by the ordered sets of arity sorts among the types of parameters, and to each signature is associated a new inductive definition with fresh names. @@ -1199,16 +1235,17 @@ a strongly normalizing reduction, we cannot accept any sort of recursion (even terminating). So the basic idea is to restrict ourselves to primitive recursive functions and functionals. -For instance, assuming a parameter :g:`A:Set` exists in the local context, -we want to build a function length of type :g:`list A -> nat` which computes -the length of the list, such that :g:`(length (nil A)) = O` and :g:`(length -(cons A a l)) = (S (length l))`. We want these equalities to be +For instance, assuming a parameter :math:`A:\Set` exists in the local context, +we want to build a function :math:`\length` of type :math:`\List~A → \nat` which computes +the length of the list, such that :math:`(\length~(\Nil~A)) = \nO` and +:math:`(\length~(\cons~A~a~l)) = (\nS~(\length~l))`. +We want these equalities to be recognized implicitly and taken into account in the conversion rule. From the logical point of view, we have built a type family by giving a set of constructors. We want to capture the fact that we do not have any other way to build an object in this type. So when trying to prove -a property about an object :math:`m` in an inductive definition it is enough +a property about an object :math:`m` in an inductive type it is enough to enumerate all the cases where :math:`m` starts with a different constructor. @@ -1216,22 +1253,22 @@ In case the inductive definition is effectively a recursive one, we want to capture the extra property that we have built the smallest fixed point of this recursive equation. This says that we are only manipulating finite objects. This analysis provides induction -principles. For instance, in order to prove :g:`∀ l:list A,(has_length A l -(length l))` it is enough to prove: +principles. For instance, in order to prove +:math:`∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l))` it is enough to prove: -+ :g:`(has_length A (nil A) (length (nil A)))` -+ :g:`∀ a:A, ∀ l:list A, (has_length A l (length l)) →` - :g:`(has_length A (cons A a l) (length (cons A a l)))` ++ :math:`(\kw{has}\_\kw{length}~A~(\Nil~A)~(\length~(\Nil~A)))` ++ :math:`∀ a:A,~∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l)) →` + :math:`(\kw{has}\_\kw{length}~A~(\cons~A~a~l)~(\length~(\cons~A~a~l)))` -which given the conversion equalities satisfied by length is the same +which given the conversion equalities satisfied by :math:`\length` is the same as proving: -+ :g:`(has_length A (nil A) O)` -+ :g:`∀ a:A, ∀ l:list A, (has_length A l (length l)) →` - :g:`(has_length A (cons A a l) (S (length l)))` ++ :math:`(\kw{has}\_\kw{length}~A~(\Nil~A)~\nO)` ++ :math:`∀ a:A,~∀ l:\List~A,~(\kw{has}\_\kw{length}~A~l~(\length~l)) →` + :math:`(\kw{has}\_\kw{length}~A~(\cons~A~a~l)~(\nS~(\length~l)))` One conceptually simple way to do that, following the basic scheme @@ -1261,7 +1298,7 @@ The |Coq| term for this proof will be written: .. math:: - \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n \kwend + \Match~m~\with~(c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\kwend In this expression, if :math:`m` eventually happens to evaluate to :math:`(c_i~u_1 … u_{p_i})` then the expression will behave as specified in its :math:`i`-th branch @@ -1269,7 +1306,7 @@ and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are repla :math:`u_1 … u_{p_i}` according to the ι-reduction. Actually, for type checking a :math:`\Match…\with…\kwend` expression we also need -to know the predicate P to be proved by case analysis. In the general +to know the predicate :math:`P` to be proved by case analysis. In the general case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I` (parameters excluded), and the last one corresponds to object :math:`m`. |Coq| @@ -1303,7 +1340,7 @@ inference rules, we use a more compact notation: .. _Allowed-elimination-sorts: -**Allowed elimination sorts.** An important question for building the typing rule for match is what +**Allowed elimination sorts.** An important question for building the typing rule for :math:`\Match` is what can be the type of :math:`λ a x . P` with respect to the type of :math:`m`. If :math:`m:I` and :math:`I:A` and :math:`λ a x . P : B` then by :math:`[I:A|B]` we mean that one can use :math:`λ a x . P` with :math:`m` in the above match-construct. @@ -1314,14 +1351,14 @@ and :math:`I:A` and :math:`λ a x . P : B` then by :math:`[I:A|B]` we mean that **Notations.** The :math:`[I:A|B]` is defined as the smallest relation satisfying the following rules: We write :math:`[I|B]` for :math:`[I:A|B]` where :math:`A` is the type of :math:`I`. -The case of inductive definitions in sorts :math:`\Set` or :math:`\Type` is simple. +The case of inductive types in sorts :math:`\Set` or :math:`\Type` is simple. There is no restriction on the sort of the predicate to be eliminated. .. inference:: Prod [(I~x):A′|B′] ----------------------- - [I:∀ x:A, A′|∀ x:A, B′] + [I:∀ x:A,~A′|∀ x:A,~B′] .. inference:: Set & Type @@ -1334,14 +1371,15 @@ There is no restriction on the sort of the predicate to be eliminated. The case of Inductive definitions of sort :math:`\Prop` is a bit more complicated, because of our interpretation of this sort. The only -harmless allowed elimination, is the one when predicate :math:`P` is also of -sort :math:`\Prop`. +harmless allowed eliminations, are the ones when predicate :math:`P` +is also of sort :math:`\Prop` or is of the morally smaller sort +:math:`\SProp`. .. inference:: Prop - ~ - --------------- - [I:Prop|I→Prop] + s ∈ \{\SProp,\Prop\} + -------------------- + [I:\Prop|I→s] :math:`\Prop` is the type of logical propositions, the proofs of properties :math:`P` in @@ -1370,7 +1408,7 @@ the proof of :g:`or A B` is not accepted: From the computational point of view, the structure of the proof of :g:`(or A B)` in this term is needed for computing the boolean value. -In general, if :math:`I` has type :math:`\Prop` then :math:`P` cannot have type :math:`I→Set,` because +In general, if :math:`I` has type :math:`\Prop` then :math:`P` cannot have type :math:`I→\Set`, because it will mean to build an informative proof of type :math:`(P~m)` doing a case analysis over a non-computational object that will disappear in the extracted program. But the other way is safe with respect to our @@ -1378,11 +1416,11 @@ interpretation we can have :math:`I` a computational object and :math:`P` a non-computational one, it just corresponds to proving a logical property of a computational object. -In the same spirit, elimination on :math:`P` of type :math:`I→Type` cannot be allowed -because it trivially implies the elimination on :math:`P` of type :math:`I→ Set` by +In the same spirit, elimination on :math:`P` of type :math:`I→\Type` cannot be allowed +because it trivially implies the elimination on :math:`P` of type :math:`I→ \Set` by cumulativity. It also implies that there are two proofs of the same -property which are provably different, contradicting the proof- -irrelevance property which is sometimes a useful axiom: +property which are provably different, contradicting the +proof-irrelevance property which is sometimes a useful axiom: .. example:: @@ -1390,8 +1428,8 @@ irrelevance property which is sometimes a useful axiom: Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. -The elimination of an inductive definition of type :math:`\Prop` on a predicate -:math:`P` of type :math:`I→ Type` leads to a paradox when applied to impredicative +The elimination of an inductive type of sort :math:`\Prop` on a predicate +:math:`P` of type :math:`I→ \Type` leads to a paradox when applied to impredicative inductive definition like the second-order existential quantifier :g:`exProp` defined above, because it gives access to the two projections on this type. @@ -1407,7 +1445,7 @@ this type. I~\kw{is an empty or singleton definition} s ∈ \Sort ------------------------------------- - [I:Prop|I→ s] + [I:\Prop|I→ s] A *singleton definition* has only one constructor and all the arguments of this constructor have type :math:`\Prop`. In that case, there is a @@ -1429,13 +1467,21 @@ type. An empty definition has no constructors, in that case also, elimination on any sort is allowed. +.. _Eliminaton-for-SProp: + +Inductive types in :math:`\SProp` must have no constructors (i.e. be +empty) to be eliminated to produce relevant values. + +Note that thanks to proof irrelevance elimination functions can be +produced for other types, for instance the elimination for a unit type +is the identity. .. _Type-of-branches: **Type of branches.** Let :math:`c` be a term of type :math:`C`, we assume :math:`C` is a type of constructor for an inductive type :math:`I`. Let :math:`P` be a term that represents the property to be -proved. We assume :math:`r` is the number of parameters and :math:`p` is the number of +proved. We assume :math:`r` is the number of parameters and :math:`s` is the number of arguments. We define a new type :math:`\{c:C\}^P` which represents the type of the branch @@ -1443,8 +1489,8 @@ corresponding to the :math:`c:C` constructor. .. math:: \begin{array}{ll} - \{c:(I~p_1\ldots p_r\ t_1 \ldots t_p)\}^P &\equiv (P~t_1\ldots ~t_p~c) \\ - \{c:\forall~x:T,C\}^P &\equiv \forall~x:T,\{(c~x):C\}^P + \{c:(I~q_1\ldots q_r\ t_1 \ldots t_s)\}^P &\equiv (P~t_1\ldots ~t_s~c) \\ + \{c:∀ x:T,~C\}^P &\equiv ∀ x:T,~\{(c~x):C\}^P \end{array} We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:`c`. @@ -1463,7 +1509,7 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math: can be represented in abstract syntax as .. math:: - \case(t,P,f 1 | f 2 ) + \case(t,P,f_1 | f_2 ) where @@ -1471,27 +1517,27 @@ We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math: :nowrap: \begin{eqnarray*} - P & = & \lambda~l~.~P^\prime\\ + P & = & λ l.~P^\prime\\ f_1 & = & t_1\\ - f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 + f_2 & = & λ (hd:\nat).~λ (tl:\List~\nat).~t_2 \end{eqnarray*} According to the definition: .. math:: - \{(\kw{nil}~\nat)\}^P ≡ \{(\kw{nil}~\nat) : (\List~\nat)\}^P ≡ (P~(\kw{nil}~\nat)) + \{(\Nil~\nat)\}^P ≡ \{(\Nil~\nat) : (\List~\nat)\}^P ≡ (P~(\Nil~\nat)) .. math:: \begin{array}{rl} - \{(\kw{cons}~\nat)\}^P & ≡\{(\kw{cons}~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, \{(\kw{cons}~\nat~n) : \List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat, \{(\kw{cons}~\nat~n~l) : \List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat,(P~(\kw{cons}~\nat~n~l)). + \{(\cons~\nat)\}^P & ≡\{(\cons~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat,~\{(\cons~\nat~n) : (\List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat,~∀ l:\List~\nat,~\{(\cons~\nat~n~l) : (\List~\nat)\}^P \\ + & ≡∀ n:\nat,~∀ l:\List~\nat,~(P~(\cons~\nat~n~l)). \end{array} - Given some :math:`P` then :math:`\{(\kw{nil}~\nat)\}^P` represents the expected type of :math:`f_1` , - and :math:`\{(\kw{cons}~\nat)\}^P` represents the expected type of :math:`f_2`. + Given some :math:`P` then :math:`\{(\Nil~\nat)\}^P` represents the expected type of :math:`f_1`, + and :math:`\{(\cons~\nat)\}^P` represents the expected type of :math:`f_2`. .. _Typing-rule: @@ -1512,7 +1558,7 @@ following typing rule E[Γ] ⊢ \case(c,P,f_1 |… |f_l ) : (P~t_1 … t_s~c) provided :math:`I` is an inductive type in a -definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_n ]` and +definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;~…;~c_n :C_n ]` and :math:`c_{p_1} … c_{p_l}` are the only constructors of :math:`I`. @@ -1527,8 +1573,8 @@ definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_ E[Γ] ⊢ t : (\List ~\nat) \\ E[Γ] ⊢ P : B \\ [(\List ~\nat)|B] \\ - E[Γ] ⊢ f_1 : {(\kw{nil} ~\nat)}^P \\ - E[Γ] ⊢ f_2 : {(\kw{cons} ~\nat)}^P + E[Γ] ⊢ f_1 : \{(\Nil ~\nat)\}^P \\ + E[Γ] ⊢ f_2 : \{(\cons ~\nat)\}^P \end{array} ------------------------------------------------ E[Γ] ⊢ \case(t,P,f_1 |f_2 ) : (P~t) @@ -1551,7 +1597,7 @@ The ι-contraction of this term is :math:`(f_i~a_1 … a_m )` leading to the general reduction rule: .. math:: - \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_n ) \triangleright_ι (f_i~a_1 … a_m ) + \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l ) \triangleright_ι (f_i~a_1 … a_m ) .. _Fixpoint-definitions: @@ -1565,14 +1611,14 @@ concrete syntax for a recursive set of mutually recursive declarations is (with :math:`Γ_i` contexts): .. math:: - \fix~f_1 (Γ_1 ) :A_1 :=t_1 \with … \with~f_n (Γ_n ) :A_n :=t_n + \fix~f_1 (Γ_1 ) :A_1 :=t_1~\with … \with~f_n (Γ_n ) :A_n :=t_n The terms are obtained by projections from this set of declarations and are written .. math:: - \fix~f_1 (Γ_1 ) :A_1 :=t_1 \with … \with~f_n (Γ_n ) :A_n :=t_n \for~f_i + \fix~f_1 (Γ_1 ) :A_1 :=t_1~\with … \with~f_n (Γ_n ) :A_n :=t_n~\for~f_i In the inference rules, we represent such a term by @@ -1580,7 +1626,7 @@ In the inference rules, we represent such a term by \Fix~f_i\{f_1 :A_1':=t_1' … f_n :A_n':=t_n'\} with :math:`t_i'` (resp. :math:`A_i'`) representing the term :math:`t_i` abstracted (resp. -generalized) with respect to the bindings in the context Γ_i , namely +generalized) with respect to the bindings in the context :math:`Γ_i`, namely :math:`t_i'=λ Γ_i . t_i` and :math:`A_i'=∀ Γ_i , A_i`. @@ -1592,7 +1638,7 @@ The typing rule is the expected one for a fixpoint. .. inference:: Fix (E[Γ] ⊢ A_i : s_i )_{i=1… n} - (E[Γ,f_1 :A_1 ,…,f_n :A_n ] ⊢ t_i : A_i )_{i=1… n} + (E[Γ;~f_1 :A_1 ;~…;~f_n :A_n ] ⊢ t_i : A_i )_{i=1… n} ------------------------------------------------------- E[Γ] ⊢ \Fix~f_i\{f_1 :A_1 :=t_1 … f_n :A_n :=t_n \} : A_i @@ -1608,31 +1654,31 @@ instance in the case of natural numbers, a proof of the induction principle of type .. math:: - ∀ P:\nat→\Prop, (P~O)→(∀ n:\nat, (P~n)→(P~(\kw{S}~n)))→ ∀ n:\nat, (P~n) + ∀ P:\nat→\Prop,~(P~\nO)→(∀ n:\nat,~(P~n)→(P~(\nS~n)))→ ∀ n:\nat,~(P~n) can be represented by the term: .. math:: \begin{array}{l} - λ P:\nat→\Prop. λ f:(P~O). λ g:(∀ n:\nat, (P~n)→(P~(S~n))).\\ - \Fix~h\{h:∀ n:\nat, (P~n):=λ n:\nat. \case(n,P,f | λp:\nat. (g~p~(h~p)))\} + λ P:\nat→\Prop.~λ f:(P~\nO).~λ g:(∀ n:\nat,~(P~n)→(P~(\nS~n))).\\ + \Fix~h\{h:∀ n:\nat,~(P~n):=λ n:\nat.~\case(n,P,f | λp:\nat.~(g~p~(h~p)))\} \end{array} Before accepting a fixpoint definition as being correctly typed, we check that the definition is “guarded”. A precise analysis of this notion can be found in :cite:`Gim94`. The first stage is to precise on which argument the fixpoint will be decreasing. The type of this argument -should be an inductive definition. For doing this, the syntax of +should be an inductive type. For doing this, the syntax of fixpoints is extended and becomes .. math:: - \Fix~f_i\{f_1/k_1 :A_1':=t_1' … f_n/k_n :A_n':=t_n'\} + \Fix~f_i\{f_1/k_1 :A_1:=t_1 … f_n/k_n :A_n:=t_n\} where :math:`k_i` are positive integers. Each :math:`k_i` represents the index of -parameter of :math:`f_i` , on which :math:`f_i` is decreasing. Each :math:`A_i` should be a +parameter of :math:`f_i`, on which :math:`f_i` is decreasing. Each :math:`A_i` should be a type (reducible to a term) starting with at least :math:`k_i` products -:math:`∀ y_1 :B_1 ,… ∀ y_{k_i} :B_{k_i} , A_i'` and :math:`B_{k_i}` an inductive type. +:math:`∀ y_1 :B_1 ,~… ∀ y_{k_i} :B_{k_i} ,~A_i'` and :math:`B_{k_i}` an inductive type. Now in the definition :math:`t_i`, if :math:`f_j` occurs then it should be applied to at least :math:`k_j` arguments and the :math:`k_j`-th argument should be @@ -1642,26 +1688,26 @@ The definition of being structurally smaller is a bit technical. One needs first to define the notion of *recursive arguments of a constructor*. For an inductive definition :math:`\ind{r}{Γ_I}{Γ_C}`, if the type of a constructor :math:`c` has the form -:math:`∀ p_1 :P_1 ,… ∀ p_r :P_r, ∀ x_1:T_1, … ∀ x_r :T_r, (I_j~p_1 … p_r~t_1 … t_s )`, +:math:`∀ p_1 :P_1 ,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_m :T_m,~(I_j~p_1 … p_r~t_1 … t_s )`, then the recursive arguments will correspond to :math:`T_i` in which one of the :math:`I_l` occurs. The main rules for being structurally smaller are the following. Given a variable :math:`y` of an inductively defined type in a declaration -:math:`\ind{r}{Γ_I}{Γ_C}` where :math:`Γ_I` is :math:`[I_1 :A_1 ;…;I_k :A_k]`, and :math:`Γ_C` is -:math:`[c_1 :C_1 ;…;c_n :C_n ]`, the terms structurally smaller than :math:`y` are: +:math:`\ind{r}{Γ_I}{Γ_C}` where :math:`Γ_I` is :math:`[I_1 :A_1 ;~…;~I_k :A_k]`, and :math:`Γ_C` is +:math:`[c_1 :C_1 ;~…;~c_n :C_n ]`, the terms structurally smaller than :math:`y` are: -+ :math:`(t~u)` and :math:`λ x:u . t` when :math:`t` is structurally smaller than :math:`y`. ++ :math:`(t~u)` and :math:`λ x:U .~t` when :math:`t` is structurally smaller than :math:`y`. + :math:`\case(c,P,f_1 … f_n)` when each :math:`f_i` is structurally smaller than :math:`y`. If :math:`c` is :math:`y` or is structurally smaller than :math:`y`, its type is an inductive - definition :math:`I_p` part of the inductive declaration corresponding to :math:`y`. + type :math:`I_p` part of the inductive definition corresponding to :math:`y`. Each :math:`f_i` corresponds to a type of constructor - :math:`C_q ≡ ∀ p_1 :P_1 ,…,∀ p_r :P_r , ∀ y_1 :B_1 , … ∀ y_k :B_k , (I~a_1 … a_k )` - and can consequently be written :math:`λ y_1 :B_1' . … λ y_k :B_k'. g_i`. (:math:`B_i'` is + :math:`C_q ≡ ∀ p_1 :P_1 ,~…,∀ p_r :P_r ,~∀ y_1 :B_1 ,~… ∀ y_m :B_m ,~(I_p~p_1 … p_r~t_1 … t_s )` + and can consequently be written :math:`λ y_1 :B_1' .~… λ y_m :B_m'.~g_i`. (:math:`B_i'` is obtained from :math:`B_i` by substituting parameters for variables) the variables :math:`y_j` occurring in :math:`g_i` corresponding to recursive arguments :math:`B_i` (the - ones in which one of the :math:`I_l` occurs) are structurally smaller than y. + ones in which one of the :math:`I_l` occurs) are structurally smaller than :math:`y`. The following definitions are correct, we enter them using the :cmd:`Fixpoint` @@ -1702,7 +1748,7 @@ Let :math:`F` be the set of declarations: The reduction for fixpoints is: .. math:: - (\Fix~f_i \{F\} a_1 …a_{k_i}) \triangleright_ι \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i} + (\Fix~f_i \{F\}~a_1 …a_{k_i}) ~\triangleright_ι~ \subst{t_i}{f_k}{\Fix~f_k \{F\}}_{k=1… n} ~a_1 … a_{k_i} when :math:`a_{k_i}` starts with a constructor. This last restriction is needed in order to keep strong normalization and corresponds to the reduction @@ -1712,13 +1758,11 @@ possible: .. math:: :nowrap: - {\def\plus{\mathsf{plus}} - \def\tri{\triangleright_\iota} - \begin{eqnarray*} - \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ - & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ - & \tri & \nS~(\nS~(\nS~\nO))\\ - \end{eqnarray*}} + \begin{eqnarray*} + \plus~(\nS~(\nS~\nO))~(\nS~\nO)~& \trii & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ + & \trii & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ + & \trii & \nS~(\nS~(\nS~\nO))\\ + \end{eqnarray*} .. _Mutual-induction: @@ -1746,11 +1790,11 @@ One can modify a global declaration by generalizing it over a previously assumed constant :math:`c`. For doing that, we need to modify the reference to the global declaration in the subsequent global environment and local context by explicitly applying this constant to -the constant :math:`c'`. +the constant :math:`c`. -Below, if :math:`Γ` is a context of the form :math:`[y_1 :A_1 ;…;y_n :A_n]`, we write -:math:`∀x:U,\subst{Γ}{c}{x}` to mean -:math:`[y_1 :∀ x:U,\subst{A_1}{c}{x};…;y_n :∀ x:U,\subst{A_n}{c}{x}]` +Below, if :math:`Γ` is a context of the form :math:`[y_1 :A_1 ;~…;~y_n :A_n]`, we write +:math:`∀x:U,~\subst{Γ}{c}{x}` to mean +:math:`[y_1 :∀ x:U,~\subst{A_1}{c}{x};~…;~y_n :∀ x:U,~\subst{A_n}{c}{x}]` and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution :math:`E\{y_1 /(y_1~c)\}…\{y_n/(y_n~c)\}`. @@ -1760,25 +1804,25 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution **First abstracting property:** .. math:: - \frac{\WF{E;c:U;E′;c′:=t:T;E″}{Γ}} - {\WF{E;c:U;E′;c′:=λ x:U. \subst{t}{c}{x}:∀x:U,\subst{T}{c}{x};\subst{E″}{c′}{(c′~c)}} - {\subst{Γ}{c}{(c~c′)}}} + \frac{\WF{E;~c:U;~E′;~c′:=t:T;~E″}{Γ}} + {\WF{E;~c:U;~E′;~c′:=λ x:U.~\subst{t}{c}{x}:∀x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}} + {\subst{Γ}{c′}{(c′~c)}}} .. math:: - \frac{\WF{E;c:U;E′;c′:T;E″}{Γ}} - {\WF{E;c:U;E′;c′:∀ x:U,\subst{T}{c}{x};\subst{E″}{c′}{(c′~c)}}{Γ{c/(c~c′)}}} + \frac{\WF{E;~c:U;~E′;~c′:T;~E″}{Γ}} + {\WF{E;~c:U;~E′;~c′:∀ x:U,~\subst{T}{c}{x};~\subst{E″}{c′}{(c′~c)}}{\subst{Γ}{c′}{(c′~c)}}} .. math:: - \frac{\WF{E;c:U;E′;\ind{p}{Γ_I}{Γ_C};E″}{Γ}} - {\WFTWOLINES{E;c:U;E′;\ind{p+1}{∀ x:U,\subst{Γ_I}{c}{x}}{∀ x:U,\subst{Γ_C}{c}{x}}; - \subst{E″}{|Γ_I ,Γ_C |}{|Γ_I ,Γ_C | c}} - {\subst{Γ}{|Γ_I ,Γ_C|}{|Γ_I ,Γ_C | c}}} + \frac{\WF{E;~c:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} + {\WFTWOLINES{E;~c:U;~E′;~\ind{p+1}{∀ x:U,~\subst{Γ_I}{c}{x}}{∀ x:U,~\subst{Γ_C}{c}{x}};~ + \subst{E″}{|Γ_I ;Γ_C |}{|Γ_I ;Γ_C | c}} + {\subst{Γ}{|Γ_I ;Γ_C|}{|Γ_I ;Γ_C | c}}} One can similarly modify a global declaration by generalizing it over -a previously defined constant :math:`c′`. Below, if :math:`Γ` is a context of the form -:math:`[y_1 :A_1 ;…;y_n :A_n]`, we write :math:`\subst{Γ}{c}{u}` to mean -:math:`[y_1 :\subst{A_1} {c}{u};…;y_n:\subst{A_n} {c}{u}]`. +a previously defined constant :math:`c`. Below, if :math:`Γ` is a context of the form +:math:`[y_1 :A_1 ;~…;~y_n :A_n]`, we write :math:`\subst{Γ}{c}{u}` to mean +:math:`[y_1 :\subst{A_1} {c}{u};~…;~y_n:\subst{A_n} {c}{u}]`. .. _Second-abstracting-property: @@ -1786,16 +1830,16 @@ a previously defined constant :math:`c′`. Below, if :math:`Γ` is a context of **Second abstracting property:** .. math:: - \frac{\WF{E;c:=u:U;E′;c′:=t:T;E″}{Γ}} - {\WF{E;c:=u:U;E′;c′:=(\letin{x}{u:U}{\subst{t}{c}{x}}):\subst{T}{c}{u};E″}{Γ}} + \frac{\WF{E;~c:=u:U;~E′;~c′:=t:T;~E″}{Γ}} + {\WF{E;~c:=u:U;~E′;~c′:=(\letin{x}{u:U}{\subst{t}{c}{x}}):\subst{T}{c}{u};~E″}{Γ}} .. math:: - \frac{\WF{E;c:=u:U;E′;c′:T;E″}{Γ}} - {\WF{E;c:=u:U;E′;c′:\subst{T}{c}{u};E″}{Γ}} + \frac{\WF{E;~c:=u:U;~E′;~c′:T;~E″}{Γ}} + {\WF{E;~c:=u:U;~E′;~c′:\subst{T}{c}{u};~E″}{Γ}} .. math:: - \frac{\WF{E;c:=u:U;E′;\ind{p}{Γ_I}{Γ_C};E″}{Γ}} - {\WF{E;c:=u:U;E′;\ind{p}{\subst{Γ_I}{c}{u}}{\subst{Γ_C}{c}{u}};E″}{Γ}} + \frac{\WF{E;~c:=u:U;~E′;~\ind{p}{Γ_I}{Γ_C};~E″}{Γ}} + {\WF{E;~c:=u:U;~E′;~\ind{p}{\subst{Γ_I}{c}{u}}{\subst{Γ_C}{c}{u}};~E″}{Γ}} .. _Pruning-the-local-context: @@ -1810,7 +1854,7 @@ One can consequently derive the following property. .. inference:: First pruning property: - \WF{E;c:U;E′}{Γ} + \WF{E;~c:U;~E′}{Γ} c~\kw{does not occur in}~E′~\kw{and}~Γ -------------------------------------- \WF{E;E′}{Γ} @@ -1820,7 +1864,7 @@ One can consequently derive the following property. .. inference:: Second pruning property: - \WF{E;c:=u:U;E′}{Γ} + \WF{E;~c:=u:U;~E′}{Γ} c~\kw{does not occur in}~E′~\kw{and}~Γ -------------------------------------- \WF{E;E′}{Γ} @@ -1861,10 +1905,10 @@ in the sort :math:`\Set`, which is extended to a domain in any sort: .. inference:: ProdImp E[Γ] ⊢ T : s - s ∈ {\Sort} - E[Γ::(x:T)] ⊢ U : Set + s ∈ \Sort + E[Γ::(x:T)] ⊢ U : \Set --------------------- - E[Γ] ⊢ ∀ x:T,U : Set + E[Γ] ⊢ ∀ x:T,~U : \Set This extension has consequences on the inductive definitions which are allowed. In the impredicative system, one can build so-called *large @@ -1879,15 +1923,15 @@ impredicative system for sort :math:`\Set` become: .. inference:: Set1 - s ∈ \{Prop, Set\} + s ∈ \{\Prop, \Set\} ----------------- - [I:Set|I→ s] + [I:\Set|I→ s] .. inference:: Set2 I~\kw{is a small inductive definition} s ∈ \{\Type(i)\} ---------------- - [I:Set|I→ s] + [I:\Set|I→ s] diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 85474a3e98..d1b95e6203 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -97,25 +97,25 @@ Logic The basic library of |Coq| comes with the definitions of standard (intuitionistic) logical connectives (they are defined as inductive constructions). They are equipped with an appealing syntax enriching the -subclass `form` of the syntactic class `term`. The syntax of `form` -is shown below: +subclass :token:`form` of the syntactic class :token:`term`. The syntax of +:token:`form` is shown below: .. /!\ Please keep the blanks in the lines below, experimentally they produce a nice last column. Or even better, find a proper way to do this! .. productionlist:: - form : True (True) - : | False (False) - : | ~ `form` (not) - : | `form` /\ `form` (and) - : | `form` \/ `form` (or) - : | `form` -> `form` (primitive implication) - : | `form` <-> `form` (iff) - : | forall `ident` : `type`, `form` (primitive for all) - : | exists `ident` [: `specif`], `form` (ex) - : | exists2 `ident` [: `specif`], `form` & `form` (ex2) - : | `term` = `term` (eq) - : | `term` = `term` :> `specif` (eq) + form : True (True) + : False (False) + : ~ `form` (not) + : `form` /\ `form` (and) + : `form` \/ `form` (or) + : `form` -> `form` (primitive implication) + : `form` <-> `form` (iff) + : forall `ident` : `type`, `form` (primitive for all) + : exists `ident` [: `specif`], `form` (ex) + : exists2 `ident` [: `specif`], `form` & `form` (ex2) + : `term` = `term` (eq) + : `term` = `term` :> `specif` (eq) .. note:: @@ -146,7 +146,7 @@ Propositional Connectives First, we find propositional calculus connectives: -.. coqtop:: in +.. coqdoc:: Inductive True : Prop := I. Inductive False : Prop := . @@ -236,7 +236,7 @@ Finally, a few easy lemmas are provided. single: eq_rect (term) single: eq_rect_r (term) -.. coqtop:: in +.. coqdoc:: Theorem absurd : forall A C:Prop, A -> ~ A -> C. Section equality. @@ -264,7 +264,7 @@ arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. -.. coqtop:: in +.. coqtop:: in abort Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) @@ -287,13 +287,13 @@ the next section :ref:`specification`): .. productionlist:: specif : `specif` * `specif` (prod) - : | `specif` + `specif` (sum) - : | `specif` + { `specif` } (sumor) - : | { `specif` } + { `specif` } (sumbool) - : | { `ident` : `specif` | `form` } (sig) - : | { `ident` : `specif` | `form` & `form` } (sig2) - : | { `ident` : `specif` & `specif` } (sigT) - : | { `ident` : `specif` & `specif` & `specif` } (sigT2) + : `specif` + `specif` (sum) + : `specif` + { `specif` } (sumor) + : { `specif` } + { `specif` } (sumbool) + : { `ident` : `specif` | `form` } (sig) + : { `ident` : `specif` | `form` & `form` } (sig2) + : { `ident` : `specif` & `specif` } (sigT) + : { `ident` : `specif` & `specif` & `specif` } (sigT2) term : (`term`, `term`) (pair) @@ -465,7 +465,7 @@ Intuitionistic Type Theory. single: Choice2 (term) single: bool_choice (term) -.. coqtop:: in +.. coqdoc:: Lemma Choice : forall (S S':Set) (R:S -> S' -> Prop), @@ -506,7 +506,7 @@ realizability interpretation. single: absurd_set (term) single: and_rect (term) -.. coqtop:: in +.. coqdoc:: Definition except := False_rec. Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. @@ -531,7 +531,7 @@ section :tacn:`refine`). This scope is opened by default. The following example is not part of the standard library, but it shows the usage of the notations: - .. coqtop:: in + .. coqtop:: in reset Fixpoint even (n:nat) : bool := match n with @@ -558,7 +558,7 @@ section :tacn:`refine`). This scope is opened by default. Now comes the content of module ``Peano``: -.. coqtop:: in +.. coqdoc:: Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := @@ -606,11 +606,14 @@ Finally, it gives the definition of the usual orderings ``le``, single: ge (term) single: gt (term) -.. coqtop:: in +.. This emits a notation already used warning but it won't be shown to + the user. + +.. coqtop:: in warn Inductive le (n:nat) : nat -> Prop := | le_n : le n n - | le_S : forall m:nat, n <= m -> n <= (S m). + | le_S : forall m:nat, n <= m -> n <= (S m) where "n <= m" := (le n m) : nat_scope. Definition lt (n m:nat) := S n <= m. Definition ge (n m:nat) := m <= n. @@ -625,7 +628,7 @@ induction principle. single: nat_case (term) single: nat_double_ind (term) -.. coqtop:: in +.. coqdoc:: Theorem nat_case : forall (n:nat) (P:nat -> Prop), @@ -652,7 +655,7 @@ well-founded induction, in module ``Wf.v``. single: Acc_rect (term) single: well_founded (term) -.. coqtop:: in +.. coqdoc:: Section Well_founded. Variable A : Type. @@ -681,7 +684,7 @@ fixpoint equation can be proved. single: Fix_F_inv (term) single: Fix_F_eq (term) -.. coqtop:: in +.. coqdoc:: Section FixPoint. Variable P : A -> Type. @@ -715,7 +718,7 @@ of equality: .. coqtop:: in Inductive identity (A:Type) (a:A) : A -> Type := - identity_refl : identity a a. + identity_refl : identity A a a. Some properties of ``identity`` are proved in the module ``Logic_Type``, which also provides the definition of ``Type`` level negation: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 9dae7fd102..695dea222f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -25,48 +25,47 @@ expressions. In this sense, the :cmd:`Record` construction allows defining record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. field : `ident` [ `binders` ] : `type` [ where `notation` ] - : | `ident` [ `binders` ] [: `type` ] := `term` - -In the expression: + : `ident` [ `binders` ] [: `type` ] := `term` .. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } } -the first identifier :token:`ident` is the name of the defined record and :token:`sort` is its -type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, -the default name ``Build_``\ :token:`ident`, where :token:`ident` is the record name, is used. If :token:`sort` is -omitted, the default sort is `\Type`. The identifiers inside the brackets are the names of -fields. For a given field :token:`ident`, its type is :g:`forall binders, type`. -Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the -order of the fields is important. Finally, :token:`binders` are parameters of the record. + The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its + type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, + the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is + omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of + fields. For a given field :token:`ident`, its type is :n:`forall @binders, @type`. + Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the + order of the fields is important. Finally, :token:`binders` are parameters of the record. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: -:n:`Record @ident @binders : @sort := { @ident₁ : @type₁ ; @ident₂ := @term₂ ; @ident₃ : @type₃ }`. -in which case the correctness of :n:`@type₃` may rely on the instance :n:`@term₂` of :n:`@ident₂` and :n:`@term₂` may in turn depend on :n:`@ident₁`. +:n:`Record @ident @binders : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`. +in which case the correctness of :n:`@type__3` may rely on the instance :n:`@term__2` of :n:`@ident__2` and :n:`@term__2` may in turn depend on :n:`@ident__1`. .. example:: The set of rational numbers may be defined as: - .. coqtop:: reset all + .. coqtop:: reset all - Record Rat : Set := mkRat - {sign : bool; - top : nat; - bottom : nat; - Rat_bottom_cond : 0 <> bottom; - Rat_irred_cond : - forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}. + Record Rat : Set := mkRat + { sign : bool + ; top : nat + ; bottom : nat + ; Rat_bottom_cond : 0 <> bottom + ; Rat_irred_cond : + forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1 + }. -Remark here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` and ``Rat_irred_cond`` -depends on both ``top`` and ``bottom``. + Note here that the fields ``Rat_bottom_cond`` depends on the field ``bottom`` + and ``Rat_irred_cond`` depends on both ``top`` and ``bottom``. Let us now see the work done by the ``Record`` macro. First the macro generates a variant type definition with just one constructor: -:n:`Variant @ident {? @binders } : @sort := @ident₀ {? @binders }`. +:n:`Variant @ident {? @binders } : @sort := @ident__0 {? @binders }`. -To build an object of type :n:`@ident`, one should provide the constructor -:n:`@ident₀` with the appropriate number of terms filling the fields of the record. +To build an object of type :token:`ident`, one should provide the constructor +:n:`@ident__0` with the appropriate number of terms filling the fields of the record. .. example:: @@ -131,7 +130,7 @@ This syntax can also be used for pattern matching. end). The macro generates also, when it is possible, the projection -functions for destructuring an object of type `\ident`. These +functions for destructuring an object of type :token:`ident`. These projection functions are given the names of the corresponding fields. If a field is named `_` then no projection is built for it. In our example: @@ -149,33 +148,33 @@ available: Eval compute in half.(top). -It can be activated for printing with - .. flag:: Printing Projections -.. example:: + This flag activates the dot notation for printing. - .. coqtop:: all + .. example:: - Set Printing Projections. - Check top half. + .. coqtop:: all + + Set Printing Projections. + Check top half. .. FIXME: move this to the main grammar in the spec chapter .. _record_projections_grammar: .. productionlist:: terms - projection : projection `.` ( `qualid` ) - : | projection `.` ( `qualid` `arg` … `arg` ) - : | projection `.` ( @`qualid` `term` … `term` ) + projection : `term` `.` ( `qualid` ) + : `term` `.` ( `qualid` `arg` … `arg` ) + : `term` `.` ( @`qualid` `term` … `term` ) Syntax of Record projections -The corresponding grammar rules are given in the preceding grammar. When `qualid` -denotes a projection, the syntax `term.(qualid)` is equivalent to `qualid term`, -the syntax `term.(qualid` |arg_1| |arg_n| `)` to `qualid` |arg_1| `…` |arg_n| `term`, -and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` |term_n| `term`. -In each case, `term` is the object projected and the +The corresponding grammar rules are given in the preceding grammar. When :token:`qualid` +denotes a projection, the syntax :n:`@term.(@qualid)` is equivalent to :n:`@qualid @term`, +the syntax :n:`@term.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term`. +and the syntax :n:`@term.(@@qualid {+ @term })` to :n:`@@qualid {+ @term } @term`. +In each case, :token:`term` is the object projected and the other arguments are the parameters of the inductive type. @@ -199,22 +198,22 @@ other arguments are the parameters of the inductive type. This message is followed by an explanation of this impossibility. There may be three reasons: - #. The name `ident` already exists in the environment (see :cmd:`Axiom`). - #. The body of `ident` uses an incorrect elimination for - `ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). - #. The type of the projections `ident` depends on previous + #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`). + #. The body of :token:`ident` uses an incorrect elimination for + :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). + #. The type of the projections :token:`ident` depends on previous projections which themselves could not be defined. .. exn:: Records declared with the keyword Record or Structure cannot be recursive. - The record name `ident` appears in the type of its fields, but uses - the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. + The record name :token:`ident` appears in the type of its fields, but uses + the keyword ``Record``. Use the keyword ``Inductive`` or ``CoInductive`` instead. .. exn:: Cannot handle mutually (co)inductive records. - Records cannot be defined as part of mutually inductive (or - co-inductive) definitions, whether with records only or mixed with - standard definitions. + Records cannot be defined as part of mutually inductive (or + co-inductive) definitions, whether with records only or mixed with + standard definitions. During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in Section @@ -235,7 +234,8 @@ Primitive Projections extended the Calculus of Inductive Constructions with a new binary term constructor `r.(p)` representing a primitive projection `p` applied to a record object `r` (i.e., primitive projections are always applied). - Even if the record type has parameters, these do not appear at + Even if the record type has parameters, these do not appear + in the internal representation of applications of the projection, considerably reducing the sizes of terms when manipulating parameterized records and type checking time. On the user level, primitive projections can be used as a replacement @@ -247,11 +247,6 @@ Primitive Projections printing time (even though they are absent in the actual AST manipulated by the kernel). -.. flag:: Printing Primitive Projection Compatibility - - This compatibility option (on by default) governs the - printing of pattern matching over primitive records. - Primitive Record Types ++++++++++++++++++++++ @@ -297,8 +292,8 @@ the folded version delta-reduces to the unfolded version. This allows to precisely mimic the usual unfolding rules of constants. Projections obey the usual ``simpl`` flags of the ``Arguments`` command in particular. There is currently no way to input unfolded primitive projections at the -user-level, and one must use the :flag:`Printing Primitive Projection Compatibility` -to display unfolded primitive projections as matches and distinguish them from folded ones. +user-level, and there is no way to display unfolded projections differently +from folded ones. Compatibility Projections and :g:`match` @@ -310,7 +305,7 @@ an object of the record type as arguments, and whose body is an application of the unfolded primitive projection of the same name. These constants are used when elaborating partial applications of the projection. One can distinguish them from applications of the primitive -projection if the :flag`Printing Primitive Projection Parameters` option +projection if the :flag:`Printing Primitive Projection Parameters` option is off: For a primitive projection application, parameters are printed as underscores while for the compatibility projections they are printed as usual. @@ -382,7 +377,7 @@ we have the following equivalence | right _ => false end). -Notice that the printing uses the :g:`if` syntax because `sumbool` is +Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is declared as such (see :ref:`controlling-match-pp`). .. _irrefutable-patterns: @@ -601,17 +596,17 @@ The following experimental command is available when the ``FunInd`` library has .. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term -This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper -for several ways of defining a function *and other useful related -objects*, namely: an induction principle that reflects the recursive -structure of the function (see :tacn:`function induction`) and its fixpoint equality. -The meaning of this declaration is to define a function ident, -similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must -be given (unless the function is not recursive), but it might not -necessarily be *structurally* decreasing. The point of the {} annotation -is to name the decreasing argument *and* to describe which kind of -decreasing criteria must be used to ensure termination of recursive -calls. + This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper + for several ways of defining a function *and other useful related + objects*, namely: an induction principle that reflects the recursive + structure of the function (see :tacn:`function induction`) and its fixpoint equality. + The meaning of this declaration is to define a function ident, + similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must + be given (unless the function is not recursive), but it might not + necessarily be *structurally* decreasing. The point of the {} annotation + is to name the decreasing argument *and* to describe which kind of + decreasing criteria must be used to ensure termination of recursive + calls. The ``Function`` construction also enjoys the ``with`` extension to define mutually recursive definitions. However, this feature does not work @@ -655,8 +650,7 @@ with applications only *at the end* of each branch. Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the -presence of partial application of `wrong` in the body of -`wrong` : +presence of partial application of :g:`wrong` in the body of :g:`wrong`: .. coqtop:: all @@ -667,27 +661,32 @@ For now, dependent cases are not treated for non structurally terminating functions. .. exn:: The recursive argument must be specified. + :undocumented: + .. exn:: No argument name @ident. + :undocumented: + .. exn:: Cannot use mutual definition with well-founded recursion or measure. + :undocumented: .. warn:: Cannot define graph for @ident. - The generation of the graph relation (`R_ident`) used to compute the induction scheme of ident - raised a typing error. Only `ident` is defined; the induction scheme - will not be generated. This error happens generally when: + The generation of the graph relation (:n:`R_@ident`) used to compute the induction scheme of ident + raised a typing error. Only :token:`ident` is defined; the induction scheme + will not be generated. This error happens generally when: - - the definition uses pattern matching on dependent types, - which ``Function`` cannot deal with yet. - - the definition is not a *pattern matching tree* as explained above. + - the definition uses pattern matching on dependent types, + which ``Function`` cannot deal with yet. + - the definition is not a *pattern matching tree* as explained above. .. warn:: Cannot define principle(s) for @ident. - The generation of the graph relation (`R_ident`) succeeded but the induction principle - could not be built. Only `ident` is defined. Please report. + The generation of the graph relation (:n:`R_@ident`) succeeded but the induction principle + could not be built. Only :token:`ident` is defined. Please report. .. warn:: Cannot build functional inversion principle. - `functional inversion` will not be available for the function. + :tacn:`functional inversion` will not be available for the function. .. seealso:: :ref:`functional-scheme` and :tacn:`function induction` @@ -696,39 +695,40 @@ used by ``Function``. A more precise description is given below. .. cmdv:: Function @ident {* @binder } : @type := @term - Defines the not recursive function `ident` as if declared with `Definition`. Moreover - the following are defined: + Defines the not recursive function :token:`ident` as if declared with + :cmd:`Definition`. Moreover the following are defined: - + `ident_rect`, `ident_rec` and `ident_ind`, which reflect the pattern - matching structure of `term` (see :cmd:`Inductive`); - + The inductive `R_ident` corresponding to the graph of `ident` (silently); - + `ident_complete` and `ident_correct` which are inversion information - linking the function and its graph. + + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, + which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); + + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); + + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which + are inversion information linking the function and its graph. .. cmdv:: Function @ident {* @binder } { struct @ident } : @type := @term - Defines the structural recursive function `ident` as if declared with ``Fixpoint``. Moreover the following are defined: + Defines the structural recursive function :token:`ident` as if declared + with :cmd:`Fixpoint`. Moreover the following are defined: + The same objects as above; - + The fixpoint equation of `ident`: `ident_equation`. + + The fixpoint equation of :token:`ident`: :n:`@ident_equation`. .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term -.. cmdv:: Function @ident {* @binder } { wf @term @ident } : @type := @term + Function @ident {* @binder } { wf @term @ident } : @type := @term Defines a recursive function by well-founded recursion. The module ``Recdef`` of the standard library must be loaded for this feature. The ``{}`` annotation is mandatory and must be one of the following: - + ``{measure`` `term` `ident` ``}`` with `ident` being the decreasing argument - and `term` being a function from type of `ident` to ``nat`` for which - value on the decreasing argument decreases (for the ``lt`` order on ``nat``) - at each recursive call of `term`. Parameters of the function are - bound in `term`\ ; - + ``{wf`` `term` `ident` ``}`` with `ident` being the decreasing argument and - `term` an ordering relation on the type of `ident` (i.e. of type + + :n:`{measure @term @ident }` with :token:`ident` being the decreasing argument + and :token:`term` being a function from type of :token:`ident` to :g:`nat` for which + value on the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) + at each recursive call of :token:`term`. Parameters of the function are + bound in :token:`term`; + + :n:`{wf @term @ident }` with :token:`ident` being the decreasing argument and + :token:`term` an ordering relation on the type of :token:`ident` (i.e. of type `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument - decreases at each recursive call of `term`. The order must be well-founded. - Parameters of the function are bound in `term`. + decreases at each recursive call of :token:`term`. The order must be well-founded. + Parameters of the function are bound in :token:`term`. Depending on the annotation, the user is left with some proof obligations that will be used to define the function. These proofs @@ -754,10 +754,46 @@ used by ``Function``. A more precise description is given below. Section mechanism ----------------- -The sectioning mechanism can be used to to organize a proof in -structured sections. Then local declarations become available (see -Section :ref:`gallina-definitions`). +Sections create local contexts which can be shared across multiple definitions. + +.. example:: + + Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. + + .. coqtop:: all + + Section s1. + + Inside a section, local parameters can be introduced using :cmd:`Variable`, + :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for + the first two). + + .. coqtop:: all + + Variables x y : nat. + The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions + won't persist when the section is closed, and all persistent definitions which + depend on `y'` will be prefixed with `let y' := y in`. + + .. coqtop:: in + + Let y' := y. + Definition x' := S x. + Definition x'' := x' + y'. + + .. coqtop:: all + + Print x'. + Print x''. + + End s1. + + Print x'. + Print x''. + + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. .. cmd:: Section @ident @@ -767,44 +803,81 @@ Section :ref:`gallina-definitions`). .. cmd:: End @ident - This command closes the section named `ident`. After closing of the - section, the local declarations (variables and local definitions) get - *discharged*, meaning that they stop being visible and that all global - objects defined in the section are generalized with respect to the - variables and local definitions they each depended on in the section. + This command closes the section named :token:`ident`. After closing of the + section, the local declarations (variables and local definitions, see :cmd:`Variable`) get + *discharged*, meaning that they stop being visible and that all global + objects defined in the section are generalized with respect to the + variables and local definitions they each depended on in the section. - .. example:: + .. exn:: This is not the last opened section. + :undocumented: - .. coqtop:: all +.. note:: + Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which + appear inside a section are canceled when the section is closed. - Section s1. +.. cmd:: Variable @ident : @type - Variables x y : nat. + This command links :token:`type` to the name :token:`ident` in the context of + the current section. When the current section is closed, name :token:`ident` + will be unknown and every object using this variable will be explicitly + parameterized (the variable is *discharged*). - Let y' := y. + .. exn:: @ident already exists. + :name: @ident already exists. (Variable) + :undocumented: - Definition x' := S x. + .. cmdv:: Variable {+ @ident } : @type - Definition x'' := x' + y'. + Links :token:`type` to each :token:`ident`. - Print x'. + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - End s1. + Declare one or more variables with various types. - Print x'. + .. cmdv:: Variables {+ ( {+ @ident } : @type) } + Hypothesis {+ ( {+ @ident } : @type) } + Hypotheses {+ ( {+ @ident } : @type) } + :name: Variables; Hypothesis; Hypotheses - Print x''. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. - Notice the difference between the value of `x’` and `x’’` inside section - `s1` and outside. +.. cmd:: Let @ident := @term - .. exn:: This is not the last opened section. + This command binds the value :token:`term` to the name :token:`ident` in the + environment of the current section. The name :token:`ident` is accessible + only within the current section. When the section is closed, all persistent + definitions and theorems within it and depending on :token:`ident` + will be prefixed by the let-in definition :n:`let @ident := @term in`. -**Remarks:** + .. exn:: @ident already exists. + :name: @ident already exists. (Let) + :undocumented: -#. Most commands, like ``Hint``, ``Notation``, option management, … which - appear inside a section are canceled when the section is closed. + .. cmdv:: Let @ident {? @binders } {? : @type } := @term + :undocumented: + .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} + :name: Let Fixpoint + :undocumented: + + .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} + :name: Let CoFixpoint + :undocumented: + +.. cmd:: Context @binders + + Declare variables in the context of the current section, like :cmd:`Variable`, + but also allowing implicit variables, :ref:`implicit-generalization`, and + let-binders. + + .. coqdoc:: + + Context {A : Type} (a b : A). + Context `{EqDec A}. + Context (b' := b). + +.. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`. Module system ------------- @@ -813,26 +886,26 @@ The module system provides a way of packaging related elements together, as well as a means of massive abstraction. .. productionlist:: modules - module_type : qualid - : | `module_type` with Definition qualid := term - : | `module_type` with Module qualid := qualid - : | qualid qualid … qualid - : | !qualid qualid … qualid - module_binding : ( [Import|Export] ident … ident : module_type ) + module_type : `qualid` + : `module_type` with Definition `qualid` := `term` + : `module_type` with Module `qualid` := `qualid` + : `qualid` `qualid` … `qualid` + : !`qualid` `qualid` … `qualid` + module_binding : ( [Import|Export] `ident` … `ident` : `module_type` ) module_bindings : `module_binding` … `module_binding` - module_expression : qualid … qualid - : | !qualid … qualid + module_expression : `qualid` … `qualid` + : !`qualid` … `qualid` Syntax of modules In the syntax of module application, the ! prefix indicates that any `Inline` directive in the type of the functor arguments will be ignored -(see the ``Module Type`` command below). +(see the :cmd:`Module Type` command below). .. cmd:: Module @ident - This command is used to start an interactive module named `ident`. + This command is used to start an interactive module named :token:`ident`. .. cmdv:: Module @ident {* @module_binding} @@ -845,21 +918,22 @@ In the syntax of module application, the ! prefix indicates that any .. cmdv:: Module @ident {* @module_binding} : @module_type - Starts an interactive functor with parameters given by the list of `module binding`, and output module - type `module_type`. + Starts an interactive functor with parameters given by the list of + :token:`module_bindings`, and output module type :token:`module_type`. .. cmdv:: Module @ident <: {+<: @module_type } - Starts an interactive module satisfying each `module_type`. + Starts an interactive module satisfying each :token:`module_type`. .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }. - Starts an interactive functor with parameters given by the list of `module_binding`. The output module type - is verified against each `module_type`. + Starts an interactive functor with parameters given by the list of + :token:`module_binding`. The output module type + is verified against each :token:`module_type`. .. cmdv:: Module [ Import | Export ] - Behaves like ``Module``, but automatically imports or exports the module. + Behaves like :cmd:`Module`, but automatically imports or exports the module. Reserved commands inside an interactive module ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -874,52 +948,55 @@ Reserved commands inside an interactive module .. cmd:: Include {+<+ @module} - is a shortcut for the commands ``Include`` `module` for each `module`. + is a shortcut for the commands :n:`Include @module` for each :token:`module`. .. cmd:: End @ident - This command closes the interactive module `ident`. If the module type + This command closes the interactive module :token:`ident`. If the module type was given the content of the module is matched against it and an error is signaled if the matching fails. If the module is basic (is not a functor) its components (constants, inductive types, submodules etc.) are now available through the dot notation. .. exn:: No such label @ident. + :undocumented: .. exn:: Signature components for label @ident do not match. + :undocumented: .. exn:: This is not the last opened module. + :undocumented: .. cmd:: Module @ident := @module_expression - This command defines the module identifier `ident` to be equal - to `module_expression`. + This command defines the module identifier :token:`ident` to be equal + to :token:`module_expression`. .. cmdv:: Module @ident {* @module_binding} := @module_expression - Defines a functor with parameters given by the list of `module_binding` and body `module_expression`. + Defines a functor with parameters given by the list of :token:`module_binding` and body :token:`module_expression`. .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression - Defines a functor with parameters given by the list of `module_binding` (possibly none), and output module type `module_type`, - with body `module_expression`. + Defines a functor with parameters given by the list of :token:`module_binding` (possibly none), and output module type :token:`module_type`, + with body :token:`module_expression`. .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression - Defines a functor with parameters given by module_bindings (possibly none) with body `module_expression`. - The body is checked against each |module_type_i|. + Defines a functor with parameters given by module_bindings (possibly none) with body :token:`module_expression`. + The body is checked against each :n:`@module_type__i`. .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression} - is equivalent to an interactive module where each `module_expression` is included. + is equivalent to an interactive module where each :token:`module_expression` is included. .. cmd:: Module Type @ident -This command is used to start an interactive module type `ident`. + This command is used to start an interactive module type :token:`ident`. - .. cmdv:: Module Type @ident {* @module_binding} + .. cmdv:: Module Type @ident {* @module_binding} - Starts an interactive functor type with parameters given by `module_bindings`. + Starts an interactive functor type with parameters given by :token:`module_bindings`. Reserved commands inside an interactive module type: @@ -931,7 +1008,7 @@ Reserved commands inside an interactive module type: .. cmd:: Include {+<+ @module} - is a shortcut for the command ``Include`` `module` for each `module`. + This is a shortcut for the command :n:`Include @module` for each :token:`module`. .. cmd:: @assumption_keyword Inline @assums :name: Inline @@ -941,31 +1018,32 @@ Reserved commands inside an interactive module type: .. cmd:: End @ident - This command closes the interactive module type `ident`. + This command closes the interactive module type :token:`ident`. .. exn:: This is not the last opened module type. + :undocumented: .. cmd:: Module Type @ident := @module_type - Defines a module type `ident` equal to `module_type`. + Defines a module type :token:`ident` equal to :token:`module_type`. .. cmdv:: Module Type @ident {* @module_binding} := @module_type - Defines a functor type `ident` specifying functors taking arguments `module_bindings` and - returning `module_type`. + Defines a functor type :token:`ident` specifying functors taking arguments :token:`module_bindings` and + returning :token:`module_type`. .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type } - is equivalent to an interactive module type were each `module_type` is included. + is equivalent to an interactive module type were each :token:`module_type` is included. .. cmd:: Declare Module @ident : @module_type - Declares a module `ident` of type `module_type`. + Declares a module :token:`ident` of type :token:`module_type`. .. cmdv:: Declare Module @ident {* @module_binding} : @module_type - Declares a functor with parameters given by the list of `module_binding` and output module type - `module_type`. + Declares a functor with parameters given by the list of :token:`module_binding` and output module type + :token:`module_type`. .. example:: @@ -1045,8 +1123,8 @@ specification: the y component is dropped as well as the body of x. End SIG. -The definition of ``N`` using the module type expression ``SIG`` with -``Definition T := nat`` is equivalent to the following one: +The definition of :g:`N` using the module type expression :g:`SIG` with +:g:`Definition T := nat` is equivalent to the following one: .. coqtop:: all @@ -1131,7 +1209,7 @@ component is equal ``nat`` and hence ``M1.T`` as specified. #. Modules and module types can be nested components of each other. #. One can have sections inside a module or a module type, but not a module or a module type inside a section. - #. Commands like ``Hint`` or ``Notation`` can also appear inside modules and + #. Commands like :cmd:`Hint` or :cmd:`Notation` can also appear inside modules and module types. Note that in case of a module definition like: :: @@ -1150,71 +1228,73 @@ component is equal ``nat`` and hence ``M1.T`` as specified. .. cmd:: Import @qualid - If `qualid` denotes a valid basic module (i.e. its module type is a - signature), makes its components available by their short names. + If :token:`qualid` denotes a valid basic module (i.e. its module type is a + signature), makes its components available by their short names. - .. example:: + .. example:: - .. coqtop:: reset all + .. coqtop:: reset all - Module Mod. + Module Mod. - Definition T:=nat. + Definition T:=nat. - Check T. + Check T. - End Mod. + End Mod. - Check Mod.T. + Check Mod.T. - Fail Check T. + Fail Check T. - Import Mod. + Import Mod. - Check T. + Check T. - Some features defined in modules are activated only when a module is - imported. This is for instance the case of notations (see :ref:`Notations`). + Some features defined in modules are activated only when a module is + imported. This is for instance the case of notations (see :ref:`Notations`). - Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` - command. Such declarations are only accessible through their fully - qualified name. + Declarations made with the ``Local`` flag are never imported by the :cmd:`Import` + command. Such declarations are only accessible through their fully + qualified name. - .. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Module A. + Module A. - Module B. + Module B. - Local Definition T := nat. + Local Definition T := nat. - End B. + End B. - End A. + End A. - Import A. + Import A. - Fail Check B.T. + Fail Check B.T. - .. cmdv:: Export @qualid - :name: Export + .. cmdv:: Export @qualid + :name: Export - When the module containing the command Export qualid - is imported, qualid is imported as well. + When the module containing the command ``Export`` qualid + is imported, qualid is imported as well. - .. exn:: @qualid is not a module. + .. exn:: @qualid is not a module. + :undocumented: - .. warn:: Trying to mask the absolute name @qualid! + .. warn:: Trying to mask the absolute name @qualid! + :undocumented: .. cmd:: Print Module @ident - Prints the module type and (optionally) the body of the module :n:`@ident`. + Prints the module type and (optionally) the body of the module :token:`ident`. .. cmd:: Print Module Type @ident - Prints the module type corresponding to :n:`@ident`. + Prints the module type corresponding to :token:`ident`. .. flag:: Short Module Printing @@ -1350,8 +1430,8 @@ with the same physical-to-logical translation and with an empty logical prefix. The command line option ``-R`` is a variant of ``-Q`` which has the strictly same behavior regarding loadpaths, but which also makes the corresponding ``.vo`` files available through their short names in a way -not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R`` `path` ``Lib`` -associates to the file path `path`\ ``/path/fOO/Bar/File.vo`` the logical name +not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R path Lib`` +associates to the file ``/path/fOO/Bar/File.vo`` the logical name ``Lib.fOO.Bar.File``, but allows this file to be accessed through the short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with identical base name are present in different subdirectories of a @@ -1365,7 +1445,7 @@ OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object files as described above. The OCaml loadpath is managed using the option ``-I`` `path` (in the OCaml world, there is neither a notion of logical name prefix nor a way to access files in -subdirectories of path). See the command ``Declare`` ``ML`` ``Module`` in +subdirectories of path). See the command :cmd:`Declare ML Module` in :ref:`compiled-files` to understand the need of the OCaml loadpath. See :ref:`command-line-options` for a more general view over the |Coq| command @@ -1566,38 +1646,39 @@ usual implicit arguments disambiguation syntax. Declaring Implicit Arguments ++++++++++++++++++++++++++++ -To set implicit arguments *a posteriori*, one can use the command: -.. cmd:: Arguments @qualid {* @possibly_bracketed_ident } - :name: Arguments (implicits) -where the list of `possibly_bracketed_ident` is a prefix of the list of -arguments of `qualid` where the ones to be declared implicit are -surrounded by square brackets and the ones to be declared as maximally -inserted implicits are surrounded by curly braces. +.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident } + :name: Arguments (implicits) -After the above declaration is issued, implicit arguments can just -(and have to) be skipped in any expression involving an application -of `qualid`. + This command is used to set implicit arguments *a posteriori*, + where the list of possibly bracketed :token:`ident` is a prefix of the list of + arguments of :token:`qualid` where the ones to be declared implicit are + surrounded by square brackets and the ones to be declared as maximally + inserted implicits are surrounded by curly braces. -Implicit arguments can be cleared with the following syntax: + After the above declaration is issued, implicit arguments can just + (and have to) be skipped in any expression involving an application + of :token:`qualid`. .. cmd:: Arguments @qualid : clear implicits -.. cmdv:: Global Arguments @qualid {* @possibly_bracketed_ident } + This command clears implicit arguments. + +.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident } - Says to recompute the implicit arguments of - `qualid` after ending of the current section if any, enforcing the + This command is used to recompute the implicit arguments of + :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* @possibly_bracketed_ident } +.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident } When in a module, tell not to activate the - implicit arguments ofqualid declared by this command to contexts that + implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } } +.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -1613,7 +1694,7 @@ Implicit arguments can be cleared with the following syntax: .. coqtop:: reset all - Inductive list (A:Type) : Type := + Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. @@ -1621,13 +1702,15 @@ Implicit arguments can be cleared with the following syntax: Arguments cons [A] _ _. - Arguments nil [A]. + Arguments nil {A}. Check (cons 3 nil). - Fixpoint map (A B:Type) (f:A->B) (l:list A) : list B := match l with nil => nil | cons a t => cons (f a) (map A B f t) end. + Fixpoint map (A B : Type) (f : A -> B) (l : list A) : list B := + match l with nil => nil | cons a t => cons (f a) (map A B f t) end. - Fixpoint length (A:Type) (l:list A) : nat := match l with nil => 0 | cons _ m => S (length A m) end. + Fixpoint length (A : Type) (l : list A) : nat := + match l with nil => 0 | cons _ m => S (length A m) end. Arguments map [A B] f l. @@ -1639,33 +1722,41 @@ Implicit arguments can be cleared with the following syntax: Check (fun l => map length l = map (list nat) nat length l). -Remark: To know which are the implicit arguments of an object, use the -command ``Print Implicit`` (see :ref:`displaying-implicit-args`). +.. note:: + To know which are the implicit arguments of an object, use the + command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). + +.. warn:: Argument number @num is a trailing implicit so must be maximal. + + For instance in + + .. coqtop:: all warn + Arguments prod _ [_]. Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| can also automatically detect what are the implicit arguments of a -defined object. The command is just - .. cmd:: Arguments @qualid : default implicits -The auto-detection is governed by options telling if strict, -contextual, or reversible-pattern implicit arguments must be -considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`, -:ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`). + This command tells |Coq| to automatically detect what are the implicit arguments of a + defined object. + + The auto-detection is governed by options telling if strict, + contextual, or reversible-pattern implicit arguments must be + considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`, + :ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`). -.. cmdv:: Global Arguments @qualid : default implicits + .. cmdv:: Global Arguments @qualid : default implicits - Tell to recompute the - implicit arguments of qualid after ending of the current section if - any. + Tell to recompute the + implicit arguments of qualid after ending of the current section if + any. -.. cmdv:: Local Arguments @qualid : default implicits + .. cmdv:: Local Arguments @qualid : default implicits - When in a module, tell not to activate the implicit arguments of `qualid` computed by this - declaration to contexts that requires the module. + When in a module, tell not to activate the implicit arguments of :token:`qualid` computed by this + declaration to contexts that requires the module. .. example:: @@ -1695,19 +1786,15 @@ of constants. For instance, the variable ``p`` below has type ``forall x,y:U, R x y -> forall z:U, R y z -> R x z``. As the variables ``x``, ``y`` and ``z`` appear strictly in the body of the type, they are implicit. -.. coqtop:: reset none - - Set Warnings "-local-declaration". - .. coqtop:: all - Variable X : Type. + Parameter X : Type. Definition Relation := X -> X -> Prop. Definition Transitivity (R:Relation) := forall x y:X, R x y -> forall z:X, R y z -> R x z. - Variables (R : Relation) (p : Transitivity R). + Parameters (R : Relation) (p : Transitivity R). Arguments p : default implicits. @@ -1715,7 +1802,7 @@ appear strictly in the body of the type, they are implicit. Print Implicit p. - Variables (a b c : X) (r1 : R a b) (r2 : R b c). + Parameters (a b c : X) (r1 : R a b) (r2 : R b c). Check (p r1 r2). @@ -1791,20 +1878,20 @@ Explicit applications In presence of non-strict or contextual argument, or in presence of partial applications, the synthesis of implicit arguments may fail, so one may have to give explicitly certain implicit arguments of an -application. The syntax for this is ``(`` `ident` ``:=`` `term` ``)`` where `ident` is the +application. The syntax for this is :n:`(@ident := @term)` where :token:`ident` is the name of the implicit argument and term is its corresponding explicit term. Alternatively, one can locally deactivate the hiding of implicit -arguments of a function by using the notation `@qualid` |term_1| … |term_n|. +arguments of a function by using the notation :n:`@qualid {+ @term }`. This syntax extension is given in the following grammar: .. _explicit_app_grammar: .. productionlist:: explicit_apps - term : @ qualid term … `term` - : | @ qualid - : | qualid `argument` … `argument` + term : @ `qualid` `term` … `term` + : @ `qualid` + : `qualid` `argument` … `argument` argument : `term` - : | (ident := `term`) + : (`ident` := `term`) Syntax for explicitly giving implicit arguments @@ -1820,10 +1907,10 @@ This syntax extension is given in the following grammar: Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Implicit arguments names can be redefined using the following syntax: - .. cmd:: Arguments @qualid {* @name} : @rename + This command is used to redefine the names of implicit arguments. + With the assert flag, ``Arguments`` can be used to assert that a given object has the expected number of arguments and that these arguments are named as expected. @@ -1845,11 +1932,12 @@ are named as expected. Displaying what the implicit arguments are ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -To display the implicit arguments associated to an object, and to know -if each of them is to be used maximally or not, use the command - .. cmd:: Print Implicit @qualid + Use this command to display the implicit arguments associated to an object, + and to know if each of them is to be used maximally or not. + + Explicit displaying of implicit arguments for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1909,9 +1997,10 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: Canonical Structure @qualid +.. cmd:: Canonical {? Structure } @qualid - This command declares :token:`qualid` as a canonical structure. + This command declares :token:`qualid` as a canonical instance of a + structure (a record). Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -1946,12 +2035,12 @@ in :ref:`canonicalstructures`; here only a simple example is given. Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - Canonical Structure nat_setoid. + Canonical nat_setoid. Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` and :g:`B` can be synthesized in the next statement. - .. coqtop:: all + .. coqtop:: all abort Lemma is_law_S : is_law S. @@ -1959,11 +2048,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. cmdv:: Canonical Structure @ident {? : @type } := @term + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the - declaration :n:`Canonical Structure @ident`. - + declaration :n:`Canonical @ident`. .. cmd:: Print Canonical Projections @@ -1984,16 +2072,16 @@ Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ It is possible to bind variable names to a given type (e.g. in a -development using arithmetic, it may be convenient to bind the names `n` -or `m` to the type ``nat`` of natural numbers). The command for that is +development using arithmetic, it may be convenient to bind the names :g:`n` +or :g:`m` to the type :g:`nat` of natural numbers). .. cmd:: Implicit Types {+ @ident } : @type -The effect of the command is to automatically set the type of bound -variables starting with `ident` (either `ident` itself or `ident` followed by -one or more single quotes, underscore or digits) to be `type` (unless -the bound variable is already declared with an explicit type in which -case, this latter type is considered). + The effect of the command is to automatically set the type of bound + variables starting with :token:`ident` (either :token:`ident` itself or + :token:`ident` followed by one or more single quotes, underscore or + digits) to be :token:`type` (unless the bound variable is already declared + with an explicit type in which case, this latter type is considered). .. example:: @@ -2004,16 +2092,16 @@ case, this latter type is considered). Implicit Types m n : nat. Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m. - - intros m n. + Proof. intros m n. Abort. Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m. + Abort. .. cmdv:: Implicit Type @ident : @type This is useful for declaring the implicit type of a single variable. -.. cmdv:: Implicit Types {+ ( {+ @ident } : @term ) } +.. cmdv:: Implicit Types {+ ( {+ @ident } : @type ) } Adds blocks of implicit types with different specifications. @@ -2137,23 +2225,29 @@ Printing universes terms apparently identical but internally different in the Calculus of Inductive Constructions. -The constraints on the internal level of the occurrences of Type -(see :ref:`Sorts`) can be printed using the command - .. cmd:: Print {? Sorted} Universes :name: Print Universes -If the optional ``Sorted`` option is given, each universe will be made -equivalent to a numbered label reflecting its level (with a linear -ordering) in the universe hierarchy. + This command can be used to print the constraints on the internal level + of the occurrences of :math:`\Type` (see :ref:`Sorts`). + + If the optional ``Sorted`` option is given, each universe will be made + equivalent to a numbered label reflecting its level (with a linear + ordering) in the universe hierarchy. -This command also accepts an optional output filename: + .. cmdv:: Print {? Sorted} Universes @string -.. cmdv:: Print {? Sorted} Universes @string + This variant accepts an optional output filename. -If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT -language, and can be processed by Graphviz tools. The format is -unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. + If :token:`string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT + language, and can be processed by Graphviz tools. The format is + unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. + +.. cmdv:: Print Universes Subgraph(@names) + + Prints the graph restricted to the requested names (adjusting + constraints to preserve the implied transitive constraints between + kept universes). .. _existential-variables: @@ -2189,13 +2283,10 @@ existential variable is represented by “?” followed by an identifier. Check identity _ (fun x => _). -In the general case, when an existential variable ``?``\ `ident` appears +In the general case, when an existential variable :n:`?@ident` appears outside of its context of definition, its instance, written under the -form - -| ``{`` :n:`{*; @ident:=@term}` ``}`` - -is appending to its name, indicating how the variables of its defining context are instantiated. +form :n:`{ {*; @ident := @term} }` is appending to its name, indicating +how the variables of its defining context are instantiated. The variables of the context of the existential variables which are instantiated by themselves are not written, unless the flag :flag:`Printing Existential Instances` is on (see Section :ref:`explicit-display-existentials`), and this is why an @@ -2248,6 +2339,51 @@ This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. -This mechanism is comparable to the ``Declare Implicit Tactic`` command -defined at :ref:`tactics-implicit-automation`, except that the used -tactic is local to each hole instead of being declared globally. +.. _primitive-integers: + +Primitive Integers +-------------------------------- + +The language of terms features 63-bit machine integers as values. The type of +such a value is *axiomatized*; it is declared through the following sentence +(excerpt from the :g:`Int63` module): + +.. coqdoc:: + + Primitive int := #int63_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, +declared and specified as follows: + +.. coqdoc:: + + Primitive eqb := #int63_eq. + Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + + Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. + +The complete set of such operators can be obtained looking at the :g:`Int63` module. + +These primitive declarations are regular axioms. As such, they must be trusted and are listed by the +:g:`Print Assumptions` command, as in the following example. + +.. coqtop:: in reset + + From Coq Require Import Int63. + Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63. + Proof. apply eqb_correct; vm_compute; reflexivity. Qed. + +.. coqtop:: all + + Print Assumptions one_minus_one_is_zero. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient, rules to reduce the applications of these primitive +operations. + +These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to +types and functions of a :g:`Uint63` module. Said module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 8c82526f0c..8a5e9d87f8 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -94,8 +94,8 @@ Keywords employed otherwise:: _ as at cofix else end exists exists2 fix for - forall fun if IF in let match mod Prop return - Set then Type using where with + forall fun if IF in let match mod return + SProp Prop Set Type then using where with Special tokens The following sequences of characters are special tokens:: @@ -127,43 +127,43 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. .. productionlist:: coq term : forall `binders` , `term` - : | fun `binders` => `term` - : | fix `fix_bodies` - : | cofix `cofix_bodies` - : | let `ident` [`binders`] [: `term`] := `term` in `term` - : | let fix `fix_body` in `term` - : | let cofix `cofix_body` in `term` - : | let ( [`name` , … , `name`] ) [`dep_ret_type`] := `term` in `term` - : | let ' `pattern` [in `term`] := `term` [`return_type`] in `term` - : | if `term` [`dep_ret_type`] then `term` else `term` - : | `term` : `term` - : | `term` <: `term` - : | `term` :> - : | `term` -> `term` - : | `term` `arg` … `arg` - : | @ `qualid` [`term` … `term`] - : | `term` % `ident` - : | match `match_item` , … , `match_item` [`return_type`] with + : fun `binders` => `term` + : fix `fix_bodies` + : cofix `cofix_bodies` + : let `ident` [`binders`] [: `term`] := `term` in `term` + : let fix `fix_body` in `term` + : let cofix `cofix_body` in `term` + : let ( [`name` , … , `name`] ) [`dep_ret_type`] := `term` in `term` + : let ' `pattern` [in `term`] := `term` [`return_type`] in `term` + : if `term` [`dep_ret_type`] then `term` else `term` + : `term` : `term` + : `term` <: `term` + : `term` :> + : `term` -> `term` + : `term` `arg` … `arg` + : @ `qualid` [`term` … `term`] + : `term` % `ident` + : match `match_item` , … , `match_item` [`return_type`] with : [[|] `equation` | … | `equation`] end - : | `qualid` - : | `sort` - : | `num` - : | _ - : | ( `term` ) + : `qualid` + : `sort` + : `num` + : _ + : ( `term` ) arg : `term` - : | ( `ident` := `term` ) + : ( `ident` := `term` ) binders : `binder` … `binder` binder : `name` - : | ( `name` … `name` : `term` ) - : | ( `name` [: `term`] := `term` ) - : | ' `pattern` + : ( `name` … `name` : `term` ) + : ( `name` [: `term`] := `term` ) + : ' `pattern` name : `ident` | _ qualid : `ident` | `qualid` `access_ident` - sort : Prop | Set | Type + sort : SProp | Prop | Set | Type fix_bodies : `fix_body` - : | `fix_body` with `fix_body` with … with `fix_body` for `ident` + : `fix_body` with `fix_body` with … with `fix_body` for `ident` cofix_bodies : `cofix_body` - : | `cofix_body` with `cofix_body` with … with `cofix_body` for `ident` + : `cofix_body` with `cofix_body` with … with `cofix_body` for `ident` fix_body : `ident` `binders` [`annotation`] [: `term`] := `term` cofix_body : `ident` [`binders`] [: `term`] := `term` annotation : { struct `ident` } @@ -173,13 +173,13 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. equation : `mult_pattern` | … | `mult_pattern` => `term` mult_pattern : `pattern` , … , `pattern` pattern : `qualid` `pattern` … `pattern` - : | @ `qualid` `pattern` … `pattern` - : | `pattern` as `ident` - : | `pattern` % `ident` - : | `qualid` - : | _ - : | `num` - : | ( `or_pattern` , … , `or_pattern` ) + : @ `qualid` `pattern` … `pattern` + : `pattern` as `ident` + : `pattern` % `ident` + : `qualid` + : _ + : `num` + : ( `or_pattern` , … , `or_pattern` ) or_pattern : `pattern` | … | `pattern` @@ -218,24 +218,28 @@ numbers (see :ref:`datatypes`). .. index:: single: Set (sort) + single: SProp single: Prop single: Type Sorts ----- -There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. +There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. + +- :g:`SProp` is the universe of *definitionally irrelevant + propositions* (also called *strict propositions*). - :g:`Prop` is the universe of *logical propositions*. The logical propositions themselves are typing the proofs. We denote propositions by :production:`form`. This constitutes a semantic subclass of the syntactic class :token:`term`. -- :g:`Set` is is the universe of *program types* or *specifications*. The +- :g:`Set` is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote specifications by :production:`specif`. This constitutes a semantic subclass of the syntactic class :token:`term`. -- :g:`Type` is the type of :g:`Prop` and :g:`Set` +- :g:`Type` is the type of sorts. More on sorts can be found in Section :ref:`sorts`. @@ -434,6 +438,10 @@ the identifier :g:`b` being used to represent the dependency. the return type. For instance, the following alternative definition is accepted and has the same meaning as the previous one. + .. coqtop:: none + + Reset bool_case. + .. coqtop:: in Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) := @@ -471,7 +479,7 @@ For instance, in the following example: Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x := match H in eq _ _ z return eq A z x with - | eq_refl _ => eq_refl A x + | eq_refl _ _ => eq_refl A x end. the type of the branch is :g:`eq A x x` because the third argument of @@ -524,38 +532,38 @@ The Vernacular .. productionlist:: coq decorated-sentence : [ `decoration` … `decoration` ] `sentence` sentence : `assumption` - : | `definition` - : | `inductive` - : | `fixpoint` - : | `assertion` `proof` + : `definition` + : `inductive` + : `fixpoint` + : `assertion` `proof` assumption : `assumption_keyword` `assums`. assumption_keyword : Axiom | Conjecture - : | Parameter | Parameters - : | Variable | Variables - : | Hypothesis | Hypotheses + : Parameter | Parameters + : Variable | Variables + : Hypothesis | Hypotheses assums : `ident` … `ident` : `term` - : | ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` ) + : ( `ident` … `ident` : `term` ) … ( `ident` … `ident` : `term` ) definition : [Local] Definition `ident` [`binders`] [: `term`] := `term` . - : | Let `ident` [`binders`] [: `term`] := `term` . + : Let `ident` [`binders`] [: `term`] := `term` . inductive : Inductive `ind_body` with … with `ind_body` . - : | CoInductive `ind_body` with … with `ind_body` . + : CoInductive `ind_body` with … with `ind_body` . ind_body : `ident` [`binders`] : `term` := : [[|] `ident` [`binders`] [:`term`] | … | `ident` [`binders`] [:`term`]] fixpoint : Fixpoint `fix_body` with … with `fix_body` . - : | CoFixpoint `cofix_body` with … with `cofix_body` . + : CoFixpoint `cofix_body` with … with `cofix_body` . assertion : `assertion_keyword` `ident` [`binders`] : `term` . assertion_keyword : Theorem | Lemma - : | Remark | Fact - : | Corollary | Proposition - : | Definition | Example + : Remark | Fact + : Corollary | Proposition + : Definition | Example proof : Proof . … Qed . - : | Proof . … Defined . - : | Proof . … Admitted . + : Proof . … Defined . + : Proof . … Admitted . decoration : #[ `attributes` ] attributes : [`attribute`, … , `attribute`] attribute : `ident` - :| `ident` = `string` - :| `ident` ( `attributes` ) + : `ident` = `string` + : `ident` ( `attributes` ) .. todo:: This use of … in this grammar is inconsistent What about removing the proof part of this grammar from this chapter @@ -622,33 +630,21 @@ has type :token:`type`. These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. -.. cmd:: Variable @ident : @type + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + Variables {+ ( {+ @ident } : @type ) } + Hypothesis {+ ( {+ @ident } : @type ) } + Hypotheses {+ ( {+ @ident } : @type ) } + :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) - This command links :token:`type` to the name :token:`ident` in the context of - the current section (see Section :ref:`section-mechanism` for a description of - the section mechanism). When the current section is closed, name :token:`ident` - will be unknown and every object using this variable will be explicitly - parametrized (the variable is *discharged*). Using the :cmd:`Variable` command out - of any section is equivalent to using :cmd:`Local Parameter`. - - .. exn:: @ident already exists. - :name: @ident already exists. (Variable) - :undocumented: + Outside of any section, these variants are synonyms of + :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. + For their meaning inside a section, see :cmd:`Variable` in + :ref:`section-mechanism`. - .. cmdv:: Variable {+ @ident } : @term + .. warn:: @ident is declared as a local axiom [local-declaration,scope] - Links :token:`type` to each :token:`ident`. - - .. cmdv:: Variable {+ ( {+ @ident } : @term ) } - - Adds blocks of variables with different specifications. - - .. cmdv:: Variables {+ ( {+ @ident } : @term) } - Hypothesis {+ ( {+ @ident } : @term) } - Hypotheses {+ ( {+ @ident } : @term) } - :name: Variables; Hypothesis; Hypotheses - - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @term) }`. + Warning generated when using :cmd:`Variable` instead of + :cmd:`Local Parameter`. .. note:: It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and @@ -657,6 +653,8 @@ has type :token:`type`. :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases (corresponding to the declaration of an abstract mathematical entity). +.. seealso:: Section :ref:`section-mechanism`. + .. _gallina-definitions: Definitions @@ -696,10 +694,10 @@ Section :ref:`typing-rules`. .. exn:: The term @term has type @type while it is expected to have type @type'. :undocumented: - .. cmdv:: Definition @ident @binders {? : @term } := @term + .. cmdv:: Definition @ident @binders {? : @type } := @term This is equivalent to - :n:`Definition @ident : forall @binders, @term := fun @binders => @term`. + :n:`Definition @ident : forall @binders, @type := fun @binders => @term`. .. cmdv:: Local Definition @ident {? @binders } {? : @type } := @term :name: Local Definition @@ -713,32 +711,18 @@ Section :ref:`typing-rules`. This is equivalent to :cmd:`Definition`. -.. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. + .. cmdv:: Let @ident := @term + :name: Let (outside a section) -.. cmd:: Let @ident := @term + Outside of any section, this variant is a synonym of + :n:`Local Definition @ident := @term`. + For its meaning inside a section, see :cmd:`Let` in + :ref:`section-mechanism`. - This command binds the value :token:`term` to the name :token:`ident` in the - environment of the current section. The name :token:`ident` disappears when the - current section is eventually closed, and all persistent objects (such - as theorems) defined within the section and depending on :token:`ident` are - prefixed by the let-in definition :n:`let @ident := @term in`. - Using the :cmd:`Let` command out of any section is equivalent to using - :cmd:`Local Definition`. + .. warn:: @ident is declared as a local definition [local-declaration,scope] - .. exn:: @ident already exists. - :name: @ident already exists. (Let) - :undocumented: - - .. cmdv:: Let @ident {? @binders } {? : @type } := @term - :undocumented: - - .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} - :name: Let Fixpoint - :undocumented: - - .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} - :name: Let CoFixpoint - :undocumented: + Warning generated when using :cmd:`Let` instead of + :cmd:`Local Definition`. .. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`, :cmd:`Transparent`, and tactic :tacn:`unfold`. @@ -763,9 +747,9 @@ Simple inductive types are the names of its constructors and :token:`type` their respective types. Depending on the universe where the inductive type :token:`ident` lives (e.g. its type :token:`sort`), Coq provides a number of destructors. - Destructors are named :token:`ident`\ ``_ind``, :token:`ident`\ ``_rec`` - or :token:`ident`\ ``_rect`` which respectively correspond to elimination - principles on :g:`Prop`, :g:`Set` and :g:`Type`. + Destructors are named :token:`ident`\ ``_sind``,:token:`ident`\ ``_ind``, + :token:`ident`\ ``_rec`` or :token:`ident`\ ``_rect`` which respectively + correspond to elimination principles on :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. The type of the destructors expresses structural induction/recursion principles over objects of type :token:`ident`. The constant :token:`ident`\ ``_ind`` is always provided, @@ -826,6 +810,10 @@ Simple inductive types .. example:: + .. coqtop:: none + + Reset nat. + .. coqtop:: in Inductive nat : Set := O | S (_:nat). @@ -865,8 +853,8 @@ which is a type whose conclusion is a sort. successor :g:`(S (S n))` satisfies also :g:`P`. This is indeed analogous to the structural induction principle we got for :g:`nat`. -Parametrized inductive types -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Parameterized inductive types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmdv:: Inductive @ident @binders {? : @type } := {? | } @ident : @type {* | @ident : @type} @@ -904,6 +892,10 @@ Parametrized inductive types Once again, it is possible to specify only the type of the arguments of the constructors, and to omit the type of the conclusion: + .. coqtop:: none + + Reset list. + .. coqtop:: in Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). @@ -938,7 +930,7 @@ Parametrized inductive types because the conclusion of the type of constructors should be :g:`listw A` in both cases. - + A parametrized inductive definition can be defined using annotations + + A parameterized inductive definition can be defined using annotations instead of parameters but it will sometimes give a different (bigger) sort for the inductive definition and will produce a less convenient rule for case elimination. @@ -949,7 +941,7 @@ Parametrized inductive types inductive definitions are abstracted over their parameters before type checking constructors, allowing to write: - .. coqtop:: all undo + .. coqtop:: all Set Uniform Inductive Parameters. Inductive list3 (A:Set) : Set := @@ -960,7 +952,7 @@ Parametrized inductive types and using :cmd:`Context` to give the uniform parameters, like so (cf. :ref:`section-mechanism`): - .. coqtop:: all undo + .. coqtop:: all reset Section list3. Context (A:Set). @@ -998,7 +990,7 @@ Mutually defined inductive types .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } } - In this variant, the inductive definitions are parametrized + In this variant, the inductive definitions are parameterized with :token:`binders`. However, parameters correspond to a local context in which the whole set of inductive declarations is done. For this reason, the parameters must be strictly the same for each inductive types. @@ -1011,7 +1003,7 @@ Mutually defined inductive types .. coqtop:: in - Variables A B : Set. + Parameters A B : Set. Inductive tree : Set := node : A -> forest -> tree @@ -1034,11 +1026,11 @@ Mutually defined inductive types Check forest_rec. - Assume we want to parametrize our mutual inductive definitions with the + Assume we want to parameterize our mutual inductive definitions with the two type variables :g:`A` and :g:`B`, the declaration should be done the following way: - .. coqtop:: in + .. coqdoc:: Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B @@ -1112,6 +1104,63 @@ co-inductive definitions are also allowed. object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite objects in Section :ref:`cofixpoint`. +Caveat +++++++ + +The ability to define co-inductive types by constructors, hereafter called +*positive co-inductive types*, is known to break subject reduction. The story is +a bit long: this is due to dependent pattern-matching which implies +propositional η-equality, which itself would require full η-conversion for +subject reduction to hold, but full η-conversion is not acceptable as it would +make type-checking undecidable. + +Since the introduction of primitive records in Coq 8.5, an alternative +presentation is available, called *negative co-inductive types*. This consists +in defining a co-inductive type as a primitive record type through its +projections. Such a technique is akin to the *co-pattern* style that can be +found in e.g. Agda, and preserves subject reduction. + +The above example can be rewritten in the following way. + +.. coqtop:: none + + Reset Stream. + +.. coqtop:: all + + Set Primitive Projections. + CoInductive Stream : Set := Seq { hd : nat; tl : Stream }. + CoInductive EqSt (s1 s2: Stream) : Prop := eqst { + eqst_hd : hd s1 = hd s2; + eqst_tl : EqSt (tl s1) (tl s2); + }. + +Some properties that hold over positive streams are lost when going to the +negative presentation, typically when they imply equality over streams. +For instance, propositional η-equality is lost when going to the negative +presentation. It is nonetheless logically consistent to recover it through an +axiom. + +.. coqtop:: all + + Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s). + +More generally, as in the case of positive coinductive types, it is consistent +to further identify extensional equality of coinductive types with propositional +equality: + +.. coqtop:: all + + Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. + +As of Coq 8.9, it is now advised to use negative co-inductive types rather than +their positive counterparts. + +.. seealso:: + :ref:`primitive_projections` for more information about negative + records and primitive projections. + + Definition of recursive functions --------------------------------- @@ -1464,7 +1513,7 @@ the following attributes names are recognized: .. example:: - .. coqtop:: all reset + .. coqtop:: all reset warn From Coq Require Program. #[program] Definition one : nat := S _. |