coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Alan Schmitt <alan.schmitt AT polytechnique.org>
To: "N. Raghavendra" <raghu AT hri.res.in>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Excluded middle and decidable equality
Date: Wed, 02 Oct 2013 13:34:16 +0200

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

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