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: Oct 13 2024 at 01:02 UTC