Indexed Coinductive Types · Coq users

I'd like to define an indexed coinductive types using the "copattern" negative style.

However, when I define, for instance:
CoInductive foo: nat -> Type := {}.
I get an (unhelpful) "Sort expected" error.

Is it possible to use indices in conjunction with copattern style coinductive types?

Kenji Maillard (Mar 04 2021 at 13:27):

Is it really an indexed family of types that you want to define ? If so at which index would you want to inhabit your family ?
Otherwise if your observations are defined at any index n : nat then you can probably parametrize by nat instead, eg

CoInductive foo (n : nat) : Type := {}.

Kenji Maillard (Mar 04 2021 at 13:39):

Looking at the doc I would really be surprised if negative indexed coinductive were really supported by Coq. It's still possible (but bothersome) to encode them with fordism, for instance:

CoInductive foo (n : nat) : Type :=
  { on_zero : n = 0 -> bool ; on_suc : forall m, n = S m -> nat }.

Definition on_z : foo 0 -> bool := fun x => on_zero _ x eq_refl.
Definition on_s {n} : foo (S n) -> nat := fun x => on_suc _ x _ eq_refl.

Klaus Ostermann (Mar 04 2021 at 13:47):

Thanks, Kenji. Unfortunately your workaround doesn't work in my situation because I need to define mutually dependent indexed coinductive types and it turns out that - for reasons I don't understand - all the types need to have exactly the same parameters (but they can have different indices).

Ali Caglayan (Mar 05 2021 at 00:01):

Ali Caglayan (Mar 05 2021 at 00:02):

In summary, mutual inductive types need to have the same arguments for no good reason other than its just the way it is implemented.

Kenji Maillard (Mar 05 2021 at 08:54):

I'm not sure it is of much help in practice because the encoding is heavy, but you can go around this limitation on uniformity of parameters using telescopes depending on some indexing type. Here is a (contrived) example with 3 indexed negative coinductive types with different sets of indices:

Set Primitive Projections.

Inductive index := T1 | T2 | T3.

Definition param_type (i : index) :=
  match i with
  | T1 => nat
  | T2 => bool
  | T3 => (nat * bool)%type
  end.

Definition getTy1 {i : index} : i = T1 -> param_type i -> nat :=
  match i as i return i = T1 -> param_type i -> nat with
  | T1 => fun _ x => x
  | T2 => ltac:(discriminate)
  | T3 => ltac:(discriminate)
  end.

Definition getTy2 {i : index} : i = T2 -> param_type i -> bool :=
  match i as i return i = T2 -> param_type i -> bool with
  | T2 => fun _ x => x
  | T1 => ltac:(discriminate)
  | T3 => ltac:(discriminate)
  end.

Definition getTy31 {i : index} : i = T3 -> param_type i -> nat :=
  match i as i return i = T3 -> param_type i -> nat with
  | T3 => fun _ x => fst x
  | T1 => ltac:(discriminate)
  | T2 => ltac:(discriminate)
  end.

Definition getTy32 {i : index} : i = T3 -> param_type i -> bool :=
  match i as i return i = T3 -> param_type i -> bool with
  | T3 => fun _ x => snd x
  | T1 => ltac:(discriminate)
  | T2 => ltac:(discriminate)
  end.

CoInductive foo1 (i : index) (p : param_type i) : Type :=
  { on_zero : forall (h : i = T1), getTy1 h p = 0 -> bool ;
    on_suc : forall (h : i = T1) m, getTy1 h p = S m -> foo1 T1 m }

with foo2 (i : index) (p : param_type i) : Type :=
  { on_true : forall (h : i = T2), getTy2 h p = true -> foo1 T1 5 }

with foo3 (i : index) (p : param_type i) : Type :=
  { on_one : forall (h : i = T3), getTy31 h p = 1 -> foo2 T2 (getTy32 h p)}.

It would be a good exercise to try to support these definitions in Coq using one of the metaprogramming frameworks (like MetaCoq or Elpi) to derive all that boilerplate generically from something closer to

foo1 : nat -> Type
foo2 : bool -> Type
foo3 : nat -> bool -> Type

.on_zero : foo1 0 -> bool
.on_suc : foo1 (S n) -> foo1 n

.on_true : foo2 true -> foo1 5

.on_one : foo3 1 b -> foo2 b

Stream: Coq users