可判定的相等如何与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书籍,以了解有关此编程风格的更多信息.

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

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

2. 涉及证明(例如eq_dec)的函数可能与Coq的简化机制非常相互影响,因为减少需要考虑证明.

您可以在Software Foundations一书中阅读有关此替代样式的更多信息.您还可以查看数学组件库,它通常使用此样式 - 例如,定义具有可判定相等性的类型概念.

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.

当您想更抽象地推断类型元素之间的相等性并且计算无法为您做任何事情时，知道此解决方案可能会非常有用。