Hello!

I am new to coninductive data-types and I have been trying to prove a seemingly trivial fact about streams but I get stuck:

```
CoInductive stream := Stream : nat -> stream -> stream.
CoFixpoint stream_map (f : nat -> nat) (s : stream)
: stream :=
match s with
| Stream n s => Stream (f n) (stream_map f s)
end.
CoInductive stream_eq : stream -> stream -> Prop :=
| Stream_eq n s1 s2 :
stream_eq s1 s2 ->
stream_eq (Stream n s1) (Stream n s2).
Lemma stream_map_id : forall s,
stream_eq (stream_map (fun x => x) s) s.
Proof.
cofix C.
intros [n s].
compute.
Abort.
```

When I try to prove `stream_map_id`

I want `stream_map (fun x => x) (Stream n s)`

to simplify to `Stream n (stream_map (fun x => x) s)`

but I am not sure how to do that.

Thank you!

You're hitting right into an issue with positive coinductive types. The way you phrased stream_eq forces you to perform an eta-expansion, which is provable for positive streams but very unwieldy

here is the proof:

```
Lemma stream_eta : forall s : stream,
s = Stream (match s with Stream n s => n end) (match s with Stream n s => s end).
Proof.
intros s.
destruct s; reflexivity.
Qed.
Lemma stream_map_id : forall s,
stream_eq (stream_map (fun x => x) s) s.
Proof.
cofix C.
intros [n s].
match goal with [ |- stream_eq ?s _ ] => rewrite (stream_eta s) end.
simpl.
constructor.
apply C.
Qed.
```

A more natural definition is to perform the eta-expansion directly in the stream_eq definition like this:

```
CoInductive stream := Stream : nat -> stream -> stream.
CoFixpoint stream_map (f : nat -> nat) (s : stream)
: stream :=
match s with
| Stream n s => Stream (f n) (stream_map f s)
end.
Definition hd s := match s with Stream n _ => n end.
Definition tl s := match s with Stream _ s => s end.
CoInductive stream_eq : stream -> stream -> Prop :=
| Stream_eq s1 s2 : hd s1 = hd s2 -> stream_eq (tl s1) (tl s2) -> stream_eq s1 s2.
Lemma stream_map_id : forall s,
stream_eq (stream_map (fun x => x) s) s.
Proof.
cofix C.
intros [n s].
constructor; simpl.
+ reflexivity.
+ apply C.
Qed.
```

As a general rule of thumb, you should never write equalities (or indexed inductive types) over streams, because you'll face hard to prove statements, or even outright unprovable.

Thanks this is super helpful!

Is there a good alternative to writing equalities or inductive types over streams?

Thanks again.

there are two general approaches to using coinductive types which affects equality, see answer here: https://proofassistants.stackexchange.com/questions/583/what-is-the-state-of-coinductive-types-and-reasoning-in-coq

Is the approach using primitive projections also suitable for types like "finite or infinite lists" ?

You'll have to use a nested type, but yes.

like this

```
CoInductive colist (A : Type) := { node : option (A * colist A) }.
```

If you do not want to encode the functor "by hand" using sums and products, you can also do the following, which might be slightly nicer, as it lets you still use pattern-matching:

```
Variant list_fun (A : Type) (X : Type) :=
| nil : list_fun A X
| cons : A -> X -> list_fun A X.
Arguments cons {_ _}.
Arguments nil {_ _}.
CoInductive colist (A : Type) :=
{ node : list_fun A (colist A) }.
CoFixpoint ones : colist nat :=
{| node := cons 1 ones |}.
Arguments node {_}.
Definition head {A : Type} (l : colist A) : option A :=
match l.(node) with
| nil => None
| cons a _ => Some a
end.
```

Ups, I didn't find the negative equivalent of the definition (from the old tutorial) yet

```
CoInductive Infinite (A:Type) : colist A -> Prop :=
Lcons_inf : forall a l, Infinite A l -> Infinite A (LCons a l).
```

@Pierre Castéran see example by Li-yao here: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Where.20to.20learn.20about.20co.20induction/near/273537431

It gives a general recipe to convert positive coind types to negative ones.

a blogpost with some more examples (of coind negative style): https://blog.poisson.chat/posts/2021-10-26-proving-lists-infinite.html

my view: the usual way of writing the neg coind types is not at all user-friendly, we need ways to "compile" the usual equational-style coind definitions to the negative style

Last updated: Feb 06 2023 at 12:04 UTC