Stream: Coq users

Topic: Congruence for setoids

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.

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)

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 :-)

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.

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: Sep 23 2023 at 08:01 UTC