Why does the entire body of a cofix need to be guarded?

Using Coq
1

I’ve been trying to test my understanding of coinduction by defining “coinduction principles”. As expected, this one works:

CoInductive colist a :=
| conil : colist a
| cocons : a → colist a → colist a.

Definition colist_coind
           {a}
           {domain}
           (cases : domain →
                    unit + (a * domain))
  : domain → colist a :=
  cofix colist_coind x :=
    match cases x with
    | inl tt => conil _
    | inr (hd, tl) => cocons hd (colist_coind tl)
    end.

But this one doesn’t:

Fail Definition colist_coind
           {a}
           {domain}
           (f : ∀
                  (conil_case : colist a)
                  (cocons_case : a → domain → colist a),
                  domain → colist a)
  : domain → colist a :=
  cofix colist_coind x :=
    f
      (conil _)
      (λ hd tl, cocons hd (colist_coind tl))
      x.
(*
The command has indeed failed with message:
Recursive definition of colist_coind is ill-formed.
In environment
a : ?X10
domain : ?X11@{__:=a}
f : colist a → (a → domain → colist a) → domain → colist a
colist_coind : domain → colist a
x : domain
Sub-expression "f (conil a) (λ (hd : a) (tl : domain), cocons hd (colist_coind tl)) x" not in guarded form (should be
a constructor, an abstraction, a match, a cofix or a recursive call).
Recursive definition is: "λ x : domain, f (conil a) (λ (hd : a) (tl : domain), cocons hd (colist_coind tl)) x".
*)

If I understand the error message correctly, the problem is that the entire body of a cofix is expected to meet the “guarded” syntax condition. But in this case my corecursive call itself is indeed obviously guarded, so I’m not sure why this couldn’t be allowed. Is this coq being overly conservative or would allowing definitions like this possibly lead to inconsistency?

(For those who are curious, I prefer the second definition because it doesn’t require bringing in the otherwise unrelated sum and product types, and because it’s easier to make appropriately symmetric with the induction principle for inductive lists).

2

Found a workaround for now (obvious in retrospect), but still curious about my general question

Definition colist_coind
           {a}
           {domain}
           (f : ∀ T
                  (conil_case : T)
                  (cocons_case : a → domain → T),
                  domain → T)
  : domain → colist a :=
  cofix colist_coind x :=
    match f _ (inl tt) (λ hd tl, inr (hd, tl)) x with
    | inl tt => conil _
    | inr (hd, tl) => cocons hd (colist_coind tl)
    end.
3

Guess what the first element of the following colist would be equal to (for the obvious definition of tail : colist a -> colist a):

@colist_coind nat unit (fun _ cons _ => tail (cons 0 tt)) tt
1 Like
4

Right, thanks! My second version works because of parametricity I guess.