我首先定义一个辅助函数，以构建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
而且无论我做什么，我似乎都无法说服Coq访问我Color_eqdec为定义的定义Decidable_witness。为什么计算会卡在这里，而不是减少betaColor_eqdec green blue并最终简化为false = false？
您需要使用终止两个实例定义（Color_eqdec和derive_decidable），Defined.以使它们的主体透明。
默认情况下，当证明终止Qed于主体时是不透明的，并且该术语不减少。这通常对证明很有用，因为调用者不应依赖于其内容。但是，使用防爆模式构建在条件时Type（即sumbool和Decidable你的情况），你真的想计算与身体的LTAC脚本构成，所以你应该使用Defined，使所产生的长期透明。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句