Stream: Coq users

Topic: Can we rewrite using this type


view this post on Zulip Julin S (Nov 05 2022 at 06:56):

I have got a type that can be used to prove the equivalence of two stream objects:

Require Import Streams.

CoInductive EqSt {A:Type} (s1 s2: Stream A) : Prop :=
| eqst : hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.

Suppose I prove Eqst a b for some a b:Stream A.

Is it possible to rewrite occurrences of a in a goal with b?

view this post on Zulip Julin S (Nov 05 2022 at 06:56):

As would've been possible if we had something like a = b as an assumption.

view this post on Zulip Pierre Castéran (Nov 05 2022 at 08:32):

You would be able to prove some kind of "stream extensionality" , like forall A (s1 s2 : Stream A), EqSt s1 s2 -> s1 = s2.

I'm not sure about the status of this proposition : not provable, but may be safely added as an axiom ?

Note that the question was asked in https://cs.stackexchange.com/questions/63197/is-extensionality-for-coinductive-datatypes-consistent-with-coqs-logic

view this post on Zulip James Wood (Nov 07 2022 at 09:13):

I'm fairly sure the last comment is correct, and thus it's consistent if univalence is.

view this post on Zulip Pierre-Marie Pédrot (Nov 07 2022 at 09:29):

IIRC it's derivable in cubical type theories, but not in CIC + univalence. In any case it's true in the Set model so it's safe.

view this post on Zulip Pierre-Marie Pédrot (Nov 07 2022 at 09:29):

Regarding @Julin S 's original question, rather than adding an axiom you could use the setoid rewriting mechanism, which was designed precisely for this kind of use case.

view this post on Zulip Pierre-Marie Pédrot (Nov 07 2022 at 09:30):

It's both quite unwieldy and inefficient at scale, but it's the best we have currently.

view this post on Zulip Pierre-Marie Pédrot (Nov 07 2022 at 09:31):

see https://coq.inria.fr/refman/addendum/generalized-rewriting.html for more details

view this post on Zulip Ali Caglayan (Nov 08 2022 at 23:59):

IIRC it's derivable in cubical type theories

@Pierre-Marie Pédrot reference?

view this post on Zulip Pierre-Marie Pédrot (Nov 09 2022 at 07:52):

at least it's derivable in Cubical Agda: https://github.com/agda/cubical/blob/6320f583a7850f99fae3189ee6c2379d9899fd63/Cubical/Codata/Stream/Properties.agda#L85


Last updated: Jan 28 2023 at 06:30 UTC