The Coq mailing list

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

At 2013-09-27T15:09:31+02:00, Arnaud Spiwack wrote:

> Require Import Coq.Classes.RelationClasses.
>
> Record Setoid := {
>   El :> Type;
>   equ : El->El->Prop;
>   equ_equiv : Equivalence equ
> }.

Sorry for the delayed reply.  Your code is beyond me.  I'm still
learning Coq from Pierce's book, and've just finished the chapter on
Logic.  I'll come back to setoids later.

Meanwhile, the best I could do with my current knowledge is to prove the
following:

----------------------------------------------------------------------

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

Definition exmid_appears_in (X : Type) : Prop :=
  forall (x : X) (l : list X), appears_in x l \/ ~ appears_in x l.

Inductive repeats {X : Type} : list X -> Prop :=
| repeats_1 : forall (x : X) (l : list X),
                appears_in x l -> repeats (x :: l)
| repeats_2 : forall (x : X) (l : list X),
                repeats l -> repeats (x :: l).

Definition pigeonhole_principle (X : Type) : Prop :=
  forall l1 l2 : list X,
    (forall x : X, appears_in x l1 -> appears_in x l2) ->
    length l2 < length l1 ->
    repeats l1.

Theorem exmid_eq_exmid_appears_in :
  forall X : Type,
    exmid_eq X -> exmid_appears_in X.

Theorem exmid_appears_in_pigeonhole_principle :
  forall X : Type,
    exmid_appears_in X -> pigeonhole_principle X.

Theorem pigeonhole_principle_exmid_eq :
  forall X : Type,
    pigeonhole_principle X -> exmid_eq X.

Definition reflexive (X : Type) (R : X -> X -> Prop) : Prop :=
  forall x : X, R x x.

Definition symmetric (X : Type) (R : X -> X -> Prop) : Prop :=
  forall x y : X, R x y -> R y x.

Definition transitive (X : Type) (R : X -> X -> Prop) : Prop :=
  forall x y z : X, R x y -> R y z -> R x z.

Definition equivalence (X : Type) (R : X -> X -> Prop) : Prop :=
  reflexive X R /\ symmetric X R /\ transitive X R.

Definition exmid_equiv (X : Type) (R : X -> X -> Prop) : Prop :=
  equivalence X R -> forall x y : X, R x y \/ ~ R x y.

Definition quotient (X : Type) (R : X -> X -> Prop) (Y : Type)
(p : X -> Y) : Prop :=
  forall x1 x2 : X, R x1 x2 <-> p x1 = p x2.

Definition quotient_exists (X : Type) (R : X -> X -> Prop) : Prop :=
  equivalence X R ->
  exists Y : Type, exists p : X -> Y, quotient X R Y p.

Theorem exmid_eq_quotient_exists_exmid_equiv :
  (forall X : Type, exmid_eq X) ->
  forall (X : Type) (R : X -> X -> Prop),
    quotient_exists X R -> exmid_equiv X R.

Theorem exmid_equiv_excluded_middle :
  (forall (X : Type) (R : X -> X -> Prop), exmid_equiv X R) ->
  excluded_middle.

----------------------------------------------------------------------

Thanks again for your help.

Best regards,
Raghu.

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