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?

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 := {}.
```

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.
```

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).

Could it be related to: https://stackoverflow.com/questions/17308978/why-must-coq-mutually-inductive-types-have-the-same-parameters

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

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
```

Last updated: Jun 25 2024 at 15:02 UTC