The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

In ordinary mathematics (such as in Blass's paper) we have
propositional extensionality, which says that logically equivalent
propositions are equal. With that in hand it is easy to finish your
exercise without fussing with quotients (although I am sure Blass has
a good reason to do it his way, probably to stick close to set
theory):

Definition lem := forall p : Prop, p \/ ~p.
Definition deceq := forall (X : Type) (x y : X), x = y \/ ~ (x = y).

Axiom prop_extensionality : forall p q : Prop, (p <-> q) -> p = q.

Lemma small_lemma : forall p : Prop, p = (p = True).
Proof.
  intro p.
  apply prop_extensionality.
  split; intro.
  - apply prop_extensionality; split; auto.
  - rewrite H; auto.
Qed.

Lemma deceq_to_lem : deceq -> lem.
Proof.
  intros D p.
  rewrite (small_lemma p).
  apply D.
Qed.

Another way to do this without propositional extensionality and
without quotients is to rephrase deceq so that it says that
equivalence relations are decidable, not just equality (if we have
deceq and quotients then it follows that equivalence relations are
decidable as well):

Require Import Relations.
Require Import Setoid.

Definition lem := forall p : Prop, p \/ ~p.

Definition decequiv :=
  forall (X : Type) (R : relation X),
    equiv X R -> forall x y, R x y \/ ~ (R x y).

Lemma small_lemma: forall p : Prop, p <-> (p <-> True).
Proof.
  tauto.
Qed.

Lemma decequiv_to_lem : decequiv -> lem.
Proof.
  intros D p.
  rewrite (small_lemma p).
  apply (D _ iff).
  firstorder.
Defined.

Note: here I used Setoid just so that I could rewrite w.r.t small_lemma.

With kind regards,

Andrej


On Thu, Sep 26, 2013 at 10:18 PM, 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/
>