我首先定义一个辅助函数来构建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 …coq ×1