我从 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
策略,其中
solves a goal of the form
forall x y:R, {x=y}+{~x=y}
, where R is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types.
所以eq_dec
可以重写:
Lemma eq_dec : forall a b : T, {a = b} + {a <> b}.
Proof. decide equality. Defined.
编辑2
我刚刚了解到 Scheme Equality for T
命令,其中
Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If identi involves some other inductive types, their equality has to be defined first.
所以T_beq : T -> T -> bool
和T_eq_dec : forall x y : T, {x = y} + {x <> y}
可以自动生成。
最佳答案
问题在于您使用了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了解有关这种编程风格的更多信息。
还有一种替代方法,我个人更喜欢。这个想法是编写返回 bool 值的正常相等测试,并在事后证明测试是正确的。这很有用,有两个原因。
它允许重用标准 bool 运算符来编写这些函数;和
涉及证明的函数(例如
eq_dec
)可能会与 Coq 的归约机制产生不良交互,因为归约需要考虑证明。
您可以在 Software Foundations book 中阅读有关此替代样式的更多信息。 。您还可以查看mathematical components库,它普遍使用这种风格——例如,定义 type with decidable equality 的概念。 .
关于coq - 可判定相等如何与 List.remove 一起使用?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/46589021/