The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You might have used some axioms accidentally via tactics in, e.g., pigeonhole_principle_exmid_eq.  Try [Print Assumptions pigeonhole_principle_exmid_eq.] (replacing pigeonhole_principle_exmid_eq with whatever theorem you want to check) to see if it depends on axioms.  (I'm suggesting pigeonhole_principle_exmid_eq because I don't see how that is possible without classical axioms.)

-Jason

On Wednesday, October 2, 2013, N. Raghavendra wrote:

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/