Is induction over mutually inductive coinductive types possible?

Question

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 := {
  head: 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
    head : A
    tail : stream A

record Forall {A : Set} (P : A → Set) (x : stream A) : Set where
  coinductive
  constructor _:>_
  field
    forhead : P (stream.head x)
    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
    forhead (gen y) = loop (head y)
    fortail (gen y) = gen (tail y)

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

Answer 1

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:

bad : ord
bads : stream ord

bad = lim λ where
  .head → zero
  .tail → bads

bads .head = bad
bads .tail = bads

$\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)
    bad refl

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

bad = lim bads

above would be rejected.