setoid_rewrite failed with MathClasses Coq

Question

I have been trying to solve the following for quite a moment now.

Require Import
  Coq.Classes.Morphisms
  MathClasses.interfaces.abstract_algebra
  MathClasses.interfaces.vectorspace
  MathClasses.misc.workaround_tactics
  MathClasses.theory.setoids
  MathClasses.theory.groups.

Lemma f_equiv' `{Equiv A} `{f : A -> A} :
  f = f -> forall x y, x = y -> f x = f y.
Proof.
  intros.
  f_equiv.
  assumption.
Qed.

Goal forall `{HVS : VectorSpace K V}, forall α : K, α · mon_unit = mon_unit.
Proof.
  intros.
  setoid_rewrite <- right_identity at 1.
  setoid_rewrite <- right_inverse with (x := α · mon_unit) at 2 3.
  setoid_rewrite associativity.
  apply @f_equiv' with (f := fun v => v & - (α · mon_unit)).
  { cbv; intros ?? Hxy; now rewrite Hxy. }
  setoid_rewrite <- distribute_l.
  setoid_rewrite left_identity. (* Error: setoid rewrite failed *)

As written in the last line, the setoid_rewrite fails with this error message :

Error: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X6739==[K V Ke Kplus Kmult Kzero Kone Knegate Krecip Ve Vop Vunit Vnegate
           sm HVS α |- relation V] (internal placeholder) {?r}
 ?X6740==[K V Ke Kplus Kmult Kzero Kone Knegate Krecip Ve Vop Vunit Vnegate
           sm HVS α (do_subrelation:=do_subrelation)
           |- Proper (equiv ==> ?r) (scalar_mult α)] (internal placeholder) {?p}
 ?X6840==[K V Ke Kplus Kmult Kzero Kone Knegate Krecip Ve Vop Vunit Vnegate
           sm HVS α |- relation V] (internal placeholder) {?r0}
 ?X6841==[K V Ke Kplus Kmult Kzero Kone Knegate Krecip Ve Vop Vunit Vnegate
           sm HVS α (do_subrelation:=do_subrelation)
           |- Proper (?r ==> ?r0 ==> flip impl) equiv] (internal placeholder) {?p0}
 ?X6842==[K V Ke Kplus Kmult Kzero Kone Knegate Krecip Ve Vop Vunit Vnegate
           sm HVS α |- ProperProxy ?r0 (α · mon_unit)] (internal placeholder) {?p1}
TYPECLASSES:?X6739 ?X6740 ?X6840 ?X6841 ?X6842
SHELF:||
FUTURE GOALS STACK:?X6842 ?X6841 ?X6840 ?X6740 ?X6739 ?X6611 ?X6610 ?X6609
?X6608 ?X6607 ?X6606 ?X6605||?X64 ?X62 ?X60 ?X58 ?X57 ?X56 ?X55 ?X54 ?X53
?X52 ?X51 ?X50 ?X49 ?X48 ?X47 ?X46 ?X45 ?X44 ?X43 ?X42

I have tried changing notations, using cbv, as suggested in this question.

How can I use the left_identity lemma without the error appearing ?

Answer 1

I'm not an expert in the details of how the unification with the implicit variables works, so I can't explain why the rewrite fails, but I've encountered it enough to at least give a "hack" solution.

Before the final "rewrite left_identity", do a

pose proof scalar_mult_proper.

As the context now contains a proof saying that it is ok to rewrite "under" scalar multiplication that the rewrite tactic is able to use, you can now finish the proof as expected with

rewrite left_identity.
reflexivity.

(Btw, you don't need the f_equiv' lemma, for this proof, simple rewriting is enough.)

To me the problem you encountered is a problem that I run into now and then. To me it is a usability-bug, or perhaps a bug in my expectation of how the instance resolution works, and I would also love a mechanistic explanation of this behaviour.

---

Some background for those who didn't paste the code into a Coq session to see what happens:

The goal just before the rewrite that fails is

α · (mon_unit & mon_unit) = α · mon_unit

Here "=" is notation for equiv which is Ve in this context (which is the equality relation for vectors), and · is notation for scalar_mult, and & is notation for the semigroup operation, i.e. vector addition in this case. And we want to rewrite one of the arguments of scalar_mult inside the equiv relation. Therefore we need instances of type Proper that enables this. These instances already exist. In particular we have

scalar_mult_proper
 : Proper (equiv ==> equiv ==> equiv) sm

which I found with Search Proper scalar_mult. To use this instance we need a lot of implicit variables to be filled in. Here is the full list:

Print scalar_mult_proper.
scalar_mult_proper = 
λ (R M : Type) (Re : Equiv R) (Rplus : Plus R) (Rmult : Mult R) 
  (Rzero : Zero R) (Rone : One R) (Rnegate : Negate R) 
  (Me : Equiv M) (Mop : SgOp M) (Munit : MonUnit M) 
  (Mnegate : Negate M) (sm : ScalarMult R M) (Module0 : Module R M),
  let (_, _, _, _, _, _, scalar_mult_proper) := Module0 in scalar_mult_proper
     : ∀ (R M : Type) (Re : Equiv R) (Rplus : Plus R) 
         (Rmult : Mult R) (Rzero : Zero R) (Rone : One R) 
         (Rnegate : Negate R) (Me : Equiv M) (Mop : SgOp M) 
         (Munit : MonUnit M) (Mnegate : Negate M) 
         (sm : ScalarMult R M),
         Module R M → Proper (equiv ==> equiv ==> equiv) sm

Almost all of those values should be filled in automatically, but for some reason the setoid_rewrite fails to do that by itself.

However, when I just add a copy of this rule to the context with pose, then the implicit variables are filled in, and the setoid_rewrite can use the rule without getting confused about what values should be used for R M Rplus Rnegate Me Module and all the other the arguments to scalar_mult_proper.