Stream: Coq users

Topic: Congruence for setoids


view this post on Zulip Stéphane Desarzens (Jul 05 2021 at 15:01):

Is there some way to use congruence with setoid-equality?
What I’d like:

Variable (A : Type) (equiv : A -> A -> Prop) (H : Equivalence equiv).
Goal (forall x y z : A, equiv x y -> ~ equiv y z -> ~ equiv x z).
  setoid_congruence equiv.

Explicitly specifying which equivalence to use is probably necessary.

view this post on Zulip Paolo Giarrusso (Jul 06 2021 at 15:35):

congruence does much more than you need here, since it knows that constructors are injective; I’ve seen setoid_subst in stdpp, and it could be enough for your goal (tho I’ve never used it, and it looks like it could be very slow)

view this post on Zulip Paolo Giarrusso (Jul 06 2021 at 15:36):

it also assumes you use stdpp’s Equiv typeclass, but you might be able to adapt its Ltac1 implementation to your needs, or use Equiv :-)

view this post on Zulip Stéphane Desarzens (Jul 06 2021 at 15:55):

I’ll have a look. That congruence knows about injectivity of constructors is also something which’d be useful, depending on context.

view this post on Zulip Paolo Giarrusso (Jul 06 2021 at 16:16):

Then you'd need to use something like stdpp's Inj typeclass, but that's not in the stdlib, and performance might be a concern.


Last updated: Jan 29 2023 at 01:02 UTC