错误消息 "setoid rewrite failed: UNDEFINED EVARS" 是什么意思？
What does the error message "setoid rewrite failed: UNDEFINED EVARS" mean?
我最近经常看到这种错误：
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.
我在使用 math-类 库进行证明时经常看到这一点。
报错信息给了我们一个提示：
|- Proper (equiv ==> ....
重写失败，因为scalar_mult函数（它的符号是·）缺少一个非常重要的属性：它是而不是Proper。
Proper 函数是一个尊重等价的函数——记住 Math-类 库中的所有东西都是等价的，甚至 = 是 equiv 的符号，而不是eq。
更正式地说，（一元）函数 f 是 proper 如果对于任何等价的 x 和 x' （x = x' 在 Math-类 说法), x 和 x' 的图像也是等价的: f x = f x'.
当x不是"free-standing"变量时，我们需要这个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 typeclass 的实例而不用轻推（显然这条定律适用于每个组并且 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.
事实证明，这确实是一个奇怪的怪癖：答案在于我使用的 Proper 实例只明确引用了 sm，没有使用点符号 (·).当我将其更改为 Anton 在上面使用的符号时，它工作得很好。我会立即向 math-类 提出拉取请求。
编辑：对这个 github 问题提供了很好的解释：https://github.com/c-corn/corn/issues/35
我最近经常看到这种错误：
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.
我在使用 math-类 库进行证明时经常看到这一点。
报错信息给了我们一个提示：
|- Proper (equiv ==> ....
重写失败，因为scalar_mult函数（它的符号是·）缺少一个非常重要的属性：它是而不是Proper。
Proper 函数是一个尊重等价的函数——记住 Math-类 库中的所有东西都是等价的，甚至 = 是 equiv 的符号，而不是eq。
更正式地说，（一元）函数 f 是 proper 如果对于任何等价的 x 和 x' （x = x' 在 Math-类 说法), x 和 x' 的图像也是等价的: f x = f x'.
当x不是"free-standing"变量时，我们需要这个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 typeclass 的实例而不用轻推（显然这条定律适用于每个组并且 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.
事实证明，这确实是一个奇怪的怪癖：答案在于我使用的 Proper 实例只明确引用了 sm，没有使用点符号 (·).当我将其更改为 Anton 在上面使用的符号时，它工作得很好。我会立即向 math-类 提出拉取请求。
编辑：对这个 github 问题提供了很好的解释：https://github.com/c-corn/corn/issues/35