Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** * The law of excluded middle *)

Monomorphic Axiom ExcludedMiddle : Type0.
Existing Class ExcludedMiddle.

(** Mark this axiom as a "global axiom", which some of our tactics will automatically handle. *)
Global Instance is_global_axiom_excludedmiddle : IsGlobalAxiom ExcludedMiddle := {}.

Axiom LEM : forall `{ExcludedMiddle} (P : Type), IsHProp P -> P + ~P.

Definition ExcludedMiddle_type := forall (P : Type), IsHProp P -> P + ~P.

(** ** LEM means that all propositions are decidable *)

Global Instance decidable_lem `{ExcludedMiddle} (P : Type) `{IsHProp P} : Decidable P
  := LEM P _.

(** ** Double-negation elimination *)

Definition DNE_type := forall P, IsHProp P -> ~~P -> P.

Definition LEM_to_DNE : ExcludedMiddle -> DNE_type.
ExcludedMiddle -> DNE_type
Proof.
ExcludedMiddle -> DNE_type
  intros lem P hp nnp.
lem: ExcludedMiddle
P: Type
hp: IsHProp P
nnp: ~~ P
P
  case (LEM P _).
lem: ExcludedMiddle
P: Type
hp: IsHProp P
nnp: ~~ P
P -> P
lem: ExcludedMiddle
P: Type
hp: IsHProp P
nnp: ~~ P
~ P -> P
  -
lem: ExcludedMiddle
P: Type
hp: IsHProp P
nnp: ~~ P
P -> P auto.
  -
lem: ExcludedMiddle
P: Type
hp: IsHProp P
nnp: ~~ P
~ P -> P intros np; elim (nnp np).
Defined.

(** This direction requires Funext. *)
Definition DNE_to_LEM `{Funext} : 
  DNE_type -> ExcludedMiddle_type.
H: Funext
DNE_type -> ExcludedMiddle_type
Proof.
H: Funext
DNE_type -> ExcludedMiddle_type
  intros dn P hp.
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
P + ~ P
  refine (dn (P + ~P) _ _).
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
IsHProp (P + ~ P)
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
~~ (P + ~ P)
  -
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
IsHProp (P + ~ P) apply ishprop_sum.
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
IsHProp P
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
IsHProp (~ P)
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
P -> ~ P -> Empty
    +
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
IsHProp P exact _.
    +
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
IsHProp (~ P) exact _.
    +
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
P -> ~ P -> Empty intros p np; exact (np p).
  -
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
~~ (P + ~ P) intros nlem.
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
nlem: ~ (P + ~ P)
Empty
    apply nlem.
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
nlem: ~ (P + ~ P)
P + ~ P
    apply inr.
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
nlem: ~ (P + ~ P)
~ P
    intros p.
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
nlem: ~ (P + ~ P)
p: P
Empty
    apply nlem.
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
nlem: ~ (P + ~ P)
p: P
P + ~ P
    apply inl.
H: Funext
dn: DNE_type
P: Type
hp: IsHProp P
nlem: ~ (P + ~ P)
p: P
P
    apply p.
Defined.

(** DNE is equivalent to "every proposition is a negation". *)
Definition allneg_from_DNE (H : DNE_type) (P : Type) `{IsHProp P}
  : {Q : Type & P <-> ~Q}.
H: DNE_type
P: Type
IsHProp0: IsHProp P
{Q : Type & P <-> ~ Q}
Proof.
H: DNE_type
P: Type
IsHProp0: IsHProp P
{Q : Type & P <-> ~ Q}
  exists (~P); split.
H: DNE_type
P: Type
IsHProp0: IsHProp P
P -> ~~ P
H: DNE_type
P: Type
IsHProp0: IsHProp P
~~ P -> P
  -
H: DNE_type
P: Type
IsHProp0: IsHProp P
P -> ~~ P intros p np; exact (np p).
  -
H: DNE_type
P: Type
IsHProp0: IsHProp P
~~ P -> P apply H; exact _.
Defined.

Definition DNE_from_allneg (H : forall P, IsHProp P -> {Q : Type & P <-> ~Q})
  : DNE_type.
H: forall P : Type,
IsHProp P -> {Q : Type & P <-> ~ Q}
DNE_type
Proof.
H: forall P : Type,
IsHProp P -> {Q : Type & P <-> ~ Q}
DNE_type
  intros P ? nnp.
H: forall P : Type,
IsHProp P -> {Q : Type & P <-> ~ Q}
P: Type
X: IsHProp P
nnp: ~~ P
P
  destruct (H P _) as [Q e].
H: forall P : Type,
IsHProp P -> {Q : Type & P <-> ~ Q}
P: Type
X: IsHProp P
nnp: ~~ P
Q: Type
e: P <-> ~ Q
P
  apply e.
H: forall P : Type,
IsHProp P -> {Q : Type & P <-> ~ Q}
P: Type
X: IsHProp P
nnp: ~~ P
Q: Type
e: P <-> ~ Q
~ Q
  intros q.
H: forall P : Type,
IsHProp P -> {Q : Type & P <-> ~ Q}
P: Type
X: IsHProp P
nnp: ~~ P
Q: Type
e: P <-> ~ Q
q: Q
Empty
  apply nnp.
H: forall P : Type,
IsHProp P -> {Q : Type & P <-> ~ Q}
P: Type
X: IsHProp P
nnp: ~~ P
Q: Type
e: P <-> ~ Q
q: Q
~ P
  intros p.
H: forall P : Type,
IsHProp P -> {Q : Type & P <-> ~ Q}
P: Type
X: IsHProp P
nnp: ~~ P
Q: Type
e: P <-> ~ Q
q: Q
p: P
Empty
  exact (fst e p q).
Defined.