(*|
論理
====
|*)

From Stdlib Require Import Logic.PropExtensionality.

Lemma hypothesis_is_true
  (P : Prop)
  : P -> P = True.
Proof.
  intro.
  apply propositional_extensionality.
  split.
  -
    trivial.
  -
    intro.
    assumption.
Qed.

Lemma negated_hypothesis_is_false
  (P : Prop)
  : ~ P -> P = False.
Proof.
  intro.
  apply propositional_extensionality.
  split.
  -
    trivial.
  -
    intro.
    contradiction.
Qed.

Lemma trivially_not_false : ~ False.
Proof.
  intro.
  assumption.
Qed.

Lemma not_or_then_and_not
  {P Q : Prop} :
  ~ (P \/ Q) ->
  ~ P /\ ~ Q.
Proof.
  intro.
  unfold not in H.
  split.
  -
    intro.
    apply H.
    left.
    assumption.
  -
    intro.
    apply H.
    right.
    assumption.
Qed.

Lemma not_false_then_true
  {P Q : Prop} :
  ~ False ->
  True.
Proof.
  trivial.
Qed.

Lemma not_true_then_false
  {P Q : Prop} :
  ~ True ->
  False.
Proof.
  intro.
  apply H.
  trivial.
Qed.

Lemma contrapositive_introduction
  {P Q : Prop} :
  (P -> Q) ->
  (~ Q -> ~ P).
Proof.
  intros H0 H1 H2.
  apply H1.
  apply H0.
  assumption.
Qed.

Lemma double_negation_introduction
  {P : Prop} :
  P ->
  ~ ~ P.
Proof.
  unfold not.
  intros.
  apply H0, H.
Qed.

Lemma not_exists_then_forall_not
  {A : Type}
  {P : A -> Prop} :
  ~ (exists x, P x) ->
  forall x, ~ P x.
Proof.
  unfold not.
  intros.
  apply H.
  exists x.
  assumption.
Qed.

Lemma uncurry_not
  {P Q : Prop} :
  ~ (P /\ Q) ->
  P -> ~ Q.
Proof.
  unfold not.
  intros.
  apply H.
  auto.
Qed.

Lemma disj_delete_right
  {P Q : Prop} :
  P \/ Q ->
  ~ Q ->
  P.
Proof.
  intros.
  destruct H.
  -
    assumption.
  -
    contradiction.
Qed.

Definition andalso
  {A : Type}
  (P : A -> Prop)
  (Q : {a : A | P a} -> Prop)
  : A -> Prop :=
  fun a =>
    exists p : P a, Q (exist P a p).

(*|
TODO: 適切なファイルに移動する：
|*)

Definition decidability_of_proposition_is_property
  (P : Prop)
  : forall x y : P + (~ P), x = y.
Proof.
  intros.
  destruct x, y.
  -
    f_equal.
    apply proof_irrelevance.
  -
    contradiction.
  -
    contradiction.
  -
    f_equal.
    apply proof_irrelevance.
Qed.