Often it matters that Coq places a type in Prop rather than in Type. Here is an example where a type ascription is needed to place a match in Prop.
Inductive even: nat -> Prop := | evenB: even 0 | evenS: forall n, even n -> even (S (S n)). Goal even 1 -> False. Proof. refine (fun a => match a in even n return match n with 1 => False | _ => True end : Prop with evenB => I | evenS _ _ => I end). Qed.
The term doesn’t type check without the ascription since Coq places it in Type, which invalidates the match on the proof
a. This type checking behavior has the unfortunate consequence that the smart match
Goal even 1 -> False. Proof. refine (fun a => match a with end). Qed.
doesn’t type check. I don’t know how to annotate the smart match so that it type checks.
So my question is whether this is a design decision or a bug?
Thanks in advance,