# Is induction over mutually inductive coinductive types possible?

You can encode ordinals in Coq as

Inductive ord := O | S (n: ord) | Lim (s: nat -> ord).

Suppose you use the following encoding instead

CoInductive stream A := {
tail: stream A ;
}.
Inductive ord := O | S (n: ord) | Sup (s: stream ord).

Can you make an induction principle go through?

I tried in both Coq and Agda but the obvious induction principle doesn't seem to work

{-# OPTIONS --guardedness #-}
module ord where

record stream (A : Set) : Set where
coinductive
constructor _::_
field
tail : stream A

record Forall {A : Set} (P : A → Set) (x : stream A) : Set where
coinductive
constructor _:>_
field
fortail : Forall P (stream.tail x)

data ord : Set where
o : ord
s : ord → ord
sup : stream ord → ord

open stream
open Forall

ind : (P : ord → Set) → P o → ((x : ord) → P x → P (s x)) → ((x : stream ord) → Forall P x → P (sup x)) → (x : ord) → P x
ind P onO onS onSup = loop where
loop : (x : ord) → P x
loop o = onO
loop (s x) = onS x (loop x)
loop (sup x) = onSup x (gen x) where
gen : (y : stream ord) → Forall P y
fortail (gen y) = gen (tail y)

(Agda termination checker complains about the recusive calls to gen and loop.)

It makes sense to want something like this, but Agda's termination/productivity checker does not actually validate this interpretation of the types. The reasoning behind your induction principle is presumably:

1. $$\mathsf{stream}\ A$$ is an infinitely long stream of whatever $$A$$ is.
2. $$\mathsf{ord}$$ is a well-founded tree that delegates to $$\mathsf{stream}$$ to achive an infinitely wide branching factor.

However, Agda accepts the following definition:

$$\mathsf{bad}$$ is not a well-founded tree, and contradicts the induction principle:

P : ord → Set
P zero = ⊤
P (suc o) = ⊤
P o@(lim s) = o ≡ head (tail s) → ⊥

lemma : ⊥
lemma =
ind P _ (λ _ _ → _)
(λ s fp eq → subst P (sym eq) (forhead (fortail fp)) eq)

The issue is that coinduction in Agda (and I suppose also Coq) does not really act in a 'compositional' way. You can't just say that $$\mathsf{ord}$$ is the initial algebra of the functor $$1 + o + \mathsf{stream}\ o$$; it actually has some more complicated specification owing to $$\mathsf{stream}$$ being defined coalgebraically.

There are some (not great) justifications you could use for this behavior. The above functor is not strictly covered by the more rigorous foundational schemas for (co)inductive definitions, so in that sense it requires some interpretation, and that interpretation could well be one that matches Agda's checker. Also, if the two types were mutually defined, it's a lot less clear whether it should mean something primarily algebraic or coalgebraic. But it's unfortunate that some mixed (co)inductive specifications just can't be written in Agda/Coq.

(Note, I'm not very familiar with coinduction in Coq; just assuming based on the question that it behaves similarly to Agda.)

Addendum: if you want to more reliably predict what definitions Agda will accept for types involving coinduction, it helps to imagine that they are actually picking out certain well-defined values of an analogous domain-theoretic definition (where coinduction is more 'lazy'). But even that is not completely straight forward. For instance, using