Stream: Coq users

Topic: CoInduction advice

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.

(* 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.

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?

Philip Zucker (Apr 04 2021 at 18:35):

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

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.

Last updated: Oct 13 2024 at 01:02 UTC