Proper instance for "nested" matching

Question

I have a Lemma of the form FnEquivInner f g implies outer t (bind t f) === outer t (bind t g) (full example posted below).

I wish to understand what kind of Proper instance I need to write for outer that lets me perform a rewrite in this case, to replace f with g in the call of outer.

In general, how does one write Proper instances where the patterns are non-trivial?

Require Import Setoid.
Require Import Morphisms.

Section PROPERINSTANCE.

  Variable T: Type.
  Variable inner:  T -> (T -> T) -> T.
  Variable outer : T -> (T -> T)  -> T.
  Variable bind: T -> (T -> T) -> (T -> T).

  Variable equiv: T -> T -> Prop.
  Infix "===" := equiv (at level 50).

  Variable equivalence_equiv: Equivalence equiv.

  (** Check that equivalence can be found by Coq *)
  Lemma check_equiv_refl: forall (t: T), t === t.
    reflexivity.
  Qed.

  Definition FnEquivInner (f g: T -> T): Prop := forall (t: T),
      inner t f === inner t g.

  (** This is a part of my theory *)
  Variable FnEquivOuter:
    forall (f g: T -> T)
      (t t1: T)
      (EQUIVINNER: FnEquivInner f g),
      outer t1 (bind t f) === outer t1 (bind t g).

  (** This is not a made up example to push coq, I have an actual theorem like this:
   * https://github.com/bollu/vellvm/blob/master/src/coq/Memory.v#L923
     inner = memEffect
     outer = memD
     bind = bindM
   *)


  Lemma useFnEquivOuter:
    forall (f g: T -> T)
      (t: T)
      (EQUIVINNER: FnEquivInner f g),
      outer t (bind t f) === outer t (bind t g).
  Proof.
    intros.
    (** What should the Proper instance look like so that if I have a FnEquivInner witness,
  I can `rewrite` using it? *)
    setoid_rewrite EQUIVINNER.
  Qed.

End PROPERINSTANCE.

Answer 1

If you Set Typeclasses Debug. and then try setoid_rewrite EQUIVINNER, and look for the lines that include looking for which come immediately before lines that mention proper_subrelation, you will see

Debug: 1.1-1: looking for (Proper (?R ==> FnEquivInner ==> ?r) bind) with backtracking
Debug: 1.1-1.2-2.1-1: looking for (Proper (?R --> FnEquivInner --> Basics.flip ?r) bind) with backtracking
Debug: 1.3-2.1-1: looking for (Proper (FnEquivInner --> Basics.flip ?r) (bind t)) with backtracking

This is basically a list of the Proper instances you can add to make typeclass resolution for setoid_rewrite go through.

For example, if I write

Global Instance: Proper (eq ==> FnEquivInner ==> eq) bind. Admitted.

then setoid_rewrite goes through.

I assume, though, that you will want something like

Global Instance bind_Proper : Proper (eq ==> FnEquivInner ==> FnEquivInner) bind. Admitted.

If I write this, then setoid_rewrite fails. Let's dig through the typeclass log again, this time looking for where resolution goes wrong after applying bind_Proper. Following the same rule as above, we see that the first line matching the above criterion is

Debug: 2.1-1: looking for (Proper (?R ==> FnEquivInner ==> ?r) outer) with backtracking

If I add

Global Instance outer_Proper: Proper (eq ==> FnEquivInner ==> equiv) outer. Admitted.

then setoid_rewrite again goes through.

Note that you get to fill in ?-prefixed relations (?R, ?r, etc) with any reflexive relation you'd like.

---

You may ask "why does this black magic work?" The answer is that proper_subrelation is where Coq generally goes wrong. It means, roughly, "I have nothing in my database matching what you're looking for; let me blindly try everything in my database and see if any of them are maybe close enough to work."* (Where "close enough" means "is a subrelation of".) So we look for the places where Coq goes wrong in its search, and we look immediately before that to see what it was looking at. (There are often many steps of partial_application_tactic, which strips arguments off of functions; this is why you only need one Proper instance for bind, rather than one for bind t and another for fun t => bind t f.)

*This is actually useful, sometimes, because eq is a subrelation of every reflexive relation, and so you can get away with not entering relations when you can just use eq. But most of the time, proper_subrelation is not what you want.