\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Coinductive types and corecursive functions¶

Coinductive 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. Coinductive 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 coinductive definitions can be found in [Gimenez95][Gimenez98][GimenezCasteran05].

Command CoInductive inductive_definition with inductive_definition*¶

Command CoInductive record_definition with record_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) and using attributes.

When record syntax is used, this command also supports the projections(primitive) attribute.

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 Top-level 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 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 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.

Co-recursive functions: cofix¶

term_cofix::=let cofix cofix_body in term|cofix cofix_body with cofix_body+ for ident?cofix_body::=ident binder* : type? := term

The expression "cofix ident₁ binder₁ : type₁ 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.

Top-level definitions of corecursive functions¶

Command CoFixpoint cofix_definition with cofix_definition*¶

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 by applying the following method to the number O (see Section Coinductive types for the definition of Stream, hd and tl):

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 of Seq. 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 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, the with 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 the refine tactic. In this case, the proof should be terminated with Defined in order to define a constant for which the computational behavior is relevant. See Entering and exiting proof mode.