The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Coq doesn't have quotients (yet?). So you cannot quite do this directly.

The way to go is to use setoids, that is (dependent) pairs of a type and an equivalence relation on that type. Then you have to quantify on setoids rather than just types. The equality at each setoid is the underlying relation. And quotient is obtained just by changing the underlying relation of the setoid.

I'm not sure what reading to suggest for a more in-depth view. Maybe the first chapter of my thesis can be of help : http://pastel.archives-ouvertes.fr/docs/00/60/58/36/PDF/thesis.spiwack.pdf .

On 26 September 2013 15:18, N. Raghavendra <raghu AT hri.res.in> wrote:

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/