Coq:为什么我不能从Decidable的实例中得到明确的证人？

Question

我首先定义一个辅助函数来构建Decidable P给定证明的实例{P} + {~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.

现在我定义一个愚蠢的类型并给它一个愚蠢的Decidable实例:

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

不管我做什么,我似乎无法说服勒柯克访问我给的定义Color_eqdec了Decidable_witness.为什么计算会被困在这里,而不是beta-减少Color_eqdec green blue并最终简化为false = false？

Answer 1

您需要终止两个实例定义(Color_eqdec和derive_decidable)Defined.以使其主体透明.

默认情况下,当证据终止时Qed,正文不透明且术语不会减少.这通常适用于校样,因为来电者不应该依赖于他们的内容.但是,使用防爆模式构建在条件时Type(即sumbool和Decidable你的情况),你真的想计算与该LTAC脚本构成,所以你应该使用身体Defined,使所产生的长期透明.