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 `Equiv`

:-)

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: Jun 15 2024 at 08:01 UTC