Require Import ClassicalFacts.

Definition XM : Prop := forall X : Prop, X \/ ~X.

Definition DN : Prop := forall X : Prop, ~~X -> X.

Definition CP : Prop := forall X Y : Prop, (~Y -> ~X) -> X -> Y.

Definition Peirce : Prop := forall X Y : Prop, ((X -> Y) -> X) -> X.
Lemma DN_XM : DN -> XM.
intros dn X. apply dn. intros f.
apply f. apply or_intror.
intros x. apply f. apply (or_introl _ x).
Qed.
Lemma XM_DN : XM -> DN.
intros xm X f. destruct (xm X). apply H.
destruct (f H).
Qed.

Lemma DN_Peirce : DN -> Peirce.
intros dn X Y f. apply dn.
intros g. apply g. apply f.
intros x. destruct (g x).
Qed.

Lemma Peirce_DN : Peirce -> DN.
intros p X. apply (p _ False).
intros f g. destruct g.
intros x. apply f.
intros _. apply x.
Qed.

Lemma XM_CP : XM -> CP.
intros xm X Y f g.
destruct (xm Y) as [h|h].
apply h. destruct (f h g).
Qed.

Definition SE : Prop := forall (X: Type) (p q : X -> Prop), (forall x, p x <-> q x) -> p = q.

Definition PCA : Prop := forall X : Prop, X=True \/ X=False.

Definition PI : Prop := forall X : Prop, forall x y : X, x = y.

Definition PE : Prop := forall X Y : Prop, (X<->Y) -> X=Y.

Definition FE : Prop := forall (X: Type) (f g : X -> Prop), (forall x, f x = g x) -> f = g.

Definition SXM : Type := forall X : Prop, sumbool X (~X).

Lemma PCA_PE : PCA -> PE.
intros pca X Y A.
destruct (pca X) as [B|B]; destruct (pca Y) as [C|C]; subst X Y.
reflexivity.
destruct A as [A B].
destruct (A I).
destruct A as [A B].
destruct (B I).
reflexivity.
Qed.

Lemma FE_PE_SE : FE -> PE -> SE.
intros fe pe X f g A. apply fe.
intros x. apply pe.
apply A.
Qed.

Lemma PCA_XM : PCA -> XM.
intros pca x. destruct (pca x) as [A|A]; rewrite A.
left. exact I.
right. intros [].
Qed.

Lemma PE_PI : PE -> PI.
exact ext_prop_dep_proof_irrel_cic.

Qed.

Lemma SE_PE : SE -> PE.
intros se x y f.
exact (f_equal (fun g => g x) (se Prop (fun _ => x) (fun _ => y) (fun _ => f))).
Qed.

Definition TR (X:Type) (lt:X->X->Prop) : Type := forall x y : X, lt x y \/ lt y x \/ x = y.

Definition STR (X:Type) (lt:X->X->Prop) : Type := forall x y : X, sumor (sumbool (lt x y) (lt y x)) (x = y).

Coercion boolp := (fun x => if x then True else False) : bool -> Prop.

Lemma reflect_eq1 {x:bool}: x -> x=true.
intros [] []. reflexivity.
Qed.

Lemma reflect_eq2 {x:bool}: x=true -> x.
intros x A. rewrite A. exact I.
Qed.

Lemma xm_bool (x:bool) : x \/ ~ x.
intros []. left. exact I.
right. intros [].
Qed.

Lemma pi_bool (x:bool) : forall p q : x, p=q.
intros [] ; simpl.
intros [] []. reflexivity.
intros [].
Qed.

Lemma pe_bool (x y:bool) : (x <-> y) -> x = y.
intros [] []; try tauto.
intros [A _]. destruct (A I).
intros [_ A]. destruct (A I).
Qed.