The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Consider the goal:  forall (A:Type), inhabited (inhabited A -> A).

It seems to be a bit like the Drinker's Paradox, but not quite. However, 
I can't seem to prove it from the Drinker's Paradox, or vice versa.  It 
is provable from excluded middle.  I think it's also weaker than 
excluded middle.

If added to a constructive logic, it would suggest that the resulting 
logic isn't really constructive ("For any type, there exists a way to 
get an instance non-constructively.").  But, if it is weaker than 
excluded middle, then paradoxically the logic still is constructive.

Anyone seen it before?

It's the most trivial general example I could come up with that can't be 
proved in Coq because Coq doesn't allow "informative" Prop case analysis 
in a non-Prop goal even if that goal is a subgoal of a parent (or 
ancestral) Prop goal - and thus isn't really informative to the overall 
proof, and would be erased during extraction.

-- Jonathan