Julin S (Nov 05 2022 at 06:56): 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?
Julin S (Nov 05 2022 at 06:56):As would've been possible if we had something like a = b as an assumption.
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
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.
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.
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.
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.
Pierre-Marie Pédrot (Nov 07 2022 at 09:31):see https://coq.inria.fr/refman/addendum/generalized-rewriting.html for more details
Ali Caglayan (Nov 08 2022 at 23:59):IIRC it's derivable in cubical type theories
@Pierre-Marie Pédrot reference?
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: Oct 13 2024 at 01:02 UTC