The Coq mailing list

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

This question arose out of the exercises on classical logic and the
pigeonhole principle in Pierce's software foundations book:

http://www.cis.upenn.edu/~bcpierce/sf/Logic.html

Consider the following propositions:

Definition excluded_middle : Prop :=
  forall P : Prop, P \/ ~ P.

Definition exmid_eq (X : Type) : Prop :=
  forall x y : X, x = y \/ x <> y.

I want to prove this:

Theorem A :
  (forall X : Type, exmid_eq X) -> excluded_middle.

I want to use a construction which I saw in a paper of Andreas Blass (An
Induction Principle and Pigeonhole Principles for K-Finite Sets,
arXiv:math/9405204 [math.LO], Proof of Theorem 4).  I am wondering how
to formalise that argument in Coq.

The construction in Blass's paper starts with a set Y = {u,v} of
cardinality 2.  For every proposition P, he defines an equivalence
relation R(P) on Y as follows:

1. (u,u) \in R(P)

2. (v,v) \in R(P)

3. P -> (u,v) \in R(P)

4. P -> (v,u) \in R(P).

Let X(P) = Y / R(P), the quotient set of Y by R(P), and let a(P) and
b(P) be the images of u and v, respectively, in X(P) under the canonical
projection Y -> X(P).  By definition,

exmid_eq -> a(P) = b (P) \/ a(P) <> b(P).

Now, a(P) = b(P) -> (u,v) \in R -> P.

Conversely, P -> (u,v) \in R -> a(P) = b(P).  Therefore, taking negations,
we get a(P) <> b(P) -> ~ P.  

Is my understating of the above construction correct?  If so, any hints
on how to define X(P) as a type in Coq?

Best regards,
Raghu.

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