|
| 1 | +/- |
| 2 | +Copyright (c) 2014 Microsoft Corporation. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn |
| 5 | +-/ |
| 6 | +import Mathlib.Tactic.TypeStar |
| 7 | + |
| 8 | +/-! |
| 9 | +# `ExistsUnique` |
| 10 | +
|
| 11 | +This file defines the `ExistsUnique` predicate, notated as `∃!`, and proves some of its |
| 12 | +basic properties. |
| 13 | +-/ |
| 14 | + |
| 15 | +variable {α : Sort*} |
| 16 | + |
| 17 | +/-- For `p : α → Prop`, `ExistsUnique p` means that there exists a unique `x : α` with `p x`. -/ |
| 18 | +def ExistsUnique (p : α → Prop) := ∃ x, p x ∧ ∀ y, p y → y = x |
| 19 | + |
| 20 | +namespace Mathlib.Notation |
| 21 | +open Lean |
| 22 | + |
| 23 | +/-- Checks to see that `xs` has only one binder. -/ |
| 24 | +def isExplicitBinderSingular (xs : TSyntax ``explicitBinders) : Bool := |
| 25 | + match xs with |
| 26 | + | `(explicitBinders| $_:binderIdent $[: $_]?) => true |
| 27 | + | `(explicitBinders| ($_:binderIdent : $_)) => true |
| 28 | + | _ => false |
| 29 | + |
| 30 | +open TSyntax.Compat in |
| 31 | +/-- |
| 32 | +`∃! x : α, p x` means that there exists a unique `x` in `α` such that `p x`. |
| 33 | +This is notation for `ExistsUnique (fun (x : α) ↦ p x)`. |
| 34 | +
|
| 35 | +This notation does not allow multiple binders like `∃! (x : α) (y : β), p x y` |
| 36 | +as a shorthand for `∃! (x : α), ∃! (y : β), p x y` since it is liable to be misunderstood. |
| 37 | +Often, the intended meaning is instead `∃! q : α × β, p q.1 q.2`. |
| 38 | +-/ |
| 39 | +macro "∃!" xs:explicitBinders ", " b:term : term => do |
| 40 | + if !isExplicitBinderSingular xs then |
| 41 | + Macro.throwErrorAt xs "\ |
| 42 | + The `ExistsUnique` notation should not be used with more than one binder.\n\ |
| 43 | + \n\ |
| 44 | + The reason for this is that `∃! (x : α), ∃! (y : β), p x y` has a completely different \ |
| 45 | + meaning from `∃! q : α × β, p q.1 q.2`. \ |
| 46 | + To prevent confusion, this notation requires that you be explicit \ |
| 47 | + and use one with the correct interpretation." |
| 48 | + expandExplicitBinders ``ExistsUnique xs b |
| 49 | + |
| 50 | +/-- |
| 51 | +Pretty-printing for `ExistsUnique`, following the same pattern as pretty printing for `Exists`. |
| 52 | +However, it does *not* merge binders. |
| 53 | +-/ |
| 54 | +@[app_unexpander ExistsUnique] def unexpandExistsUnique : Lean.PrettyPrinter.Unexpander |
| 55 | + | `($(_) fun $x:ident ↦ $b) => `(∃! $x:ident, $b) |
| 56 | + | `($(_) fun ($x:ident : $t) ↦ $b) => `(∃! $x:ident : $t, $b) |
| 57 | + | _ => throw () |
| 58 | + |
| 59 | +/-- |
| 60 | +`∃! x ∈ s, p x` means `∃! x, x ∈ s ∧ p x`, which is to say that there exists a unique `x ∈ s` |
| 61 | +such that `p x`. |
| 62 | +Similarly, notations such as `∃! x ≤ n, p n` are supported, |
| 63 | +using any relation defined using the `binder_predicate` command. |
| 64 | +-/ |
| 65 | +syntax "∃! " binderIdent binderPred ", " term : term |
| 66 | + |
| 67 | +macro_rules |
| 68 | + | `(∃! $x:ident $p:binderPred, $b) => `(∃! $x:ident, satisfies_binder_pred% $x $p ∧ $b) |
| 69 | + | `(∃! _ $p:binderPred, $b) => `(∃! x, satisfies_binder_pred% x $p ∧ $b) |
| 70 | + |
| 71 | +end Mathlib.Notation |
| 72 | + |
| 73 | +-- @[intro] -- TODO |
| 74 | +theorem ExistsUnique.intro {p : α → Prop} (w : α) |
| 75 | + (h₁ : p w) (h₂ : ∀ y, p y → y = w) : ∃! x, p x := ⟨w, h₁, h₂⟩ |
| 76 | + |
| 77 | +theorem ExistsUnique.elim {p : α → Prop} {b : Prop} |
| 78 | + (h₂ : ∃! x, p x) (h₁ : ∀ x, p x → (∀ y, p y → y = x) → b) : b := |
| 79 | + Exists.elim h₂ (fun w hw ↦ h₁ w (And.left hw) (And.right hw)) |
| 80 | + |
| 81 | +theorem exists_unique_of_exists_of_unique {p : α → Prop} |
| 82 | + (hex : ∃ x, p x) (hunique : ∀ y₁ y₂, p y₁ → p y₂ → y₁ = y₂) : ∃! x, p x := |
| 83 | + Exists.elim hex (fun x px ↦ ExistsUnique.intro x px (fun y (h : p y) ↦ hunique y x h px)) |
| 84 | + |
| 85 | +theorem ExistsUnique.exists {p : α → Prop} : (∃! x, p x) → ∃ x, p x | ⟨x, h, _⟩ => ⟨x, h⟩ |
| 86 | + |
| 87 | +theorem ExistsUnique.unique {p : α → Prop} |
| 88 | + (h : ∃! x, p x) {y₁ y₂ : α} (py₁ : p y₁) (py₂ : p y₂) : y₁ = y₂ := |
| 89 | + let ⟨_, _, hy⟩ := h; (hy _ py₁).trans (hy _ py₂).symm |
| 90 | + |
| 91 | +-- TODO |
| 92 | +-- attribute [congr] forall_congr' |
| 93 | +-- attribute [congr] exists_congr' |
| 94 | + |
| 95 | +-- @[congr] |
| 96 | +theorem existsUnique_congr {p q : α → Prop} (h : ∀ a, p a ↔ q a) : (∃! a, p a) ↔ ∃! a, q a := |
| 97 | + exists_congr fun _ ↦ and_congr (h _) <| forall_congr' fun _ ↦ imp_congr_left (h _) |
| 98 | + |
| 99 | +@[simp] theorem exists_unique_iff_exists [Subsingleton α] {p : α → Prop} : |
| 100 | + (∃! x, p x) ↔ ∃ x, p x := |
| 101 | + ⟨fun h ↦ h.exists, Exists.imp fun x hx ↦ ⟨hx, fun y _ ↦ Subsingleton.elim y x⟩⟩ |
| 102 | + |
| 103 | +theorem exists_unique_const {b : Prop} (α : Sort*) [i : Nonempty α] [Subsingleton α] : |
| 104 | + (∃! _ : α, b) ↔ b := by simp |
| 105 | + |
| 106 | +@[simp] theorem exists_unique_eq {a' : α} : ∃! a, a = a' := by |
| 107 | + simp only [eq_comm, ExistsUnique, and_self, forall_eq', exists_eq'] |
| 108 | + |
| 109 | +@[simp] theorem exists_unique_eq' {a' : α} : ∃! a, a' = a := by |
| 110 | + simp only [ExistsUnique, and_self, forall_eq', exists_eq'] |
| 111 | + |
| 112 | +theorem exists_unique_prop {p q : Prop} : (∃! _ : p, q) ↔ p ∧ q := by simp |
| 113 | + |
| 114 | +@[simp] theorem exists_unique_false : ¬∃! _ : α, False := fun ⟨_, h, _⟩ ↦ h |
| 115 | + |
| 116 | +theorem exists_unique_prop_of_true {p : Prop} {q : p → Prop} (h : p) : (∃! h' : p, q h') ↔ q h := |
| 117 | + @exists_unique_const (q h) p ⟨h⟩ _ |
| 118 | + |
| 119 | +theorem ExistsUnique.elim₂ {p : α → Sort*} [∀ x, Subsingleton (p x)] |
| 120 | + {q : ∀ (x) (_ : p x), Prop} {b : Prop} (h₂ : ∃! x, ∃! h : p x, q x h) |
| 121 | + (h₁ : ∀ (x) (h : p x), q x h → (∀ (y) (hy : p y), q y hy → y = x) → b) : b := by |
| 122 | + simp only [exists_unique_iff_exists] at h₂ |
| 123 | + apply h₂.elim |
| 124 | + exact fun x ⟨hxp, hxq⟩ H ↦ h₁ x hxp hxq fun y hyp hyq ↦ H y ⟨hyp, hyq⟩ |
| 125 | + |
| 126 | +theorem ExistsUnique.intro₂ {p : α → Sort*} [∀ x, Subsingleton (p x)] |
| 127 | + {q : ∀ (x : α) (_ : p x), Prop} (w : α) (hp : p w) (hq : q w hp) |
| 128 | + (H : ∀ (y) (hy : p y), q y hy → y = w) : ∃! x, ∃! hx : p x, q x hx := by |
| 129 | + simp only [exists_unique_iff_exists] |
| 130 | + exact ExistsUnique.intro w ⟨hp, hq⟩ fun y ⟨hyp, hyq⟩ ↦ H y hyp hyq |
| 131 | + |
| 132 | +theorem ExistsUnique.exists₂ {p : α → Sort*} {q : ∀ (x : α) (_ : p x), Prop} |
| 133 | + (h : ∃! x, ∃! hx : p x, q x hx) : ∃ (x : _) (hx : p x), q x hx := |
| 134 | + h.exists.imp fun _ hx ↦ hx.exists |
| 135 | + |
| 136 | +theorem ExistsUnique.unique₂ {p : α → Sort*} [∀ x, Subsingleton (p x)] |
| 137 | + {q : ∀ (x : α) (_ : p x), Prop} (h : ∃! x, ∃! hx : p x, q x hx) {y₁ y₂ : α} |
| 138 | + (hpy₁ : p y₁) (hqy₁ : q y₁ hpy₁) (hpy₂ : p y₂) (hqy₂ : q y₂ hpy₂) : y₁ = y₂ := by |
| 139 | + simp only [exists_unique_iff_exists] at h |
| 140 | + exact h.unique ⟨hpy₁, hqy₁⟩ ⟨hpy₂, hqy₂⟩ |
0 commit comments