The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Damien Pous wrote:
> I am stuck with the following simple goal (even with
> `standard' axioms like JMeq_eq or eq_rect_eq...).
> Is there a way to solve it ?
>
> Thanks!
> Damien
>
>
> Require Import JMeq.
>
> Inductive B: bool -> Set :=
> | ff: B false
> | tt: B true.
>
> Goal ~ (JMeq ff tt).
>   

This goal has a lot in common with a class of goals that often turn out 
unsolvable.  The crux of the theorem is in proving the inequality of 
types.  The only effective way I've yet found to prove type inequality 
is by demonstrating unequal cardinalities.  (Proving that a true [Prop] 
isn't equal to a false [Prop] is a special case of this.)

I'll be curious to see if anyone can give a rigorous argument that your 
special case isn't provable.  I'm guessing that you'd be better off 
refactoring your higher-level theorems so that they don't depend on 
proofs of type inequality.  Often introducing an extra layer of syntax 
helps accomplish this goal.  You might also try defining a specialized 
equality for your inductive type, proving that it coincides with the 
normal equality in the important cases.