Coinductive types and corecursive functions¶
Coinductive types¶
The objects of an inductive type are wellfounded with respect to the constructors of the type. In other words, such objects contain only a finite number of constructors. Coinductive types arise from relaxing this condition, and admitting types whose objects contain an infinity of constructors. Infinite objects are introduced by a nonending (but effective) process of construction, defined in terms of the constructors of the type.
More information on coinductive definitions can be found in [Gimenez95][Gimenez98][GimenezCasteran05].

Command
CoInductive inductive_definition with inductive_definition*
¶ This command introduces a coinductive type. The syntax of the command is the same as the command
Inductive
. No principle of induction is derived from the definition of a coinductive type, since such principles only make sense for inductive types. For coinductive types, the only elimination principle is case analysis.This command supports the
universes(polymorphic)
,universes(template)
,universes(cumulative)
,private(matching)
,bypass_check(universes)
,bypass_check(positivity)
, andusing
attributes.
Example
The type of infinite sequences of natural numbers, usually called streams, is an example of a coinductive 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 coinductive predicates and blocks of mutually coinductive definitions are also allowed.
Example
The extensional equality on streams is an example of a coinductive 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 Toplevel definitions of corecursive functions.
Caveat¶
The ability to define coinductive types by constructors, hereafter called positive coinductive types, is known to break subject reduction. The story is a bit long: this is due to dependent patternmatching 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 coinductive types. This consists in defining a coinductive type as a primitive record type through its projections. Such a technique is akin to the copattern 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 coinductive types rather than their positive counterparts.
See also
Primitive Projections for more information about negative records and primitive projections.
Corecursive functions: cofix¶
The expression
"cofix ident_{1} binder_{1} : type_{1} with … with ident_{n} binder_{n} : type_{n} for ident_{i}
"
denotes the \(i\)th component of a block of terms defined by a mutual guarded
corecursion. It is the local counterpart of the CoFixpoint
command. When
\(n=1\), the "for ident_{i}
" clause is omitted.
Toplevel definitions of corecursive 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 Coinductive 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 corecursive 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 corecursive 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 illformed. 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 corecursive 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 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 exiting proof mode.