## Stream: Coq users

### Topic: ✔ CoInductive equality

#### Julin S (Jun 23 2022 at 07:48):

Given two values of a coinductive type, is it possible to have a function determining whether they represent they are equal?

Like `Stream` from https://coq.inria.fr/stdlib/Coq.Lists.Streams.html.

Is a function like

``````Definition strm_eq {A:Type} (a b:Stream A) : bool := ..
``````

possible?

#### James Wood (Jun 23 2022 at 08:09):

No. From `strm_eq`, you can solve the halting problem. The idea is that for each Turing machine with each input, there's a stream representing its trace. You can then do some transformations on this trace so that the machine (not) halting is equivalent to the stream being all 0s.

#### Yannick Zakowski (Jun 23 2022 at 08:15):

The closest you could do, assuming decidable equality on `A`, is basically semi-deciding if they are different via a function in the delay monad, i.e. of type: `Definition strm_eq (a b : Stream A) : Delay bool.`. Fixing `A` to nat, something of this style:

``````From Coq Require Import Arith.
Set Primitive Projections.
CoInductive stream := cons { hd: nat; tl: stream }.

Variant step (R : Type) := | Error | Next (r : R).
CoInductive delay := go { next: step delay }.
Notation different := (go (@Error delay)).
Notation "'wait' x" := (go (@Next delay x)) (at level 20).

Definition str_eq : stream -> stream -> delay :=
cofix F (s t : stream) : delay :=
if hd s =? hd t
then wait (F (tl s) (tl t))
else different.
``````

Thanks!

#### Notification Bot (Jun 25 2022 at 07:08):

Julin S has marked this topic as resolved.

Last updated: Sep 26 2023 at 11:01 UTC