错误信息“setoid rewrite failed：UNDEFINED EVARS”是什么意思？

Question

我最近看到这种错误的一个很好的协议：

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} 
. 

这是什么错误想告诉我？作为参考，我最近我对下面的引理工作中看到了这一点：

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. 

我经常会看到这样同时用数学类图书馆证明工作。

Answer 1

事实证明，这是一个奇怪的怪癖实在：答案就在于一个事实，即Proper比如我用过唯一引用sm明确，不使用点符号（·）。当我将其更改为Anton使用的符号时，它工作得很好。我会及时向数学课进行拉取请求。

编辑：一个很好的解释提供了关于这个问题的GitHub：https://github.com/c-corn/corn/issues/35

Answer 2

错误消息给我们一个提示： |- Proper (equiv ==> ...。

重写失败，因为scalar_mult功能（它的符号是·）缺少一个非常重要的特性：它是不Proper。 A Proper函数是一个尊重等价的函数 - 记住数学类库中的所有内容都被定义为等价，即使=是equiv的符号，而不是eq。 更正式地，一个（一元）函数f是适当如果对于任何等效x和x'（x = x'数学-类的说法），的x和x'图像是等效太：f x = f x'。

我们需要这个Proper属性能够改写x到x'时x不是一个“独立”的变量，但f适用于它。修复错误

一种方式是一个附加字段添加到的Module类型类定义：上述

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

说(·)是一个二进制函数，它尊重等价为它的参数。

像这样

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! *) 
    }. 

例如SemiGroup有&类似的领域：

Class SemiGroup {Aop: SgOp A} : Prop := 
    { sg_setoid :> Setoid A 
    ; sg_ass :> Associative (&) 
    ; sg_op_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. 
Qed. 

我要补充有另一种方式来证明引理，但不知何故勒柯克无法找到的LeftCancellation类型类实例，而不轻推（显然这法举行各组和MathClasses.theory.groups进口）：

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. 

这里是充分发展与发挥：

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.