Hi,

is the `under`

tactic supposed to work with setoid? I've been trying this

```
From mathcomp Require Import all_ssreflect.
Require Import Setoid.
Goal forall (A B : Prop), A /\ B -> B /\ A.
by move=> A B H; rewrite and_comm.
Qed.
Lemma all_equiv A (P Q : A -> Prop) :
(forall a, P a <-> Q a) -> (forall a, P a) <-> (forall a, Q a).
Proof. by move=> H; split=> H1 a; rewrite ?H // -H. Qed.
Goal forall (A B : nat -> Prop), (forall x, A x /\ B x) -> (forall x, B x /\ A x).
move=> A B H.
under all_equiv do rewrite and_comm.
```

```
```

We needed to add some extra Proper instances, and there was some discussion here

They seemed to work, but I don't think anybody was confident they wouldn't cause performance problems

Paolo Giarrusso said:

We needed to add some extra Proper instances, and there was some discussion here

where?

Great it works! I would like to make a PR but it is not clear to me where this new instance should be put.

I though about `ssrunder.v`

but this comment scared me :

```
(*
This preserves the following feature: we can use [Setoid] without
requiring [ssreflect] and use [ssreflect] without requiring [Setoid]. *)
```

I think I have code better than in the link...

This is the latest version https://github.com/bedrocksystems/BRiCk/blob/master/theories/prelude/under_rel_proper.v

Beware the bedrock license isn't compatible with math-comp's, I expect we'll relicense it but this needs an okay from @Gregory Malecha

It sounds like the right place for these tactics should eventually be https://github.com/coq/coq/blob/d8db2fd7e6df24d56160651d570603d935dac170/theories/ssr/ssrsetoid.v.

ok if @Gregory Malecha gives his ok, I will make a PR with his code.

the code is currently licensed under the usual Affero GPL-like license. This is a really cumbersome license to abide by. I hope "giving OK" means "relicensing under MathComp's license"

Why mathcomp? I was thinking to do a PR for Coq.

OK, but same story there, only different relicensing (to `LGPL-2.1-only`

)

@Karl Palmskog absolutely

Last updated: Jul 25 2024 at 16:02 UTC