古典論理

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.
excluded_middle
     : forall P : Prop, P \/ ~ P

2重否定除去：

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

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

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

Lemma not_and_then_or_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
  destruct (excluded_middle (~ P)).
P, Q: Prop
H: P /\ Q -> False
H0: ~ P
~ P \/ ~ Q
P, Q: Prop
H: P /\ Q -> False
H0: ~ ~ P
~ P \/ ~ Q
  -
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
H0: ~ ~ P
~ P \/ ~ Q
    right.
P, Q: Prop
H: P /\ Q -> False
H0: ~ ~ P
~ Q
    intro.
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
    rewrite involutive_negation in H0.
P, Q: Prop
H: P /\ Q -> False
H0: P
H1: Q
P /\ Q
    exact (conj H0 H1).
Qed.

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

Lemma not_forall_then_exists_not
  {A : Type}
  {P : A -> Prop} :
  ~ (forall x, P x) ->
  exists x, ~ P x.
A: Type
P: A -> Prop
~ (forall x : A, P x) -> exists x : A, ~ P x
Proof.
A: Type
P: A -> Prop
~ (forall x : A, P x) -> exists x : A, ~ P x
  intro.
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
exists x : A, ~ P x
  apply double_negation_elimination.
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
~ ~ exists x : A, ~ P x
  intro.
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
H0: ~ exists x : A, ~ P x
False
  apply H.
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
H0: ~ exists x : A, ~ P x
forall x : A, P x
  intro.
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
H0: ~ exists x : A, ~ P x
x: A
P x
  destruct (excluded_middle (P x)).
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
H0: ~ exists x : A, ~ P x
x: A
H1: P x
P x
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
H0: ~ exists x : A, ~ P x
x: A
H1: ~ P x
P x
  -
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
H0: ~ exists x : A, ~ P x
x: A
H1: P x
P x
    assumption.
  -
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
H0: ~ exists x : A, ~ P x
x: A
H1: ~ P x
P x
    contradict H0.
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
x: A
H1: ~ P x
exists x0 : A, ~ P x0
    exists x.
A: Type
P: A -> Prop
H: ~ (forall x : A, P x)
x: A
H1: ~ P x
~ P 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).
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)
  destruct (excluded_middle (exists x, P x)).
A: Type
P: A -> Prop
H: exists x : A, P x
(exists x : A, P x) \/ (forall x : A, ~ P x)
A: Type
P: A -> Prop
H: ~ exists x : A, P x
(exists x : A, P x) \/ (forall x : A, ~ P x)
  -
A: Type
P: A -> Prop
H: exists x : A, P x
(exists x : A, P x) \/ (forall x : A, ~ P x)
    left.
A: Type
P: A -> Prop
H: exists x : A, P x
exists x : A, P x
    assumption.
  -
A: Type
P: A -> Prop
H: ~ exists x : A, P x
(exists x : A, P x) \/ (forall x : A, ~ P x)
    right.
A: Type
P: A -> Prop
H: ~ exists x : A, P x
forall x : A, ~ P x
    apply not_exists_then_forall_not.
A: Type
P: A -> Prop
H: ~ exists x : A, P x
~ exists x : A, P x
    assumption.
Qed.

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

存在を排中律によって示す。

  -
P: Prop
exists x : bool, (P -> x = true) /\ (~ P -> x = false)
    destruct (excluded_middle P).
P: Prop
H: P
exists x : bool, (P -> x = true) /\ (~ P -> x = false)
P: Prop
H: ~ P
exists x : bool, (P -> x = true) /\ (~ P -> x = false)
    +
P: Prop
H: P
exists x : bool, (P -> x = true) /\ (~ P -> x = false)
      exists true.
P: Prop
H: P
(P -> true = true) /\ (~ P -> true = false)
      split.
P: Prop
H: P
P -> true = true
P: Prop
H: P
~ P -> true = false
      *
P: Prop
H: P
P -> true = true
        intro.
P: Prop
H, H0: P
true = true
        reflexivity.
      *
P: Prop
H: P
~ P -> true = false
        contradiction.
    +
P: Prop
H: ~ P
exists x : bool, (P -> x = true) /\ (~ P -> x = false)
      exists false.
P: Prop
H: ~ P
(P -> false = true) /\ (~ P -> false = false)
      split.
P: Prop
H: ~ P
P -> false = true
P: Prop
H: ~ P
~ P -> false = false
      *
P: Prop
H: ~ P
P -> false = true
        contradiction.
      *
P: Prop
H: ~ P
~ P -> false = false
        intro.
P: Prop
H, H0: ~ P
false = false
        reflexivity.

一意性も排中律によって示す。

  -
P: Prop
uniqueness (fun x : bool => (P -> x = true) /\ (~ P -> x = false))
    unfold uniqueness.
P: Prop
forall x y : bool,
(P -> x = true) /\ (~ P -> x = false) ->
(P -> y = true) /\ (~ P -> y = false) -> x = y
    intros.
P: Prop
x, y: bool
H: (P -> x = true) /\ (~ P -> x = false)
H0: (P -> y = true) /\ (~ P -> y = false)
x = y
    destruct H, H0.
P: Prop
x, y: bool
H: P -> x = true
H1: ~ P -> x = false
H0: P -> y = true
H2: ~ P -> y = false
x = y
    destruct (excluded_middle P).
P: Prop
x, y: bool
H: P -> x = true
H1: ~ P -> x = false
H0: P -> y = true
H2: ~ P -> y = false
H3: P
x = y
P: Prop
x, y: bool
H: P -> x = true
H1: ~ P -> x = false
H0: P -> y = true
H2: ~ P -> y = false
H3: ~ P
x = y
    +
P: Prop
x, y: bool
H: P -> x = true
H1: ~ P -> x = false
H0: P -> y = true
H2: ~ P -> y = false
H3: P
x = y
      specialize (H H3).
P: Prop
x, y: bool
H: x = true
H1: ~ P -> x = false
H0: P -> y = true
H2: ~ P -> y = false
H3: P
x = y
      specialize (H0 H3).
P: Prop
x, y: bool
H: x = true
H1: ~ P -> x = false
H0: y = true
H2: ~ P -> y = false
H3: P
x = y
      subst x y.
P: Prop
H1, H2: ~ P -> true = false
H3: P
true = true
      reflexivity.
    +
P: Prop
x, y: bool
H: P -> x = true
H1: ~ P -> x = false
H0: P -> y = true
H2: ~ P -> y = false
H3: ~ P
x = y
      specialize (H1 H3).
P: Prop
x, y: bool
H: P -> x = true
H1: x = false
H0: P -> y = true
H2: ~ P -> y = false
H3: ~ P
x = y
      specialize (H2 H3).
P: Prop
x, y: bool
H: P -> x = true
H1: x = false
H0: P -> y = true
H2: y = false
H3: ~ P
x = y
      subst x y.
P: Prop
H, H0: P -> false = true
H3: ~ P
false = false
      reflexivity.
Qed.

Definition prop_to_bool
  (P : Prop)
  : bool.
P: Prop
bool
Proof.
P: Prop
bool
  pose (constructive_definite_description _ (bool_by_cases P)) as s.
P: Prop
s:= constructive_definite_description
  (fun b : bool => (P -> b = true) /\ (~ P -> b = false)) 
  (bool_by_cases P): {x : bool | (fun b : bool => (P -> b = true) /\ (~ P -> b = false)) x}
bool
  exact (proj1_sig s).
Defined.

Lemma bool_by_cases_prf
  (P : Prop)
  : (P -> prop_to_bool P = true)
    /\ (~ P -> prop_to_bool P = false).
P: Prop
(P -> prop_to_bool P = true) /\ (~ P -> prop_to_bool P = false)
Proof.
P: Prop
(P -> prop_to_bool P = true) /\ (~ P -> prop_to_bool P = false)
  pose (constructive_definite_description _ (bool_by_cases P)) as s.
P: Prop
s:= constructive_definite_description
  (fun b : bool => (P -> b = true) /\ (~ P -> b = false)) 
  (bool_by_cases P): {x : bool | (fun b : bool => (P -> b = true) /\ (~ P -> b = false)) x}
(P -> prop_to_bool P = true) /\ (~ P -> prop_to_bool P = false)
  exact (proj2_sig s).
Qed.

Lemma Prop_is_retract_of_bool
  (P : Prop)
  : bool_to_prop (prop_to_bool P) = P.
P: Prop
bool_to_prop (prop_to_bool P) = P
Proof.
P: Prop
bool_to_prop (prop_to_bool P) = P
  pose proof (bool_by_cases_prf P).
P: Prop
H: (P -> prop_to_bool P = true) /\ (~ P -> prop_to_bool P = false)
bool_to_prop (prop_to_bool P) = P
  destruct H.
P: Prop
H: P -> prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
bool_to_prop (prop_to_bool P) = P
  destruct (excluded_middle P).
P: Prop
H: P -> prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
H1: P
bool_to_prop (prop_to_bool P) = P
P: Prop
H: P -> prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
H1: ~ P
bool_to_prop (prop_to_bool P) = P
  -
P: Prop
H: P -> prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
H1: P
bool_to_prop (prop_to_bool P) = P
    specialize (H H1).
P: Prop
H: prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
H1: P
bool_to_prop (prop_to_bool P) = P
    rewrite H.
P: Prop
H: prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
H1: P
bool_to_prop true = P
    simpl.
P: Prop
H: prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
H1: P
True = P
    symmetry.
P: Prop
H: prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
H1: P
P = True
    apply hypothesis_is_true.
P: Prop
H: prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
H1: P
P
    assumption.
  -
P: Prop
H: P -> prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
H1: ~ P
bool_to_prop (prop_to_bool P) = P
    specialize (H0 H1).
P: Prop
H: P -> prop_to_bool P = true
H0: prop_to_bool P = false
H1: ~ P
bool_to_prop (prop_to_bool P) = P
    rewrite H0.
P: Prop
H: P -> prop_to_bool P = true
H0: prop_to_bool P = false
H1: ~ P
bool_to_prop false = P
    simpl.
P: Prop
H: P -> prop_to_bool P = true
H0: prop_to_bool P = false
H1: ~ P
False = P
    symmetry.
P: Prop
H: P -> prop_to_bool P = true
H0: prop_to_bool P = false
H1: ~ P
P = False
    apply negated_hypothesis_is_false.
P: Prop
H: P -> prop_to_bool P = true
H0: prop_to_bool P = false
H1: ~ P
~ P
    assumption.
Qed.

Lemma bool_is_retract_of_Prop
  (b : bool)
  : prop_to_bool (bool_to_prop b) = b.
b: bool
prop_to_bool (bool_to_prop b) = b
Proof.
b: bool
prop_to_bool (bool_to_prop b) = b
  pose proof (bool_by_cases_prf (bool_to_prop b)).
b: bool
H: (bool_to_prop b -> prop_to_bool (bool_to_prop b) = true) /\
(~ bool_to_prop b -> prop_to_bool (bool_to_prop b) = false)
prop_to_bool (bool_to_prop b) = b
  destruct H.
b: bool
H: bool_to_prop b -> prop_to_bool (bool_to_prop b) = true
H0: ~ bool_to_prop b -> prop_to_bool (bool_to_prop b) = false
prop_to_bool (bool_to_prop b) = b
  destruct b.
H: bool_to_prop true -> prop_to_bool (bool_to_prop true) = true
H0: ~ bool_to_prop true -> prop_to_bool (bool_to_prop true) = false
prop_to_bool (bool_to_prop true) = true
H: bool_to_prop false -> prop_to_bool (bool_to_prop false) = true
H0: ~ bool_to_prop false -> prop_to_bool (bool_to_prop false) = false
prop_to_bool (bool_to_prop false) = false
  -
H: bool_to_prop true -> prop_to_bool (bool_to_prop true) = true
H0: ~ bool_to_prop true -> prop_to_bool (bool_to_prop true) = false
prop_to_bool (bool_to_prop true) = true
    simpl in *.
H: True -> prop_to_bool True = true
H0: ~ True -> prop_to_bool True = false
prop_to_bool True = true
    apply H.
H: True -> prop_to_bool True = true
H0: ~ True -> prop_to_bool True = false
True
    trivial.
  -
H: bool_to_prop false -> prop_to_bool (bool_to_prop false) = true
H0: ~ bool_to_prop false -> prop_to_bool (bool_to_prop false) = false
prop_to_bool (bool_to_prop false) = false
    simpl in *.
H: False -> prop_to_bool False = true
H0: ~ False -> prop_to_bool False = false
prop_to_bool False = false
    apply H0.
H: False -> prop_to_bool False = true
H0: ~ False -> prop_to_bool False = false
~ False
    apply trivially_not_false.
Qed.

Definition every_proposition_is_decidable
  (P : Prop)
  : P + (~ P).
P: Prop
P + (~ P)
Proof.
P: Prop
P + (~ P)
  destruct (bool_by_cases_prf P).
P: Prop
H: P -> prop_to_bool P = true
H0: ~ P -> prop_to_bool P = false
P + (~ P)
  destruct (prop_to_bool P).
P: Prop
H: P -> true = true
H0: ~ P -> true = false
P + (~ P)
P: Prop
H: P -> false = true
H0: ~ P -> false = false
P + (~ P)
  -
P: Prop
H: P -> true = true
H0: ~ P -> true = false
P + (~ P)
    apply inl.
P: Prop
H: P -> true = true
H0: ~ P -> true = false
P
    destruct (excluded_middle P).
P: Prop
H: P -> true = true
H0: ~ P -> true = false
H1: P
P
P: Prop
H: P -> true = true
H0: ~ P -> true = false
H1: ~ P
P
    +
P: Prop
H: P -> true = true
H0: ~ P -> true = false
H1: P
P
      assumption.
    +
P: Prop
H: P -> true = true
H0: ~ P -> true = false
H1: ~ P
P
      specialize (H0 H1).
P: Prop
H: P -> true = true
H0: true = false
H1: ~ P
P
      contradict H0.
P: Prop
H: P -> true = true
H1: ~ P
true <> false
      apply true_is_not_false.
  -
P: Prop
H: P -> false = true
H0: ~ P -> false = false
P + (~ P)
    apply inr.
P: Prop
H: P -> false = true
H0: ~ P -> false = false
~ P
    destruct (excluded_middle P).
P: Prop
H: P -> false = true
H0: ~ P -> false = false
H1: P
~ P
P: Prop
H: P -> false = true
H0: ~ P -> false = false
H1: ~ P
~ P
    +
P: Prop
H: P -> false = true
H0: ~ P -> false = false
H1: P
~ P
      specialize (H H1).
P: Prop
H: false = true
H0: ~ P -> false = false
H1: P
~ P
      contradict H.
P: Prop
H0: ~ P -> false = false
H1, H: P
false <> true
      symmetry.
P: Prop
H0: ~ P -> false = false
H1, H: P
true <> false
      apply true_is_not_false.
    +
P: Prop
H: P -> false = true
H0: ~ P -> false = false
H1: ~ P
~ P
      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.
general_definition_by_cases =
fun (P : Prop) (x : P -> A) (y : ~ P -> A) =>
match every_proposition_is_decidable P with
| inl p => x p
| inr q => y q
end
     : forall P : Prop, (P -> A) -> (~ P -> A) -> A

Arguments general_definition_by_cases P%_type_scope (x y)%_function_scope
general_definition_by_cases uses section variable A.

  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.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
forall p : P, general_definition_by_cases P x y = x p
  Proof.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
forall p : P, general_definition_by_cases P x y = x p
    unfold general_definition_by_cases.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
forall p : P,
match every_proposition_is_decidable P with
| inl p0 => x p0
| inr q => y q
end = x p
    destruct (every_proposition_is_decidable P).
A: Type
P: Prop
x: P -> A
y: ~ P -> A
p: P
forall p0 : P, x p = x p0
A: Type
P: Prop
x: P -> A
y: ~ P -> A
n: ~ P
forall p : P, y n = x p
    +
A: Type
P: Prop
x: P -> A
y: ~ P -> A
p: P
forall p0 : P, x p = x p0
      intro.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
p, p0: P
x p = x p0
      f_equal.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
p, p0: P
p = p0
      apply proof_irrelevance.
    +
A: Type
P: Prop
x: P -> A
y: ~ P -> A
n: ~ P
forall p : P, y n = x p
      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.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
forall q : ~ P, general_definition_by_cases P x y = y q
  Proof.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
forall q : ~ P, general_definition_by_cases P x y = y q
    unfold general_definition_by_cases.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
forall q : ~ P,
match every_proposition_is_decidable P with
| inl p => x p
| inr q0 => y q0
end = y q
    destruct (every_proposition_is_decidable P).
A: Type
P: Prop
x: P -> A
y: ~ P -> A
p: P
forall q : ~ P, x p = y q
A: Type
P: Prop
x: P -> A
y: ~ P -> A
n: ~ P
forall q : ~ P, y n = y q
    +
A: Type
P: Prop
x: P -> A
y: ~ P -> A
p: P
forall q : ~ P, x p = y q
      contradiction.
    +
A: Type
P: Prop
x: P -> A
y: ~ P -> A
n: ~ P
forall q : ~ P, y n = y q
      intro.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
n, q: ~ P
y n = y q
      f_equal.
A: Type
P: Prop
x: P -> A
y: ~ P -> A
n, q: ~ P
n = q
      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.
A: Type
P: Prop
x, y: A
P -> definition_by_cases = x
  Proof.
A: Type
P: Prop
x, y: A
P -> definition_by_cases = x
    intro.
A: Type
P: Prop
x, y: A
H: P
definition_by_cases = x
    unfold definition_by_cases.
A: Type
P: Prop
x, y: A
H: P
match every_proposition_is_decidable P with
| inl _ => x
| inr _ => y
end = x
    destruct (every_proposition_is_decidable P).
A: Type
P: Prop
x, y: A
H, p: P
x = x
A: Type
P: Prop
x, y: A
H: P
n: ~ P
y = x
    -
A: Type
P: Prop
x, y: A
H, p: P
x = x
      reflexivity.
    -
A: Type
P: Prop
x, y: A
H: P
n: ~ P
y = x
      contradiction.
  Qed.

  Lemma definition_by_cases_prf_2
    : ~ P -> definition_by_cases = y.
A: Type
P: Prop
x, y: A
~ P -> definition_by_cases = y
  Proof.
A: Type
P: Prop
x, y: A
~ P -> definition_by_cases = y
    intro.
A: Type
P: Prop
x, y: A
H: ~ P
definition_by_cases = y
    unfold definition_by_cases.
A: Type
P: Prop
x, y: A
H: ~ P
match every_proposition_is_decidable P with
| inl _ => x
| inr _ => y
end = y
    destruct (every_proposition_is_decidable P).
A: Type
P: Prop
x, y: A
H: ~ P
p: P
x = y
A: Type
P: Prop
x, y: A
H, n: ~ P
y = y
    -
A: Type
P: Prop
x, y: A
H: ~ P
p: P
x = y
      contradiction.
    -
A: Type
P: Prop
x, y: A
H, n: ~ P
y = y
      reflexivity.
  Qed.
End DefByCases.