## Stream: Coq users

#### Philip Zucker (Apr 04 2021 at 15:42):

I was playing with coinduction and I note that the manual https://coq.inria.fr/refman/language/core/coinductive.html says to not define coinductives by constructors and instead set primitive projections and use records. I don't really understand what the issue is, something to do with dependent pattern matching, but I believe it. Is this an issue that will expose itself even on simple types? If I guard the coinductive definition with a Thunk record am I ok then? Or even if that is ok in this exact case, is that idea playing with fire?

``````Set Primitive Projections.

CoInductive CoNat1 :=
| Suc : CoNat1 -> CoNat1
| Zero : CoNat1.

(* Manual suggestion basically *)
CoInductive CoNat2 := {
conat : option CoNat2
}.

(* Is this ok? *)
CoInductive Thunk a := thunk {
force : a
}.
Arguments thunk {a} force.
CoInductive CoNat3 :=
| Suc3 : Thunk CoNat3 -> CoNat3
| Zero3 : CoNat3.
``````

#### Li-yao (Apr 04 2021 at 17:36):

Yes, you can witness the death of subject reduction with any coinductive type that allows dependent pattern-matching (which primitive projections prevents), by equating a cofixpoint to its unfolding.

In this typical example, `bad3` reduces to an ill-typed `eq_refl` because the two sides of the equation are not convertible:

``````CoFixpoint w : CoNat3 :=
Suc3 (thunk w).

Lemma frob x : x = match x with Suc3 y => Suc3 y | Zero3 => Zero3 end.
Proof.
destruct x; reflexivity.
Qed.

Theorem bad3 : w = Suc3 (thunk w).
Proof.
apply frob.
Qed.
``````

#### Philip Zucker (Apr 04 2021 at 18:29):

Is that ill typed? Aren't both side of the equation `CoNat3`?

#### Philip Zucker (Apr 04 2021 at 18:31):

Naively that equation seems true since it was kind of the definition of `w`? This is unsound though?

#### Li-yao (Apr 04 2021 at 20:39):
They seem intuitively equal, but the type system actually doesn't equate `cofix f x := F x` and `F (cofix f x := F x)` (and idem with `fix`), it only does so in certain contexts.
It doesn't lead to unsoundness (i.e., you can't prove `False`), you can probably "fix" the subject reduction theorem by allowing types to change "up to bisimilarity", but that makes the metatheory of Coq quite more sophisticated, for little gain.