What does the error message "setoid rewrite failed: UNDEFINED EVARS" mean?

Question

I've seen this kind of error a good deal recently:

Error:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X1700==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H c
           intermediate H0 |- relation M] (internal placeholder) {?r}
 ?X1701==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H c
           intermediate H0 (do_subrelation:=do_subrelation)
           |- Proper
                (equiv ==>
                 ?X1700@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero;
                         __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit;
                         __:=Mnegate; __:=sm; __:=H; __:=c; __:=intermediate;
                         __:=H0}) (sm c)] (internal placeholder) {?p}
 ?X1705==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H c
           intermediate H0 |- relation M] (internal placeholder) {?r0}
 ?X1706==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H c
           intermediate H0 |- relation M] (internal placeholder) {?r1}
 ?X1707==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H c
           intermediate H0 (do_subrelation:=do_subrelation)
           |- Proper
                (?X1700@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero;
                         __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit;
                         __:=Mnegate; __:=sm; __:=H; __:=c; __:=intermediate;
                         __:=H0} ==>
                 ?X1706@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero;
                         __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit;
                         __:=Mnegate; __:=sm; __:=H; __:=c; __:=intermediate;
                         __:=H0} ==>
                 ?X1705@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero;
                         __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit;
                         __:=Mnegate; __:=sm; __:=H; __:=c; __:=intermediate;
                         __:=H0}) sg_op] (internal placeholder) {?p0}
 ?X1708==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H c
           intermediate H0
           |- ProperProxy
                ?X1706@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero;
                        __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit;
                        __:=Mnegate; __:=sm; __:=H; __:=c; __:=intermediate;
                        __:=H0} (- sm c mon_unit)] (internal placeholder) {?p1}
 ?X1710==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H c
           intermediate H0 |- relation M] (internal placeholder) {?r2}
 ?X1711==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H c
           intermediate H0 (do_subrelation:=do_subrelation)
           |- Proper
                (?X1705@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero;
                         __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit;
                         __:=Mnegate; __:=sm; __:=H; __:=c; __:=intermediate;
                         __:=H0} ==>
                 ?X1710@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero;
                         __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit;
                         __:=Mnegate; __:=sm; __:=H; __:=c; __:=intermediate;
                         __:=H0} ==> flip impl) equiv] (internal placeholder) {?p2}
 ?X1712==[R M Re Rplus Rmult Rzero Rone Rnegate Me Mop Munit Mnegate sm H c
           intermediate H0
           |- ProperProxy
                ?X1710@{__:=R; __:=M; __:=Re; __:=Rplus; __:=Rmult; __:=Rzero;
                        __:=Rone; __:=Rnegate; __:=Me; __:=Mop; __:=Munit;
                        __:=Mnegate; __:=sm; __:=H; __:=c; __:=intermediate;
                        __:=H0} mon_unit] (internal placeholder) {?p3}
.

What is this error trying to tell me? For reference, I most recently saw this during my work on the following lemma:

From MathClasses.interfaces Require Import
  abstract_algebra vectorspace canonical_names.
From MathClasses.theory Require Import groups.
Lemma mult_munit `{Module R M} : forall c : R, sm c mon_unit = mon_unit.
  intros.
  rewrite <- right_identity.
  assert (intermediate : mon_unit = sm c mon_unit & - sm c mon_unit).
  {
    rewrite right_inverse; reflexivity.
  }
  rewrite intermediate at 2.
  rewrite associativity.
  rewrite <- distribute_l.
  assert (forall x y : M, x = y -> x & sm c mon_unit = y & sm c mon_unit).
  {
    intros.
    rewrite H0.
    reflexivity.
  }
  rewrite right_identity.

I often see this while working on proofs with the math-classes library.

Answer 1

As it turns out, this is a strange quirk indeed: the answer lies in the fact that the Proper instance I used only referenced sm explicitly, without using the dot notation (·). When I change it to the notation that Anton used above, it works just fine. I will make a pull request to math-classes promptly.

Edit: A good explanation was provided on this github issue: https://github.com/c-corn/corn/issues/35

Answer 2

The error message gives us a hint: |- Proper (equiv ==> ....

The rewrite fails because the scalar_mult function (its notation is ·) lacks one very important property: it is not Proper. A Proper function is a function which respects equivalence -- remember everything in the Math-Classes library is defined up to equivalence, even = is a notation for equiv, not eq. More formally, a (unary) function f is proper if for any equivalent x and x' (x = x' in Math-Classes parlance), images of x and x' are equivalent too: f x = f x'.

We need this Proper property to be able to rewrite x to x' when x is not a "free-standing" variable, but f is applied to it.

One way to fix the error is to add an additional field to the definition of Module typeclass:

sm_proper   :> Proper ((=) ==> (=) ==> (=)) (·)

The above says that (·) is a binary function, which respects equivalence for both of its parameters.

Like this

Class Module (R M : Type)
  {Re Rplus Rmult Rzero Rone Rnegate}
  {Me Mop Munit Mnegate}
  {sm : ScalarMult R M}
:=
  { lm_ring     :>> @Ring R Re Rplus Rmult Rzero Rone Rnegate
  ; lm_group    :>> @AbGroup M Me Mop Munit Mnegate
  ; lm_distr_l  :> LeftHeteroDistribute (·) (&) (&)
  ; lm_distr_r  :> RightHeteroDistribute (·) (+) (&)
  ; lm_assoc    :> HeteroAssociative (·) (·) (·) (.*.)
  ; lm_identity :> LeftIdentity (·) 1
  ; sm_proper   :> Proper ((=) ==> (=) ==> (=)) (·)       (* new! *)
  }.

E.g. SemiGroup has an analogous field for &:

Class SemiGroup {Aop: SgOp A} : Prop :=
  { sg_setoid :> Setoid A
  ; sg_ass :> Associative (&)
  ; sg_op_proper :> Proper ((=) ==> (=) ==> (=)) (&) }.

After that amendment everything should work:

Lemma mult_munit `{Module R M} :
  forall c : R, c · mon_unit = mon_unit.
Proof.
  intro c.
  rewrite <- right_identity.
  assert (intermediate : mon_unit = c · mon_unit & - (c · mon_unit)) by
    now rewrite right_inverse.
  rewrite intermediate at 2.
  rewrite associativity.
  rewrite <- distribute_l.
  rewrite right_identity.
  apply right_inverse.
Qed.

I have to add there is another way to prove the lemma, but Coq somehow can't find an instance of LeftCancellation typeclass without a nudge (obviously this law holds in every group and MathClasses.theory.groups is imported):

  intro c.
  enough ((c · mon_unit) & (c · mon_unit) = c · mon_unit & mon_unit).
  apply (left_cancellation (&)) in H0.
  assumption.
  Print Instances LeftCancellation.   (* ! *)
  apply LeftCancellation_instance_0.  (* this is ugly, but Coq doesn't use this instance, defined in MathClasses.theory.groups *)
  rewrite <- distribute_l.
  now rewrite !right_identity.

Here is the full development to play with:

From MathClasses.interfaces
Require Import abstract_algebra orders.
From MathClasses.theory
Require Import groups.

(** Scalar multiplication function class *)
Class ScalarMult K V := scalar_mult: K → V → V.
Instance: Params (@scalar_mult) 3.

Infix "·" := scalar_mult (at level 50) : mc_scope.
Notation "(·)" := scalar_mult (only parsing) : mc_scope.
Notation "( x ·)" := (scalar_mult x) (only parsing) : mc_scope.
Notation "(· x )" := (λ y, y · x) (only parsing) : mc_scope.

(** The inproduct function class *)
Class Inproduct K V := inprod : V → V → K.
Instance: Params (@inprod) 3.

Notation "⟨ u , v ⟩" := (inprod u v) (at level 51) : mc_scope.
Notation "⟨ u , ⟩" := (λ v, ⟨u,v⟩) (at level 50, only parsing) : mc_scope.
Notation "⟨ , v ⟩" := (λ u, ⟨u,v⟩) (at level 50, only parsing) : mc_scope.
Notation "x ⊥ y" := (⟨x,y⟩ = 0) (at level 70) : mc_scope.

(** The norm function class *)
Class Norm K V := norm : V → K.
Instance: Params (@norm) 2.

Notation "∥ L ∥" := (norm L) (at level 50) : mc_scope.
Notation "∥·∥" := norm (only parsing) : mc_scope.

(** Let [M] be an R-Module. *)
Class Module (R M : Type)
  {Re Rplus Rmult Rzero Rone Rnegate}
  {Me Mop Munit Mnegate}
  {sm : ScalarMult R M}
:=
  { lm_ring     :>> @Ring R Re Rplus Rmult Rzero Rone Rnegate
  ; lm_group    :>> @AbGroup M Me Mop Munit Mnegate
  ; lm_distr_l  :> LeftHeteroDistribute (·) (&) (&)
  ; lm_distr_r  :> RightHeteroDistribute (·) (+) (&)
  ; lm_assoc    :> HeteroAssociative (·) (·) (·) (.*.)
  ; lm_identity :> LeftIdentity (·) 1
  ; sm_proper   :> Proper ((=) ==> (=) ==> (=)) (·)
  }.

Lemma mult_munit `{Module R M} :
  forall c : R, c · mon_unit = mon_unit.
Proof.
  intro c.
  rewrite <- right_identity.
  assert (intermediate : mon_unit = c · mon_unit & - (c · mon_unit)) by
    now rewrite right_inverse.
  rewrite intermediate at 2.
  rewrite associativity.
  rewrite <- distribute_l.
  rewrite right_identity.
  apply right_inverse.

  (* alternative proof, which doesn't quite work *)
  Restart.
  intro c.
  enough ((c · mon_unit) & (c · mon_unit) = c · mon_unit & mon_unit).
  apply (left_cancellation (&)) in H0.
  assumption.
  Print Instances LeftCancellation.
  apply LeftCancellation_instance_0.
  rewrite <- distribute_l.
  now rewrite !right_identity.
Qed.