論理

From Stdlib Require Import Logic.PropExtensionality.

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

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

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

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

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

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

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

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

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

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

Lemma disj_delete_right
  {P Q : Prop} :
  P \/ Q ->
  ~ Q ->
  P.P, Q: Prop
P \/ Q -> ~ Q -> P
Proof.P, Q: Prop
P \/ Q -> ~ Q -> P
  intros.P, Q: Prop
H: P \/ Q
H0: ~ Q
P
  destruct H.P, Q: Prop
H: P
H0: ~ Q
P
P, Q: Prop
H: Q
H0: ~ Q
P
  -P, Q: Prop
H: P
H0: ~ Q
P
    assumption.
  -P, Q: Prop
H: Q
H0: ~ Q
P
    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.P: Prop
forall x y : P + (~ P), x = y
Proof.P: Prop
forall x y : P + (~ P), x = y
  intros.P: Prop
x, y: P + (~ P)
x = y
  destruct x, y.P: Prop
p, p0: P
inl p = inl p0
P: Prop
p: P
n: ~ P
inl p = inr n
P: Prop
n: ~ P
p: P
inr n = inl p
P: Prop
n, n0: ~ P
inr n = inr n0
  -P: Prop
p, p0: P
inl p = inl p0
    f_equal.P: Prop
p, p0: P
p = p0
    apply proof_irrelevance.
  -P: Prop
p: P
n: ~ P
inl p = inr n
    contradiction.
  -P: Prop
n: ~ P
p: P
inr n = inl p
    contradiction.
  -P: Prop
n, n0: ~ P
inr n = inr n0
    f_equal.P: Prop
n, n0: ~ P
n = n0
    apply proof_irrelevance.
Qed.