coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Excluded middle and decidable equality

From: Cedric Auger <sedrikov AT gmail.com>
To: Alan Schmitt <alan.schmitt AT polytechnique.org>
Cc: "N. Raghavendra" <raghu AT hri.res.in>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Excluded middle and decidable equality
Date: Wed, 2 Oct 2013 14:36:05 +0200

2013/10/2 Alan Schmitt <alan.schmitt AT polytechnique.org>

raghu AT hri.res.in writes:

> 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

I may be missing something here but this look like a tautology.

Alan

I guess he meant "(exmid_eq X → exmid_appears_in X) ∧ (exmid_appears_in X → pingeonhole_principle X) ∧ (pigeonhole_principle X → exmid_eq X)"

--
.../Sedrikov\...

Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Daniel Schepler, 10/02/2013
  - Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
    - Re: [Coq-Club] Excluded middle and decidable equality, Jason Gross, 10/02/2013
      - Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
    - Re: [Coq-Club] Excluded middle and decidable equality, Alan Schmitt, 10/02/2013
      - Re: [Coq-Club] Excluded middle and decidable equality, Cedric Auger, 10/02/2013
        
        Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
  - Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/04/2013