typeclass - 错误消息 "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

错误信息给了我们一个提示:|- 正确(相当于 ==> ....

重写失败，因为scalar_mult函数(其符号为·)缺少一个非常重要的属性:它不正确。Proper 函数是一个尊重等价性的函数 - 请记住 Math-Classes 库中的所有内容都定义为等价性，甚至 = 也是 equiv< 的表示法，而不是eq 。更正式地说，如果对于任何等效的 x 和 x' (x')，(一元)函数 f 就是正确。 >x = x'(数学类用语))，x 和 x' 的图像也是等效的:f x = f x'.

当 x 不是一个时，我们需要这个 Proper 属性才能将 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.

我必须补充一点，还有另一种方法可以证明这个引理，但是 Coq 不知何故无法在没有轻推的情况下找到 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.