Co-inductive types and co-recursive functions¶
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.
More information on co-inductive definitions can be found in [Gimenez95][Gimenez98][GimenezCasteran05].
-
Command
CoInductive inductive_definition with inductive_definition*
¶ This command introduces a co-inductive type. The syntax of the command is the same as the command
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
universes(polymorphic)
,universes(monomorphic)
,universes(template)
,universes(notemplate)
,universes(cumulative)
,universes(noncumulative)
andprivate(matching)
attributes.
Example
The type of infinite sequences of natural numbers, usually called streams, is an example of a co-inductive type.
- CoInductive Stream : Set := Seq : nat -> Stream -> Stream.
- Stream is defined
The usual destructors on streams hd:Stream->nat
and tl:Str->Str
can be defined as follows:
- Definition hd (x:Stream) := let (a,s) := x in a.
- hd is defined
- Definition tl (x:Stream) := let (a,s) := x in s.
- tl is defined
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:
- CoInductive EqSt : Stream -> Stream -> Prop := eqst : forall s1 s2:Stream, hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
- EqSt is defined
In order to prove the extensional equality of two streams s1
and s2
we have to construct an infinite proof of equality, that is, an infinite
object of type (EqSt s1 s2)
. We will see how to introduce infinite
objects in Section Top-level definitions of co-recursive functions.
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.
- Reset Stream.
- Set Primitive Projections.
- CoInductive Stream : Set := Seq { hd : nat; tl : Stream }.
- Stream is defined hd is defined tl is defined
- CoInductive EqSt (s1 s2: Stream) : Prop := eqst { eqst_hd : hd s1 = hd s2; eqst_tl : EqSt (tl s1) (tl s2); }.
- EqSt is defined eqst_hd is defined eqst_tl is defined
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.
- Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s).
- Stream_eta is declared
More generally, as in the case of positive coinductive types, it is consistent to further identify extensional equality of coinductive types with propositional equality:
- Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2.
- Stream_ext is declared
As of Coq 8.9, it is now advised to use negative co-inductive types rather than their positive counterparts.
See also
Primitive Projections for more information about negative records and primitive projections.
Co-recursive functions: cofix¶
The expression
"cofix ident1 binder1 : type1 with … with identn bindern : typen for identi
"
denotes the \(i\)-th component of a block of terms defined by a mutual guarded
co-recursion. It is the local counterpart of the CoFixpoint
command. When
\(n=1\), the "for identi
" clause is omitted.
Top-level definitions of co-recursive functions¶
-
Command
CoFixpoint cofix_definition with cofix_definition*
¶ 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
O
(see Section Co-inductive types for the definition ofStream
,hd
andtl
):- CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
- from is defined from is corecursively defined
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
from
is guarded by an application ofSeq
. On the contrary, the following recursive function does not satisfy the guard condition:- 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 command has indeed failed with message: Recursive definition of filter is ill-formed. In environment filter : (nat -> bool) -> Stream -> Stream p : nat -> bool s : Stream Unguarded recursive call in "filter p (tl s)". Recursive definition is: "fun (p : nat -> bool) (s : Stream) => if p (hd s) then {| hd := hd s; tl := 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
Eval
, which computes the normal forms of a term:- Eval compute in (from 0).
- = (cofix from (n : nat) : Stream := {| hd := n; tl := from (S n) |}) 0 : Stream
- Eval compute in (hd (from 0)).
- = 0 : nat
- Eval compute in (tl (from 0)).
- = (cofix from (n : nat) : Stream := {| hd := n; tl := from (S n) |}) 1 : Stream
As in the
Fixpoint
command, thewith
clause allows simultaneously defining several mutual cofixpoints.If
term
is omitted,type
is required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on therefine
tactic. In this case, the proof should be terminated withDefined
in order to define a constant for which the computational behavior is relevant. See Entering and leaving proof editing mode.