錯誤信息「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.