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`

?

As would've been possible if we had something like `a = b`

as an assumption.

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

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

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.

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.

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

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

IIRC it's derivable in cubical type theories

@Pierre-Marie Pédrot reference?

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

Last updated: Jun 18 2024 at 08:01 UTC