## Stream: Coq users

### Topic: `Proper ... (Under_rel ...)`

#### Paolo Giarrusso (Jul 21 2022 at 00:38):

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

#### Enrico Tassi (Jul 21 2022 at 18:14):

cc @Erik Martin-Dorel

#### Paolo Giarrusso (Jul 21 2022 at 18:35):

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

#### Cyril Cohen (Nov 22 2022 at 19:39):

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

#### Paolo Giarrusso (Nov 22 2022 at 21:08):

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...

#### Cyril Cohen (Nov 22 2022 at 21:54):

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

Last updated: Oct 04 2023 at 23:01 UTC