## Stream: Coq users

### Topic: Simplifying CoFixpoints

#### Rudy Peterson (Oct 11 2022 at 20:27):

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!

#### Pierre-Marie Pédrot (Oct 11 2022 at 20:33):

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

#### Pierre-Marie Pédrot (Oct 11 2022 at 20:34):

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

#### Pierre-Marie Pédrot (Oct 11 2022 at 20:36):

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

#### Pierre-Marie Pédrot (Oct 11 2022 at 20:37):

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.

#### Rudy Peterson (Oct 12 2022 at 00:29):

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

#### Karl Palmskog (Oct 12 2022 at 06:53):

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

#### Pierre Castéran (Oct 12 2022 at 08:09):

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

#### Pierre-Marie Pédrot (Oct 12 2022 at 08:11):

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

#### Pierre-Marie Pédrot (Oct 12 2022 at 08:11):

like this

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

#### Meven Lennon-Bertrand (Oct 12 2022 at 09:19):

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

#### Pierre Castéran (Oct 12 2022 at 16:34):

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

#### Karl Palmskog (Oct 12 2022 at 16:50):

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

#### Karl Palmskog (Oct 12 2022 at 16:53):

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

#### Karl Palmskog (Oct 12 2022 at 16:56):

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