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.
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)
it also assumes you use stdpp’s
Equiv typeclass, but you might be able to adapt its Ltac1 implementation to your needs, or use
I’ll have a look. That
congruence knows about injectivity of constructors is also something which’d be useful, depending on context.
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