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.

Julin S (Jun 25 2022 at 07:08):

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