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.
(* Bad? *)
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.
```

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.
```

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

?

Naively that equation seems true since it was kind of the definition of `w`

? This is unsound though?

Ah I guess the comments here are addressing exactly this https://www.joachim-breitner.de/blog/726-Coinduction_in_Coq_and_Isabelle

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.

Last updated: May 18 2024 at 10:02 UTC