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: Apr 19 2024 at 10:02 UTC