(*|
古典論理
========
|*)

Require Import boolean.
Require Import logic.
From Stdlib Require Logic.Classical_Prop.
From Stdlib Require Import Logic.Description.
From Stdlib Require Import Logic.PropExtensionality.
From Stdlib Require Import Logic.FunctionalExtensionality.

(*|
排中律：
|*)

Abbreviation excluded_middle :=
  Classical_Prop.classic.

Check excluded_middle. (* .unfold *)

(*|
2重否定除去：
|*)

Theorem double_negation_elimination
  (P : Prop)
  : ~ ~ P -> P.
Proof.
  intro.
  destruct (excluded_middle P).
  -
    assumption.
  -
    contradiction.
Qed.

(*|
2重否定除去より、どんな命題もその2重否定と同一視できるようになる。
|*)

Theorem involutive_negation
  (P : Prop)
  : (~ ~ P) = P.
Proof.
  apply propositional_extensionality.
  split.
  -
    apply double_negation_elimination.
  -
    apply double_negation_introduction.
Qed.

(*|
|*)

Lemma not_and_then_or_not
  {P Q : Prop} :
  ~ (P /\ Q) ->
  ~ P \/ ~ Q.
Proof.
  intro.
  unfold not in H.
  destruct (excluded_middle (~ P)).
  -
    left.
    assumption.
  -
    right.
    intro.
    apply H.
    rewrite involutive_negation in H0.
    exact (conj H0 H1).
Qed.

Lemma proof_by_contrapositive
  {P Q : Prop} :
  (~ Q -> ~ P) ->
  (P -> Q).
Proof.
  intros.
  destruct (excluded_middle Q).
  -
    assumption.
  -
    specialize (H H1).
    contradiction.
Qed.

Lemma not_forall_then_exists_not
  {A : Type}
  {P : A -> Prop} :
  ~ (forall x, P x) ->
  exists x, ~ P x.
Proof.
  intro.
  apply double_negation_elimination.
  intro.
  apply H.
  intro.
  destruct (excluded_middle (P x)).
  -
    assumption.
  -
    contradict H0.
    exists x.
    assumption.
Qed.

(*|
``A`` 上の述語 ``P`` は、「ある ``x : A`` に対して成り立つ」、あるいは「すべての ``x : A`` について成り立たない」。
|*)

Lemma exists_or_none
  {A : Type}
  (P : A -> Prop)
  : (exists x, P x) \/ (forall x, ~ P x).
Proof.
  destruct (excluded_middle (exists x, P x)).
  -
    left.
    assumption.
  -
    right.
    apply not_exists_then_forall_not.
    assumption.
Qed.

(*|
|*)

Theorem bool_by_cases
  (P : Prop)
  : exists! b : bool,
    (P -> b = true)
    /\ (~ P -> b = false).
Proof.
  apply-> unique_existence; split.

(*|
存在を排中律によって示す。
|*)

  -
    destruct (excluded_middle P).
    +
      exists true.
      split.
      *
        intro.
        reflexivity.
      *
        contradiction.
    +
      exists false.
      split.
      *
        contradiction.
      *
        intro.
        reflexivity.

(*|
一意性も排中律によって示す。
|*)

  -
    unfold uniqueness.
    intros.
    destruct H, H0.
    destruct (excluded_middle P).
    +
      specialize (H H3).
      specialize (H0 H3).
      subst x y.
      reflexivity.
    +
      specialize (H1 H3).
      specialize (H2 H3).
      subst x y.
      reflexivity.
Qed.

Definition prop_to_bool
  (P : Prop)
  : bool.
Proof.
  pose (constructive_definite_description _ (bool_by_cases P)) as s.
  exact (proj1_sig s).
Defined.

Lemma bool_by_cases_prf
  (P : Prop)
  : (P -> prop_to_bool P = true)
    /\ (~ P -> prop_to_bool P = false).
Proof.
  pose (constructive_definite_description _ (bool_by_cases P)) as s.
  exact (proj2_sig s).
Qed.

Lemma Prop_is_retract_of_bool
  (P : Prop)
  : bool_to_prop (prop_to_bool P) = P.
Proof.
  pose proof (bool_by_cases_prf P).
  destruct H.
  destruct (excluded_middle P).
  -
    specialize (H H1).
    rewrite H.
    simpl.
    symmetry.
    apply hypothesis_is_true.
    assumption.
  -
    specialize (H0 H1).
    rewrite H0.
    simpl.
    symmetry.
    apply negated_hypothesis_is_false.
    assumption.
Qed.

Lemma bool_is_retract_of_Prop
  (b : bool)
  : prop_to_bool (bool_to_prop b) = b.
Proof.
  pose proof (bool_by_cases_prf (bool_to_prop b)).
  destruct H.
  destruct b.
  -
    simpl in *.
    apply H.
    trivial.
  -
    simpl in *.
    apply H0.
    apply trivially_not_false.
Qed.

Definition every_proposition_is_decidable
  (P : Prop)
  : P + (~ P).
Proof.
  destruct (bool_by_cases_prf P).
  destruct (prop_to_bool P).
  -
    apply inl.
    destruct (excluded_middle P).
    +
      assumption.
    +
      specialize (H0 H1).
      contradict H0.
      apply true_is_not_false.
  -
    apply inr.
    destruct (excluded_middle P).
    +
      specialize (H H1).
      contradict H.
      symmetry.
      apply true_is_not_false.
    +
      assumption.
Defined.

Section GeneralDefByCases.
  Context {A : Type}.

(*|
命題 ``P`` が成り立つときと成り立たないときの場合分けによって値を与えることができる：
|*)

  Definition general_definition_by_cases
    (P : Prop)
    (x : P -> A)
    (y : ~ P -> A)
    : A :=
    match every_proposition_is_decidable P with
    | inl p => x p
    | inr q => y q
    end.

  Print general_definition_by_cases.

  Definition general_definition_by_cases_prf_1
    (P : Prop)
    (x : P -> A)
    (y : ~ P -> A)
    : forall p : P, general_definition_by_cases P x y = x p.
  Proof.
    unfold general_definition_by_cases.
    destruct (every_proposition_is_decidable P).
    +
      intro.
      f_equal.
      apply proof_irrelevance.
    +
      contradiction.
  Qed.

  Definition general_definition_by_cases_prf_2
    (P : Prop)
    (x : P -> A)
    (y : ~ P -> A)
    : forall q : ~ P, general_definition_by_cases P x y = y q.
  Proof.
    unfold general_definition_by_cases.
    destruct (every_proposition_is_decidable P).
    +
      contradiction.
    +
      intro.
      f_equal.
      apply proof_irrelevance.
  Qed.
End GeneralDefByCases.

Section DefByCases.
  Context {A : Type}.
  Variable (P : Prop).
  Variable (x : A).
  Variable (y : A).

  Definition definition_by_cases
    : A :=
    match every_proposition_is_decidable P with
    | inl _ => x
    | inr _ => y
    end.

  Lemma definition_by_cases_prf_1
    : P -> definition_by_cases = x.
  Proof.
    intro.
    unfold definition_by_cases.
    destruct (every_proposition_is_decidable P).
    -
      reflexivity.
    -
      contradiction.
  Qed.

  Lemma definition_by_cases_prf_2
    : ~ P -> definition_by_cases = y.
  Proof.
    intro.
    unfold definition_by_cases.
    destruct (every_proposition_is_decidable P).
    -
      contradiction.
    -
      reflexivity.
  Qed.
End DefByCases.