Stream: Coq users

Topic: ✔ CoInductive equality


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julin S (Jun 25 2022 at 07:08):

Thanks!

view this post on Zulip Notification Bot (Jun 25 2022 at 07:08):

Julin S has marked this topic as resolved.


Last updated: Jun 18 2024 at 07:01 UTC