diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 1845 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 988 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 2358 | ||||
| -rw-r--r-- | doc/sphinx/language/module-system.rst | 459 |
4 files changed, 5650 insertions, 0 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst new file mode 100644 index 0000000000..7ed6524095 --- /dev/null +++ b/doc/sphinx/language/cic.rst @@ -0,0 +1,1845 @@ +.. include:: ../preamble.rst +.. include:: ../replaces.rst + +.. _calculusofinductiveconstructions: + + +Calculus of Inductive Constructions +==================================== + +The underlying formal language of |Coq| is a *Calculus of Inductive +Constructions* (|Cic|) whose inference rules are presented in this +chapter. The history of this formalism as well as pointers to related +work are provided in a separate chapter; see *Credits*. + + +.. _The-terms: + +The terms +------------- + +The expressions of the |Cic| are *terms* and all terms have a *type*. +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”. + +The types of types are *sorts*. Types and sorts are themselves terms +so that terms, types and sorts are all components of a common +syntactic language of terms which is described in Section :ref:`terms` but, +first, we describe sorts. + + +.. _Sorts: + +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`. + +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:`\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. +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`. + +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 +types over small sets. But, unlike :math:`\Set`, they also contain large sets, +namely the sorts :math:`\Set` and :math:`\Type(j)` for :math:`j<i`, and all products, subsets +and function types over these sorts. + +Formally, we call :math:`\Sort` the set of sorts which is defined by: + +.. math:: + + \Sort \equiv \{\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`. + +The user does not have to mention explicitly the index :math:`i` when +referring to the universe :math:`\Type(i)`. One only writes :math:`\Type`. The system +itself generates for each instance of :math:`\Type` a new index for the +universe and checks that the constraints between these indexes can be +solved. From the user point of view we consequently have :math:`\Type:\Type`. We +shall make precise in the typing rules the constraints between the +indices. + + +.. _Implementation-issues: + +**Implementation issues** In practice, the Type hierarchy is +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 +:math:`0`) which corresponds, in the arity of template polymorphic inductive +types (see Section +:ref:`well-formed-inductive-definitions`), +to the predicative sort :math:`\Set`. A graph of +constraints between the universe variables is maintained globally. To +ensure the existence of a mapping of the universes to the positive +integers, the graph of constraints must remain acyclic. Typing +expressions that violate the acyclicity of the graph of constraints +results in a Universe inconsistency error (see also Section +:ref:`TODO-2.10`). + + +.. _Terms: + +Terms +~~~~~ + + + +Terms are built from sorts, variables, constants, abstractions, +applications, local definitions, and products. From a syntactic point +of view, types cannot be distinguished from terms, except that they +cannot start by an abstraction or a constructor. More precisely the +language of the *Calculus of Inductive Constructions* is built from +the following rules. + + +#. the sorts :math:`\Set`, :math:`\Prop`, :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 + “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 + a *dependent product*. If :math:`x` does not occur in :math:`U` then + :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` + 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 + 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 + 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. + + + +.. _Free-variables: + +**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. + + +.. _Substitution: + +**Substitution.** +The notion of substituting a term :math:`t` to free occurrences of a variable +:math:`x` in a term :math:`u` is defined as usual. The resulting term is written +:math:`\subst{u}{x}{t}`. + + +.. _The-logical-vs-programming-readings: + +**The logical vs programming readings.** +The constructions of the |Cic| can be used to express both logical and +programming notions, accordingly to the Curry-Howard correspondence +between proofs and programs, and between propositions and types +:cite:`Cur58,How80,Bru72`. + +For instance, let us assume that :math:`\nat` is the type of natural numbers +with zero element written :math:`0` and that :g:`True` is the always true +proposition. Then :math:`→` is used both to denote :math:`\nat→\nat` which is the type +of functions from :math:`\nat` to :math:`\nat`, to denote True→True which is an +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. +: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)` +(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 +:math:`\nat → \Prop` +and it can be applied to any expression of type :math:`\nat`, say :math:`t`, to give an +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`)”. + + +.. _Typing-rules: + +Typing rules +---------------- + +As objects of type theory, terms are subjected to *type discipline*. +The well typing of a term depends on a global environment and a local +context. + + +.. _Local-context: + +**Local context.** +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 +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 +assumption in :math:`Γ` or that there exists some :math:`t` such that :math:`x:=t:T` is a +definition in :math:`Γ`. If :math:`Γ` defines some :math:`x:=t:T`, we also write :math:`(x:=t:T) ∈ Γ`. +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` . + + +.. _Global-environment: + +**Global environment.** +A *global environment* is an ordered list of *global declarations*. +Global declarations are either *global assumptions* or *global +definitions*, but also declarations of inductive objects. Inductive +objects themselves declare both inductive or coinductive types and +constructors (see Section :ref:`inductive-definitions`). + +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 +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 +global definition :math:`(c:=t:T)`. + +The rules for inductive definitions (see Section +:ref:`inductive-definitions`) have to be considered as assumption +rules to which the following definitions apply: if the name :math:`c` +is declared in :math:`E`, we write :math:`c ∈ E` and if :math:`c:T` or +:math:`c:=t:T` is declared in :math:`E`, we write :math:`(c : T) ∈ E`. + + +.. _Typing-rules2: + +**Typing rules.** +In the following, we define simultaneously two judgments. The first +one :math:`\WTEG{t}{T}` means the term :math:`t` is well-typed and has type :math:`T` in the +global environment :math:`E` and local context :math:`Γ`. The second judgment :math:`\WFE{Γ}` +means that the global environment :math:`E` is well-formed and the local +context :math:`Γ` is a valid local context in this global environment. + +A term :math:`t` is well typed in a global environment :math:`E` iff +there exists a local context :math:`\Gamma` and a term :math:`T` such +that the judgment :math:`\WTEG{t}{T}` can be derived from the +following rules. + +.. inference:: W-Empty + + --------- + \WF{[]}{} + +.. inference:: W-Local-Assum + + \WTEG{T}{s} + s \in \Sort + x \not\in \Gamma % \cup E + ------------------------- + \WFE{\Gamma::(x:T)} + +.. inference:: W-Local-Def + + \WTEG{t}{T} + x \not\in \Gamma % \cup E + ------------------------- + \WFE{\Gamma::(x:=t:T)} + +.. inference:: W-Global-Assum + + \WTE{}{T}{s} + s \in \Sort + c \notin E + ------------ + \WF{E;c:T}{} + +.. inference:: W-Global-Def + + \WTE{}{t}{T} + c \notin E + --------------- + \WF{E;c:=t:T}{} + +.. inference:: Ax-Prop + + \WFE{\Gamma} + ---------------------- + \WTEG{\Prop}{\Type(1)} + +.. inference:: Ax-Set + + \WFE{\Gamma} + --------------------- + \WTEG{\Set}{\Type(1)} + +.. inference:: Ax-Type + + \WFE{\Gamma} + --------------------------- + \WTEG{\Type(i)}{\Type(i+1)} + +.. inference:: Var + + \WFE{\Gamma} + (x:T) \in \Gamma~~\mbox{or}~~(x:=t:T) \in \Gamma~\mbox{for some $t$} + -------------------------------------------------------------------- + \WTEG{x}{T} + +.. inference:: Const + + \WFE{\Gamma} + (c:T) \in E~~\mbox{or}~~(c:=t:T) \in E~\mbox{for some $t$} + ---------------------------------------------------------- + \WTEG{c}{T} + +.. inference:: Prod-Prop + + \WTEG{T}{s} + s \in {\Sort} + \WTE{\Gamma::(x:T)}{U}{\Prop} + ----------------------------- + \WTEG{\forall~x:T,U}{\Prop} + +.. inference:: Prod-Set + + \WTEG{T}{s} + s \in \{\Prop, \Set\} + \WTE{\Gamma::(x:T)}{U}{\Set} + ---------------------------- + \WTEG{\forall~x:T,U}{\Set} + +.. inference:: Prod-Type + + \WTEG{T}{\Type(i)} + \WTE{\Gamma::(x:T)}{U}{\Type(i)} + -------------------------------- + \WTEG{\forall~x:T,U}{\Type(i)} + +.. inference:: Lam + + \WTEG{\forall~x:T,U}{s} + \WTE{\Gamma::(x:T)}{t}{U} + ------------------------------------ + \WTEG{\lb x:T\mto t}{\forall x:T, U} + +.. inference:: App + + \WTEG{t}{\forall~x:U,T} + \WTEG{u}{U} + ------------------------------ + \WTEG{(t\ u)}{\subst{T}{x}{u}} + +.. inference:: Let + + \WTEG{t}{T} + \WTE{\Gamma::(x:=t:T)}{u}{U} + ----------------------------------------- + \WTEG{\letin{x}{t:T}{u}}{\subst{U}{x}{t}} + + + +**Remark**: **Prod-Prop** and **Prod-Set** typing-rules make sense if we consider the +semantic difference between :math:`\Prop` and :math:`\Set`: + + ++ All values of a type that has a sort :math:`\Set` are extractable. ++ No values of a type that has a sort :math:`\Prop` are extractable. + + + +**Remark**: 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:`t`). This is because the value :math:`t` associated to +:math:`x` may be used in a conversion rule (see Section :ref:`Conversion-rules`). + + +.. _Conversion-rules: + +Conversion rules +-------------------- + +In |Cic|, there is an internal reduction mechanism. In particular, it +can decide if two programs are *intentionally* equal (one says +*convertible*). Convertibility is described in this section. + + +.. _β-reduction: + +**β-reduction.** +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 +:math:`Γ`, we want to identify any object :math:`a` (of type +: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} + +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 +*β-expansion* of :math:`\subst{t}{x}{u}`. + +According to β-reduction, terms of the *Calculus of Inductive +Constructions* enjoy some fundamental properties such as confluence, +strong normalization, subject reduction. These results are +theoretically of great importance but we will not detail them here and +refer the interested reader to :cite:`Coq85`. + + +.. _ι-reduction: + +**ι-reduction.** +A specific conversion rule is associated to the inductive objects in +the global environment. We shall give later on (see Section +:ref:`Well-formed-inductive-definitions`) the precise rules but it +just says that a destructor applied to an object built from a +constructor behaves as expected. This reduction is called ι-reduction +and is more precisely studied in :cite:`Moh93,Wer94`. + + +.. _δ-reduction: + +**δ-reduction.** +We may have variables defined in local contexts or constants defined +in the global environment. It is legal to identify such a reference +with its value, that is to expand (or unfold) it into its value. This +reduction is called δ-reduction and shows as follows. + +.. inference:: Delta-Local + + \WFE{\Gamma} + (x:=t:T) ∈ Γ + -------------- + E[Γ] ⊢ x~\triangleright_Δ~t + +.. inference:: Delta-Global + + \WFE{\Gamma} + (c:=t:T) ∈ E + -------------- + E[Γ] ⊢ c~\triangleright_δ~t + + +.. _ζ-reduction: + +**ζ-reduction.** +|Coq| allows also to remove local definitions occurring in terms by +replacing the defined variable by its value. The declaration being +destroyed, this reduction differs from δ-reduction. It is called +ζ-reduction and shows as follows. + +.. inference:: Zeta + + \WFE{\Gamma} + \WTEG{u}{U} + \WTE{\Gamma::(x:=u:U)}{t}{T} + -------------- + E[Γ] ⊢ \letin{x}{u}{t}~\triangleright_ζ~\subst{t}{x}{u} + + +.. _η-expansion: + +**η-expansion.** +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 + +.. math:: + λx:T. (t~x) + +for :math:`x` an arbitrary variable name fresh in :math:`t`. + + +**Remark**: We deliberately do not define η-reduction: + +.. math:: + λ 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: + +.. math:: + f : ∀ x:\Type(2),\Type(1) + +then + +.. math:: + λ x:\Type(1),(f~x) : ∀ x:\Type(1),\Type(1) + +We could not allow + +.. math:: + λ 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).` + + +.. _Convertibility: + +**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 ζ. + +We say that two terms :math:`t_1` and :math:`t_2` are +*βιδζη-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` . + +Apart from this we consider two instances of polymorphic and +cumulative (see Chapter :ref:`polymorphicuniverses`) inductive types +(see below) convertible + +.. math:: + E[Γ] ⊢ t~w_1 … w_m =_{βδιζη} t~w_1' … w_m' + +if we have subtypings (see below) in both directions, i.e., + +.. math:: + E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m' + +and + +.. math:: + E[Γ] ⊢ t~w_1' … w_m' ≤_{βδιζη} t~w_1 … w_m. + +Furthermore, we consider + +.. math:: + E[Γ] ⊢ c~v_1 … v_m =_{βδιζη} c'~v_1' … v_m' + +convertible if + +.. math:: + E[Γ] ⊢ v_i =_{βδιζη} v_i' + +and we have that :math:`c` and :math:`c'` +are the same constructors of different instances of the same inductive +types (differing only in universe levels) such that + +.. math:: + E[Γ] ⊢ c~v_1 … v_m : t~w_1 … w_m + +and + +.. math:: + E[Γ] ⊢ c'~v_1' … v_m' : t'~ w_1' … w_m ' + +and we have + +.. math:: + E[Γ] ⊢ t~w_1 … w_m =_{βδιζη} t~w_1' … w_m'. + +The convertibility relation allows introducing a new typing rule which +says that two convertible well-formed types have the same inhabitants. + + +.. _subtyping-rules: + +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|). +This property extends the equivalence relation of convertibility into +a *subtyping* relation inductively defined by: + + +#. if :math:`E[Γ] ⊢ t =_{βδιζη} u` then :math:`E[Γ] ⊢ t ≤_{βδιζη} u`, +#. if :math:`i ≤ j` then :math:`E[Γ] ⊢ \Type(i) ≤_{βδιζη} \Type(j)`, +#. 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` +#. if :math:`E[Γ] ⊢ T =_{βδιζη} U` and + :math:`E[Γ::(x:T)] ⊢ T' ≤_{βδιζη} U'` then + :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` + and + :math:`(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', \Sort')∈Γ_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} ] + + 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}' ] + + respectively then + + .. math:: + E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m' + + (notice that :math:`t` and :math:`t'` are both + fully applied, i.e., they have a sort as a type) if + + .. math:: + E[Γ] ⊢ w_i =_{βδιζη} w_i' + + for :math:`1 ≤ i ≤ m` and we have + + + .. math:: + E[Γ] ⊢ T_{i,j} ≤_{βδιζη} T_{i,j}' + + and + + .. 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']`. + + +The conversion rule up to subtyping is now exactly: + +.. inference:: Conv + + E[Γ] ⊢ U : s + E[Γ] ⊢ t : T + E[Γ] ⊢ T ≤_{βδιζη} U + -------------- + E[Γ] ⊢ t : U + + +.. _Normal-form: + +**Normal form**. A term which cannot be any more reduced is said to be in *normal +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 . (λ 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 ) + +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` +can be reducible. Similar notions of head-normal forms involving δ, ι +and ζ reductions or any combination of those can also be defined. + + +.. _inductive-definitions: + +Inductive Definitions +------------------------- + +Formally, we can represent any *inductive definition* as +:math:`\ind{p}{Γ_I}{Γ_C}` where: + ++ :math:`Γ_I` determines the names and types of inductive types; ++ :math:`Γ_C` determines the names and types of constructors of these + inductive types; ++ :math:`p` determines the number of parameters of these inductive types. + + +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 +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). + + +** Examples** The declaration for parameterized lists 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 + \end{array} + \right]} + +which corresponds to the result of the |Coq| declaration: + +.. example:: + .. coqtop:: in + + Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. + +The declaration for a mutual inductive definition of tree and forest +is: + +.. math:: + \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} + {\left[\begin{array}{rcl} + \node &:& \forest → \tree\\ + \emptyf &:& \forest\\ + \consf &:& \tree → \forest → \forest\\ + \end{array}\right]} + +which corresponds to the result of the |Coq| declaration: + +.. example:: + .. coqtop:: in + + Inductive tree : Set := + | node : forest -> tree + with forest : Set := + | emptyf : forest + | consf : tree -> forest -> forest. + +The declaration for a mutual inductive definition of even and odd is: + +.. math:: + \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ + \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) + \end{array}\right]} + +which corresponds to the result of the |Coq| declaration: + +.. example:: + .. coqtop:: in + + Inductive even : nat -> prop := + | even_O : even 0 + | even_S : forall n, odd n -> even (S n) + with odd : nat -> prop := + | odd_S : forall n, even n -> odd (S n). + + + +.. _Types-of-inductive-objects: + +Types of inductive objects +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We have to give the type of constants in a global environment E which +contains an inductive declaration. + +.. inference:: Ind + + \WFE{Γ} + \ind{p}{Γ_I}{Γ_C} ∈ E + (a:A)∈Γ_I + --------------------- + E[Γ] ⊢ a : A + +.. inference:: Constr + + \WFE{Γ} + \ind{p}{Γ_I}{Γ_C} ∈ E + (c:C)∈Γ_C + --------------------- + E[Γ] ⊢ c : C + +**Example.** +Provided that our environment :math:`E` contains inductive definitions we showed before, +these two inference rules above enable us to conclude that: + +.. math:: + \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) + \end{array} + + + + +.. _Well-formed-inductive-definitions: + +Well-formed inductive definitions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We cannot accept any inductive declaration 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: + + +**Type is an Arity of Sort S.** +A type :math:`T` is an *arity of sort s* if it converts to the sort s or to a +product :math:`∀ x:T,U` with :math:`U` an arity of sort s. + +.. example:: + + :math:`A→\Set` is an arity of sort :math:`\Set`. :math:`∀ A:\Prop,A→ \Prop` is an arity of sort + :math:`\Prop`. + + +**Type is an Arity.** +A type :math:`T` is an *arity* if there is a :math:`s∈ \Sort` such that :math:`T` is an arity of +sort s. + + +.. example:: + + :math:`A→ Set` and :math:`∀ A:\Prop,A→ \Prop` are arities. + + +**Type of Constructor of I.** +We say that T is a *type of constructor of 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` + + + +.. 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`. + +**Positivity Condition.** +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` + satisfies the positivity condition for :math:`X`. + + +**Occurs Strictly Positively.** +The constant :math:`X` *occurs strictly positively* in :math:`T` in the following +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 + 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 + + .. 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} + + (in particular, it is + not mutually defined and it has :math:`m` parameters) and :math:`X` does not occur in + any of the :math:`t_i`, and the (instantiated) types of constructor + :math:`\subst{C_i}{p_j}{a_j}_{j=1… m}` of :math:`I` satisfy the nested positivity condition for :math:`X` + +**Nested Positivity Condition.** +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` + 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` + satisfies the nested positivity condition for :math:`X` + + +For instance, if one considers the type + +.. example:: + .. coqtop:: all + + Module TreeExample. + Inductive tree (A:Type) : Type := + | leaf : tree A + | node : A -> (nat -> tree A) -> tree A. + End TreeExample. + +:: + + [TODO Note: This commentary does not seem to correspond to the + preceding example. Instead it is referring to the first example + in Inductive Definitions section. It seems we should either + delete the preceding example and refer the the example above of + type `list A`, or else we should rewrite the commentary below.] + + Then every instantiated constructor of list A satisfies the nested positivity + condition for list + │ + ├─ concerning type list A of constructor nil: + │ Type list A of constructor nil satisfies the positivity condition for list + │ because list does not appear in any (real) arguments of the type of that + | constructor (primarily because list does not have any (real) + | arguments) ... (bullet 1) + │ + ╰─ concerning type ∀ A → list A → list A of constructor cons: + Type ∀ A : Type, A → list A → list A of constructor cons + satisfies the positivity condition for list because: + │ + ├─ list occurs only strictly positively in Type ... (bullet 3) + │ + ├─ list occurs only strictly positively in A ... (bullet 3) + │ + ├─ list occurs only strictly positively in list A ... (bullet 4) + │ + ╰─ list satisfies the positivity condition for list A ... (bullet 1) + + + + +.. _Correctness-rules: + +**Correctness rules.** +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 + +.. 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}}{Γ} + + +provided that the following side conditions hold: + + + :math:`k>0` and all of :math:`I_j` and :math:`c_i` are distinct names for :math:`j=1… k` and :math:`i=1… n`, + + :math:`p` is the number of parameters of :math:`\ind{p}{Γ_I}{Γ_C}` and :math:`Γ_P` is the + 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`. + +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 +sortProp but may fail to define inductive definition on sort Set and +generate constraints between universes for inductive definitions in +the Type hierarchy. + + +**Examples**. 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)`. + +.. example:: + .. coqtop:: in + + Inductive exProp (P:Prop->Prop) : Prop := + | exP_intro : forall X:Prop, P X -> exProp P. + +The same definition on Set is not allowed and fails: + +.. example:: + .. coqtop:: all + + Fail Inductive exSet (P:Set->Prop) : Set := + exS_intro : forall X:Set, P X -> exSet P. + +It is possible to declare the same inductive definition in the +universe Type. The exType inductive definition has type +:math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` +has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. + +.. example:: + .. coqtop:: all + + Inductive exType (P:Type->Prop) : Type := + exT_intro : forall X:Type, P X -> exType P. + + + +.. _Template-polymorphism: + +**Template polymorphism.** +Inductive types declared in Type are polymorphic over their arguments +in Type. If :math:`A` is an arity of some sort and s is a sort, we write :math:`A_{/s}` +for the arity obtained from :math:`A` by replacing its sort with s. +Especially, if :math:`A` is well-typed in some global environment and local +context, then :math:`A_{/s}` is typable by typability of all products in the +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, +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 +:math:`0≤ r≤ m`, be a (possibly) partial instantiation of the recursively +uniform parameters of :math:`Γ_P` . We have: + +.. inference:: Ind-Family + + \left\{\begin{array}{l} + \ind{p}{Γ_I}{Γ_C} \in E\\ + (E[] ⊢ q_l : P'_l)_{l=1\ldots r}\\ + (E[] ⊢ P'_l ≤_{βδιζη} \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1})_{l=1\ldots r}\\ + 1 \leq j \leq k + \end{array} + \right. + ----------------------------- + 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}]` + 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 + (see Section Destructors_). + + + +Notice that if :math:`I_j~q_1 … q_r` is typable using the rules **Ind-Const** and +**App**, then it is typable using the rule **Ind-Family**. Conversely, the +extended theory is not stronger than the theory without **Ind-Family**. We +get an equiconsistency result by mapping each :math:`\ind{p}{Γ_I}{Γ_C}` +occurring into a given derivation into as many different inductive +types and constructors as the number of different (partial) +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 +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. +Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or +:math:`C_i~q_1 … q_r` is mapped to the names chosen in the specific instance of +:math:`\ind{p}{Γ_I}{Γ_C}`. + +In practice, the rule **Ind-Family** is used by |Coq| only when all the +inductive types of the inductive definition are declared with an arity +whose sort is in the Type hierarchy. Then, the polymorphism is over +the parameters whose type is an arity of sort in the Type hierarchy. +The sorts :math:`s_j` are chosen canonically so that each :math:`s_j` is minimal with +respect to the hierarchy :math:`\Prop ⊂ \Set_p ⊂ \Type` where :math:`\Set_p` is predicative +:math:`\Set`. More precisely, an empty or small singleton inductive definition +(i.e. an inductive definition of which all inductive types are +singleton – see paragraph Destructors_) is set in :math:`\Prop`, a small non-singleton +inductive type is set in :math:`\Set` (even in case :math:`\Set` is impredicative – see +Section The-Calculus-of-Inductive-Construction-with-impredicative-Set_), +and otherwise in the Type hierarchy. + +Note that the side-condition about allowed elimination sorts in the +rule **Ind-Family** is just to avoid to recompute the allowed elimination +sorts at each instance of a pattern-matching (see section Destructors_). As +an example, let us consider the following definition: + +.. example:: + .. coqtop:: in + + Inductive option (A:Type) : Type := + | None : option A + | Some : A -> option A. + +As the definition is set in the Type hierarchy, it is used +polymorphically over its parameters whose types are arities of a sort +in the Type hierarchy. Here, the parameter :math:`A` has this property, hence, +if :g:`option` is applied to a type in :math:`\Set`, the result is in :math:`\Set`. Note that +if :g:`option` is applied to a type in :math:`\Prop`, then, the result is not set in +:math:`\Prop` but in :math:`\Set` still. This is because :g:`option` is not a singleton type +(see section Destructors_) and it would lose the elimination to :math:`\Set` and :math:`\Type` +if set in :math:`\Prop`. + +.. example:: + .. coqtop:: all + + Check (fun A:Set => option A). + Check (fun A:Prop => option A). + +Here is another example. + +.. example:: + .. coqtop:: in + + Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. + +As :g:`prod` is a singleton type, it will be in :math:`\Prop` if applied twice to +propositions, in :math:`\Set` if applied twice to at least one type in :math:`\Set` and +none in :math:`\Type`, and in :math:`\Type` otherwise. In all cases, the three kind of +eliminations schemes are allowed. + +.. example:: + .. coqtop:: all + + Check (fun A:Set => prod A). + Check (fun A:Prop => prod A A). + Check (fun (A:Prop) (B:Set) => prod A B). + Check (fun (A:Type) (B:Prop) => prod A B). + +Remark: Template polymorphism used to be called “sort-polymorphism of +inductive types” before universe polymorphism (see Chapter :ref:`polymorphicuniverses`) was +introduced. + + +.. _Destructors: + +Destructors +~~~~~~~~~~~~~~~~~ + +The specification of inductive definitions with arities and +constructors is quite natural. But we still have to say how to use an +object in an inductive type. + +This problem is rather delicate. There are actually several different +ways to do that. Some of them are logically equivalent but not always +equivalent from the computational point of view or from the user point +of view. + +From the computational point of view, we want to be able to define a +function whose domain is an inductively defined type by using a +combination of case analysis over the possible constructors of the +object and recursion. + +Because we need to keep a consistent theory and also we prefer to keep +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, so such that :g:`(length (nil A)) = O` and :g:`(length +(cons A a l)) = (S (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 +to enumerate all the cases where :math:`m` starts with a different +constructor. + +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: + + ++ :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)))` + + +which given the conversion equalities satisfied by 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)))` + + +One conceptually simple way to do that, following the basic scheme +proposed by Martin-Löf in his Intuitionistic Type Theory, is to +introduce for each inductive definition an elimination operator. At +the logical level it is a proof of the usual induction principle and +at the computational level it implements a generic operator for doing +primitive recursion over the structure. + +But this operator is rather tedious to implement and use. We choose in +this version of |Coq| to factorize the operator for primitive recursion +into two more primitive operations as was first suggested by Th. +Coquand in :cite:`Coq92`. One is the definition by pattern-matching. The +second one is a definition by guarded fixpoints. + + +.. _The-match…with-end-construction: + +**The match…with …end construction** +The basic idea of this operator is that we have an object :math:`m` in an +inductive type :math:`I` and we want to prove a property which possibly +depends on :math:`m`. For this, it is enough to prove the property for +:math:`m = (c_i~u_1 … u_{p_i} )` for each constructor of :math:`I`. +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 \endkw + +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 +and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the +:math:`u_1 … u_{p_i}` according to the ι-reduction. + +Actually, for type-checking a :math:`\Match…\with…\endkw` expression we also need +to know the predicate 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| +can sometimes infer this predicate but sometimes not. The concrete +syntax for describing this predicate uses the :math:`\as…\In…\return` +construction. For instance, let us assume that :math:`I` is an unary predicate +with one parameter and one argument. The predicate is made explicit +using the syntax: + +.. math:: + \Match~m~\as~x~\In~I~\_~a~\return~P~\with~ + (c_1~x_{11} ... x_{1p_1} ) ⇒ f_1 | … + | (c_n~x_{n1} ... x_{np_n} ) ⇒ f_n~\endkw + +The :math:`\as` part can be omitted if either the result type does not depend +on :math:`m` (non-dependent elimination) or :math:`m` is a variable (in this case, :math:`m` +can occur in :math:`P` where it is considered a bound variable). The :math:`\In` part +can be omitted if the result type does not depend on the arguments +of :math:`I`. Note that the arguments of :math:`I` corresponding to parameters *must* +be :math:`\_`, because the result type is not generalized to all possible +values of the parameters. The other arguments of :math:`I` (sometimes called +indices in the literature) have to be variables (:math:`a` above) and these +variables can occur in :math:`P`. The expression after :math:`\In` must be seen as an +*inductive type pattern*. Notice that expansion of implicit arguments +and notations apply to this pattern. For the purpose of presenting the +inference rules, we use a more compact notation: + +.. math:: + \case(m,(λ a x . P), λ x_{11} ... x_{1p_1} . f_1~| … |~λ x_{n1} ...x_{np_n} . f_n ) + + +.. _Allowed-elimination-sorts: + +**Allowed elimination sorts.** An important question for building the typing rule for 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. + + +.. _Notations: + +**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. +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′] + + +.. inference:: Set & Type + + s_1 ∈ \{\Set,\Type(j)\} + s_2 ∈ \Sort + ---------------- + [I:s_1 |I→ s_2 ] + + +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`. + +.. inference:: Prop + + ~ + --------------- + [I:Prop|I→Prop] + + +:math:`\Prop` is the type of logical propositions, the proofs of properties :math:`P` in +:math:`\Prop` could not be used for computation and are consequently ignored by +the extraction mechanism. Assume :math:`A` and :math:`B` are two propositions, and the +logical disjunction :math:`A ∨ B` is defined inductively by: + +.. example:: + .. coqtop:: in + + Inductive or (A B:Prop) : Prop := + or_introl : A -> or A B | or_intror : B -> or A B. + + +The following definition which computes a boolean value by case over +the proof of :g:`or A B` is not accepted: + +.. example:: + .. coqtop:: all + + Fail Definition choice (A B: Prop) (x:or A B) := + match x with or_introl _ _ a => true | or_intror _ _ b => false end. + +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 +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 +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 +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: + +.. example:: + .. coqtop:: all + + 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 +inductive definition like the second-order existential quantifier +:g:`exProp` defined above, because it give access to the two projections on +this type. + + +.. _Empty-and-singleton-elimination: + +**Empty and singleton elimination.** There are special inductive definitions in +:math:`\Prop` for which more eliminations are allowed. + +.. inference:: Prop-extended + + I~\kw{is an empty or singleton definition} + s ∈ \Sort + ------------------------------------- + [I:Prop|I→ s] + +A *singleton definition* has only one constructor and all the +arguments of this constructor have type Prop. In that case, there is a +canonical way to interpret the informative extraction on an object in +that type, such that the elimination on any sort :math:`s` is legal. Typical +examples are the conjunction of non-informative propositions and the +equality. If there is an hypothesis :math:`h:a=b` in the local context, it can +be used for rewriting not only in logical propositions but also in any +type. + +.. example:: + .. coqtop:: all + + Print eq_rec. + Require Extraction. + Extraction eq_rec. + +An empty definition has no constructors, in that case also, +elimination on any sort is allowed. + + +.. _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 +arguments. + +We define a new type :math:`\{c:C\}^P` which represents the type of the branch +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 + \end{array} + +We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:`c`. + + +**Example.** +The following term in concrete syntax:: + + match t as l return P' with + | nil _ => t1 + | cons _ hd tl => t2 + end + + +can be represented in abstract syntax as + +.. math:: + \case(t,P,f 1 | f 2 ) + +where + +.. math:: + \begin{eqnarray*} + P & = & \lambda~l~.~P^\prime\\ + f_1 & = & t_1\\ + f_2 & = & \lambda~(hd:\nat)~.~\lambda~(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)) + +.. 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)). + \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`. + + +.. _Typing-rule: + +**Typing rule.** +Our very general destructor for inductive definition enjoys the +following typing rule + +.. inference:: match + + \begin{array}{l} + E[Γ] ⊢ c : (I~q_1 … q_r~t_1 … t_s ) \\ + E[Γ] ⊢ P : B \\ + [(I~q_1 … q_r)|B] \\ + (E[Γ] ⊢ f_i : \{(c_{p_i}~q_1 … q_r)\}^P)_{i=1… l} + \end{array} + ------------------------------------------------ + 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 +:math:`c_{p_1} … c_{p_l}` are the only constructors of :math:`I`. + + + +**Example.** +Below is a typing rule for the term shown in the previous example: + +.. inference:: list example + + \begin{array}{l} + E[Γ] ⊢ t : (\List ~\nat) \\ + E[Γ] ⊢ P : B \\ + [(\List ~\nat)|B] \\ + E[Γ] ⊢ f_1 : {(\kw{nil} ~\nat)}^P \\ + E[Γ] ⊢ f_2 : {(\kw{cons} ~\nat)}^P + \end{array} + ------------------------------------------------ + E[Γ] ⊢ \case(t,P,f_1 |f_2 ) : (P~t) + + +.. _Definition-of-ι-reduction: + +**Definition of ι-reduction.** +We still have to define the ι-reduction in the general case. + +An ι-redex is a term of the following form: + +.. math:: + \case((c_{p_i}~q_1 … q_r~a_1 … a_m ),P,f_1 |… |f_l ) + +with :math:`c_{p_i}` the :math:`i`-th constructor of the inductive type :math:`I` with :math:`r` +parameters. + +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 ) + + +.. _Fixpoint-definitions: + +Fixpoint definitions +~~~~~~~~~~~~~~~~~~~~ + +The second operator for elimination is fixpoint definition. This +fixpoint may involve several mutually recursive definitions. The basic +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 + + +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 + +In the inference rules, we represent such a term by + +.. math:: + \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 +:math:`t_i'=λ Γ_i . t_i` and :math:`A_i'=∀ Γ_i , A_i`. + + +Typing rule ++++++++++++ + +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[Γ] ⊢ \Fix~f_i\{f_1 :A_1 :=t_1 … f_n :A_n :=t_n \} : A_i + + +Any fixpoint definition cannot be accepted because non-normalizing +terms allow proofs of absurdity. The basic scheme of recursion that +should be allowed is the one needed for defining primitive recursive +functionals. In that case the fixpoint enjoys a special syntactic +restriction, namely one of the arguments belongs to an inductive type, +the function starts with a case analysis and recursive calls are done +on variables coming from patterns and representing subterms. For +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) + +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)))\} + \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 +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'\} + + +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 +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. + +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 +syntactically recognized as structurally smaller than :math:`y_{k_i}`. + +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 )`, +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 type an inductive definition 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:`(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`. + 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 + obtained from :math:`B_i` by substituting parameters 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. + + +The following definitions are correct, we enter them using the ``Fixpoint`` +command as described in Section :ref:`TODO-1.3.4` and show the internal +representation. + +.. example:: + .. coqtop:: all + + Fixpoint plus (n m:nat) {struct n} : nat := + match n with + | O => m + | S p => S (plus p m) + end. + + Print plus. + Fixpoint lgth (A:Set) (l:list A) {struct l} : nat := + match l with + | nil _ => O + | cons _ a l' => S (lgth A l') + end. + Print lgth. + Fixpoint sizet (t:tree) : nat := let (f) := t in S (sizef f) + with sizef (f:forest) : nat := + match f with + | emptyf => O + | consf t f => plus (sizet t) (sizef f) + end. + Print sizet. + +.. _Reduction-rule: + +Reduction rule +++++++++++++++ + +Let :math:`F` be the set of declarations: +:math:`f_1 /k_1 :A_1 :=t_1 …f_n /k_n :A_n:=t_n`. +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} + +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 +for primitive recursive operators. The following reductions are now +possible: + +.. math:: + \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*} + +.. _Mutual-induction: + +**Mutual induction** + +The principles of mutual induction can be automatically generated +using the Scheme command described in Section :ref:`TODO-13.1`. + + +.. _Admissible-rules-for-global-environments: + +Admissible rules for global environments +-------------------------------------------- + +From the original rules of the type system, one can show the +admissibility of rules which change the local context of definition of +objects in the global environment. We show here the admissible rules +that are used in the discharge mechanism at the end of a section. + + +.. _Abstraction: + +**Abstraction.** +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'`. + +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)\}`. + + +.. _First-abstracting-property: + +**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′)}}} + + +.. 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′)}}} + +.. 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}}} + +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}]`. + + +.. _Second-abstracting-property: + +**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″}{Γ}} + +.. math:: + \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″}{Γ}} + +.. _Pruning-the-local-context: + +**Pruning the local context.** +If one abstracts or substitutes constants with the above rules then it +may happen that some declared or defined constant does not occur any +more in the subsequent global environment and in the local context. +One can consequently derive the following property. + + +.. _First-pruning-property: + +.. inference:: First pruning property: + + \WF{E;c:U;E′}{Γ} + c~\kw{does not occur in}~E′~\kw{and}~Γ + -------------------------------------- + \WF{E;E′}{Γ} + + +.. _Second-pruning-property: + +.. inference:: Second pruning property: + + \WF{E;c:=u:U;E′}{Γ} + c~\kw{does not occur in}~E′~\kw{and}~Γ + -------------------------------------- + \WF{E;E′}{Γ} + + +.. _Co-inductive-types: + +Co-inductive types +---------------------- + +The implementation contains also co-inductive definitions, which are +types inhabited by infinite objects. More information on co-inductive +definitions can be found in :cite:`Gimenez95b,Gim98,GimCas05`. + + +.. _The-Calculus-of-Inductive-Construction-with-impredicative-Set: + +The Calculus of Inductive Construction with impredicative Set +----------------------------------------------------------------- + +|Coq| can be used as a type-checker for the Calculus of Inductive +Constructions with an impredicative sort :math:`\Set` by using the compiler +option ``-impredicative-set``. For example, using the ordinary `coqtop` +command, the following is rejected, + +.. example:: + .. coqtop:: all + + Fail Definition id: Set := forall X:Set,X->X. + +while it will type-check, if one uses instead the `coqtop` +``-impredicative-set`` option.. + +The major change in the theory concerns the rule for product formation +in the sort Set, which is extended to a domain in any sort: + +.. inference:: ProdImp + + E[Γ] ⊢ T : s + s ∈ {\Sort} + 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 +inductive definitions* like the example of second-order existential +quantifier (exSet). + +There should be restrictions on the eliminations which can be +performed on such definitions. The eliminations rules in the +impredicative system for sort Set become: + + + +.. inference:: Set1 + + s ∈ \{Prop, Set\} + ----------------- + [I:Set|I→ s] + +.. inference:: Set2 + + I~\kw{is a small inductive definition} + s ∈ \{\Type(i)\} + ---------------- + [I:Set|I→ s] + + diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst new file mode 100644 index 0000000000..29053d6a57 --- /dev/null +++ b/doc/sphinx/language/coq-library.rst @@ -0,0 +1,988 @@ +.. include:: ../replaces.rst + +.. _thecoqlibrary: + +The |Coq| library +================= + +:Source: https://coq.inria.fr/distrib/current/refman/stdlib.html +:Converted by: Pierre Letouzey + +.. index:: + single: Theories + + +The |Coq| library is structured into two parts: + + * **The initial library**: it contains elementary logical notions and + data-types. It constitutes the basic state of the system directly + available when running |Coq|; + + * **The standard library**: general-purpose libraries containing various + developments of |Coq| axiomatizations about sets, lists, sorting, + arithmetic, etc. This library comes with the system and its modules + are directly accessible through the ``Require`` command (see + Section :ref:`TODO-6.5.1-Require`); + +In addition, user-provided libraries or developments are provided by +|Coq| users' community. These libraries and developments are available +for download at http://coq.inria.fr (see +Section :ref:`userscontributions`). + +This chapter briefly reviews the |Coq| libraries whose contents can +also be browsed at http://coq.inria.fr/stdlib. + + + + +The basic library +----------------- + +This section lists the basic notions and results which are directly +available in the standard |Coq| system. Most of these constructions +are defined in the ``Prelude`` module in directory ``theories/Init`` +at the |Coq| root directory; this includes the modules +``Notations``, +``Logic``, +``Datatypes``, +``Specif``, +``Peano``, +``Wf`` and +``Tactics``. +Module ``Logic_Type`` also makes it in the initial state. + + +Notations +~~~~~~~~~ + +This module defines the parsing and pretty-printing of many symbols +(infixes, prefixes, etc.). However, it does not assign a meaning to +these notations. The purpose of this is to define and fix once for all +the precedence and associativity of very common notations. The main +notations fixed in the initial state are : + +================ ============ =============== +Notation Precedence Associativity +================ ============ =============== +``_ -> _`` 99 right +``_ <-> _`` 95 no +``_ \/ _`` 85 right +``_ /\ _`` 80 right +``~ _`` 75 right +``_ = _`` 70 no +``_ = _ = _`` 70 no +``_ = _ :> _`` 70 no +``_ <> _`` 70 no +``_ <> _ :> _`` 70 no +``_ < _`` 70 no +``_ > _`` 70 no +``_ <= _`` 70 no +``_ >= _`` 70 no +``_ < _ < _`` 70 no +``_ < _ <= _`` 70 no +``_ <= _ < _`` 70 no +``_ <= _ <= _`` 70 no +``_ + _`` 50 left +``_ || _`` 50 left +``_ - _`` 50 left +``_ * _`` 40 left +``_ _`` 40 left +``_ / _`` 40 left +``- _`` 35 right +``/ _`` 35 right +``_ ^ _`` 30 right +================ ============ =============== + +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: + +.. /!\ 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) + +.. note:: + + Implication is not defined but primitive (it is a non-dependent + product of a proposition over another proposition). There is also a + primitive universal quantification (it is a dependent product over a + proposition). The primitive universal quantification allows both + first-order and higher-order quantification. + +Propositional Connectives ++++++++++++++++++++++++++ + +.. index:: + single: Connectives + single: True (term) + single: I (term) + single: False (term) + single: not (term) + single: and (term) + single: conj (term) + single: proj1 (term) + single: proj2 (term) + single: or (term) + single: or_introl (term) + single: or_intror (term) + single: iff (term) + single: IF_then_else (term) + +First, we find propositional calculus connectives: + +.. coqtop:: in + + Inductive True : Prop := I. + Inductive False : Prop := . + Definition not (A: Prop) := A -> False. + Inductive and (A B:Prop) : Prop := conj (_:A) (_:B). + Section Projections. + Variables A B : Prop. + Theorem proj1 : A /\ B -> A. + Theorem proj2 : A /\ B -> B. + End Projections. + Inductive or (A B:Prop) : Prop := + | or_introl (_:A) + | or_intror (_:B). + Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P). + Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R. + +Quantifiers ++++++++++++ + +.. index:: + single: Quantifiers + single: all (term) + single: ex (term) + single: exists (term) + single: ex_intro (term) + single: ex2 (term) + single: exists2 (term) + single: ex_intro2 (term) + +Then we find first-order quantifiers: + +.. coqtop:: in + + Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. + Inductive ex (A: Set) (P:A -> Prop) : Prop := + ex_intro (x:A) (_:P x). + Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop := + ex_intro2 (x:A) (_:P x) (_:Q x). + +The following abbreviations are allowed: + +====================== ======================================= +``exists x:A, P`` ``ex A (fun x:A => P)`` +``exists x, P`` ``ex _ (fun x => P)`` +``exists2 x:A, P & Q`` ``ex2 A (fun x:A => P) (fun x:A => Q)`` +``exists2 x, P & Q`` ``ex2 _ (fun x => P) (fun x => Q)`` +====================== ======================================= + +The type annotation ``:A`` can be omitted when ``A`` can be +synthesized by the system. + +Equality +++++++++ + +.. index:: + single: Equality + single: eq (term) + single: eq_refl (term) + +Then, we find equality, defined as an inductive relation. That is, +given a type ``A`` and an ``x`` of type ``A``, the +predicate :g:`(eq A x)` is the smallest one which contains ``x``. +This definition, due to Christine Paulin-Mohring, is equivalent to +define ``eq`` as the smallest reflexive relation, and it is also +equivalent to Leibniz' equality. + +.. coqtop:: in + + Inductive eq (A:Type) (x:A) : A -> Prop := + eq_refl : eq A x x. + +Lemmas +++++++ + +Finally, a few easy lemmas are provided. + +.. index:: + single: absurd (term) + single: eq_sym (term) + single: eq_trans (term) + single: f_equal (term) + single: sym_not_eq (term) + single: eq_ind_r (term) + single: eq_rec_r (term) + single: eq_rect (term) + single: eq_rect_r (term) + +.. coqtop:: in + + Theorem absurd : forall A C:Prop, A -> ~ A -> C. + Section equality. + Variables A B : Type. + Variable f : A -> B. + Variables x y z : A. + Theorem eq_sym : x = y -> y = x. + Theorem eq_trans : x = y -> y = z -> x = z. + Theorem f_equal : x = y -> f x = f y. + Theorem not_eq_sym : x <> y -> y <> x. + End equality. + Definition eq_ind_r : + forall (A:Type) (x:A) (P:A->Prop), P x -> forall y:A, y = x -> P y. + Definition eq_rec_r : + forall (A:Type) (x:A) (P:A->Set), P x -> forall y:A, y = x -> P y. + Definition eq_rect_r : + forall (A:Type) (x:A) (P:A->Type), P x -> forall y:A, y = x -> P y. + Hint Immediate eq_sym not_eq_sym : core. + +.. index:: + single: f_equal2 ... f_equal5 (term) + +The theorem ``f_equal`` is extended to functions with two to five +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 + + Theorem f_equal3 : + forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) + (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), + x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. + +.. _datatypes: + +Datatypes +~~~~~~~~~ + +.. index:: + single: Datatypes + +In the basic library, we find in ``Datatypes.v`` the definition +of the basic data-types of programming, +defined as inductive constructions over the sort ``Set``. Some of +them come with a special syntax shown below (this syntax table is common with +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) + term : (`term`, `term`) (pair) + + +Programming ++++++++++++ + +.. index:: + single: Programming + single: unit (term) + single: tt (term) + single: bool (term) + single: true (term) + single: false (term) + single: nat (term) + single: O (term) + single: S (term) + single: option (term) + single: Some (term) + single: None (term) + single: identity (term) + single: refl_identity (term) + +.. coqtop:: in + + Inductive unit : Set := tt. + Inductive bool : Set := true | false. + Inductive nat : Set := O | S (n:nat). + Inductive option (A:Set) : Set := Some (_:A) | None. + Inductive identity (A:Type) (a:A) : A -> Type := + refl_identity : identity A a a. + +Note that zero is the letter ``O``, and *not* the numeral ``0``. + +The predicate ``identity`` is logically +equivalent to equality but it lives in sort ``Type``. +It is mainly maintained for compatibility. + +We then define the disjoint sum of ``A+B`` of two sets ``A`` and +``B``, and their product ``A*B``. + +.. index:: + single: sum (term) + single: A+B (term) + single: + (term) + single: inl (term) + single: inr (term) + single: prod (term) + single: A*B (term) + single: * (term) + single: pair (term) + single: fst (term) + single: snd (term) + +.. coqtop:: in + + Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B). + Inductive prod (A B:Set) : Set := pair (_:A) (_:B). + Section projections. + Variables A B : Set. + Definition fst (H: prod A B) := match H with + | pair _ _ x y => x + end. + Definition snd (H: prod A B) := match H with + | pair _ _ x y => y + end. + End projections. + +Some operations on ``bool`` are also provided: ``andb`` (with +infix notation ``&&``), ``orb`` (with +infix notation ``||``), ``xorb``, ``implb`` and ``negb``. + +.. _specification: + +Specification +~~~~~~~~~~~~~ + +The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. +They are available with the syntax shown in the previous section :ref:`datatypes`. + +For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct +:g:`{x:A | P x}` (in abstract syntax :g:`(sig A P)`) is a +``Type``. We may build elements of this set as :g:`(exist x p)` +whenever we have a witness :g:`x:A` with its justification +:g:`p:P x`. + +From such a :g:`(exist x p)` we may in turn extract its witness +:g:`x:A` (using an elimination construct such as ``match``) but +*not* its justification, which stays hidden, like in an abstract +data-type. In technical terms, one says that ``sig`` is a *weak +(dependent) sum*. A variant ``sig2`` with two predicates is also +provided. + +.. index:: + single: {x:A | P x} (term) + single: sig (term) + single: exist (term) + single: sig2 (term) + single: exist2 (term) + +.. coqtop:: in + + Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). + Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := + exist2 (x:A) (_:P x) (_:Q x). + +A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined, +when the predicate ``P`` is now defined as a +constructor of types in ``Type``. + +.. index:: + single: {x:A & P x} (term) + single: sigT (term) + single: existT (term) + single: sigT2 (term) + single: existT2 (term) + single: projT1 (term) + single: projT2 (term) + +.. coqtop:: in + + Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x). + Section Projections2. + Variable A : Type. + Variable P : A -> Type. + Definition projT1 (H:sigT A P) := let (x, h) := H in x. + Definition projT2 (H:sigT A P) := + match H return P (projT1 H) with + existT _ _ x h => h + end. + End Projections2. + Inductive sigT2 (A: Type) (P Q:A -> Type) : Type := + existT2 (x:A) (_:P x) (_:Q x). + +A related non-dependent construct is the constructive sum +:g:`{A}+{B}` of two propositions ``A`` and ``B``. + +.. index:: + single: sumbool (term) + single: left (term) + single: right (term) + single: {A}+{B} (term) + +.. coqtop:: in + + Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B). + +This ``sumbool`` construct may be used as a kind of indexed boolean +data-type. An intermediate between ``sumbool`` and ``sum`` is +the mixed ``sumor`` which combines :g:`A:Set` and :g:`B:Prop` +in the construction :g:`A+{B}` in ``Set``. + +.. index:: + single: sumor (term) + single: inleft (term) + single: inright (term) + single: A+{B} (term) + +.. coqtop:: in + + Inductive sumor (A:Set) (B:Prop) : Set := + | inleft (_:A) + | inright (_:B). + +We may define variants of the axiom of choice, like in Martin-Löf's +Intuitionistic Type Theory. + +.. index:: + single: Choice (term) + single: Choice2 (term) + single: bool_choice (term) + +.. coqtop:: in + + Lemma Choice : + forall (S S':Set) (R:S -> S' -> Prop), + (forall x:S, {y : S' | R x y}) -> + {f : S -> S' | forall z:S, R z (f z)}. + Lemma Choice2 : + forall (S S':Set) (R:S -> S' -> Set), + (forall x:S, {y : S' & R x y}) -> + {f : S -> S' & forall z:S, R z (f z)}. + Lemma bool_choice : + forall (S:Set) (R1 R2:S -> Prop), + (forall x:S, {R1 x} + {R2 x}) -> + {f : S -> bool | + forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}. + +The next construct builds a sum between a data-type :g:`A:Type` and +an exceptional value encoding errors: + +.. index:: + single: Exc (term) + single: value (term) + single: error (term) + +.. coqtop:: in + + Definition Exc := option. + Definition value := Some. + Definition error := None. + +This module ends with theorems, relating the sorts ``Set`` or +``Type`` and ``Prop`` in a way which is consistent with the +realizability interpretation. + +.. index:: + single: False_rect (term) + single: False_rec (term) + single: eq_rect (term) + single: absurd_set (term) + single: and_rect (term) + +.. coqtop:: in + + Definition except := False_rec. + Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. + Theorem and_rect2 : + forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P. + + +Basic Arithmetics +~~~~~~~~~~~~~~~~~ + +The basic library includes a few elementary properties of natural +numbers, together with the definitions of predecessor, addition and +multiplication, in module ``Peano.v``. It also +provides a scope ``nat_scope`` gathering standard notations for +common operations (``+``, ``*``) and a decimal notation for +numbers, allowing for instance to write ``3`` for :g:`S (S (S O)))`. This also works on +the left hand side of a ``match`` expression (see for example +section :ref:`TODO-refine-example`). This scope is opened by default. + +.. example:: + + The following example is not part of the standard library, but it + shows the usage of the notations: + + .. coqtop:: in + + Fixpoint even (n:nat) : bool := + match n with + | 0 => true + | 1 => false + | S (S n) => even n + end. + +.. index:: + single: eq_S (term) + single: pred (term) + single: pred_Sn (term) + single: eq_add_S (term) + single: not_eq_S (term) + single: IsSucc (term) + single: O_S (term) + single: n_Sn (term) + single: plus (term) + single: plus_n_O (term) + single: plus_n_Sm (term) + single: mult (term) + single: mult_n_O (term) + single: mult_n_Sm (term) + +Now comes the content of module ``Peano``: + +.. coqtop:: in + + Theorem eq_S : forall x y:nat, x = y -> S x = S y. + Definition pred (n:nat) : nat := + match n with + | 0 => 0 + | S u => u + end. + Theorem pred_Sn : forall m:nat, m = pred (S m). + Theorem eq_add_S : forall n m:nat, S n = S m -> n = m. + Hint Immediate eq_add_S : core. + Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. + Definition IsSucc (n:nat) : Prop := + match n with + | 0 => False + | S p => True + end. + Theorem O_S : forall n:nat, 0 <> S n. + Theorem n_Sn : forall n:nat, n <> S n. + Fixpoint plus (n m:nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (p + m) + end + where "n + m" := (plus n m) : nat_scope. + Lemma plus_n_O : forall n:nat, n = n + 0. + Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. + Fixpoint mult (n m:nat) {struct n} : nat := + match n with + | 0 => 0 + | S p => m + p * m + end + where "n * m" := (mult n m) : nat_scope. + Lemma mult_n_O : forall n:nat, 0 = n * 0. + Lemma mult_n_Sm : forall n m:nat, n * m + n = n * (S m). + + +Finally, it gives the definition of the usual orderings ``le``, +``lt``, ``ge`` and ``gt``. + +.. index:: + single: le (term) + single: le_n (term) + single: le_S (term) + single: lt (term) + single: ge (term) + single: gt (term) + +.. coqtop:: in + + Inductive le (n:nat) : nat -> Prop := + | le_n : le n n + | 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. + Definition gt (n m:nat) := m < n. + +Properties of these relations are not initially known, but may be +required by the user from modules ``Le`` and ``Lt``. Finally, +``Peano`` gives some lemmas allowing pattern-matching, and a double +induction principle. + +.. index:: + single: nat_case (term) + single: nat_double_ind (term) + +.. coqtop:: in + + Theorem nat_case : + forall (n:nat) (P:nat -> Prop), + P 0 -> (forall m:nat, P (S m)) -> P n. + Theorem nat_double_ind : + forall R:nat -> nat -> Prop, + (forall n:nat, R 0 n) -> + (forall n:nat, R (S n) 0) -> + (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m. + + +Well-founded recursion +~~~~~~~~~~~~~~~~~~~~~~ + +The basic library contains the basics of well-founded recursion and +well-founded induction, in module ``Wf.v``. + +.. index:: + single: Well foundedness + single: Recursion + single: Well founded induction + single: Acc (term) + single: Acc_inv (term) + single: Acc_rect (term) + single: well_founded (term) + +.. coqtop:: in + + Section Well_founded. + Variable A : Type. + Variable R : A -> A -> Prop. + Inductive Acc (x:A) : Prop := + Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x. + Lemma Acc_inv x : Acc x -> forall y:A, R y x -> Acc y. + Definition well_founded := forall a:A, Acc a. + Hypothesis Rwf : well_founded. + Theorem well_founded_induction : + forall P:A -> Set, + (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. + Theorem well_founded_ind : + forall P:A -> Prop, + (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. + +The automatically generated scheme ``Acc_rect`` +can be used to define functions by fixpoints using +well-founded relations to justify termination. Assuming +extensionality of the functional used for the recursive call, the +fixpoint equation can be proved. + +.. index:: + single: Fix_F (term) + single: fix_eq (term) + single: Fix_F_inv (term) + single: Fix_F_eq (term) + +.. coqtop:: in + + Section FixPoint. + Variable P : A -> Type. + Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x. + Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x := + F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)). + Definition Fix (x:A) := Fix_F x (Rwf x). + Hypothesis F_ext : + forall (x:A) (f g:forall y:A, R y x -> P y), + (forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g. + Lemma Fix_F_eq : + forall (x:A) (r:Acc x), + F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r. + Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s. + Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y). + End FixPoint. + End Well_founded. + +Accessing the Type level +~~~~~~~~~~~~~~~~~~~~~~~~ + +The basic library includes the definitions of the counterparts of some data-types and logical +quantifiers at the ``Type``: level: negation, pair, and properties +of ``identity``. This is the module ``Logic_Type.v``. + +.. index:: + single: notT (term) + single: prodT (term) + single: pairT (term) + +.. coqtop:: in + + Definition notT (A:Type) := A -> False. + Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B). + +At the end, it defines data-types at the ``Type`` level. + +Tactics +~~~~~~~ + +A few tactics defined at the user level are provided in the initial +state, in module ``Tactics.v``. They are listed at +http://coq.inria.fr/stdlib, in paragraph ``Init``, link ``Tactics``. + + +The standard library +-------------------- + +Survey +~~~~~~ + +The rest of the standard library is structured into the following +subdirectories: + + * **Logic** : Classical logic and dependent equality + * **Arith** : Basic Peano arithmetic + * **PArith** : Basic positive integer arithmetic + * **NArith** : Basic binary natural number arithmetic + * **ZArith** : Basic relative integer arithmetic + * **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words) + * **Bool** : Booleans (basic functions and results) + * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) + * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) + * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees) + * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...) + * **Relations** : Relations (definitions and basic results) + * **Sorting** : Sorted list (basic definitions and heapsort correctness) + * **Strings** : 8-bits characters and strings + * **Wellfounded** : Well-founded relations (basic results) + + +These directories belong to the initial load path of the system, and +the modules they provide are compiled at installation time. So they +are directly accessible with the command ``Require`` (see +Section :ref:`TODO-6.5.1-Require`). + +The different modules of the |Coq| standard library are documented +online at http://coq.inria.fr/stdlib. + +Peano’s arithmetic (nat) +~~~~~~~~~~~~~~~~~~~~~~~~ + +.. index:: + single: Peano's arithmetic + single: nat_scope + +While in the initial state, many operations and predicates of Peano's +arithmetic are defined, further operations and results belong to other +modules. For instance, the decidability of the basic predicates are +defined here. This is provided by requiring the module ``Arith``. + +The following table describes the notations available in scope +``nat_scope`` : + +=============== =================== +Notation Interpretation +=============== =================== +``_ < _`` ``lt`` +``_ <= _`` ``le`` +``_ > _`` ``gt`` +``_ >= _`` ``ge`` +``x < y < z`` ``x < y /\ y < z`` +``x < y <= z`` ``x < y /\ y <= z`` +``x <= y < z`` ``x <= y /\ y < z`` +``x <= y <= z`` ``x <= y /\ y <= z`` +``_ + _`` ``plus`` +``_ - _`` ``minus`` +``_ * _`` ``mult`` +=============== =================== + + +Notations for integer arithmetics +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. index:: + single: Arithmetical notations + single: + (term) + single: * (term) + single: - (term) + singel: / (term) + single: <= (term) + single: >= (term) + single: < (term) + single: > (term) + single: ?= (term) + single: mod (term) + + +The following table describes the syntax of expressions +for integer arithmetics. It is provided by requiring and opening the module ``ZArith`` and opening scope ``Z_scope``. +It specifies how notations are interpreted and, when not +already reserved, the precedence and associativity. + +=============== ==================== ========== ============= +Notation Interpretation Precedence Associativity +=============== ==================== ========== ============= +``_ < _`` ``Z.lt`` +``_ <= _`` ``Z.le`` +``_ > _`` ``Z.gt`` +``_ >= _`` ``Z.ge`` +``x < y < z`` ``x < y /\ y < z`` +``x < y <= z`` ``x < y /\ y <= z`` +``x <= y < z`` ``x <= y /\ y < z`` +``x <= y <= z`` ``x <= y /\ y <= z`` +``_ ?= _`` ``Z.compare`` 70 no +``_ + _`` ``Z.add`` +``_ - _`` ``Z.sub`` +``_ * _`` ``Z.mul`` +``_ / _`` ``Z.div`` +``_ mod _`` ``Z.modulo`` 40 no +``- _`` ``Z.opp`` +``_ ^ _`` ``Z.pow`` +=============== ==================== ========== ============= + + +.. example:: + .. coqtop:: all reset + + Require Import ZArith. + Check (2 + 3)%Z. + Open Scope Z_scope. + Check 2 + 3. + + +Real numbers library +~~~~~~~~~~~~~~~~~~~~ + +Notations for real numbers +++++++++++++++++++++++++++ + +This is provided by requiring and opening the module ``Reals`` and +opening scope ``R_scope``. This set of notations is very similar to +the notation for integer arithmetics. The inverse function was added. + +=============== =================== +Notation Interpretation +=============== =================== +``_ < _`` ``Rlt`` +``_ <= _`` ``Rle`` +``_ > _`` ``Rgt`` +``_ >= _`` ``Rge`` +``x < y < z`` ``x < y /\ y < z`` +``x < y <= z`` ``x < y /\ y <= z`` +``x <= y < z`` ``x <= y /\ y < z`` +``x <= y <= z`` ``x <= y /\ y <= z`` +``_ + _`` ``Rplus`` +``_ - _`` ``Rminus`` +``_ * _`` ``Rmult`` +``_ / _`` ``Rdiv`` +``- _`` ``Ropp`` +``/ _`` ``Rinv`` +``_ ^ _`` ``pow`` +=============== =================== + +.. example:: + .. coqtop:: all reset + + Require Import Reals. + Check (2 + 3)%R. + Open Scope R_scope. + Check 2 + 3. + +Some tactics for real numbers ++++++++++++++++++++++++++++++ + +In addition to the powerful ``ring``, ``field`` and ``fourier`` +tactics (see Chapter :ref:`tactics`), there are also: + +.. tacn:: discrR + :name: discrR + + Proves that two real integer constants are different. + +.. example:: + .. coqtop:: all reset + + Require Import DiscrR. + Open Scope R_scope. + Goal 5 <> 0. + discrR. + +.. tacn:: split_Rabs + :name: split_Rabs + + Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions. + +.. example:: + .. coqtop:: all reset + + Require Import Reals. + Open Scope R_scope. + Goal forall x:R, x <= Rabs x. + intro; split_Rabs. + +.. tacn:: split_Rmult + :name: split_Rmult + + Splits a condition that a product is non null into subgoals + corresponding to the condition on each operand of the product. + +.. example:: + .. coqtop:: all reset + + Require Import Reals. + Open Scope R_scope. + Goal forall x y z:R, x * y * z <> 0. + intros; split_Rmult. + +These tactics has been written with the tactic language Ltac +described in Chapter :ref:`thetacticlanguage`. + + +List library +~~~~~~~~~~~~ + +.. index:: + single: Notations for lists + single: length (term) + single: head (term) + single: tail (term) + single: app (term) + single: rev (term) + single: nth (term) + single: map (term) + single: flat_map (term) + single: fold_left (term) + single: fold_right (term) + +Some elementary operations on polymorphic lists are defined here. +They can be accessed by requiring module ``List``. + +It defines the following notions: + + * ``length`` + * ``head`` : first element (with default) + * ``tail`` : all but first element + * ``app`` : concatenation + * ``rev`` : reverse + * ``nth`` : accessing n-th element (with default) + * ``map`` : applying a function + * ``flat_map`` : applying a function returning lists + * ``fold_left`` : iterator (from head to tail) + * ``fold_right`` : iterator (from tail to head) + +The following table shows notations available when opening scope ``list_scope``. + +========== ============== ========== ============= +Notation Interpretation Precedence Associativity +========== ============== ========== ============= +``_ ++ _`` ``app`` 60 right +``_ :: _`` ``cons`` 60 right +========== ============== ========== ============= + +.. _userscontributions: + +Users’ contributions +-------------------- + +Numerous users' contributions have been collected and are available at +URL http://coq.inria.fr/opam/www/. On this web page, you have a list +of all contributions with informations (author, institution, quick +description, etc.) and the possibility to download them one by one. +You will also find informations on how to submit a new +contribution. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst new file mode 100644 index 0000000000..68066faa30 --- /dev/null +++ b/doc/sphinx/language/gallina-extensions.rst @@ -0,0 +1,2358 @@ +.. include:: ../replaces.rst + +.. _extensionsofgallina: + +Extensions of |Gallina| +======================= + +|Gallina| is the kernel language of |Coq|. We describe here extensions of +|Gallina|’s syntax. + +.. _record-types: + +Record types +---------------- + +The ``Record`` construction is a macro allowing the definition of +records as is done in many programming languages. Its syntax is +described in the grammar below. In fact, the ``Record`` macro is more general +than the usual record types, since it allows also for “manifest” +expressions. In this sense, the ``Record`` construction allows defining +“signatures”. + +.. _record_grammar: + + .. productionlist:: `sentence` + record : `record_keyword` ident [binders] [: sort] := [ident] { [`field` ; … ; `field`] }. + record_keyword : Record | Inductive | CoInductive + field : name [binders] : type [ where notation ] + : | name [binders] [: term] := term + +In the expression: + +.. cmd:: Record @ident {* @param } {? : @sort} := {? @ident} { {*; @ident {* @binder } : @term } }. + +the first identifier `ident` is the name of the defined record and `sort` is its +type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, +the default name ``Build_``\ `ident`, where `ident` is the record name, is used. If `sort` is +omitted, the default sort is `\Type`. The identifiers inside the brackets are the names of +fields. For a given field `ident`, its type is :g:`forall binder …, term`. +Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the +order of the fields is important. Finally, each `param` is a parameter of the record. + +More generally, a record may have explicitly defined (a.k.a. manifest) +fields. For instance, we might have:: + + Record ident param : sort := { ident₁ : type₁ ; ident₂ := term₂ ; ident₃ : type₃ }. + +in which case the correctness of |type_3| may rely on the instance |term_2| of |ident_2| and |term_2| in turn +may depend on |ident_1|. + +.. example:: + + .. 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}. + +Remark 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: + +.. cmd:: Variant @ident {* @params} : @sort := @ident {* (@ident : @term_1)}. + +To build an object of type `ident`, one should provide the constructor +|ident_0| with the appropriate number of terms filling the fields of the record. + +.. example:: Let us define the rational :math:`1/2`: + + .. coqtop:: in + + Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. + Admitted. + + Definition half := mkRat true 1 2 (O_S 1) one_two_irred. + Check half. + +.. _record-named-fields-grammar: + + .. productionlist:: + term : {| [`field_def` ; … ; `field_def`] |} + field_def : name [binders] := `term` + +Alternatively, the following syntax allows creating objects by using named fields, as +shown in this grammar. The fields do not have to be in any particular order, nor do they have +to be all present if the missing ones can be inferred or prompted for +(see :ref:`programs`). + +.. coqtop:: all + + Definition half' := + {| sign := true; + Rat_bottom_cond := O_S 1; + Rat_irred_cond := one_two_irred |}. + +This syntax can be disabled globally for printing by + +.. cmd:: Unset Printing Records. + +For a given type, one can override this using either + +.. cmd:: Add Printing Record @ident. + +to get record syntax or + +.. cmd:: Add Printing Constructor @ident. + +to get constructor syntax. + +This syntax can also be used for pattern matching. + +.. coqtop:: all + + Eval compute in ( + match half with + | {| sign := true; top := n |} => n + | _ => 0 + end). + +The macro generates also, when it is possible, the projection +functions for destructuring an object of type `\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: + +.. coqtop:: all + + Eval compute in top half. + Eval compute in bottom half. + Eval compute in Rat_bottom_cond half. + +An alternative syntax for projections based on a dot notation is +available: + +.. coqtop:: all + + Eval compute in half.(top). + +It can be activated for printing with + +.. cmd:: Set Printing Projections. + +.. example:: + + .. coqtop:: all + + Set Printing Projections. + Check top half. + +.. _record_projections_grammar: + + .. productionlist:: terms + term : 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 +other arguments are the parameters of the inductive type. + +.. note::. Records defined with the ``Record`` keyword are not allowed to be + recursive (references to the record's name in the type of its field + raises an error). To define recursive records, one can use the ``Inductive`` + and ``CoInductive`` keywords, resulting in an inductive or co-inductive record. + A *caveat*, however, is that records cannot appear in mutually inductive + (or co-inductive) definitions. + +.. note:: Induction schemes are automatically generated for inductive records. + Automatic generation of induction schemes for non-recursive records + defined with the ``Record`` keyword can be activated with the + ``Nonrecursive Elimination Schemes`` option (see :ref:`TODO-13.1.1-nonrecursive-elimination-schemes`). + +.. note::``Structure`` is a synonym of the keyword ``Record``. + +.. warn:: @ident cannot be defined. + + It can happen that the definition of a projection is impossible. + This message is followed by an explanation of this impossibility. + There may be three reasons: + + #. The name `ident` already exists in the environment (see Section :ref:`TODO-1.3.1-axioms`). + #. The body of `ident` uses an incorrect elimination for + `ident` (see Sections :ref:`TODO-1.3.4-fixpoint` and :ref:`TODO-4.5.3-case-expr`). + #. The type of the projections `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. + +.. 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. + +During the definition of the one-constructor inductive definition, all +the errors of inductive definitions, as described in Section +:ref:`TODO-1.3.3-inductive-definitions`, may also occur. + +**See also** Coercions and records in Section :ref:`TODO-18.9-coercions-and-records` of the chapter devoted to coercions. + +.. _primitive_projections: + +Primitive Projections +~~~~~~~~~~~~~~~~~~~~~ + +The option ``Set Primitive Projections`` turns on the use of primitive +projections when defining subsequent records (even through the ``Inductive`` +and ``CoInductive`` commands). 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 +applications of the projection, considerably reducing the sizes of +terms when manipulating parameterized records and typechecking time. +On the user level, primitive projections can be used as a replacement +for the usual defined ones, although there are a few notable differences. + +The internally omitted parameters can be reconstructed at printing time +even though they are absent in the actual AST manipulated by the kernel. This +can be obtained by setting the ``Printing Primitive Projection Parameters`` +flag. Another compatibility printing can be activated thanks to the +``Printing Primitive Projection Compatibility`` option which governs the +printing of pattern-matching over primitive records. + +Primitive Record Types +++++++++++++++++++++++ + +When the ``Set Primitive Projections`` option is on, definitions of +record types change meaning. When a type is declared with primitive +projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). +To eliminate the (co-)inductive type, one must use its defined primitive projections. + +For compatibility, the parameters still appear to the user when +printing terms even though they are absent in the actual AST +manipulated by the kernel. This can be changed by unsetting the +``Printing Primitive Projection Parameters`` flag. Further compatibility +printing can be deactivated thanks to the ``Printing Primitive Projection +Compatibility`` option which governs the printing of pattern-matching +over primitive records. + +There are currently two ways to introduce primitive records types: + +#. Through the ``Record`` command, in which case the type has to be + non-recursive. The defined type enjoys eta-conversion definitionally, + that is the generalized form of surjective pairing for records: + `r` ``= Build_``\ `R` ``(``\ `r`\ ``.(``\ |p_1|\ ``) …`` `r`\ ``.(``\ |p_n|\ ``))``. + Eta-conversion allows to define dependent elimination for these types as well. +#. Through the ``Inductive`` and ``CoInductive`` commands, when + the body of the definition is a record declaration of the form + ``Build_``\ `R` ``{`` |p_1| ``:`` |t_1|\ ``; … ;`` |p_n| ``:`` |t_n| ``}``. + In this case the types can be recursive and eta-conversion is disallowed. These kind of record types + differ from their traditional versions in the sense that dependent + elimination is not available for them and only non-dependent case analysis + can be defined. + +Reduction ++++++++++ + +The basic reduction rule of a primitive projection is +|p_i| ``(Build_``\ `R` |t_1| … |t_n|\ ``)`` :math:`{\rightarrow_{\iota}}` |t_i|. +However, to take the :math:`{\delta}` flag into +account, projections can be in two states: folded or unfolded. An +unfolded primitive projection application obeys the rule above, while +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 ``Printing Primitive Projection Compatibility`` +to display unfolded primitive projections as matches and distinguish them from folded ones. + + +Compatibility Projections and :g:`match` +++++++++++++++++++++++++++++++++++++++++ + +To ease compatibility with ordinary record types, each primitive +projection is also defined as a ordinary constant taking parameters and +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 ``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. + +Additionally, user-written :g:`match` constructs on primitive records +are desugared into substitution of the projections, they cannot be +printed back as :g:`match` constructs. + +Variants and extensions of :g:`match` +------------------------------------- + +.. _extended pattern-matching: + +Multiple and nested pattern-matching +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The basic version of :g:`match` allows pattern-matching on simple +patterns. As an extension, multiple nested patterns or disjunction of +patterns are allowed, as in ML-like languages. + +The extension just acts as a macro that is expanded during parsing +into a sequence of match on simple patterns. Especially, a +construction defined using the extended match is generally printed +under its expanded form (see ``Set Printing Matching`` in :ref:`controlling-match-pp`). + +See also: :ref:`extended pattern-matching`. + + +Pattern-matching on boolean values: the if expression +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +For inductive types with exactly two constructors and for pattern-matching +expressions that do not depend on the arguments of the constructors, it is possible +to use a ``if … then … else`` notation. For instance, the definition + +.. coqtop:: all + + Definition not (b:bool) := + match b with + | true => false + | false => true + end. + +can be alternatively written + +.. coqtop:: reset all + + Definition not (b:bool) := if b then false else true. + +More generally, for an inductive type with constructors |C_1| and |C_2|, +we have the following equivalence + +:: + + if term [dep_ret_type] then term₁ else term₂ ≡ + match term [dep_ret_type] with + | C₁ _ … _ => term₁ + | C₂ _ … _ => term₂ + end + +.. example:: + + .. coqtop:: all + + Check (fun x (H:{x=0}+{x<>0}) => + match H with + | left _ => true + | right _ => false + end). + +Notice that the printing uses the :g:`if` syntax because `sumbool` is +declared as such (see :ref:`controlling-match-pp`). + + +Irrefutable patterns: the destructuring let variants +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern-matching on terms inhabiting inductive type having only one +constructor can be alternatively written using :g:`let … in …` +constructions. There are two variants of them. + + +First destructuring let syntax +++++++++++++++++++++++++++++++ + +The expression :g:`let (`\ |ident_1|:g:`, … ,` |ident_n|\ :g:`) :=` |term_0|\ :g:`in` |term_1| performs +case analysis on |term_0| which must be in an inductive type with one +constructor having itself :math:`n` arguments. Variables |ident_1| … |ident_n| are +bound to the :math:`n` arguments of the constructor in expression |term_1|. For +instance, the definition + +.. coqtop:: reset all + + Definition fst (A B:Set) (H:A * B) := match H with + | pair x y => x + end. + +can be alternatively written + +.. coqtop:: reset all + + Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x. + +Notice that reduction is different from regular :g:`let … in …` +construction since it happens only if |term_0| is in constructor form. +Otherwise, the reduction is blocked. + +The pretty-printing of a definition by matching on a irrefutable +pattern can either be done using :g:`match` or the :g:`let` construction +(see Section :ref:`controlling-match-pp`). + +If term inhabits an inductive type with one constructor `C`, we have an +equivalence between + +:: + + let (ident₁, …, identₙ) [dep_ret_type] := term in term' + +and + +:: + + match term [dep_ret_type] with + C ident₁ … identₙ => term' + end + + +Second destructuring let syntax ++++++++++++++++++++++++++++++++ + +Another destructuring let syntax is available for inductive types with +one constructor by giving an arbitrary pattern instead of just a tuple +for all the arguments. For example, the preceding example can be +written: + +.. coqtop:: reset all + + Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x. + +This is useful to match deeper inside tuples and also to use notations +for the pattern, as the syntax :g:`let ’p := t in b` allows arbitrary +patterns to do the deconstruction. For example: + +.. coqtop:: all + + Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A := + let '((a,b), (c, d)) := x in (a,b,c,d). + + Notation " x 'With' p " := (exist _ x p) (at level 20). + + Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A := + let 'x With p := t in x. + +When printing definitions which are written using this construct it +takes precedence over let printing directives for the datatype under +consideration (see Section :ref:`controlling-match-pp`). + + +.. _controlling-match-pp: + +Controlling pretty-printing of match expressions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following commands give some control over the pretty-printing +of :g:`match` expressions. + +Printing nested patterns ++++++++++++++++++++++++++ + +The Calculus of Inductive Constructions knows pattern-matching only +over simple patterns. It is however convenient to re-factorize nested +pattern-matching into a single pattern-matching over a nested +pattern. |Coq|’s printer tries to do such limited re-factorization. + +.. cmd:: Set Printing Matching. + +This tells |Coq| to try to use nested patterns. This is the default +behavior. + +.. cmd:: Unset Printing Matching. + +This tells |Coq| to print only simple pattern-matching problems in the +same way as the |Coq| kernel handles them. + +.. cmd:: Test Printing Matching. + +This tells if the printing matching mode is on or off. The default is +on. + +Factorization of clauses with same right-hand side +++++++++++++++++++++++++++++++++++++++++++++++++++ + +When several patterns share the same right-hand side, it is additionally +possible to share the clauses using disjunctive patterns. Assuming that the +printing matching mode is on, whether |Coq|'s printer shall try to do this kind +of factorization is governed by the following commands: + +.. cmd:: Set Printing Factorizable Match Patterns. + +This tells |Coq|'s printer to try to use disjunctive patterns. This is the +default behavior. + +.. cmd:: Unset Printing Factorizable Match Patterns. + +This tells |Coq|'s printer not to try to use disjunctive patterns. + +.. cmd:: Test Printing Factorizable Match Patterns. + +This tells if the factorization of clauses with same right-hand side is on or +off. + +Use of a default clause ++++++++++++++++++++++++ + +When several patterns share the same right-hand side which do not depend on the +arguments of the patterns, yet an extra factorization is possible: the +disjunction of patterns can be replaced with a `_` default clause. Assuming that +the printing matching mode and the factorization mode are on, whether |Coq|'s +printer shall try to use a default clause is governed by the following commands: + +.. cmd:: Set Printing Allow Default Clause. + +This tells |Coq|'s printer to use a default clause when relevant. This is the +default behavior. + +.. cmd:: Unset Printing Allow Default Clause. + +This tells |Coq|'s printer not to use a default clause. + +.. cmd:: Test Printing Allow Default Clause. + +This tells if the use of a default clause is allowed. + +Printing of wildcard patterns +++++++++++++++++++++++++++++++ + +Some variables in a pattern may not occur in the right-hand side of +the pattern-matching clause. There are options to control the display +of these variables. + +.. cmd:: Set Printing Wildcard. + +The variables having no occurrences in the right-hand side of the +pattern-matching clause are just printed using the wildcard symbol +“_”. + +.. cmd:: Unset Printing Wildcard. + +The variables, even useless, are printed using their usual name. But +some non-dependent variables have no name. These ones are still +printed using a “_”. + +.. cmd:: Test Printing Wildcard. + +This tells if the wildcard printing mode is on or off. The default is +to print wildcard for useless variables. + + +Printing of the elimination predicate ++++++++++++++++++++++++++++++++++++++ + +In most of the cases, the type of the result of a matched term is +mechanically synthesizable. Especially, if the result type does not +depend of the matched term. + +.. cmd:: Set Printing Synth. + +The result type is not printed when |Coq| knows that it can re- +synthesize it. + +.. cmd:: Unset Printing Synth. + +This forces the result type to be always printed. + +.. cmd:: Test Printing Synth. + +This tells if the non-printing of synthesizable types is on or off. +The default is to not print synthesizable types. + + +Printing matching on irrefutable patterns +++++++++++++++++++++++++++++++++++++++++++ + +If an inductive type has just one constructor, pattern-matching can be +written using the first destructuring let syntax. + +.. cmd:: Add Printing Let @ident. + + This adds `ident` to the list of inductive types for which pattern-matching + is written using a let expression. + +.. cmd:: Remove Printing Let @ident. + + This removes ident from this list. Note that removing an inductive + type from this list has an impact only for pattern-matching written + using :g:`match`. Pattern-matching explicitly written using a destructuring + :g:`let` are not impacted. + +.. cmd:: Test Printing Let for @ident. + + This tells if `ident` belongs to the list. + +.. cmd:: Print Table Printing Let. + + This prints the list of inductive types for which pattern-matching is + written using a let expression. + + The list of inductive types for which pattern-matching is written + using a :g:`let` expression is managed synchronously. This means that it is + sensitive to the command ``Reset``. + + +Printing matching on booleans ++++++++++++++++++++++++++++++ + +If an inductive type is isomorphic to the boolean type, pattern-matching +can be written using ``if`` … ``then`` … ``else`` …: + +.. cmd:: Add Printing If @ident. + + This adds ident to the list of inductive types for which pattern-matching is + written using an if expression. + +.. cmd:: Remove Printing If @ident. + + This removes ident from this list. + +.. cmd:: Test Printing If for @ident. + + This tells if ident belongs to the list. + +.. cmd:: Print Table Printing If. + + This prints the list of inductive types for which pattern-matching is + written using an if expression. + +The list of inductive types for which pattern-matching is written +using an ``if`` expression is managed synchronously. This means that it is +sensitive to the command ``Reset``. + +This example emphasizes what the printing options offer. + +.. example:: + + .. coqtop:: all + + Definition snd (A B:Set) (H:A * B) := match H with + | pair x y => y + end. + + Test Printing Let for prod. + + Print snd. + + Remove Printing Let prod. + + Unset Printing Synth. + + Unset Printing Wildcard. + + Print snd. + +.. _advanced-recursive-functions: + +Advanced recursive functions +---------------------------- + +The following experimental command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``: + +.. 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 Section :ref:`TODO-8.5.5-functional-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 +for non structurally recursive functions. + +See the documentation of functional induction (:ref:`TODO-8.5.5-functional-induction`) +and ``Functional Scheme`` (:ref:`TODO-13.2-functional-scheme`) for how to use +the induction principle to easily reason about the function. + +Remark: To obtain the right principle, it is better to put rigid +parameters of the function as first arguments. For example it is +better to define plus like this: + +.. coqtop:: reset none + + Require Import FunInd. + +.. coqtop:: all + + Function plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. + +than like this: + +.. coqtop:: reset all + + Function plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus p m) + end. + + +*Limitations* + +|term_0| must be built as a *pure pattern-matching tree* (:g:`match … with`) +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` : + +.. coqtop:: all + + Fail Function wrong (C:nat) : nat := + List.hd 0 (List.map wrong (C::nil)). + +For now, dependent cases are not treated for non structurally +terminating functions. + +.. exn:: The recursive argument must be specified +.. exn:: No argument name @ident +.. exn:: Cannot use mutual definition with well-founded recursion or measure + +.. 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 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. + +.. warn:: Cannot build functional inversion principle + + `functional inversion` will not be available for the function. + +See also: :ref:`TODO-13.2-generating-ind-principles` and ref:`TODO-8.5.5-functional-induction` + +Depending on the ``{…}`` annotation, different definition mechanisms are +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: + + + `ident_rect`, `ident_rec` and `ident_ind`, which reflect the pattern + matching structure of `term` (see the documentation of :ref:`TODO-1.3.3-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. + +.. cmdv:: Function @ident {* @binder } { struct @ident } : @type := @term + + Defines the structural recursive function `ident` as if declared with ``Fixpoint``. Moreover the following are defined: + + + The same objects as above; + + The fixpoint equation of `ident`: `ident_equation`. + +.. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term +.. cmdv:: 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 + `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`. + + Depending on the annotation, the user is left with some proof + obligations that will be used to define the function. These proofs + are: proofs that each recursive call is actually decreasing with + respect to the given criteria, and (if the criteria is `wf`) a proof + that the ordering relation is well-founded. Once proof obligations are + discharged, the following objects are defined: + + + The same objects as with the struct; + + The lemma `ident`\ :math:`_{\sf tcc}` which collects all proof obligations in one + property; + + The lemmas `ident`\ :math:`_{\sf terminate}` and `ident`\ :math:`_{\sf F}` which is needed to be inlined + during extraction of ident. + + The way this recursive function is defined is the subject of several + papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles + Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other + hand. Remark: Proof obligations are presented as several subgoals + belonging to a Lemma `ident`\ :math:`_{\sf tcc}`. + + +Section mechanism +----------------- + +The sectioning mechanism can be used to to organize a proof in +structured sections. Then local declarations become available (see +Section :ref:`TODO-1.3.2-Definitions`). + + +.. cmd:: Section @ident. + + This command is used to open a section named `ident`. + + +.. 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. + + .. example:: + + .. coqtop:: all + + Section s1. + + Variables x y : nat. + + Let y' := y. + + Definition x' := S x. + + Definition x'' := x' + y'. + + Print x'. + + End s1. + + Print x'. + + Print x''. + + Notice the difference between the value of `x’` and `x’’` inside section + `s1` and outside. + + .. exn:: This is not the last opened section + +**Remarks:** + +#. Most commands, like ``Hint``, ``Notation``, option management, … which + appear inside a section are canceled when the section is closed. + + +Module system +------------- + +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_bindings : `module_binding` … `module_binding` + 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 :ref:`named_module_type` below). + + +.. cmd:: Module @ident. + + This command is used to start an interactive module named `ident`. + +.. cmdv:: Module @ident {* @module_binding}. + + Starts an interactive functor with + parameters given by module_bindings. + +.. cmdv:: Module @ident : @module_type. + + Starts an interactive module specifying its module type. + +.. 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`. + +.. cmdv:: Module @ident <: {+<: @module_type }. + + Starts an interactive module satisfying each `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`. + +.. cmdv:: Module [ Import | Export ]. + + Behaves like ``Module``, but automatically imports or exports the module. + +Reserved commands inside an interactive module +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Include @module. + + Includes the content of module in the current + interactive module. Here module can be a module expression or a module + type expression. If module is a high-order module or module type + expression then the system tries to instantiate module by the current + interactive module. + +.. cmd:: Include {+<+ @module}. + + is a shortcut for the commands ``Include`` `module` for each `module`. + +.. cmd:: End @ident. + + This command closes the interactive module `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 + + .. exn:: Signature components for label @ident do not match + + .. exn:: This is not the last opened module + +.. cmd:: Module @ident := @module_expression. + + This command defines the module identifier `ident` to be equal + to `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`. + + .. 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`. + + .. 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|. + + .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression}. + + is equivalent to an interactive module where each `module_expression` is included. + +.. _named_module_type: + +.. cmd:: Module Type @ident. + +This command is used to start an interactive module type `ident`. + + .. cmdv:: Module Type @ident {* @module_binding}. + + Starts an interactive functor type with parameters given by `module_bindings`. + + +Reserved commands inside an interactive module type: +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Include @module. + + Same as ``Include`` inside a module. + +.. cmd:: Include {+<+ @module}. + + is a shortcut for the command ``Include`` `module` for each `module`. + +.. cmd:: @assumption_keyword Inline @assums. + + The instance of this assumption will be automatically expanded at functor application, except when + this functor application is prefixed by a ``!`` annotation. + +.. cmd:: End @ident. + + This command closes the interactive module type `ident`. + + .. exn:: This is not the last opened module type + +.. cmd:: Module Type @ident := @module_type. + + Defines a module type `ident` equal to `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`. + + .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type }. + + is equivalent to an interactive module type were each `module_type` is included. + +.. cmd:: Declare Module @ident : @module_type. + + Declares a module `ident` of type `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`. + +.. example:: + + Let us define a simple module. + + .. coqtop:: all + + Module M. + + Definition T := nat. + + Definition x := 0. + + Definition y : bool. + + exact true. + + Defined. + + End M. + +Inside a module one can define constants, prove theorems and do any +other things that can be done in the toplevel. Components of a closed +module can be accessed using the dot notation: + +.. coqtop:: all + + Print M.x. + +A simple module type: + +.. coqtop:: all + + Module Type SIG. + + Parameter T : Set. + + Parameter x : T. + + End SIG. + +Now we can create a new module from M, giving it a less precise +specification: the y component is dropped as well as the body of x. + +.. coqtop:: all + + Module N : SIG with Definition T := nat := M. + + Print N.T. + + Print N.x. + + Fail Print N.y. + +.. reset to remove N (undo in last coqtop block doesn't seem to do that), invisibly redefine M, SIG +.. coqtop:: none reset + + Module M. + + Definition T := nat. + + Definition x := 0. + + Definition y : bool. + + exact true. + + Defined. + + End M. + + Module Type SIG. + + Parameter T : Set. + + Parameter x : T. + + End SIG. + +The definition of ``N`` using the module type expression ``SIG`` with +``Definition T := nat`` is equivalent to the following one: + +.. coqtop:: all + + Module Type SIG'. + + Definition T : Set := nat. + + Parameter x : T. + + End SIG'. + + Module N : SIG' := M. + +If we just want to be sure that the our implementation satisfies a +given module type without restricting the interface, we can use a +transparent constraint + +.. coqtop:: all + + Module P <: SIG := M. + + Print P.y. + +Now let us create a functor, i.e. a parametric module + +.. coqtop:: all + + Module Two (X Y: SIG). + + Definition T := (X.T * Y.T)%type. + + Definition x := (X.x, Y.x). + + End Two. + +and apply it to our modules and do some computations: + +.. coqtop:: all + + Module Q := Two M N. + + Eval compute in (fst Q.x + snd Q.x). + +In the end, let us define a module type with two sub-modules, sharing +some of the fields and give one of its possible implementations: + +.. coqtop:: all + + Module Type SIG2. + + Declare Module M1 : SIG. + + Module M2 <: SIG. + + Definition T := M1.T. + + Parameter x : T. + + End M2. + + End SIG2. + + Module Mod <: SIG2. + + Module M1. + + Definition T := nat. + + Definition x := 1. + + End M1. + + Module M2 := M. + + End Mod. + +Notice that ``M`` is a correct body for the component ``M2`` since its ``T`` +component is equal ``nat`` and hence ``M1.T`` as specified. + +**Remarks:** + +#. 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 + module types. Note that in case of a module definition like: + +:: + + Module N : SIG := M. + +or:: + + Module N : SIG. … End N. + +hints and the like valid for ``N`` are not those defined in ``M`` (or the module body) but the ones defined +in ``SIG``. + + +.. _import_qualid: + +.. 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. + +.. example:: + + .. coqtop:: reset all + + Module Mod. + + Definition T:=nat. + + Check T. + + End Mod. + + Check Mod.T. + + Fail Check T. + + Import Mod. + + 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:`TODO-12.1-Notations`). + +Declarations made with the Local flag are never imported by theImport +command. Such declarations are only accessible through their fully +qualified name. + +.. example:: + + .. coqtop:: all + + Module A. + + Module B. + + Local Definition T := nat. + + End B. + + End A. + + Import A. + + Fail Check B.T. + + .. cmdv:: Export @qualid + + When the module containing the command Export qualid + is imported, qualid is imported as well. + + .. exn:: @qualid is not a module + + .. warn:: Trying to mask the absolute name @qualid! + +.. cmd:: Print Module @ident. + + Prints the module type and (optionally) the body of the module `ident`. + +.. cmd:: Print Module Type @ident. + + Prints the module type corresponding to `ident`. + +.. opt:: Short Module Printing + + This option (off by default) disables the printing of the types of fields, + leaving only their names, for the commands ``Print Module`` and ``Print Module Type``. + +.. cmd:: Locate Module @qualid. + + Prints the full name of the module `qualid`. + +Libraries and qualified names +--------------------------------- + +Names of libraries +~~~~~~~~~~~~~~~~~~ + +The theories developed in |Coq| are stored in *library files* which are +hierarchically classified into *libraries* and *sublibraries*. To +express this hierarchy, library names are represented by qualified +identifiers qualid, i.e. as list of identifiers separated by dots (see +:ref:`TODO-1.2.3-identifiers`). For instance, the library file ``Mult`` of the standard +|Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts +the name of a library is called a *library root*. All library files of +the standard library of |Coq| have the reserved root |Coq| but library +file names based on other roots can be obtained by using |Coq| commands +(coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`TODO-14.3.3-command-line-options`). +Also, when an interactive |Coq| session starts, a library of root ``Top`` is +started, unless option ``-top`` or ``-notop`` is set (see :ref:`TODO-14.3.3-command-line-options`). + + +Qualified names +~~~~~~~~~~~~~~~ + +Library files are modules which possibly contain submodules which +eventually contain constructions (axioms, parameters, definitions, +lemmas, theorems, remarks or facts). The *absolute name*, or *full +name*, of a construction in some library file is a qualified +identifier starting with the logical name of the library file, +followed by the sequence of submodules names encapsulating the +construction and ended by the proper name of the construction. +Typically, the absolute name ``Coq.Init.Logic.eq`` denotes Leibniz’ +equality defined in the module Logic in the sublibrary ``Init`` of the +standard library of |Coq|. + +The proper name that ends the name of a construction is the short name +(or sometimes base name) of the construction (for instance, the short +name of ``Coq.Init.Logic.eq`` is ``eq``). Any partial suffix of the absolute +name is a *partially qualified name* (e.g. ``Logic.eq`` is a partially +qualified name for ``Coq.Init.Logic.eq``). Especially, the short name of a +construction is its shortest partially qualified name. + +|Coq| does not accept two constructions (definition, theorem, …) with +the same absolute name but different constructions can have the same +short name (or even same partially qualified names as soon as the full +names are different). + +Notice that the notion of absolute, partially qualified and short +names also applies to library file names. + +**Visibility** + +|Coq| maintains a table called the name table which maps partially qualified +names of constructions to absolute names. This table is updated by the +commands ``Require`` (see :ref:`TODO-6.5.1-Require`), Import and Export (see :ref:`import_qualid`) and +also each time a new declaration is added to the context. An absolute +name is called visible from a given short or partially qualified name +when this latter name is enough to denote it. This means that the +short or partially qualified name is mapped to the absolute name in +|Coq| name table. Definitions flagged as Local are only accessible with +their fully qualified name (see :ref:`TODO-1.3.2-definitions`). + +It may happen that a visible name is hidden by the short name or a +qualified name of another construction. In this case, the name that +has been hidden must be referred to using one more level of +qualification. To ensure that a construction always remains +accessible, absolute names can never be hidden. + +.. example:: + + .. coqtop:: all + + Check 0. + + Definition nat := bool. + + Check 0. + + Check Datatypes.nat. + + Locate nat. + +See also: Command Locate in :ref:`TODO-6.3.10-locate-qualid` and Locate Library in +:ref:`TODO-6.6.11-locate-library`. + + +Libraries and filesystem +~~~~~~~~~~~~~~~~~~~~~~~~ + +Please note that the questions described here have been subject to +redesign in |Coq| v8.5. Former versions of |Coq| use the same terminology +to describe slightly different things. + +Compiled files (``.vo`` and ``.vio``) store sub-libraries. In order to refer +to them inside |Coq|, a translation from file-system names to |Coq| names +is needed. In this translation, names in the file system are called +*physical* paths while |Coq| names are contrastingly called *logical* +names. + +A logical prefix Lib can be associated to a physical pathpath using +the command line option ``-Q`` `path` ``Lib``. All subfolders of path are +recursively associated to the logical path ``Lib`` extended with the +corresponding suffix coming from the physical path. For instance, the +folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding +to invalid |Coq| identifiers are skipped, and, by convention, +subdirectories named ``CVS`` or ``_darcs`` are skipped too. + +Thanks to this mechanism, .vo files are made available through the +logical name of the folder they are in, extended with their own +basename. For example, the name associated to the file +``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for +invalid identifiers. When compiling a source file, the ``.vo`` file stores +its logical name, so that an error is issued if it is loaded with the +wrong loadpath afterwards. + +Some folders have a special status and are automatically put in the +path. |Coq| commands associate automatically a logical path to files in +the repository trees rooted at the directory from where the command is +launched, coqlib/user-contrib/, the directories listed in the +`$COQPATH`, `${XDG_DATA_HOME}/coq/` and `${XDG_DATA_DIRS}/coq/` +environment variables (see`http://standards.freedesktop.org/basedir- +spec/basedir-spec-latest.html`_) 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:`import_qualid`). For instance, ``-R`` `path` ``Lib`` +associates to the ``filepath/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 +recursive loadpath, which of these files is found first may be system- +dependent and explicit qualification is recommended. The ``From`` argument +of the ``Require`` command can be used to bypass the implicit shortening +by providing an absolute root to the required file (see :ref:`TODO-6.5.1-require-qualid`). + +There also exists another independent loadpath mechanism attached to +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 +:ref:`TODO-6.5-compiled-files` to understand the need of the OCaml loadpath. + +See :ref:`TODO-14.3.3-command-line-options` for a more general view over the |Coq| command +line options. + + +Implicit arguments +------------------ + +An implicit argument of a function is an argument which can be +inferred from contextual knowledge. There are different kinds of +implicit arguments that can be considered implicit in different ways. +There are also various commands to control the setting or the +inference of implicit arguments. + + +The different kinds of implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Implicit arguments inferable from the knowledge of other arguments of a function +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +The first kind of implicit arguments covers the arguments that are +inferable from the knowledge of the type of other arguments of the +function, or of the type of the surrounding context of the +application. Especially, such implicit arguments correspond to +parameters dependent in the type of the function. Typical implicit +arguments are the type arguments in polymorphic functions. There are +several kinds of such implicit arguments. + +**Strict Implicit Arguments** + +An implicit argument can be either strict or non strict. An implicit +argument is said to be *strict* if, whatever the other arguments of the +function are, it is still inferable from the type of some other +argument. Technically, an implicit argument is strict if it +corresponds to a parameter which is not applied to a variable which +itself is another parameter of the function (since this parameter may +erase its arguments), not in the body of a match, and not itself +applied or matched against patterns (since the original form of the +argument can be lost by reduction). + +For instance, the first argument of +:: + + cons: forall A:Set, A -> list A -> list A + +in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A` +will always be inferable from the type :g:`list A` of the third argument of +:g:`cons`. On the contrary, the second argument of a term of type +:: + + forall P:nat->Prop, forall n:nat, P n -> ex nat P + +is implicit but not strict, since it can only be inferred from the +type :g:`P n` of the third argument and if :g:`P` is, e.g., :g:`fun _ => True`, it +reduces to an expression where ``n`` does not occur any longer. The first +argument :g:`P` is implicit but not strict either because it can only be +inferred from :g:`P n` and :g:`P` is not canonically inferable from an arbitrary +:g:`n` and the normal form of :g:`P n`. Consider, e.g., that :g:`n` is :math:`0` and the third +argument has type :g:`True`, then any :g:`P` of the form +:: + + fun n => match n with 0 => True | _ => anything end + +would be a solution of the inference problem. + +**Contextual Implicit Arguments** + +An implicit argument can be *contextual* or not. An implicit argument +is said *contextual* if it can be inferred only from the knowledge of +the type of the context of the current expression. For instance, the +only argument of:: + + nil : forall A:Set, list A` + +is contextual. Similarly, both arguments of a term of type:: + + forall P:nat->Prop, forall n:nat, P n \/ n = 0 + +are contextual (moreover, :g:`n` is strict and :g:`P` is not). + +**Reversible-Pattern Implicit Arguments** + +There is another class of implicit arguments that can be reinferred +unambiguously if all the types of the remaining arguments are known. +This is the class of implicit arguments occurring in the type of +another argument in position of reversible pattern, which means it is +at the head of an application but applied only to uninstantiated +distinct variables. Such an implicit argument is called *reversible- +pattern implicit argument*. A typical example is the argument :g:`P` of +nat_rec in +:: + + nat_rec : forall P : nat -> Set, P 0 -> + (forall n : nat, P n -> P (S n)) -> forall x : nat, P x + +(:g:`P` is reinferable by abstracting over :g:`n` in the type :g:`P n`). + +See :ref:`controlling-rev-pattern-implicit-args` for the automatic declaration of reversible-pattern +implicit arguments. + +Implicit arguments inferable by resolution +++++++++++++++++++++++++++++++++++++++++++ + +This corresponds to a class of non-dependent implicit arguments that +are solved based on the structure of their type only. + + +Maximal or non maximal insertion of implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In case a function is partially applied, and the next argument to be +applied is an implicit argument, two disciplines are applicable. In +the first case, the function is considered to have no arguments +furtherly: one says that the implicit argument is not maximally +inserted. In the second case, the function is considered to be +implicitly applied to the implicit arguments it is waiting for: one +says that the implicit argument is maximally inserted. + +Each implicit argument can be declared to have to be inserted +maximally or non maximally. This can be governed argument per argument +by the command ``Implicit Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the +command ``Set Maximal Implicit Insertion`` (see Section :ref:`controlling-insertion-implicit-args`). +See also :ref:`displaying-implicit-args`. + + +Casual use of implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In a given expression, if it is clear that some argument of a function +can be inferred from the type of the other arguments, the user can +force the given argument to be guessed by replacing it by “_”. If +possible, the correct argument will be automatically generated. + +.. exn:: Cannot infer a term for this placeholder. + + |Coq| was not able to deduce an instantiation of a “_”. + +.. _declare-implicit-args: + +Declaration of implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In case one wants that some arguments of a given object (constant, +inductive types, constructors, assumptions, local or not) are always +inferred by |Coq|, one may declare once and for all which are the +expected implicit arguments of this object. There are two ways to do +this, *a priori* and *a posteriori*. + + +Implicit Argument Binders ++++++++++++++++++++++++++ + +In the first setting, one wants to explicitly give the implicit +arguments of a declared object as part of its definition. To do this, +one has to surround the bindings of implicit arguments by curly +braces: + +.. coqtop:: all + + Definition id {A : Type} (x : A) : A := x. + +This automatically declares the argument A of id as a maximally +inserted implicit argument. One can then do as-if the argument was +absent in every situation but still be able to specify it if needed: + +.. coqtop:: all + + Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x => g (f x). + + Goal forall A, compose id id = id (A:=A). + + +The syntax is supported in all top-level definitions: +``Definition``, ``Fixpoint``, ``Lemma`` and so on. For (co-)inductive datatype +declarations, the semantics are the following: an inductive parameter +declared as an implicit argument need not be repeated in the inductive +definition but will become implicit for the constructors of the +inductive only, not the inductive type itself. For example: + +.. coqtop:: all + + Inductive list {A : Type} : Type := + | nil : list + | cons : A -> list -> list. + + Print list. + +One can always specify the parameter if it is not uniform using the +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 }. + +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. + +After the above declaration is issued, implicit arguments can just +(and have to) be skipped in any expression involving an application +of `qualid`. + +Implicit arguments can be cleared with the following syntax: + +.. cmd:: Arguments @qualid : clear implicits. + +.. cmdv:: Global Arguments @qualid {* @possibly_bracketed_ident } + + Says to recompute the implicit arguments of + `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 }. + + When in a module, tell not to activate the + implicit arguments ofqualid declared by this command to contexts that + require the module. + +.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } }. + + For names of constants, inductive types, + constructors, lemmas which can only be applied to a fixed number of + arguments (this excludes for instance constants whose type is + polymorphic), multiple implicit arguments declarations can be given. + Depending on the number of arguments qualid is applied to in practice, + the longest applicable list of implicit arguments is used to select + which implicit arguments are inserted. For printing, the omitted + arguments are the ones of the longest list of implicit arguments of + the sequence. + +.. example:: + + .. coqtop:: reset all + + Inductive list (A:Type) : Type := + | nil : list A + | cons : A -> list A -> list A. + + Check (cons nat 3 (nil nat)). + + Arguments cons [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 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. + + Arguments length {A} l. (* A has to be maximally inserted *) + + Check (fun l:list (list nat) => map length l). + + Arguments map [A B] f l, [A] B f l, A B f l. + + 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`). + + +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`). + +.. cmdv:: Global Arguments @qualid : default implicits + + Tell to recompute the + implicit arguments of qualid after ending of the current section if + any. + +.. 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. + +.. example:: + + .. coqtop:: reset all + + Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. + + Arguments cons : default implicits. + + Print Implicit cons. + + Arguments nil : default implicits. + + Print Implicit nil. + + Set Contextual Implicit. + + Arguments nil : default implicits. + + Print Implicit nil. + +The computation of implicit arguments takes account of the unfolding +of constants. For instance, the variable ``p`` below has type +``(Transitivity R)`` which is reducible to +``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. + + 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). + + Arguments p : default implicits. + + Print p. + + Print Implicit p. + + Variables (a b c : X) (r1 : R a b) (r2 : R b c). + + Check (p r1 r2). + + +Mode for automatic declaration of implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In case one wants to systematically declare implicit the arguments +detectable as such, one may switch to the automatic declaration of +implicit arguments mode by using the command: + +.. cmd:: Set Implicit Arguments. + +Conversely, one may unset the mode by using ``Unset Implicit Arguments``. +The mode is off by default. Auto-detection of implicit arguments is +governed by options controlling whether strict and contextual implicit +arguments have to be considered or not. + +.. _controlling-strict-implicit-args: + +Controlling strict implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When the mode for automatic declaration of implicit arguments is on, +the default is to automatically set implicit only the strict implicit +arguments plus, for historical reasons, a small subset of the non-strict +implicit arguments. To relax this constraint and to set +implicit all non strict implicit arguments by default, use the command: + +.. cmd:: Unset Strict Implicit. + +Conversely, use the command ``Set Strict Implicit`` to restore the +original mode that declares implicit only the strict implicit +arguments plus a small subset of the non strict implicit arguments. + +In the other way round, to capture exactly the strict implicit +arguments and no more than the strict implicit arguments, use the +command + +.. cmd:: Set Strongly Strict Implicit. + +Conversely, use the command ``Unset Strongly Strict Implicit`` to let the +option “Strict Implicit” decide what to do. + +Remark: In versions of |Coq| prior to version 8.0, the default was to +declare the strict implicit arguments as implicit. + +.. _controlling-contextual-implicit-args: + +Controlling contextual implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +By default, |Coq| does not automatically set implicit the contextual +implicit arguments. To tell |Coq| to infer also contextual implicit +argument, use command + +.. cmd:: Set Contextual Implicit. + +Conversely, use command ``Unset Contextual Implicit`` to unset the +contextual implicit mode. + +.. _controlling-rev-pattern-implicit-args: + +Controlling reversible-pattern implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +By default, |Coq| does not automatically set implicit the reversible-pattern +implicit arguments. To tell |Coq| to infer also reversible- +pattern implicit argument, use command + +.. cmd:: Set Reversible Pattern Implicit. + +Conversely, use command ``Unset Reversible Pattern Implicit`` to unset the +reversible-pattern implicit mode. + +.. _controlling-insertion-implicit-args: + +Controlling the insertion of implicit arguments not followed by explicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Implicit arguments can be declared to be automatically inserted when a +function is partially applied and the next argument of the function is +an implicit one. In case the implicit arguments are automatically +declared (with the command ``Set Implicit Arguments``), the command + +.. cmd:: Set Maximal Implicit Insertion. + +is used to tell to declare the implicit arguments with a maximal +insertion status. By default, automatically declared implicit +arguments are not declared to be insertable maximally. To restore the +default mode for maximal insertion, use the command + +.. cmd:: Unset Maximal Implicit Insertion. + +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 +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|. +This syntax extension is given in the following grammar: + +.. _explicit_app_grammar: + + .. productionlist:: explicit_apps + term : @ qualid term … `term` + : | @ qualid + : | qualid `argument` … `argument` + argument : `term` + : | (ident := `term`) + + Syntax for explicitly giving implicit arguments + +.. example:: (continued) + + .. coqtop:: all + + Check (p r1 (z:=c)). + + Check (p (x:=a) (y:=b) r1 (z:=c) r2). + + +Renaming implicit arguments +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Implicit arguments names can be redefined using the following syntax: + +.. cmd:: Arguments @qualid {* @name} : @rename. + +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. + +.. example:: (continued) + +.. coqtop:: all + + Arguments p [s t] _ [u] _: rename. + + Check (p r1 (u:=c)). + + Check (p (s:=a) (t:=b) r1 (u:=c) r2). + + Fail Arguments p [s t] _ [w] _ : assert. + +.. _displaying-implicit-args: + +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. + +Explicit displaying of implicit arguments for pretty-printing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +By default the basic pretty-printing rules hide the inferable implicit +arguments of an application. To force printing all implicit arguments, +use command + +.. cmd:: Set Printing Implicit. + +Conversely, to restore the hiding of implicit arguments, use command + +.. cmd:: Unset Printing Implicit. + +By default the basic pretty-printing rules display the implicit +arguments that are not detected as strict implicit arguments. This +“defensive” mode can quickly make the display cumbersome so this can +be deactivated by using the command + +.. cmd:: Unset Printing Implicit Defensive. + +Conversely, to force the display of non strict arguments, use command + +.. cmd:: Set Printing Implicit Defensive. + +See also: ``Set Printing All`` in :ref:`printing_constructions_full`. + +Interaction with subtyping +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When an implicit argument can be inferred from the type of more than +one of the other arguments, then only the type of the first of these +arguments is taken into account, and not an upper type of all of them. +As a consequence, the inference of the implicit argument of “=” fails +in + +.. coqtop:: all + + Fail Check nat = Prop. + +but succeeds in + +.. coqtop:: all + + Check Prop = nat. + + +Deactivation of implicit arguments for parsing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Use of implicit arguments can be deactivated by issuing the command: + +.. cmd:: Set Parsing Explicit. + +In this case, all arguments of constants, inductive types, +constructors, etc, including the arguments declared as implicit, have +to be given as if none arguments were implicit. By symmetry, this also +affects printing. To restore parsing and normal printing of implicit +arguments, use: + +.. cmd:: Unset Parsing Explicit. + +Canonical structures +~~~~~~~~~~~~~~~~~~~~ + +A canonical structure is an instance of a record/structure type that +can be used to solve unification problems involving a projection +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. + +Assume that `qualid` denotes an object ``(Build_struc`` |c_1| … |c_n| ``)`` in the +structure *struct* of which the fields are |x_1|, …, |x_n|. Assume that +`qualid` is declared as a canonical structure using the command + +.. cmd:: Canonical Structure @qualid. + +Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be +solved during the type-checking process, `qualid` is used as a solution. +Otherwise said, `qualid` is canonically used to extend the field |c_i| +into a complete structure built on |c_i|. + +Canonical structures are particularly useful when mixed with coercions +and strict implicit arguments. Here is an example. + +.. coqtop:: all + + Require Import Relations. + + Require Import EqNat. + + Set Implicit Arguments. + + Unset Strict Implicit. + + Structure Setoid : Type := {Carrier :> Set; Equal : relation Carrier; + Prf_equiv : equivalence Carrier Equal}. + + Definition is_law (A B:Setoid) (f:A -> B) := forall x y:A, Equal x y -> Equal (f x) (f y). + + Axiom eq_nat_equiv : equivalence nat eq_nat. + + Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. + + Canonical Structure nat_setoid. + +Thanks to ``nat_setoid`` declared as canonical, the implicit arguments ``A`` +and ``B`` can be synthesized in the next statement. + +.. coqtop:: all + + Lemma is_law_S : is_law S. + +Remark: If a same field occurs in several canonical structure, then +only the structure declared first as canonical is considered. + +.. cmdv:: Canonical Structure @ident := @term : @type. + +.. cmdv:: Canonical Structure @ident := @term. + +.. cmdv:: Canonical Structure @ident : @type := @term. + +These are equivalent to a regular definition of `ident` followed by the declaration +``Canonical Structure`` `ident`. + +See also: more examples in user contribution category (Rocq/ALGEBRA). + + +Print Canonical Projections. +++++++++++++++++++++++++++++ + +This displays the list of global names that are components of some +canonical structure. For each of them, the canonical structure of +which it is a projection is indicated. For instance, the above example +gives the following output: + +.. coqtop:: all + + Print Canonical Projections. + + +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 + +.. 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). + +.. example:: + + .. coqtop:: all + + Require Import List. + + Implicit Types m n : nat. + + Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m. + + intros m n. + + Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m. + +.. cmdv:: Implicit Type @ident : @type. + + This is useful for declaring the implicit type of a single variable. + +.. cmdv:: Implicit Types {+ ( {+ @ident } : @term ) } + + Adds blocks of implicit types with different specifications. + +.. _implicit-generalization: + +Implicit generalization +~~~~~~~~~~~~~~~~~~~~~~~ + +.. index:: `{ } +.. index:: `( ) + +Implicit generalization is an automatic elaboration of a statement +with free variables into a closed statement where these variables are +quantified explicitly. Implicit generalization is done inside binders +starting with a \` and terms delimited by \`{ } and \`( ), always +introducing maximally inserted implicit arguments for the generalized +variables. Inside implicit generalization delimiters, free variables +in the current context are automatically quantified using a product or +a lambda abstraction to generate a closed term. In the following +statement for example, the variables n and m are automatically +generalized and become explicit arguments of the lemma as we are using +\`( ): + +.. coqtop:: all + + Generalizable All Variables. + + Lemma nat_comm : `(n = n + 0). + +One can control the set of generalizable identifiers with +the ``Generalizable`` vernacular command to avoid unexpected +generalizations when mistyping identifiers. There are several commands +that specify which variables should be generalizable. + +.. cmd:: Generalizable All Variables. + + All variables are candidate for + generalization if they appear free in the context under a + generalization delimiter. This may result in confusing errors in case + of typos. In such cases, the context will probably contain some + unexpected generalized variable. + +.. cmd:: Generalizable No Variables. + + Disable implicit generalization entirely. This is the default behavior. + +.. cmd:: Generalizable (Variable | Variables) {+ @ident }. + + Allow generalization of the given identifiers only. Calling this command multiple times + adds to the allowed identifiers. + +.. cmd:: Global Generalizable. + + Allows exporting the choice of generalizable variables. + +One can also use implicit generalization for binders, in which case +the generalized variables are added as binders and set maximally +implicit. + +.. coqtop:: all + + Definition id `(x : A) : A := x. + + Print id. + +The generalizing binders \`{ } and \`( ) work similarly to their +explicit counterparts, only binding the generalized variables +implicitly, as maximally-inserted arguments. In these binders, the +binding name for the bound object is optional, whereas the type is +mandatory, dually to regular binders. + + +Coercions +--------- + +Coercions can be used to implicitly inject terms from one *class* in +which they reside into another one. A *class* is either a sort +(denoted by the keyword ``Sortclass``), a product type (denoted by the +keyword ``Funclass``), or a type constructor (denoted by its name), e.g. +an inductive type or any constant with a type of the form +``forall (`` |x_1| : |A_1| ) … ``(``\ |x_n| : |A_n|\ ``)``, `s` where `s` is a sort. + +Then the user is able to apply an object that is not a function, but +can be coerced to a function, and more generally to consider that a +term of type ``A`` is of type ``B`` provided that there is a declared coercion +between ``A`` and ``B``. The main command is + +.. cmd:: Coercion @qualid : @class >-> @class. + +which declares the construction denoted by qualid as a coercion +between the two given classes. + +More details and examples, and a description of the commands related +to coercions are provided in :ref:`implicitcoercions`. + +.. _printing_constructions_full: + +Printing constructions in full +------------------------------ + +Coercions, implicit arguments, the type of pattern-matching, but also +notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some +tactics (typically the tactics applying to occurrences of subterms are +sensitive to the implicit arguments). The command + +.. cmd:: Set Printing All. + +deactivates all high-level printing features such as coercions, +implicit arguments, returned type of pattern-matching, notations and +various syntactic sugar for pattern-matching or record projections. +Otherwise said, ``Set Printing All`` includes the effects of the commands +``Set Printing Implicit``, ``Set Printing Coercions``, ``Set Printing Synth``, +``Unset Printing Projections``, and ``Unset Printing Notations``. To reactivate +the high-level printing features, use the command + +.. cmd:: Unset Printing All. + +Printing universes +------------------ + +The following command: + +.. cmd:: Set Printing Universes. + +activates the display of the actual level of each occurrence of ``Type``. +See :ref:`TODO-4.1.1-sorts` for details. This wizard option, in combination +with ``Set Printing All`` (see :ref:`printing_constructions_full`) can help to diagnose failures +to unify terms apparently identical but internally different in the +Calculus of Inductive Constructions. To reactivate the display of the +actual level of the occurrences of Type, use + +.. cmd:: Unset Printing Universes. + +The constraints on the internal level of the occurrences of Type +(see :ref:`TODO-4.1.1-sorts`) can be printed using the command + +.. cmd:: Print {? Sorted} 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 also accepts an optional output filename: + +.. cmd:: Print {? Sorted} Universes @string. + +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``. + + +Existential variables +--------------------- + +|Coq| terms can include existential variables which represents unknown +subterms to eventually be replaced by actual subterms. + +Existential variables are generated in place of unsolvable implicit +arguments or “_” placeholders when using commands such as ``Check`` (see +Section :ref:`TODO-6.3.1-check`) or when using tactics such as ``refine`` (see Section +:ref:`TODO-8.2.3-refine`), as well as in place of unsolvable instances when using +tactics such that ``eapply`` (see Section :ref:`TODO-8.2.4-apply`). An existential +variable is defined in a context, which is the context of variables of +the placeholder which generated the existential variable, and a type, +which is the expected type of the placeholder. + +As a consequence of typing constraints, existential variables can be +duplicated in such a way that they possibly appear in different +contexts than their defining context. Thus, any occurrence of a given +existential variable comes with an instance of its original context. +In the simple case, when an existential variable denotes the +placeholder which generated it, or is used in the same context as the +one in which it was generated, the context is not displayed and the +existential variable is represented by “?” followed by an identifier. + +.. coqtop:: all + + Parameter identity : forall (X:Set), X -> X. + + Check identity _ _. + + Check identity _ (fun x => _). + +In the general case, when an existential variable ``?``\ `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. +The variables of the context of the existential variables which are +instantiated by themselves are not written, unless the flag ``Printing Existential Instances`` +is on (see Section :ref:`explicit-display-existentials`), and this is why an +existential variable used in the same context as its context of definition is written with no instance. + +.. coqtop:: all + + Check (fun x y => _) 0 1. + + Set Printing Existential Instances. + + Check (fun x y => _) 0 1. + +Existential variables can be named by the user upon creation using +the syntax ``?``\ `ident`. This is useful when the existential +variable needs to be explicitly handled later in the script (e.g. +with a named-goal selector, see :ref:`TODO-9.2-goal-selectors`). + +.. _explicit-display-existentials: + +Explicit displaying of existential instances for pretty-printing +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The command: + +.. cmd:: Set Printing Existential Instances. + +activates the full display of how the context of an existential +variable is instantiated at each of the occurrences of the existential +variable. + +To deactivate the full display of the instances of existential +variables, use + +.. cmd:: Unset Printing Existential Instances. + +Solving existential variables using tactics +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Instead of letting the unification engine try to solve an existential +variable by itself, one can also provide an explicit hole together +with a tactic to solve it. Using the syntax ``ltac:(``\ `tacexpr`\ ``)``, the user +can put a tactic anywhere a term is expected. The order of resolution +is not specified and is implementation-dependent. The inner tactic may +use any variable defined in its scope, including repeated alternations +between variables introduced by term binding as well as those +introduced by tactic binding. The expression `tacexpr` can be any tactic +expression as described in :ref:`thetacticlanguage`. + +.. coqtop:: all + + Definition foo (x : nat) : nat := ltac:(exact x). + +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:`TODO-8.9.7-implicit-automation`, except that the used +tactic is local to each hole instead of being declared globally. diff --git a/doc/sphinx/language/module-system.rst b/doc/sphinx/language/module-system.rst new file mode 100644 index 0000000000..e6a6736654 --- /dev/null +++ b/doc/sphinx/language/module-system.rst @@ -0,0 +1,459 @@ +.. include:: ../preamble.rst +.. include:: ../replaces.rst + +.. _themodulesystem: + +The Module System +================= + +The module system extends the Calculus of Inductive Constructions +providing a convenient way to structure large developments as well as +a means of massive abstraction. + + +Modules and module types +---------------------------- + +**Access path.** An access path is denoted by :math:`p` and can be +either a module variable :math:`X` or, if :math:`p′` is an access path +and :math:`id` an identifier, then :math:`p′.id` is an access path. + + +**Structure element.** A structure element is denoted by :math:`e` and +is either a definition of a constant, an assumption, a definition of +an inductive, a definition of a module, an alias of a module or a module +type abbreviation. + + +**Structure expression.** A structure expression is denoted by :math:`S` and can be: + ++ an access path :math:`p` ++ a plain structure :math:`\Struct~e ; … ; e~\End` ++ a functor :math:`\Functor(X:S)~S′`, where :math:`X` is a module variable, :math:`S` and :math:`S′` are + structure expressions ++ an application :math:`S~p`, where :math:`S` is a structure expression and :math:`p` an + access path ++ a refined structure :math:`S~\with~p := p`′ or :math:`S~\with~p := t:T` where :math:`S` is a + structure expression, :math:`p` and :math:`p′` are access paths, :math:`t` is a term and :math:`T` is + the type of :math:`t`. + +**Module definition.** A module definition is written :math:`\Mod{X}{S}{S'}` +and consists of a module variable :math:`X`, a module type +:math:`S` which can be any structure expression and optionally a +module implementation :math:`S′` which can be any structure expression +except a refined structure. + + +**Module alias.** A module alias is written :math:`\ModA{X}{p}` +and consists of a module variable :math:`X` and a module path +:math:`p`. + +**Module type abbreviation.** +A module type abbreviation is written :math:`\ModType{Y}{S}`, +where :math:`Y` is an identifier and :math:`S` is any structure +expression . + + +Typing Modules +------------------ + +In order to introduce the typing system we first slightly extend the syntactic +class of terms and environments given in section :ref:`The-terms`. The +environments, apart from definitions of constants and inductive types now also +hold any other structure elements. Terms, apart from variables, constants and +complex terms, include also access paths. + +We also need additional typing judgments: + + ++ :math:`\WFT{E}{S}`, denoting that a structure :math:`S` is well-formed, ++ :math:`\WTM{E}{p}{S}`, denoting that the module pointed by :math:`p` has type :math:`S` in + environment :math:`E`. ++ :math:`\WEV{E}{S}{\ovl{S}}`, denoting that a structure :math:`S` is evaluated to a + structure :math:`S` in weak head normal form. ++ :math:`\WS{E}{S_1}{S_2}` , denoting that a structure :math:`S_1` is a subtype of a + structure :math:`S_2`. ++ :math:`\WS{E}{e_1}{e_2}` , denoting that a structure element e_1 is more + precise than a structure element e_2. + +The rules for forming structures are the following: + +.. inference:: WF-STR + + \WF{E;E′}{} + ------------------------ + \WFT{E}{ \Struct~E′ ~\End} + +.. inference:: WF-FUN + + \WFT{E; \ModS{X}{S}}{ \ovl{S′} } + -------------------------- + \WFT{E}{ \Functor(X:S)~S′} + + +Evaluation of structures to weak head normal form: + +.. inference:: WEVAL-APP + + \begin{array}{c} + \WEV{E}{S}{\Functor(X:S_1 )~S_2}~~~~~\WEV{E}{S_1}{\ovl{S_1}} \\ + \WTM{E}{p}{S_3}~~~~~ \WS{E}{S_3}{\ovl{S_1}} + \end{array} + -------------------------- + \WEV{E}{S~p}{S_2 \{p/X,t_1 /p_1 .c_1 ,…,t_n /p_n.c_n \}} + + +In the last rule, :math:`\{t_1 /p_1 .c_1 ,…,t_n /p_n .c_n \}` is the resulting +substitution from the inlining mechanism. We substitute in :math:`S` the +inlined fields :math:`p_i .c_i` from :math:`\ModS{X}{S_1 }` by the corresponding delta- +reduced term :math:`t_i` in :math:`p`. + +.. inference:: WEVAL-WITH-MOD + + \begin{array}{c} + E[] ⊢ S \lra \Struct~e_1 ;…;e_i ; \ModS{X}{S_1 };e_{i+2} ;… ;e_n ~\End \\ + E;e_1 ;…;e_i [] ⊢ S_1 \lra \ovl{S_1} ~~~~~~ + E[] ⊢ p : S_2 \\ + E;e_1 ;…;e_i [] ⊢ S_2 <: \ovl{S_1} + \end{array} + ---------------------------------- + \begin{array}{c} + \WEV{E}{S~\with~x := p}{}\\ + \Struct~e_1 ;…;e_i ; \ModA{X}{p};e_{i+2} \{p/X\} ;…;e_n \{p/X\} ~\End + \end{array} + +.. inference:: WEVAL-WITH-MOD-REC + + \begin{array}{c} + \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1}{S_1 };e_{i+2} ;… ;e_n ~\End} \\ + \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}} + \end{array} + -------------------------- + \begin{array}{c} + \WEV{E}{S~\with~X_1.p := p_1}{} \\ + \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2}};e_{i+2} \{p_1 /X_1.p\} ;…;e_n \{p_1 /X_1.p\} ~\End + \end{array} + +.. inference:: WEVAL-WITH-DEF + + \begin{array}{c} + \WEV{E}{S}{\Struct~e_1 ;…;e_i ;\Assum{}{c}{T_1};e_{i+2} ;… ;e_n ~\End} \\ + \WS{E;e_1 ;…;e_i }{Def()(c:=t:T)}{\Assum{}{c}{T_1}} + \end{array} + -------------------------- + \begin{array}{c} + \WEV{E}{S~\with~c := t:T}{} \\ + \Struct~e_1 ;…;e_i ;Def()(c:=t:T);e_{i+2} ;… ;e_n ~\End + \end{array} + +.. inference:: WEVAL-WITH-DEF-REC + + \begin{array}{c} + \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1 }{S_1 };e_{i+2} ;… ;e_n ~\End} \\ + \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}} + \end{array} + -------------------------- + \begin{array}{c} + \WEV{E}{S~\with~X_1.p := t:T}{} \\ + \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2} };e_{i+2} ;… ;e_n ~\End + \end{array} + +.. inference:: WEVAL-PATH-MOD1 + + \begin{array}{c} + \WEV{E}{p}{\Struct~e_1 ;…;e_i ; \Mod{X}{S}{S_1};e_{i+2} ;… ;e_n End} \\ + \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}} + \end{array} + -------------------------- + E[] ⊢ p.X \lra \ovl{S} + +.. inference:: WEVAL-PATH-MOD2 + + \WF{E}{} + \Mod{X}{S}{S_1}∈ E + \WEV{E}{S}{\ovl{S}} + -------------------------- + \WEV{E}{X}{\ovl{S}} + +.. inference:: WEVAL-PATH-ALIAS1 + + \begin{array}{c} + \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModA{X}{p_1};e_{i+2} ;… ;e_n End} \\ + \WEV{E;e_1 ;…;e_i }{p_1}{\ovl{S}} + \end{array} + -------------------------- + \WEV{E}{p.X}{\ovl{S}} + +.. inference:: WEVAL-PATH-ALIAS2 + + \WF{E}{} + \ModA{X}{p_1 }∈ E + \WEV{E}{p_1}{\ovl{S}} + -------------------------- + \WEV{E}{X}{\ovl{S}} + +.. inference:: WEVAL-PATH-TYPE1 + + \begin{array}{c} + \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModType{Y}{S};e_{i+2} ;… ;e_n End} \\ + \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}} + \end{array} + -------------------------- + \WEV{E}{p.Y}{\ovl{S}} + +.. inference:: WEVAL-PATH-TYPE2 + + \WF{E}{} + \ModType{Y}{S}∈ E + \WEV{E}{S}{\ovl{S}} + -------------------------- + \WEV{E}{Y}{\ovl{S}} + + +Rules for typing module: + +.. inference:: MT-EVAL + + \WEV{E}{p}{\ovl{S}} + -------------------------- + E[] ⊢ p : \ovl{S} + +.. inference:: MT-STR + + E[] ⊢ p : S + -------------------------- + E[] ⊢ p : S/p + + +The last rule, called strengthening is used to make all module fields +manifestly equal to themselves. The notation :math:`S/p` has the following +meaning: + + ++ if :math:`S\lra~\Struct~e_1 ;…;e_n ~\End` then :math:`S/p=~\Struct~e_1 /p;…;e_n /p ~\End` + where :math:`e/p` is defined as follows (note that opaque definitions are processed + as assumptions): + + + :math:`\Def{}{c}{t}{T}/p = \Def{}{c}{t}{T}` + + :math:`\Assum{}{c}{U}/p = \Def{}{c}{p.c}{U}` + + :math:`\ModS{X}{S}/p = \ModA{X}{p.X}` + + :math:`\ModA{X}{p′}/p = \ModA{X}{p′}` + + :math:`\Ind{}{Γ_P}{Γ_C}{Γ_I}/p = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` + + :math:`\Indpstr{}{Γ_P}{Γ_C}{Γ_I}{p'}{p} = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'}` + ++ if :math:`S \lra \Functor(X:S′)~S″` then :math:`S/p=S` + + +The notation :math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` +denotes an inductive definition that is definitionally equal to the +inductive definition in the module denoted by the path :math:`p`. All rules +which have :math:`\Ind{}{Γ_P}{Γ_C}{Γ_I}` as premises are also valid for +:math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}`. We give the formation rule for +:math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` +below as well as the equality rules on inductive types and +constructors. + +The module subtyping rules: + +.. inference:: MSUB-STR + + \begin{array}{c} + \WS{E;e_1 ;…;e_n }{e_{σ(i)}}{e'_i ~\for~ i=1..m} \\ + σ : \{1… m\} → \{1… n\} ~\injective + \end{array} + -------------------------- + \WS{E}{\Struct~e_1 ;…;e_n ~\End}{~\Struct~e'_1 ;…;e'_m ~\End} + +.. inference:: MSUB-FUN + + \WS{E}{\ovl{S_1'}}{\ovl{S_1}} + \WS{E; \ModS{X}{S_1'}}{\ovl{S_2}}{\ovl{S_2'}} + -------------------------- + E[] ⊢ \Functor(X:S_1 ) S_2 <: \Functor(X:S_1') S_2' + + +Structure element subtyping rules: + +.. inference:: ASSUM-ASSUM + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + -------------------------- + \WS{E}{\Assum{}{c}{T_1 }}{\Assum{}{c}{T_2 }} + +.. inference:: DEF-ASSUM + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + -------------------------- + \WS{E}{\Def{}{c}{t}{T_1 }}{\Assum{}{c}{T_2 }} + +.. inference:: ASSUM-DEF + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + E[] ⊢ c =_{βδιζη} t_2 + -------------------------- + \WS{E}{\Assum{}{c}{T_1 }}{\Def{}{c}{t_2 }{T_2 }} + +.. inference:: DEF-DEF + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + E[] ⊢ t_1 =_{βδιζη} t_2 + -------------------------- + \WS{E}{\Def{}{c}{t_1 }{T_1 }}{\Def{}{c}{t_2 }{T_2 }} + +.. inference:: IND-IND + + E[] ⊢ Γ_P =_{βδιζη} Γ_P' + E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' + E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' + -------------------------- + \WS{E}{\ind{Γ_P}{Γ_C}{Γ_I}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}} + +.. inference:: INDP-IND + + E[] ⊢ Γ_P =_{βδιζη} Γ_P' + E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' + E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' + -------------------------- + \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}} + +.. inference:: INDP-INDP + + \begin{array}{c} + E[] ⊢ Γ_P =_{βδιζη} Γ_P' + E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' \\ + E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' + E[] ⊢ p =_{βδιζη} p' + \end{array} + -------------------------- + \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\Indp{}{Γ_P'}{Γ_C'}{Γ_I'}{p'}} + +.. inference:: MOD-MOD + + \WS{E}{S_1}{S_2} + -------------------------- + \WS{E}{\ModS{X}{S_1 }}{\ModS{X}{S_2 }} + +.. inference:: ALIAS-MOD + + E[] ⊢ p : S_1 + \WS{E}{S_1}{S_2} + -------------------------- + \WS{E}{\ModA{X}{p}}{\ModS{X}{S_2 }} + +.. inference:: MOD-ALIAS + + E[] ⊢ p : S_2 + \WS{E}{S_1}{S_2} + E[] ⊢ X =_{βδιζη} p + -------------------------- + \WS{E}{\ModS{X}{S_1 }}{\ModA{X}{p}} + +.. inference:: ALIAS-ALIAS + + E[] ⊢ p_1 =_{βδιζη} p_2 + -------------------------- + \WS{E}{\ModA{X}{p_1 }}{\ModA{X}{p_2 }} + +.. inference:: MODTYPE-MODTYPE + + \WS{E}{S_1}{S_2} + \WS{E}{S_2}{S_1} + -------------------------- + \WS{E}{\ModType{Y}{S_1 }}{\ModType{Y}{S_2 }} + + +New environment formation rules + + +.. inference:: WF-MOD1 + + \WF{E}{} + \WFT{E}{S} + -------------------------- + WF(E; \ModS{X}{S})[] + +.. inference:: WF-MOD2 + + \WS{E}{S_2}{S_1} + \WF{E}{} + \WFT{E}{S_1} + \WFT{E}{S_2} + -------------------------- + \WF{E; \Mod{X}{S_1}{S_2}}{} + +.. inference:: WF-ALIAS + + \WF{E}{} + E[] ⊢ p : S + -------------------------- + \WF{E, \ModA{X}{p}}{} + +.. inference:: WF-MODTYPE + + \WF{E}{} + \WFT{E}{S} + -------------------------- + \WF{E, \ModType{Y}{S}}{} + +.. inference:: WF-IND + + \begin{array}{c} + \WF{E;\ind{Γ_P}{Γ_C}{Γ_I}}{} \\ + E[] ⊢ p:~\Struct~e_1 ;…;e_n ;\ind{Γ_P'}{Γ_C'}{Γ_I'};… ~\End : \\ + E[] ⊢ \ind{Γ_P'}{Γ_C'}{Γ_I'} <: \ind{Γ_P}{Γ_C}{Γ_I} + \end{array} + -------------------------- + \WF{E; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p} }{} + + +Component access rules + + +.. inference:: ACC-TYPE1 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Assum{}{c}{T};… ~\End + -------------------------- + E[Γ] ⊢ p.c : T + +.. inference:: ACC-TYPE2 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{T};… ~\End + -------------------------- + E[Γ] ⊢ p.c : T + +Notice that the following rule extends the delta rule defined in section :ref:`Conversion-rules` + +.. inference:: ACC-DELTA + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{U};… ~\End + -------------------------- + E[Γ] ⊢ p.c \triangleright_δ t + +In the rules below we assume +:math:`Γ_P` is :math:`[p_1 :P_1 ;…;p_r :P_r ]`, +: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 ]`. + +.. inference:: ACC-IND1 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End + -------------------------- + E[Γ] ⊢ p.I_j : (p_1 :P_1 )…(p_r :P_r )A_j + +.. inference:: ACC-IND2 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End + -------------------------- + E[Γ] ⊢ p.c_m : (p_1 :P_1 )…(p_r :P_r )C_m I_j (I_j~p_1 …p_r )_{j=1… k} + +.. inference:: ACC-INDP1 + + E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End + -------------------------- + E[] ⊢ p.I_i \triangleright_δ p'.I_i + +.. inference:: ACC-INDP2 + + E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End + -------------------------- + E[] ⊢ p.c_i \triangleright_δ p'.c_i |