I start by defining a helper function for building instances of Decidable P given a proof of {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.
Now I define a silly type and give it a silly Decidable instance:
Inductive Color := red | green | blue.
Instance Color_eqdec (x y : Color) : Decidable (x = y).
apply derive_decidable; decide equality.
Qed.
Now I want to be able to use this instance to prove propositions about colors, but I'm getting a surprising result. After
Lemma green_neq_blue : green <> blue.
apply (Decidable_complete_alt _ (Color_eqdec green blue)).
I'm left with a goal of
Decidable_witness = false
So far so good. Now I expect to be able to discharge this goal by compute; reflexivity, but it's not working. After compute, my goal becomes
(let (Decidable_witness, _) := Color_eqdec green blue in Decidable_witness) = false
and no matter what I do, I can't seem to convince Coq to access the definition I gave in Color_eqdec for Decidable_witness. Why is computation getting stuck here, rather than beta-reducing Color_eqdec green blue and eventually simplifying to false = false?
You need to terminate your two instance definitions (Color_eqdec and derive_decidable) with Defined. in order to make their bodies transparent.
By default, when a proof is terminated with Qed the body is opaque and the term does not reduce. This is generally good for proofs because callers shouldn't depend on their contents. However, when using proof mode to construct terms that are in Type (namely sumbool and Decidable in your case), you actually want to compute with the body that the Ltac script constructed, so you should instead use Defined to make the resulting term transparent.