diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 186 | ||||
| -rw-r--r-- | doc/sphinx/language/core/coinductive.rst | 198 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 203 |
3 files changed, 587 insertions, 0 deletions
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst new file mode 100644 index 0000000000..9943e0aa76 --- /dev/null +++ b/doc/sphinx/language/core/assumptions.rst @@ -0,0 +1,186 @@ +Functions and assumptions +========================= + +.. _binders: + +Binders +------- + +.. insertprodn open_binders binder + +.. prodn:: + open_binders ::= {+ @name } : @term + | {+ @binder } + name ::= _ + | @ident + binder ::= @name + | ( {+ @name } : @type ) + | ( @name {? : @type } := @term ) + | @implicit_binders + | @generalizing_binder + | ( @name : @type %| @term ) + | ' @pattern0 + +Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix` +*bind* variables. A binding is represented by an identifier. If the binding +variable is not used in the expression, the identifier can be replaced by the +symbol :g:`_`. When the type of a bound variable cannot be synthesized by the +system, it can be specified with the notation :n:`(@ident : @type)`. There is also +a notation for a sequence of binding variables sharing the same type: +:n:`({+ @ident} : @type)`. A +binder can also be any pattern prefixed by a quote, e.g. :g:`'(x,y)`. + +Some constructions allow the binding of a variable to value. This is +called a “let-binder”. The entry :n:`@binder` of the grammar accepts +either an assumption binder as defined above or a let-binder. The notation in +the latter case is :n:`(@ident := @term)`. In a let-binder, only one +variable can be introduced at the same time. It is also possible to give +the type of the variable as follows: +:n:`(@ident : @type := @term)`. + +Lists of :n:`@binder`\s are allowed. In the case of :g:`fun` and :g:`forall`, +it is intended that at least one binder of the list is an assumption otherwise +fun and forall gets identical. Moreover, parentheses can be omitted in +the case of a single sequence of bindings sharing the same type (e.g.: +:g:`fun (x y z : A) => t` can be shortened in :g:`fun x y z : A => t`). + +.. index:: fun ... => ... + +Abstractions: fun +----------------- + +.. insertprodn term_forall_or_fun term_forall_or_fun + +.. prodn:: + term_forall_or_fun ::= forall @open_binders , @term + | fun @open_binders => @term + +The expression :n:`fun @ident : @type => @term` defines the +*abstraction* of the variable :n:`@ident`, of type :n:`@type`, over the term +:n:`@term`. It denotes a function of the variable :n:`@ident` that evaluates to +the expression :n:`@term` (e.g. :g:`fun x : A => x` denotes the identity +function on type :g:`A`). The keyword :g:`fun` can be followed by several +binders as given in Section :ref:`binders`. Functions over +several variables are equivalent to an iteration of one-variable +functions. For instance the expression +:n:`fun {+ @ident__i } : @type => @term` +denotes the same function as :n:`{+ fun @ident__i : @type => } @term`. If +a let-binder occurs in +the list of binders, it is expanded to a let-in definition (see +Section :ref:`let-in`). + +.. index:: forall + +Products: forall +---------------- + +The expression :n:`forall @ident : @type, @term` denotes the +*product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`. +As for abstractions, :g:`forall` is followed by a binder list, and products +over several variables are equivalent to an iteration of one-variable +products. Note that :n:`@term` is intended to be a type. + +If the variable :n:`@ident` occurs in :n:`@term`, the product is called +*dependent product*. The intention behind a dependent product +:g:`forall x : A, B` is twofold. It denotes either +the universal quantification of the variable :g:`x` of type :g:`A` +in the proposition :g:`B` or the functional dependent product from +:g:`A` to :g:`B` (a construction usually written +:math:`\Pi_{x:A}.B` in set theory). + +Non dependent product types have a special notation: :g:`A -> B` stands for +:g:`forall _ : A, B`. The *non dependent product* is used both to denote +the propositional implication and function types. + +Applications +------------ + +.. insertprodn term_application arg + +.. prodn:: + term_application ::= @term1 {+ @arg } + | @ @qualid_annotated {+ @term1 } + arg ::= ( @ident := @term ) + | @term1 + +:n:`@term__fun @term` denotes applying the function :n:`@term__fun` to :token:`term`. + +:n:`@term__fun {+ @term__i }` denotes applying +:n:`@term__fun` to the arguments :n:`@term__i`. It is +equivalent to :n:`( … ( @term__fun @term__1 ) … ) @term__n`: +associativity is to the left. + +The notation :n:`(@ident := @term)` for arguments is used for making +explicit the value of implicit arguments (see +Section :ref:`explicit-applications`). + +.. _gallina-assumptions: + +Assumptions +----------- + +Assumptions extend the environment with axioms, parameters, hypotheses +or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted +by Coq if and only if this :n:`@type` is a correct type in the environment +preexisting the declaration and if :n:`@ident` was not previously defined in +the same module. This :n:`@type` is considered to be the type (or +specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` +has type :n:`@type`. + +.. _Axiom: + +.. cmd:: @assumption_token {? Inline {? ( @num ) } } {| {+ ( @assumpt ) } | @assumpt } + :name: Axiom; Axioms; Conjecture; Conjectures; Hypothesis; Hypotheses; Parameter; Parameters; Variable; Variables + + .. insertprodn assumption_token of_type + + .. prodn:: + assumption_token ::= {| Axiom | Axioms } + | {| Conjecture | Conjectures } + | {| Parameter | Parameters } + | {| Hypothesis | Hypotheses } + | {| Variable | Variables } + assumpt ::= {+ @ident_decl } @of_type + ident_decl ::= @ident {? @univ_decl } + of_type ::= {| : | :> | :>> } @type + + These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in + the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence + of an object of this type) is accepted as a postulate. + + :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms + are equivalent. They can take the :attr:`local` :term:`attribute`, + which makes the defined :n:`@ident`\s accessible by :cmd:`Import` and its variants + only through their fully qualified names. + + Similarly, :cmd:`Hypothesis`, :cmd:`Variable` and their plural forms are equivalent. Outside + of a section, these are equivalent to :n:`Local Parameter`. Inside a section, the + :n:`@ident`\s defined are only accessible within the section. When the current section + is closed, the :n:`@ident`\(s) become undefined and every object depending on them will be explicitly + parameterized (i.e., the variables are *discharged*). See Section :ref:`section-mechanism`. + + The :n:`Inline` clause is only relevant inside functors. See :cmd:`Module`. + +.. example:: Simple assumptions + + .. coqtop:: reset in + + Parameter X Y : Set. + Parameter (R : X -> Y -> Prop) (S : Y -> X -> Prop). + Axiom R_S_inv : forall x y, R x y <-> S y x. + +.. exn:: @ident already exists. + :name: @ident already exists. (Axiom) + :undocumented: + +.. warn:: @ident is declared as a local axiom + + Warning generated when using :cmd:`Variable` or its equivalent + instead of :n:`Local Parameter` or its equivalent. + +.. note:: + We advise using the commands :cmd:`Axiom`, :cmd:`Conjecture` and + :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when + the assertion :n:`@type` is of sort :g:`Prop`), and to use the commands + :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases + (corresponding to the declaration of an abstract object of the given type). diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst new file mode 100644 index 0000000000..51860aec0d --- /dev/null +++ b/doc/sphinx/language/core/coinductive.rst @@ -0,0 +1,198 @@ +Co-inductive types and co-recursive functions +============================================= + +.. _coinductive-types: + +Co-inductive types +------------------ + +The objects of an inductive type are well-founded with respect to the +constructors of the type. In other words, such objects contain only a +*finite* number of constructors. Co-inductive types arise from relaxing +this condition, and admitting types whose objects contain an infinity of +constructors. Infinite objects are introduced by a non-ending (but +effective) process of construction, defined in terms of the constructors +of the type. + +.. cmd:: CoInductive @inductive_definition {* with @inductive_definition } + + This command introduces a co-inductive type. + The syntax of the command is the same as the command :cmd:`Inductive`. + No principle of induction is derived from the definition of a co-inductive + type, since such principles only make sense for inductive types. + For co-inductive types, the only elimination principle is case analysis. + + This command supports the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`universes(template)`, + :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, + :attr:`universes(noncumulative)` and :attr:`private(matching)` + attributes. + +.. example:: + + The type of infinite sequences of natural numbers, usually called streams, + is an example of a co-inductive type. + + .. coqtop:: in + + CoInductive Stream : Set := Seq : nat -> Stream -> Stream. + + The usual destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str` + can be defined as follows: + + .. coqtop:: in + + Definition hd (x:Stream) := let (a,s) := x in a. + Definition tl (x:Stream) := let (a,s) := x in s. + +Definitions of co-inductive predicates and blocks of mutually +co-inductive definitions are also allowed. + +.. example:: + + The extensional equality on streams is an example of a co-inductive type: + + .. coqtop:: in + + CoInductive EqSt : Stream -> Stream -> Prop := + eqst : forall s1 s2:Stream, + hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2. + + In order to prove the extensional equality of two streams :g:`s1` and :g:`s2` + we have to construct an infinite proof of equality, that is, an infinite + object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite + objects in Section :ref:`cofixpoint`. + +Caveat +~~~~~~ + +The ability to define co-inductive types by constructors, hereafter called +*positive co-inductive types*, is known to break subject reduction. The story is +a bit long: this is due to dependent pattern-matching which implies +propositional η-equality, which itself would require full η-conversion for +subject reduction to hold, but full η-conversion is not acceptable as it would +make type checking undecidable. + +Since the introduction of primitive records in Coq 8.5, an alternative +presentation is available, called *negative co-inductive types*. This consists +in defining a co-inductive type as a primitive record type through its +projections. Such a technique is akin to the *co-pattern* style that can be +found in e.g. Agda, and preserves subject reduction. + +The above example can be rewritten in the following way. + +.. coqtop:: none + + Reset Stream. + +.. coqtop:: all + + Set Primitive Projections. + CoInductive Stream : Set := Seq { hd : nat; tl : Stream }. + CoInductive EqSt (s1 s2: Stream) : Prop := eqst { + eqst_hd : hd s1 = hd s2; + eqst_tl : EqSt (tl s1) (tl s2); + }. + +Some properties that hold over positive streams are lost when going to the +negative presentation, typically when they imply equality over streams. +For instance, propositional η-equality is lost when going to the negative +presentation. It is nonetheless logically consistent to recover it through an +axiom. + +.. coqtop:: all + + Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s). + +More generally, as in the case of positive coinductive types, it is consistent +to further identify extensional equality of coinductive types with propositional +equality: + +.. coqtop:: all + + Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. + +As of Coq 8.9, it is now advised to use negative co-inductive types rather than +their positive counterparts. + +.. seealso:: + :ref:`primitive_projections` for more information about negative + records and primitive projections. + +.. index:: + single: cofix + +Co-recursive functions: cofix +----------------------------- + +.. insertprodn term_cofix cofix_body + +.. prodn:: + term_cofix ::= let cofix @cofix_body in @term + | cofix @cofix_body {? {+ with @cofix_body } for @ident } + cofix_body ::= @ident {* @binder } {? : @type } := @term + +The expression +":n:`cofix @ident__1 @binder__1 : @type__1 with … with @ident__n @binder__n : @type__n for @ident__i`" +denotes the :math:`i`-th component of a block of terms defined by a mutual guarded +co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When +:math:`n=1`, the ":n:`for @ident__i`" clause is omitted. + +.. _cofixpoint: + +Top-level definitions of co-recursive functions +----------------------------------------------- + +.. cmd:: CoFixpoint @cofix_definition {* with @cofix_definition } + + .. insertprodn cofix_definition cofix_definition + + .. prodn:: + cofix_definition ::= @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations } + + This command introduces a method for constructing an infinite object of a + coinductive type. For example, the stream containing all natural numbers can + be introduced applying the following method to the number :g:`O` (see + Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd` + and :g:`tl`): + + .. coqtop:: all + + CoFixpoint from (n:nat) : Stream := Seq n (from (S n)). + + Unlike recursive definitions, there is no decreasing argument in a + co-recursive definition. To be admissible, a method of construction must + provide at least one extra constructor of the infinite object for each + iteration. A syntactical guard condition is imposed on co-recursive + definitions in order to ensure this: each recursive call in the + definition must be protected by at least one constructor, and only by + constructors. That is the case in the former definition, where the single + recursive call of :g:`from` is guarded by an application of :g:`Seq`. + On the contrary, the following recursive function does not satisfy the + guard condition: + + .. coqtop:: all + + Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream := + if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s). + + The elimination of co-recursive definition is done lazily, i.e. the + definition is expanded only when it occurs at the head of an application + which is the argument of a case analysis expression. In any other + context, it is considered as a canonical expression which is completely + evaluated. We can test this using the command :cmd:`Eval`, which computes + the normal forms of a term: + + .. coqtop:: all + + Eval compute in (from 0). + Eval compute in (hd (from 0)). + Eval compute in (tl (from 0)). + + As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously + defining several mutual cofixpoints. + + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. + In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant + for which the computational behavior is relevant. See :ref:`proof-editing-mode`. diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst new file mode 100644 index 0000000000..679022a5b1 --- /dev/null +++ b/doc/sphinx/language/core/definitions.rst @@ -0,0 +1,203 @@ +Definitions +=========== + +.. index:: let ... := ... (term) + +.. _let-in: + +Let-in definitions +------------------ + +.. insertprodn term_let term_let + +.. prodn:: + term_let ::= let @name {? : @type } := @term in @term + | let @name {+ @binder } {? : @type } := @term in @term + | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term + | let ' @pattern := @term {? return @term100 } in @term + | let ' @pattern in @pattern := @term return @term100 in @term + +:n:`let @ident := @term in @term’` +denotes the local binding of :n:`@term` to the variable +:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in +definition of functions: :n:`let @ident {+ @binder} := @term in @term’` +stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. + +.. index:: + single: ... : ... (type cast) + single: ... <: ... + single: ... <<: ... + +Type cast +--------- + +.. insertprodn term_cast term_cast + +.. prodn:: + term_cast ::= @term10 <: @term + | @term10 <<: @term + | @term10 : @term + | @term10 :> + +The expression :n:`@term : @type` is a type cast expression. It enforces +the type of :n:`@term` to be :n:`@type`. + +:n:`@term <: @type` locally sets up the virtual machine for checking that +:n:`@term` has type :n:`@type`. + +:n:`@term <<: @type` uses native compilation for checking that :n:`@term` +has type :n:`@type`. + +.. _gallina-definitions: + +Top-level definitions +--------------------- + +Definitions extend the environment with associations of names to terms. +A definition can be seen as a way to give a meaning to a name or as a +way to abbreviate a term. In any case, the name can later be replaced at +any time by its definition. + +The operation of unfolding a name into its definition is called +:math:`\delta`-conversion (see Section :ref:`delta-reduction`). A +definition is accepted by the system if and only if the defined term is +well-typed in the current context of the definition and if the name is +not already used. The name defined by the definition is called a +*constant* and the term it refers to is its *body*. A definition has a +type which is the type of its body. + +A formal presentation of constants and environments is given in +Section :ref:`typing-rules`. + +.. cmd:: {| Definition | Example } @ident_decl @def_body + :name: Definition; Example + + .. insertprodn def_body def_body + + .. prodn:: + def_body ::= {* @binder } {? : @type } := {? @reduce } @term + | {* @binder } : @type + + These commands bind :n:`@term` to the name :n:`@ident` in the environment, + provided that :n:`@term` is well-typed. They can take the :attr:`local` :term:`attribute`, + which makes the defined :n:`@ident` accessible by :cmd:`Import` and its variants + only through their fully qualified names. + If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified + computation on :n:`@term`. + + These commands also support the :attr:`universes(polymorphic)`, + :attr:`universes(monomorphic)`, :attr:`program` and + :attr:`canonical` attributes. + + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. + In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant + for which the computational behavior is relevant. See :ref:`proof-editing-mode`. + + The form :n:`Definition @ident : @type := @term` checks that the type of :n:`@term` + is definitionally equal to :n:`@type`, and registers :n:`@ident` as being of type + :n:`@type`, and bound to value :n:`@term`. + + The form :n:`Definition @ident {* @binder } : @type := @term` is equivalent to + :n:`Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`. + + .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. + + .. exn:: @ident already exists. + :name: @ident already exists. (Definition) + :undocumented: + + .. exn:: The term @term has type @type while it is expected to have type @type'. + :undocumented: + +.. _Assertions: + +Assertions and proofs +--------------------- + +An assertion states a proposition (or a type) of which the proof (or an +inhabitant of the type) is interactively built using tactics. The interactive +proof mode is described in Chapter :ref:`proofhandling` and the tactics in +Chapter :ref:`Tactics`. The basic assertion command is: + +.. cmd:: @thm_token @ident_decl {* @binder } : @type {* with @ident_decl {* @binder } : @type } + :name: Theorem; Lemma; Fact; Remark; Corollary; Proposition; Property + + .. insertprodn thm_token thm_token + + .. prodn:: + thm_token ::= Theorem + | Lemma + | Fact + | Remark + | Corollary + | Proposition + | Property + + After the statement is asserted, Coq needs a proof. Once a proof of + :n:`@type` under the assumptions represented by :n:`@binder`\s is given and + validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and + the theorem is bound to the name :n:`@ident` in the environment. + + Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction + over a mutually inductive assumption, or that assert mutually dependent + statements in some mutual co-inductive type. It is equivalent to + :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of + the statements (or the body of the specification, depending on the point of + view). The inductive or co-inductive types on which the induction or + coinduction has to be done is assumed to be non ambiguous and is guessed by + the system. + + Like in a :cmd:`Fixpoint` or :cmd:`CoFixpoint` definition, the induction hypotheses + have to be used on *structurally smaller* arguments (for a :cmd:`Fixpoint`) or + be *guarded by a constructor* (for a :cmd:`CoFixpoint`). The verification that + recursive proof arguments are correct is done only at the time of registering + the lemma in the environment. To know if the use of induction hypotheses is + correct at some time of the interactive development of a proof, use the + command :cmd:`Guarded`. + + .. exn:: The term @term has type @type which should be Set, Prop or Type. + :undocumented: + + .. exn:: @ident already exists. + :name: @ident already exists. (Theorem) + + The name you provided is already defined. You have then to choose + another name. + + .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on. + + You are asserting a new statement while already being in proof editing mode. + This feature, called nested proofs, is disabled by default. + To activate it, turn the :flag:`Nested Proofs Allowed` flag on. + +Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode +until the proof is completed. In proof editing mode, the user primarily enters +tactics, which are described in chapter :ref:`Tactics`. The user may also enter +commands to manage the proof editing mode. They are described in Chapter +:ref:`proofhandling`. + +When the proof is complete, use the :cmd:`Qed` command so the kernel verifies +the proof and adds it to the environment. + +.. note:: + + #. Several statements can be simultaneously asserted provided the + :flag:`Nested Proofs Allowed` flag was turned on. + + #. Not only other assertions but any vernacular command can be given + while in the process of proving a given assertion. In this case, the + command is understood as if it would have been given before the + statements still to be proved. Nonetheless, this practice is discouraged + and may stop working in future versions. + + #. Proofs ended by :cmd:`Qed` are declared opaque. Their content cannot be + unfolded (see :ref:`performingcomputations`), thus + realizing some form of *proof-irrelevance*. To be able to unfold a + proof, the proof should be ended by :cmd:`Defined`. + + #. :cmd:`Proof` is recommended but can currently be omitted. On the opposite + side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof. + + #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the + current asserted statement into an axiom and exit the proof editing mode. |