Coq:为什么我不能从Decidable的实例中获得显式的见证？

Question

我首先定义一个帮助器函数，用于构建给定{P} + {~P}证明的Decidable P实例

Require Import Coq.Classes.DecidableClass.

Definition derive_decidable : forall P : Prop, {P} + {~P} -> Decidable P.
intros P H; destruct H; 
[ apply (Build_Decidable P true) | apply (Build_Decidable P false) ];
intuition congruence.
Qed.

现在我定义了一个愚蠢的类型，并给了它一个愚蠢的可判定的实例：

Inductive Color := red | green | blue.

Instance Color_eqdec (x y : Color) : Decidable (x = y).
apply derive_decidable; decide equality.
Qed.

现在我希望能够使用这个实例来证明关于颜色的命题，但我得到了一个令人惊讶的结果。之后

Lemma green_neq_blue : green <> blue.
apply (Decidable_complete_alt _ (Color_eqdec green blue)).

我只剩下一个目标：

Decidable_witness = false

到目前一切尚好。现在我希望能够通过compute; reflexivity实现这个目标，但它不起作用。在compute之后，我的目标变成了

(let (Decidable_witness, _) := Color_eqdec green blue in Decidable_witness) = false

无论我做什么，我似乎都无法说服Coq访问我在Color_eqdec中为Decidable_witness给出的定义。为什么计算停留在这里，而不是测试版-减少Color_eqdec green blue并最终简化为false = false

Answer 1

您需要使用Defined.终止两个实例定义(Color_eqdec和derive_decidable)，以便使它们的主体透明。

默认情况下，当校样以Qed终止时，正文是不透明的，并且术语不会减少。这通常对证明是有好处的，因为调用者不应该依赖它们的内容。但是，当使用证明模式构造Type中的术语(即本例中的sumbool和Decidable )时，您实际上希望使用Ltac脚本构造的主体进行计算，因此应该改用Defined来使结果术语透明。