The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-10-02T02:02:12-07:00, Daniel Schepler wrote:

> On Wednesday, October 02, 2013 11:05:44 AM N. Raghavendra wrote:
>> Definition pigeonhole_principle (X : Type) : Prop :=
>>   forall l1 l2 : list X,
>>     (forall x : X, appears_in x l1 -> appears_in x l2) ->
>>     length l2 < length l1 ->
>>     repeats l1.
> [...]
>> Theorem exmid_appears_in_pigeonhole_principle :
>>   forall X : Type,
>>     exmid_appears_in X -> pigeonhole_principle X.
>
> For what it's worth, here's a proof of pigeonhole_principle without any 
> excluded middle assumptions.

I am a bit confused now, because I've proved in Coq, without invoking
any libraries other than Init, that

exmid_eq X -> exmid_appears_in X -> pigeonhole_principle X -> 
exmid_eq X

for every type X, where (exmid_eq X) is the proposition that equality in
X is decidable, and (exmid_appears_in X) is the prop that list
membership in X is decidable.  So, if one can prove the pigeonhole
principle without any classical logic assumptions, it follows that
equality is decidable for all types, without any classical logic
assumptions.  Does that sound right?

Best regards,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/