From 20f6b4c6bd53fca808bffcf6640b237a2a7b5e2d Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sat, 12 Sep 2015 08:16:13 -0400
Subject: [PATCH] feat(library/logic/quantifiers): add 'the'

---
 library/logic/quantifiers.lean | 77 ++++++++++++++++++++++++----------
 1 file changed, 56 insertions(+), 21 deletions(-)

diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean
index edf1c6ef22..0665e5cfe9 100644
--- a/library/logic/quantifiers.lean
+++ b/library/logic/quantifiers.lean
@@ -14,43 +14,43 @@ iff.intro (λ e x H, e (exists.intro x H)) Exists.rec
 theorem forall_iff_not_exists {A : Type} {P : A → Prop} : (¬ ∃ a : A, P a) ↔ ∀ a : A, ¬ P a :=
 exists_imp_distrib
 
-theorem not_forall_not_of_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬∀x, ¬p x :=
-assume H1 : ∀x, ¬p x,
+theorem not_forall_not_of_exists {A : Type} {p : A → Prop} (H : ∃x, p x) : ¬ ∀ x, ¬ p x :=
+assume H1 : ∀ x, ¬ p x,
   obtain (w : A) (Hw : p w), from H,
   absurd Hw (H1 w)
 
-theorem not_exists_not_of_forall {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬∃x, ¬p x :=
-assume H1 : ∃x, ¬p x,
-  obtain (w : A) (Hw : ¬p w), from H1,
+theorem not_exists_not_of_forall {A : Type} {p : A → Prop} (H2 : ∀x, p x) : ¬ ∃ x, ¬p x :=
+assume H1 : ∃ x, ¬ p x,
+  obtain (w : A) (Hw : ¬ p w), from H1,
   absurd (H2 w) Hw
 
-theorem forall_congr {A : Type} {φ ψ : A → Prop} : (∀x, φ x ↔ ψ x) → ((∀x, φ x) ↔ (∀x, ψ x)) :=
+theorem forall_congr {A : Type} {φ ψ : A → Prop} : (∀ x, φ x ↔ ψ x) → ((∀ x, φ x) ↔ (∀ x, ψ x)) :=
 forall_iff_forall
 
-theorem exists_congr {A : Type} {φ ψ : A → Prop} : (∀x, φ x ↔ ψ x) → ((∃x, φ x) ↔ (∃x, ψ x)) :=
+theorem exists_congr {A : Type} {φ ψ : A → Prop} : (∀ x, φ x ↔ ψ x) → ((∃ x, φ x) ↔ (∃ x, ψ x)) :=
 exists_iff_exists
 
-theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true :=
+theorem forall_true_iff_true (A : Type) : (∀ x : A, true) ↔ true :=
 iff_true_intro (λH, trivial)
 
-theorem forall_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∀x : A, p) ↔ p :=
-iff.intro (inhabited.destruct H) (λHr x, Hr)
+theorem forall_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∀ x : A, p) ↔ p :=
+iff.intro (inhabited.destruct H) (λ Hr x, Hr)
 
-theorem exists_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∃x : A, p) ↔ p :=
-iff.intro (Exists.rec (λx Hp, Hp)) (inhabited.destruct H exists.intro)
+theorem exists_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∃ x : A, p) ↔ p :=
+iff.intro (Exists.rec (λ x Hp, Hp)) (inhabited.destruct H exists.intro)
 
 theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) :
-  (∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
+  (∀ x, φ x ∧ ψ x) ↔ (∀ x, φ x) ∧ (∀ x, ψ x) :=
 iff.intro
   (assume H, and.intro (take x, and.left (H x)) (take x, and.right (H x)))
   (assume H x, and.intro (and.left H x) (and.right H x))
 
 theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) :
-  (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) :=
+  (∃ x, φ x ∨ ψ x) ↔ (∃ x, φ x) ∨ (∃ x, ψ x) :=
 iff.intro
-  (Exists.rec (λx, or.imp !exists.intro !exists.intro))
-  (or.rec (exists_imp_exists (λx, or.inl))
-          (exists_imp_exists (λx, or.inr)))
+  (Exists.rec (λ x, or.imp !exists.intro !exists.intro))
+  (or.rec (exists_imp_exists (λ x, or.inl))
+          (exists_imp_exists (λ x, or.inr)))
 
 section
   open decidable eq.ops
@@ -83,19 +83,54 @@ theorem exists_unique.elim {A : Type} {p : A → Prop} {b : Prop}
 obtain w Hw, from H2,
 H1 w (and.left Hw) (and.right Hw)
 
+theorem exists_unique_of_exists_of_unique {A : Type} {p : A → Prop}
+    (Hex : ∃ x, p x) (Hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) :
+  ∃! x, p x :=
+obtain x px, from Hex,
+exists_unique.intro x px (take y, suppose p y, show y = x, from !Hunique this px)
+
+theorem exists_of_exists_unique {A : Type} {p : A → Prop} (H : ∃! x, p x) :
+  ∃ x, p x :=
+obtain x Hx, from H,
+exists.intro x (and.left Hx)
+
+theorem unique_of_exists_unique {A : Type} {p : A → Prop}
+    (H : ∃! x, p x) {y₁ y₂ : A} (py₁ : p y₁) (py₂ : p y₂) :
+  y₁ = y₂ :=
+exists_unique.elim H
+  (take x, suppose p x,
+    assume unique : ∀ y, p y → y = x,
+    show y₁ = y₂, from eq.trans (unique _ py₁) (eq.symm (unique _ py₂)))
+
+/- definite description -/
+
+section
+  open classical
+
+  noncomputable definition the {A : Type} {p : A → Prop} (H : ∃! x, p x) : A :=
+  some (exists_of_exists_unique H)
+
+  theorem the_spec {A : Type} {p : A → Prop} (H : ∃! x, p x) : p (the H) :=
+  some_spec (exists_of_exists_unique H)
+
+  theorem eq_the {A : Type} {p : A → Prop} (H : ∃! x, p x) {y : A} (Hy : p y) :
+    y = the H :=
+  unique_of_exists_unique H Hy (the_spec H)
+end
+
 /- congruences -/
 
 section
-  variables {A : Type} {p₁ p₂ : A → Prop} (H : ∀x, p₁ x ↔ p₂ x)
+  variables {A : Type} {p₁ p₂ : A → Prop} (H : ∀ x, p₁ x ↔ p₂ x)
 
-  theorem congr_forall : (∀x, p₁ x) ↔ (∀x, p₂ x) :=
+  theorem congr_forall : (∀ x, p₁ x) ↔ (∀ x, p₂ x) :=
   forall_congr H
 
-  theorem congr_exists : (∃x, p₁ x) ↔ (∃x, p₂ x) :=
+  theorem congr_exists : (∃ x, p₁ x) ↔ (∃ x, p₂ x) :=
   exists_congr H
 
   include H
-  theorem congr_exists_unique : (∃!x, p₁ x) ↔ (∃!x, p₂ x) :=
+  theorem congr_exists_unique : (∃! x, p₁ x) ↔ (∃! x, p₂ x) :=
    congr_exists (λx, congr_and (H x) (congr_forall
      (λy, congr_imp (H y) iff.rfl)))
 end