\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \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}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \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{\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}\]

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) and private(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.

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 co-recursion. It is the local counterpart of the CoFixpoint command. When $n=1$, the "for ident_i" clause is omitted.

Top-level definitions of co-recursive 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 applying the following method to the number O (see Section Co-inductive 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 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 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 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, the with 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 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 leaving proof editing mode.