A colleague ended up needing a `Proper`

instance for ssreflect's `Under_rel`

— let's say:

```
#[global] Instance Proper_under T (R : relation T)
`{!Symmetric R} `{!Transitive R} :
Proper (R ==> eq ==> iff) (Under_rel T R).
```

but it's not clear to me that this instance is generally the right one, and whether it is sufficient or it'd require too many variations to maintain.

It's not clear how to nest `under`

, with or without this instance, and whether we're missing something, or this scenario is indeed too hard to support properly?

A full example:

```
Require Import iris.prelude.prelude.
#[global] Instance Proper_under T (R : relation T)
`{!Symmetric R} `{!Transitive R} :
Proper (R ==> eq ==> iff) (Under_rel T R).
Proof.
move=> x y Heq ? _ <-.
rewrite Under_relE.
have ? : RewriteRelation R by [].
by split; rewrite Heq.
Qed.
Axiom T : Type.
#[global] Declare Instance equiv_t : Equiv T.
#[global] Declare Instance equiv_Equivalence : Equivalence (@equiv T _).
Axiom f : T -> T -> T.
Axiom binder : forall {A}, (A -> T) -> T.
Axiom law : forall x y, f x y ≡ f y x.
#[global] Declare Instance proper_binder {A} :
Proper (pointwise_relation A equiv ==> equiv) binder.
Goal forall x, binder (fun y => f x y) ≡
binder (fun y => f y x).
Proof.
move => >.
under proper_binder => y do rewrite law.
done.
Qed.
Goal binder (fun x => binder (fun y => f x y)) ≡
binder (fun x => binder (fun y => f y x)).
Proof.
under proper_binder => x.
{ under proper_binder => y do
rewrite law.
over.
}
reflexivity.
Qed.
```

cc @Erik Martin-Dorel

by now I got rid of the symmetry assumption so I can't name specific problems with this instance

I recall we added something similar with @Erik Martin-Dorel and it caused loops somewhere in the proof search, but I cannot remember where...

With Coq 8.16, adding `Global Hint Mode Reflexive ! ! : typeclass_instances`

fixes some performance issues with setoid rewriting, so there's a chance things got better. Either way, it's useful to confirm these scenarios aren't properly supported...

Maybe you could PR this to Coq and see if it has a performance impact in mathcomp projects?

Last updated: Jun 24 2024 at 00:02 UTC