可判定相等性如何与 List.remove 一起使用？

Question

我从 Coq 开始，发现我必须提供可判定相等性的证明才能使用 List.remove。例如

Require Import Coq.Lists.List.

Import List.ListNotations.

Inductive T : Set := A | B | C.

Lemma eq_dec : forall a b : T, {a = b} + {a <> b}.
Proof.
  destruct a, b; try (left; reflexivity); try (right; congruence).
Qed.

Definition f (xs : list T) : list T := List.remove eq_dec A xs.

现在可以进行类型检查，但我不明白如何使用它。

Theorem foo : f [ A; B; C ] = [ B; C ].
Proof. reflexivity.

给我

Error: Unable to unify "[B; C]" with "f [A; B; C]".

这种可判定的平等是如何工作的，我可以阅读哪些好的资料？

编辑 1

我刚刚了解了decide equality 策略，

解决forall x y:R, {x=y}+{~x=y} 形式的目标，其中 R 是 归纳类型，使得它的构造函数不采取证明或 作为参数的函数，也不是依赖类型中的对象。

所以eq_dec可以改写：

Lemma eq_dec : forall a b : T, {a = b} + {a <> b}.
Proof. decide equality. Defined.

编辑 2

我刚刚了解了Scheme Equality for T 命令，它

尝试生成布尔等式和可判定性证明 通常的平等。如果 identi 涉及其他一些归纳类型， 必须首先定义它们的相等性。

所以T_beq : T -> T -> bool和T_eq_dec : forall x y : T, {x = y} + {x <> y}可以自动生成。

Answer 1

问题是你使用了Qed 命令来结束你的证明。这会导致您刚刚定义的 eq_dec 函数变得不透明，从而阻止 Coq 简化涉及它的表达式。在这种情况下，一个简单的解决方案是改用Defined：

Require Import Coq.Lists.List.

Import List.ListNotations.

Inductive T : Set := A | B | C.

Lemma eq_dec : forall a b : T, {a = b} + {a <> b}.
Proof.
  destruct a, b; try (left; reflexivity); try (right; congruence).
Defined.

Definition f (xs : list T) : list T := List.remove eq_dec A xs.

Theorem foo : f [ A; B; C ] = [ B; C ].
Proof. reflexivity. Qed.

您可以查看 Adam Chlipala 的 CPDT book 以了解有关这种编程风格的更多信息。

还有一种替代方法，我个人更喜欢这种方法。这个想法是编写返回布尔值的正常相等测试，并在测试是正确的事实之后证明。这有两个原因。

1. 它允许重用标准布尔运算符来编写这些函数；和

2. 涉及证明的函数（如 eq_dec）可能与 Coq 的归约机制发生不良交互，因为归约需要考虑证明。

您可以在Software Foundations book 中阅读有关这种替代样式的更多信息。您还可以查看mathematical components 库，它普遍使用这种风格——例如，定义type with decidable equality 的概念。

Answer 2

您也可以保持可判定相等性的证明不透明，但在这种情况下，您必须使用 reflexivity 以外的其他策略来证明您的结果。

在与您的示例相同的上下文中，试试这个：

Theorem foo : f [ A; B; C ] = [ B; C ].
Proof.
unfold f; simpl; case (eq_dec A A);[intros _ | intros abs; case abs; auto].
case (eq_dec A B);[discriminate | intros _].  
case (eq_dec A C);[discriminate | intros _].
reflexivity.
Qed.

当您想要更抽象地推理类型元素之间的相等性以及计算无法为您完成所有事情时，知道此解决方案的存在可能非常有用。