From 218c1dd308f1f67dec3ebfd6957f3cccc419b69f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Fri, 11 Aug 2017 17:57:57 -0400 Subject: [PATCH] algebra/lattice/filter: cleanup move theorems to appropriate places --- algebra/lattice/boolean_algebra.lean | 24 +++ algebra/lattice/filter.lean | 265 +-------------------------- category/basic.lean | 37 ++++ data/prod.lean | 29 +++ data/set/basic.lean | 62 ++++++- data/set/default.lean | 2 +- data/set/lattice.lean | 69 ++++++- data/set/prod.lean | 73 ++++++++ logic/basic.lean | 12 ++ topology/topological_space.lean | 21 +-- topology/uniform_space.lean | 6 +- 11 files changed, 312 insertions(+), 288 deletions(-) create mode 100644 category/basic.lean create mode 100644 data/prod.lean create mode 100644 data/set/prod.lean diff --git a/algebra/lattice/boolean_algebra.lean b/algebra/lattice/boolean_algebra.lean index 8fa3f77dbf7fb..cca9d8c9cbdab 100644 --- a/algebra/lattice/boolean_algebra.lean +++ b/algebra/lattice/boolean_algebra.lean @@ -39,10 +39,34 @@ calc x ⊓ (y ⊔ z) = (x ⊓ (x ⊔ z)) ⊓ (y ⊔ z) : by rw [inf_sup_se theorem inf_sup_right : (y ⊔ z) ⊓ x = (y ⊓ x) ⊔ (z ⊓ x) := by simp [inf_sup_left, λy:α, @inf_comm α _ y x] +lemma eq_of_sup_eq_inf_eq {α : Type u} [distrib_lattice α] {a b c : α} + (h₁ : b ⊓ a = c ⊓ a) (h₂ : b ⊔ a = c ⊔ a) : b = c := +le_antisymm + (calc b ≤ (c ⊓ a) ⊔ b : le_sup_right + ... = (c ⊔ b) ⊓ (a ⊔ b) : sup_inf_right + ... = c ⊔ (c ⊓ a) : by rw [←h₁, sup_inf_left, ←h₂]; simp [sup_comm] + ... = c : sup_inf_self) + (calc c ≤ (b ⊓ a) ⊔ c : le_sup_right + ... = (b ⊔ c) ⊓ (a ⊔ c) : sup_inf_right + ... = b ⊔ (b ⊓ a) : by rw [h₁, sup_inf_left, h₂]; simp [sup_comm] + ... = b : sup_inf_self) + end distrib_lattice class bounded_distrib_lattice α extends distrib_lattice α, bounded_lattice α +lemma inf_eq_bot_iff_le_compl {α : Type u} [bounded_distrib_lattice α] {a b c : α} + (h₁ : b ⊔ c = ⊤) (h₂ : b ⊓ c = ⊥) : a ⊓ b = ⊥ ↔ a ≤ c := +⟨assume : a ⊓ b = ⊥, + calc a ≤ a ⊓ (b ⊔ c) : by simp [h₁] + ... = (a ⊓ b) ⊔ (a ⊓ c) : by simp [inf_sup_left] + ... ≤ c : by simp [this, inf_le_right], + assume : a ≤ c, + bot_unique $ + calc a ⊓ b ≤ b ⊓ c : by rw [inf_comm]; exact inf_le_inf (le_refl _) this + ... = ⊥ : h₂⟩ + + class boolean_algebra α extends bounded_distrib_lattice α, has_neg α, has_sub α := (inf_neg_eq_bot : ∀x:α, x ⊓ - x = ⊥) (sup_neg_eq_top : ∀x:α, x ⊔ - x = ⊤) diff --git a/algebra/lattice/filter.lean b/algebra/lattice/filter.lean index ed7bc7f10abe8..1299be2903b98 100644 --- a/algebra/lattice/filter.lean +++ b/algebra/lattice/filter.lean @@ -14,61 +14,7 @@ open set classical local attribute [instance] decidable_inhabited local attribute [instance] prop_decidable -lemma classical.cases {p : Prop → Prop} (h1 : p true) (h2 : p false) : ∀a, p a := -assume a, classical.cases_on a h1 h2 - -@[simp] lemma false_neq_true : false ≠ true := -begin intro h, rw [h], trivial end - -section applicative -variables {f : Type u → Type v} [applicative f] {α β : Type u} - -lemma pure_seq_eq_map : ∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x := -@applicative.pure_seq_eq_map f _ - -end applicative - -section monad -variables {α β γ : Type u} {m : Type u → Type v} [monad m] - -lemma map_bind (x : m α) {g : α → m β} {f : β → γ} : f <$> (x >>= g) = (x >>= λa, f <$> g a) := -by simp [monad.bind_assoc, (∘), (monad.bind_pure_comp_eq_map _ _ _).symm] - -lemma seq_bind_eq (x : m α) {g : β → m γ} {f : α → β} : (f <$> x) >>= g = (x >>= g ∘ f) := -show bind (f <$> x) g = bind x (g ∘ f), -by rw [←monad.bind_pure_comp_eq_map, monad.bind_assoc]; simp [monad.pure_bind] - -lemma seq_eq_bind_map {x : m α} {f : m (α → β)} : f <*> x = (f >>= (<$> x)) := -(monad.bind_map_eq_seq m f x).symm - -lemma bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), - x >>= f >>= g = x >>= λ x, f x >>= g := -@monad.bind_assoc m _ - -end monad - -section prod -variables {α : Type u} {β : Type v} - --- copied from parser -@[simp] lemma prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p -| (a, b) := rfl - -def prod.swap : (α×β) → (β×α) := λp, (p.2, p.1) - -@[simp] lemma prod.swap_swap : ∀x:α×β, prod.swap (prod.swap x) = x -| ⟨a, b⟩ := rfl - -@[simp] lemma prod.fst_swap {p : α×β} : (prod.swap p).1 = p.2 := rfl - -@[simp] lemma prod.snd_swap {p : α×β} : (prod.swap p).2 = p.1 := rfl - -@[simp] lemma prod.swap_prod_mk {a : α} {b : β} : prod.swap (a, b) = (b, a) := rfl - -@[simp] lemma prod.swap_swap_eq : prod.swap ∘ prod.swap = @id (α × β) := -funext $ prod.swap_swap - -end prod +-- should be handled by implies_true_iff namespace lattice variables {α : Type u} {ι : Sort v} [complete_lattice α] @@ -81,229 +27,20 @@ le_antisymm end lattice -instance : monad set := -{ monad . - pure := λ(α : Type u) a, {a}, - bind := λ(α β : Type u) s f, ⋃i∈s, f i, - map := λ(α β : Type u), set.image, - pure_bind := assume α β x f, by simp, - bind_assoc := assume α β γ s f g, set.ext $ assume a, - by simp; exact ⟨assume ⟨b, ag, a, as, bf⟩, ⟨a, as, b, bf, ag⟩, - assume ⟨a, as, b, bf, ag⟩, ⟨b, ag, a, as, bf⟩⟩, - id_map := assume α, functor.id_map, - bind_pure_comp_eq_map := assume α β f s, set.ext $ by simp [set.image, eq_comm] } - namespace set -section -variables {α β : Type u} - -@[simp] lemma bind_def (s : set α) (f : α → set β) : s >>= f = ⋃i∈s, f i := rfl - -lemma ne_empty_iff_exists_mem {s : set α} : s ≠ ∅ ↔ ∃ x, x ∈ s := -⟨exists_mem_of_ne_empty, assume ⟨x, (hx : x ∈ s)⟩ h, by rw [h] at hx; assumption⟩ - -lemma fmap_eq_image {f : α → β} {s : set α} : f <$> s = f '' s := rfl - -lemma mem_seq_iff {f : set (α → β)} {s : set α} {b : β} : - b ∈ (f <*> s) ↔ (∃(f' : α → β), ∃a ∈ s, f' ∈ f ∧ b = f' a) := -begin - simp [seq_eq_bind_map], - apply exists_congr, - intro f', - exact ⟨assume ⟨hf', a, ha, h_eq⟩, ⟨a, h_eq.symm, ha, hf'⟩, - assume ⟨a, h_eq, ha, hf'⟩, ⟨hf', a, ha, h_eq.symm⟩⟩ -end - -lemma univ_eq_true_false : univ = ({true, false} : set Prop) := -eq.symm $ top_unique $ classical.cases (by simp) (by simp) - -end - variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort y} -lemma not_eq_empty_iff_exists {s : set α} : ¬ (s = ∅) ↔ ∃ x, x ∈ s := -ne_empty_iff_exists_mem - -lemma image_inter {f : α → β} {s t : set α} (h : ∀ x y, f x = f y → x = y) : - f '' s ∩ f '' t = f '' (s ∩ t) := -subset.antisymm - (assume b ⟨⟨a₁, ha₁, h₁⟩, ⟨a₂, ha₂, h₂⟩⟩, - have a₂ = a₁, from h a₂ a₁ $ h₁.symm ▸ h₂.symm ▸ rfl, - ⟨a₁, ⟨ha₁, this ▸ ha₂⟩, h₁⟩) - (subset_inter (mono_image $ inter_subset_left _ _) (mono_image $ inter_subset_right _ _)) - -lemma image_Union {f : α → β} {s : ι → set α} : f '' (⋃ i, s i) = (⋃i, f '' s i) := -begin - apply set.ext, intro x, - simp [image], - exact ⟨assume ⟨a, h, i, hi⟩, ⟨i, a, h, hi⟩, assume ⟨i, a, h, hi⟩, ⟨a, h, i, hi⟩⟩ -end - -@[simp] lemma image_singleton {f : α → β} {a : α} : f '' {a} = {f a} := -begin - apply set.ext, intro x, - simp [image], - exact ⟨assume ⟨a', ha', hx⟩, hx ▸ ha' ▸ rfl, assume h, ⟨a, rfl, h.symm⟩⟩ -end - -protected def prod (s : set α) (t : set β) : set (α × β) := -{p | p.1 ∈ s ∧ p.2 ∈ t} - -lemma mem_prod_eq {s : set α} {t : set β} {p : α × β} : - p ∈ set.prod s t = (p.1 ∈ s ∧ p.2 ∈ t) := rfl - -theorem prod_preimage_eq {s : set α} {t : set β} {f : γ → α} {g : δ → β} : - set.prod (preimage f s) (preimage g t) = preimage (λp, (f p.1, g p.2)) (set.prod s t) := rfl - -lemma prod_mono {s₁ s₂ : set α} {t₁ t₂ : set β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : - set.prod s₁ t₁ ⊆ set.prod s₂ t₂ := -assume x ⟨h₁, h₂⟩, ⟨hs h₁, ht h₂⟩ - -lemma prod_inter_prod {s₁ s₂ : set α} {t₁ t₂ : set β} : - set.prod s₁ t₁ ∩ set.prod s₂ t₂ = set.prod (s₁ ∩ s₂) (t₁ ∩ t₂) := -subset.antisymm - (assume ⟨a, b⟩ ⟨⟨ha₁, hb₁⟩, ⟨ha₂, hb₂⟩⟩, ⟨⟨ha₁, ha₂⟩, ⟨hb₁, hb₂⟩⟩) - (subset_inter - (prod_mono (inter_subset_left _ _) (inter_subset_left _ _)) - (prod_mono (inter_subset_right _ _) (inter_subset_right _ _))) - -theorem monotone_prod [preorder α] {f : α → set β} {g : α → set γ} - (hf : monotone f) (hg : monotone g) : monotone (λx, set.prod (f x) (g x)) := -assume a b h, prod_mono (hf h) (hg h) - -lemma image_swap_prod {s : set α} {t : set β} : - image (λp:β×α, (p.2, p.1)) (set.prod t s) = set.prod s t := -set.ext $ assume ⟨a, b⟩, by simp [mem_image_eq, set.prod]; exact -⟨ assume ⟨b', a', h_a, h_b, h⟩, by rw [h_a, h_b] at h; assumption, - assume ⟨ha, hb⟩, ⟨b, a, rfl, rfl, ⟨ha, hb⟩⟩⟩ - -lemma prod_image_image_eq {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} - {s₁ : set α₁} {s₂ : set α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} : - set.prod (image m₁ s₁) (image m₂ s₂) = image (λp:α₁×α₂, (m₁ p.1, m₂ p.2)) (set.prod s₁ s₂) := -set.ext $ assume ⟨b₁, b₂⟩, - ⟨assume ⟨⟨a₁, ha₁, (eq₁ : m₁ a₁ = b₁)⟩, ⟨a₂, ha₂, (eq₂ : m₂ a₂ = b₂)⟩⟩, - mem_image - (show (a₁, a₂) ∈ set.prod s₁ s₂, from ⟨ha₁, ha₂⟩) - (by simp [eq₁, eq₂]), - assume ⟨⟨a₁, a₂⟩, ⟨ha₁, ha₂⟩, eq⟩, eq ▸ ⟨mem_image_of_mem m₁ ha₁, mem_image_of_mem m₂ ha₂⟩⟩ - -@[simp] lemma prod_singleton_singleton {a : α} {b : β} : - set.prod {a} {b} = ({(a, b)} : set (α×β)) := -set.ext $ assume ⟨a', b'⟩, by simp [set.prod] - -lemma prod_neq_empty_iff {s : set α} {t : set β} : - set.prod s t ≠ ∅ ↔ (s ≠ ∅ ∧ t ≠ ∅) := -begin - rw [ne_empty_iff_exists_mem, ne_empty_iff_exists_mem, ne_empty_iff_exists_mem, - prod.exists], - exact ⟨assume ⟨a, b, ha, hb⟩, ⟨⟨a, ha⟩, ⟨b, hb⟩⟩, - assume ⟨⟨a, ha⟩, ⟨b, hb⟩⟩, ⟨a, b, ha, hb⟩⟩ -end - -@[simp] lemma prod_mk_mem_set_prod_eq {a : α} {b : β} {s : set α} {t : set β} : - (a, b) ∈ set.prod s t = (a ∈ s ∧ b ∈ t) := rfl - theorem monotone_inter [preorder β] {f g : β → set α} (hf : monotone f) (hg : monotone g) : monotone (λx, (f x) ∩ (g x)) := assume a b h x ⟨h₁, h₂⟩, ⟨hf h h₁, hg h h₂⟩ -@[simp] theorem preimage_set_of_eq {p : α → Prop} {f : β → α} : - preimage f {a | p a} = {a | p (f a)} := rfl - -@[simp] lemma set_of_mem_eq {s : set α} : {x | x ∈ s} = s := rfl - -theorem image_swap_eq_preimage_swap : image (@prod.swap α β) = preimage prod.swap := -image_eq_preimage_of_inverse (@prod.swap α β) (@prod.swap β α) - begin simp; intros; trivial end - begin simp; intros; trivial end - theorem monotone_set_of [preorder α] {p : α → β → Prop} (hp : ∀b, monotone (λa, p a b)) : monotone (λa, {b | p a b}) := assume a a' h b, hp b h -lemma diff_right_antimono {s t u : set α} (h : t ⊆ u) : s - u ⊆ s - t := -assume x ⟨hs, hnx⟩, ⟨hs, assume hx, hnx $ h hx⟩ - end set -section -variables {α : Type u} {ι : Sort v} - -lemma sUnion_mono {s t : set (set α)} (h : s ⊆ t) : (⋃₀ s) ⊆ (⋃₀ t) := -sUnion_subset $ assume t' ht', subset_sUnion_of_mem $ h ht' - -lemma Union_subset_Union {s t : ι → set α} (h : ∀i, s i ⊆ t i) : (⋃i, s i) ⊆ (⋃i, t i) := -@supr_le_supr (set α) ι _ s t h - -lemma Union_subset_Union2 {ι₂ : Sort x} {s : ι → set α} {t : ι₂ → set α} (h : ∀i, ∃j, s i ⊆ t j) : - (⋃i, s i) ⊆ (⋃i, t i) := -@supr_le_supr2 (set α) ι ι₂ _ s t h - -lemma Union_subset_Union_const {ι₂ : Sort x} {s : set α} (h : ι → ι₂) : (⋃ i:ι, s) ⊆ (⋃ j:ι₂, s) := -@supr_le_supr_const (set α) ι ι₂ _ s h - -lemma diff_neq_empty {s t : set α} : s - t = ∅ ↔ s ⊆ t := -⟨assume h x hx, classical.by_contradiction $ assume : x ∉ t, show x ∈ (∅ : set α), from h ▸ ⟨hx, this⟩, - assume h, bot_unique $ assume x ⟨hx, hnx⟩, hnx $ h hx⟩ - -@[simp] lemma diff_empty {s : set α} : s - ∅ = s := -set.ext $ assume x, ⟨assume ⟨hx, _⟩, hx, assume h, ⟨h, not_false⟩⟩ - -end - --- should be handled by implies_true_iff -@[simp] lemma implies_implies_true_iff {α : Sort u} {β : Sort v} : (α → β → true) ↔ true := -⟨assume _, trivial, assume _ _ _ , trivial⟩ - -@[simp] lemma not_not_mem_iff {α : Type u} {a : α} {s : set α} : ¬ (a ∉ s) ↔ a ∈ s := -not_not_iff - -@[simp] lemma singleton_neq_emptyset {α : Type u} {a : α} : {a} ≠ (∅ : set α) := -assume h, -have a ∉ ({a} : set α), - by simp [h], -this $ mem_singleton a - -lemma eq_of_sup_eq_inf_eq {α : Type u} [distrib_lattice α] {a b c : α} - (h₁ : b ⊓ a = c ⊓ a) (h₂ : b ⊔ a = c ⊔ a) : b = c := -le_antisymm - (calc b ≤ (c ⊓ a) ⊔ b : le_sup_right - ... = (c ⊔ b) ⊓ (a ⊔ b) : sup_inf_right - ... = c ⊔ (c ⊓ a) : by rw [←h₁, sup_inf_left, ←h₂]; simp [sup_comm] - ... = c : sup_inf_self) - (calc c ≤ (b ⊓ a) ⊔ c : le_sup_right - ... = (b ⊔ c) ⊓ (a ⊔ c) : sup_inf_right - ... = b ⊔ (b ⊓ a) : by rw [h₁, sup_inf_left, h₂]; simp [sup_comm] - ... = b : sup_inf_self) - -lemma inf_eq_bot_iff_le_compl {α : Type u} [bounded_distrib_lattice α] {a b c : α} - (h₁ : b ⊔ c = ⊤) (h₂ : b ⊓ c = ⊥) : a ⊓ b = ⊥ ↔ a ≤ c := -⟨assume : a ⊓ b = ⊥, - calc a ≤ a ⊓ (b ⊔ c) : by simp [h₁] - ... = (a ⊓ b) ⊔ (a ⊓ c) : by simp [inf_sup_left] - ... ≤ c : by simp [this, inf_le_right], - assume : a ≤ c, - bot_unique $ - calc a ⊓ b ≤ b ⊓ c : by rw [inf_comm]; exact inf_le_inf (le_refl _) this - ... = ⊥ : h₂⟩ - -lemma compl_image_set_of {α : Type u} {p : set α → Prop} : - compl '' {x | p x} = {x | p (- x)} := -set.ext $ assume x, ⟨assume ⟨y, (hy : p y), (h_eq : -y = x)⟩, - show p (- x), by rw [←h_eq, lattice.neg_neg]; assumption, - assume h : p (-x), ⟨_, h, lattice.neg_neg⟩⟩ - -lemma neg_subset_neg_iff_subset {α : Type u} {x y : set α} : - y ⊆ - x ↔ x ⊆ y := -@neg_le_neg_iff_le (set α) _ _ _ - -lemma sUnion_eq_Union {α : Type u} {s : set (set α)} : - (⋃₀ s) = (⋃ (i : set α) (h : i ∈ s), i) := -set.ext $ by simp - -lemma not_or_iff_implies {a b : Prop} : (¬ a ∨ b) ↔ (a → b) := -⟨assume h ha, h.neg_resolve_left ha, not_or_of_implies⟩ - section order variables {α : Type u} (r : α → α → Prop) local infix `≼` : 50 := r diff --git a/category/basic.lean b/category/basic.lean new file mode 100644 index 0000000000000..12b64227d15fb --- /dev/null +++ b/category/basic.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2017 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl + +Extends the theory on functors, applicatives and monads. +-/ + +universes u v w x y +variables {α β γ : Type u} + +section applicative +variables {f : Type u → Type v} [applicative f] + +lemma pure_seq_eq_map : ∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x := +@applicative.pure_seq_eq_map f _ + +end applicative + +section monad +variables {m : Type u → Type v} [monad m] + +lemma map_bind (x : m α) {g : α → m β} {f : β → γ} : f <$> (x >>= g) = (x >>= λa, f <$> g a) := +by simp [monad.bind_assoc, (∘), (monad.bind_pure_comp_eq_map _ _ _).symm] + +lemma seq_bind_eq (x : m α) {g : β → m γ} {f : α → β} : (f <$> x) >>= g = (x >>= g ∘ f) := +show bind (f <$> x) g = bind x (g ∘ f), +by rw [←monad.bind_pure_comp_eq_map, monad.bind_assoc]; simp [monad.pure_bind] + +lemma seq_eq_bind_map {x : m α} {f : m (α → β)} : f <*> x = (f >>= (<$> x)) := +(monad.bind_map_eq_seq m f x).symm + +lemma bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), + x >>= f >>= g = x >>= λ x, f x >>= g := +@monad.bind_assoc m _ + +end monad diff --git a/data/prod.lean b/data/prod.lean new file mode 100644 index 0000000000000..b0ec4377d19b2 --- /dev/null +++ b/data/prod.lean @@ -0,0 +1,29 @@ +/- +Copyright (c) 2017 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl + +Extends theory on products +-/ + +universes u v +variables {α : Type u} {β : Type v} + +-- copied from parser +@[simp] lemma prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p +| (a, b) := rfl + +def prod.swap : (α×β) → (β×α) := λp, (p.2, p.1) + +@[simp] lemma prod.swap_swap : ∀x:α×β, prod.swap (prod.swap x) = x +| ⟨a, b⟩ := rfl + +@[simp] lemma prod.fst_swap {p : α×β} : (prod.swap p).1 = p.2 := rfl + +@[simp] lemma prod.snd_swap {p : α×β} : (prod.swap p).2 = p.1 := rfl + +@[simp] lemma prod.swap_prod_mk {a : α} {b : β} : prod.swap (a, b) = (b, a) := rfl + +@[simp] lemma prod.swap_swap_eq : prod.swap ∘ prod.swap = @id (α × β) := +funext $ prod.swap_swap + diff --git a/data/set/basic.lean b/data/set/basic.lean index a3f9086566e09..46aa4c1dc8495 100644 --- a/data/set/basic.lean +++ b/data/set/basic.lean @@ -17,12 +17,17 @@ funext (assume x, propext (h x)) theorem set_eq_def (s t : set α) : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t := ⟨begin intros h x, rw h end, set.ext⟩ +@[trans] lemma mem_of_mem_of_subset {α : Type u} {x : α} {s t : set α} (hx : x ∈ s) (h : s ⊆ t) : x ∈ t := +h hx + /- mem and set_of -/ @[simp] theorem mem_set_of_eq {a : α} {p : α → Prop} : a ∈ {a | p a} = p a := rfl @[simp] theorem nmem_set_of_eq {a : α} {P : α → Prop} : a ∉ {a : α | P a} = ¬ P a := rfl +@[simp] lemma set_of_mem_eq {s : set α} : {x | x ∈ s} = s := rfl + /- subset -/ -- TODO(Jeremy): write a tactic to unfold specific instances of generic notation? @@ -57,6 +62,11 @@ theorem ssubset_def {s t : set α} : (s ⊂ t) = (s ⊆ t ∧ s ≠ t) := rfl theorem not_mem_empty (x : α) : ¬ (x ∈ (∅ : set α)) := assume h : x ∈ ∅, h +@[simp] lemma not_not_mem_iff {α : Type u} {a : α} {s : set α} [decidable (a ∈ s)] : + ¬ (a ∉ s) ↔ a ∈ s := +not_not_iff + + /- empty set -/ theorem empty_def : (∅ : set α) = {x | false} := rfl @@ -80,6 +90,13 @@ subset.antisymm h (empty_subset s) theorem exists_mem_of_ne_empty {s : set α} (h : s ≠ ∅) : ∃ x, x ∈ s := by finish [set_eq_def] +lemma ne_empty_iff_exists_mem {s : set α} : s ≠ ∅ ↔ ∃ x, x ∈ s := +⟨exists_mem_of_ne_empty, assume ⟨x, hx⟩, ne_empty_of_mem hx⟩ + +-- TODO: remove when simplifier stops rewriting `a ≠ b` to `¬ a = b` +lemma not_eq_empty_iff_exists {s : set α} : ¬ (s = ∅) ↔ ∃ x, x ∈ s := +ne_empty_iff_exists_mem + theorem subset_empty_iff (s : set α) : s ⊆ ∅ ↔ s = ∅ := by finish [set_eq_def] @@ -341,7 +358,7 @@ by simp [insert_eq] @[simp] theorem pair_eq_singleton (a : α) : ({a, a} : set α) = {a} := by finish -theorem singleton_ne_empty (a : α) : ({a} : set α) ≠ ∅ := insert_ne_empty _ _ +@[simp] theorem singleton_ne_empty (a : α) : ({a} : set α) ≠ ∅ := insert_ne_empty _ _ @[simp] theorem singleton_subset_iff {a : α} {s : set α} : {a} ⊆ s ↔ a ∈ s := ⟨λh, h (by simp), λh b e, by simp at e; simp [*]⟩ @@ -416,6 +433,9 @@ by finish [set_eq_def] theorem compl_comp_compl : compl ∘ compl = @id (set α) := funext compl_compl +lemma compl_subset_of_compl_subset {α : Type u} {s t : set α} (h : -s ⊆ t) : -t ⊆ s := +assume x hx, classical.by_contradiction $ assume : x ∉ s, hx $ h $ this + /- set difference -/ theorem diff_eq (s t : set α) : s \ t = s ∩ -t := rfl @@ -439,9 +459,22 @@ by finish [set_eq_def, iff_def, subset_def] theorem diff_subset (s t : set α) : s \ t ⊆ s := by finish [subset_def] +lemma diff_subset_diff {s₁ s₂ t₁ t₂ : set α} : s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂ := +by finish [subset_def] + +lemma diff_right_antimono {s t u : set α} (h : t ⊆ u) : s \ u ⊆ s \ t := +diff_subset_diff (subset.refl s) h + theorem compl_eq_univ_diff (s : set α) : -s = univ \ s := by finish [set_eq_def] +lemma diff_neq_empty {s t : set α} : s \ t = ∅ ↔ s ⊆ t := +⟨assume h x hx, classical.by_contradiction $ assume : x ∉ t, show x ∈ (∅ : set α), from h ▸ ⟨hx, this⟩, + assume h, eq_empty_of_subset_empty $ assume x ⟨hx, hnx⟩, hnx $ h hx⟩ + +@[simp] lemma diff_empty {s : set α} : s \ ∅ = s := +set.ext $ assume x, ⟨assume ⟨hx, _⟩, hx, assume h, ⟨h, not_false⟩⟩ + /- powerset -/ theorem mem_powerset {x s : set α} (h : x ⊆ s) : x ∈ powerset s := h @@ -510,6 +543,21 @@ by finish [set_eq_def, iff_def, mem_image_eq] theorem image_empty (f : α → β) : f '' ∅ = ∅ := by finish [set_eq_def, mem_image_eq] +lemma image_inter {f : α → β} {s t : set α} (h : ∀ x y, f x = f y → x = y) : + f '' s ∩ f '' t = f '' (s ∩ t) := +subset.antisymm + (assume b ⟨⟨a₁, ha₁, h₁⟩, ⟨a₂, ha₂, h₂⟩⟩, + have a₂ = a₁, from h a₂ a₁ $ h₁.symm ▸ h₂.symm ▸ rfl, + ⟨a₁, ⟨ha₁, this ▸ ha₂⟩, h₁⟩) + (subset_inter (mono_image $ inter_subset_left _ _) (mono_image $ inter_subset_right _ _)) + +@[simp] lemma image_singleton {f : α → β} {a : α} : f '' {a} = {f a} := +begin + apply set.ext, intro x, + simp [image], + exact ⟨assume ⟨a', ha', hx⟩, hx ▸ ha' ▸ rfl, assume h, ⟨a, rfl, h.symm⟩⟩ +end + theorem fix_set_compl (t : set α) : compl t = - t := rfl -- TODO(Jeremy): there is an issue with - t unfolding to compl t @@ -528,6 +576,12 @@ theorem compl_compl_image (S : set (set α)) : compl '' (compl '' S) = S := by rw [←image_comp, compl_comp_compl, image_id] +lemma compl_image_set_of {α : Type u} {p : set α → Prop} : + compl '' {x | p x} = {x | p (- x)} := +set.ext $ assume x, ⟨assume ⟨y, (hy : p y), (h_eq : -y = x)⟩, + show p (- x), by rw [←h_eq, compl_compl]; assumption, + assume h : p (-x), ⟨_, h, compl_compl _⟩⟩ + theorem bounded_forall_image_of_bounded_forall {f : α → β} {s : set α} {p : β → Prop} (h : ∀ x ∈ s, p (f x)) : ∀ y ∈ f '' s, p y := by finish [mem_image_eq] @@ -550,6 +604,9 @@ end end image +lemma univ_eq_true_false : univ = ({true, false} : set Prop) := +eq.symm $ eq_univ_of_forall $ classical.cases (by simp) (by simp) + /- inverse image -/ def preimage {α : Type u} {β : Type v} (f : α → β) (s : set β) : set α := {x | f x ∈ s} @@ -577,6 +634,9 @@ set.ext $ assume x, ⟨assume ⟨y, hy, y_eq⟩, h y_eq ▸ hy, assume hx, mem_i @[simp] theorem preimage_compl {s : set β} : f ⁻¹' (- s) = - (f ⁻¹' s) := rfl +@[simp] theorem preimage_set_of_eq {p : α → Prop} {f : β → α} : f ⁻¹' {a | p a} = {a | p (f a)} := +rfl + theorem preimage_id {s : set α} : id ⁻¹' s = s := rfl theorem preimage_comp {s : set γ} : (g ∘ f) ⁻¹' s = f ⁻¹' (g ⁻¹' s) := rfl diff --git a/data/set/default.lean b/data/set/default.lean index 341118034f0d3..fbb49ecae6ef4 100644 --- a/data/set/default.lean +++ b/data/set/default.lean @@ -1 +1 @@ -import data.set.lattice data.set.finite +import data.set.lattice data.set.finite data.set.prod diff --git a/data/set/lattice.lean b/data/set/lattice.lean index ec7b6df679984..8bd4756058f44 100644 --- a/data/set/lattice.lean +++ b/data/set/lattice.lean @@ -6,7 +6,7 @@ Authors Jeremy Avigad, Leonardo de Moura, Johannes Hölzl -- QUESTION: can make the first argument in ∀ x ∈ a, ... implicit? -/ import logic.basic data.set.basic -import algebra.lattice algebra.order algebra.lattice.complete_boolean_algebra +import algebra.lattice algebra.order algebra.lattice.complete_boolean_algebra category.basic import tactic.finish open function tactic set lattice auto @@ -304,6 +304,22 @@ by simp theorem Inter_eq_sInter_image {α I : Type} (s : I → set α) : (⋂ i, s i) = ⋂₀ (s '' univ) := by simp +lemma sUnion_mono {s t : set (set α)} (h : s ⊆ t) : (⋃₀ s) ⊆ (⋃₀ t) := +sUnion_subset $ assume t' ht', subset_sUnion_of_mem $ h ht' + +lemma Union_subset_Union {s t : ι → set α} (h : ∀i, s i ⊆ t i) : (⋃i, s i) ⊆ (⋃i, t i) := +@supr_le_supr (set α) ι _ s t h + +lemma Union_subset_Union2 {ι₂ : Sort x} {s : ι → set α} {t : ι₂ → set α} (h : ∀i, ∃j, s i ⊆ t j) : + (⋃i, s i) ⊆ (⋃i, t i) := +@supr_le_supr2 (set α) ι ι₂ _ s t h + +lemma Union_subset_Union_const {ι₂ : Sort x} {s : set α} (h : ι → ι₂) : (⋃ i:ι, s) ⊆ (⋃ j:ι₂, s) := +@supr_le_supr_const (set α) ι ι₂ _ s h + +lemma sUnion_eq_Union {s : set (set α)} : (⋃₀ s) = (⋃ (i : set α) (h : i ∈ s), i) := +set.ext $ by simp + instance : complete_boolean_algebra (set α) := { set.lattice_set with neg := compl, @@ -333,6 +349,25 @@ sub_eq_left $ eq_empty_of_forall_not_mem $ assume x ⟨ht, ha⟩, insert a (s \ {a}) = insert a s := by simp [insert_eq, union_sdiff_same] +lemma compl_subset_compl_iff_subset {α : Type u} {x y : set α} : - y ⊆ - x ↔ x ⊆ y := +@neg_le_neg_iff_le (set α) _ _ _ + +section image + +lemma image_Union {f : α → β} {s : ι → set α} : f '' (⋃ i, s i) = (⋃i, f '' s i) := +begin + apply set.ext, intro x, + simp [image], + exact ⟨assume ⟨a, h, i, hi⟩, ⟨i, a, h, hi⟩, assume ⟨i, a, h, hi⟩, ⟨a, h, i, hi⟩⟩ +end + +lemma univ_subtype {p : α → Prop} : (univ : set (subtype p)) = (⋃x (h : p x), {⟨x, h⟩}) := +set.ext $ assume ⟨x, h⟩, begin simp, exact ⟨x, h, rfl⟩ end + +end image + +section preimage + theorem monotone_preimage {f : α → β} : monotone (preimage f) := assume a b h, preimage_mono h @[simp] theorem preimage_Union {ι : Sort w} {f : α → β} {s : ι → set β} : @@ -343,6 +378,38 @@ set.ext $ by simp [preimage] preimage f (⋃₀ s) = (⋃t ∈ s, preimage f t) := set.ext $ by simp [preimage] +end preimage + +instance : monad set := +{ monad . + pure := λ(α : Type u) a, {a}, + bind := λ(α β : Type u) s f, ⋃i∈s, f i, + map := λ(α β : Type u), set.image, + pure_bind := assume α β x f, by simp, + bind_assoc := assume α β γ s f g, set.ext $ assume a, + by simp; exact ⟨assume ⟨b, ag, a, as, bf⟩, ⟨a, as, b, bf, ag⟩, + assume ⟨a, as, b, bf, ag⟩, ⟨b, ag, a, as, bf⟩⟩, + id_map := assume α, functor.id_map, + bind_pure_comp_eq_map := assume α β f s, set.ext $ by simp [set.image, eq_comm] } + +section monad +variables {α' β' : Type u} {s : set α'} {f : α' → set β'} {g : set (α' → β')} + +@[simp] lemma bind_def : s >>= f = ⋃i∈s, f i := rfl + +lemma fmap_eq_image : f <$> s = f '' s := rfl + +lemma mem_seq_iff {b : β'} : b ∈ (g <*> s) ↔ (∃(f' : α' → β'), ∃a∈s, f' ∈ g ∧ b = f' a) := +begin + simp [seq_eq_bind_map], + apply exists_congr, + intro f', + exact ⟨assume ⟨hf', a, ha, h_eq⟩, ⟨a, h_eq.symm, ha, hf'⟩, + assume ⟨a, h_eq, ha, hf'⟩, ⟨hf', a, ha, h_eq.symm⟩⟩ +end + +end monad + /- disjoint sets -/ section disjoint diff --git a/data/set/prod.lean b/data/set/prod.lean new file mode 100644 index 0000000000000..93906ece7575b --- /dev/null +++ b/data/set/prod.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2014 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Johannes Hölzl +-/ +import data.set.lattice data.prod + +universes u v w x +variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} +variables {s s₁ s₂ : set α} {t t₁ t₂ : set β} + +namespace set + +protected def prod (s : set α) (t : set β) : set (α × β) := +{p | p.1 ∈ s ∧ p.2 ∈ t} + +lemma mem_prod_eq {p : α × β} : p ∈ set.prod s t = (p.1 ∈ s ∧ p.2 ∈ t) := +rfl + +theorem prod_preimage_eq {f : γ → α} {g : δ → β} : + set.prod (preimage f s) (preimage g t) = preimage (λp, (f p.1, g p.2)) (set.prod s t) := rfl + +lemma prod_mono {s₁ s₂ : set α} {t₁ t₂ : set β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : + set.prod s₁ t₁ ⊆ set.prod s₂ t₂ := +assume x ⟨h₁, h₂⟩, ⟨hs h₁, ht h₂⟩ + +lemma prod_inter_prod : set.prod s₁ t₁ ∩ set.prod s₂ t₂ = set.prod (s₁ ∩ s₂) (t₁ ∩ t₂) := +subset.antisymm + (assume ⟨a, b⟩ ⟨⟨ha₁, hb₁⟩, ⟨ha₂, hb₂⟩⟩, ⟨⟨ha₁, ha₂⟩, ⟨hb₁, hb₂⟩⟩) + (subset_inter + (prod_mono (inter_subset_left _ _) (inter_subset_left _ _)) + (prod_mono (inter_subset_right _ _) (inter_subset_right _ _))) + +theorem monotone_prod [preorder α] {f : α → set β} {g : α → set γ} + (hf : monotone f) (hg : monotone g) : monotone (λx, set.prod (f x) (g x)) := +assume a b h, prod_mono (hf h) (hg h) + +lemma image_swap_prod : (λp:β×α, (p.2, p.1)) '' set.prod t s = set.prod s t := +set.ext $ assume ⟨a, b⟩, by simp [mem_image_eq, set.prod]; exact +⟨ assume ⟨b', a', h_a, h_b, h⟩, by rw [h_a, h_b] at h; assumption, + assume ⟨ha, hb⟩, ⟨b, a, rfl, rfl, ⟨ha, hb⟩⟩⟩ + +theorem image_swap_eq_preimage_swap : image (@prod.swap α β) = preimage prod.swap := +image_eq_preimage_of_inverse (@prod.swap α β) (@prod.swap β α) + begin simp; intros; trivial end + begin simp; intros; trivial end + +lemma prod_image_image_eq {m₁ : α → γ} {m₂ : β → δ} : + set.prod (image m₁ s) (image m₂ t) = image (λp:α×β, (m₁ p.1, m₂ p.2)) (set.prod s t) := +set.ext $ assume ⟨b₁, b₂⟩, + ⟨assume ⟨⟨a₁, ha₁, (eq₁ : m₁ a₁ = b₁)⟩, ⟨a₂, ha₂, (eq₂ : m₂ a₂ = b₂)⟩⟩, + mem_image + (show (a₁, a₂) ∈ set.prod s t, from ⟨ha₁, ha₂⟩) + (by simp [eq₁, eq₂]), + assume ⟨⟨a₁, a₂⟩, ⟨ha₁, ha₂⟩, eq⟩, eq ▸ ⟨mem_image_of_mem m₁ ha₁, mem_image_of_mem m₂ ha₂⟩⟩ + +@[simp] lemma prod_singleton_singleton {a : α} {b : β} : + set.prod {a} {b} = ({(a, b)} : set (α×β)) := +set.ext $ assume ⟨a', b'⟩, by simp [set.prod] + +lemma prod_neq_empty_iff {s : set α} {t : set β} : + set.prod s t ≠ ∅ ↔ (s ≠ ∅ ∧ t ≠ ∅) := +begin + rw [ne_empty_iff_exists_mem, ne_empty_iff_exists_mem, ne_empty_iff_exists_mem, + prod.exists], + exact ⟨assume ⟨a, b, ha, hb⟩, ⟨⟨a, ha⟩, ⟨b, hb⟩⟩, + assume ⟨⟨a, ha⟩, ⟨b, hb⟩⟩, ⟨a, b, ha, hb⟩⟩ +end + +@[simp] lemma prod_mk_mem_set_prod_eq {a : α} {b : β} {s : set α} {t : set β} : + (a, b) ∈ set.prod s t = (a ∈ s ∧ b ∈ t) := rfl + +end set \ No newline at end of file diff --git a/logic/basic.lean b/logic/basic.lean index af3a1b7d1434f..66527397775d7 100644 --- a/logic/basic.lean +++ b/logic/basic.lean @@ -45,6 +45,9 @@ end miscellany propositional connectives -/ +@[simp] lemma false_neq_true : false ≠ true := +begin intro h, rw [h], trivial end + section propositional variables {a b c d : Prop} @@ -65,6 +68,9 @@ iff.intro (λ h hp hq, h ⟨hp, hq⟩) (λ h ⟨hp, hq⟩, h hp hq) theorem iff_def (p q : Prop) : (p ↔ q) ↔ (p → q) ∧ (q → p) := ⟨ λh, ⟨h.1, h.2⟩, λ ⟨h₁, h₂⟩, ⟨h₁, h₂⟩ ⟩ +@[simp] lemma {u v} implies_implies_true_iff {α : Sort u} {β : Sort v} : (α → β → true) ↔ true := +⟨assume _, trivial, assume _ _ _ , trivial⟩ + /- not -/ theorem {u} not_elim {A : Sort u} (H1 : ¬a) (H2 : a) : A := absurd H2 H1 @@ -227,6 +233,9 @@ else theorem not_and_iff [decidable a] : ¬ (a ∧ b) ↔ ¬a ∨ ¬b := iff.intro not_or_not_of_not_and not_and_of_not_or_not +theorem not_and_iff_imp_not {p q : Prop} : ¬ (p ∧ q) ↔ (p → ¬ q) := +⟨assume h hp hq, h ⟨hp, hq⟩, assume h ⟨hp, hq⟩, h hp hq⟩ + theorem not_or_of_not_and_not (h : ¬ a ∧ ¬ b) : ¬ (a ∨ b) := assume h₁, or.elim h₁ (assume ha, and.left h ha) (assume hb, and.right h hb) @@ -357,6 +366,9 @@ theorem forall_or_distrib_left {q : Prop} {p : α → Prop} : (∀x, q ∨ p x) ↔ q ∨ (∀x, p x) := forall_or_distrib_left +lemma cases {p : Prop → Prop} (h1 : p true) (h2 : p false) : ∀a, p a := +assume a, cases_on a h1 h2 + end classical /- diff --git a/topology/topological_space.lean b/topology/topological_space.lean index b6c965b1456a9..736bf75cad03c 100644 --- a/topology/topological_space.lean +++ b/topology/topological_space.lean @@ -16,21 +16,6 @@ local attribute [instance] decidable_inhabited prop_decidable universes u v w -lemma compl_subset_of_compl_subset {α : Type u} {s t : set α} (h : -s ⊆ t) : -t ⊆ s := -assume x hx, classical.by_contradiction $ assume : x ∉ s, hx $ h $ this - -lemma not_and_iff_imp_not {p q : Prop} : ¬ (p ∧ q) ↔ (p → ¬ q) := -⟨assume h hp hq, h ⟨hp, hq⟩, assume h ⟨hp, hq⟩, h hp hq⟩ - -lemma diff_subset_diff {α : Type u} {s₁ s₂ t₁ t₂ : set α} : s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂ := -by finish [subset_def] - -@[trans] lemma mem_of_mem_of_subset {α : Type u} {x : α} {s t : set α} (hx : x ∈ s) (h : s ⊆ t) : x ∈ t := -h hx - -lemma univ_subtype {α : Type u} {p : α → Prop} : (univ : set (subtype p)) = (⋃x (h : p x), {⟨x, h⟩}) := -set.ext $ assume ⟨x, h⟩, begin simp, exact ⟨x, h, rfl⟩ end - structure topological_space (α : Type u) := (is_open : set α → Prop) (is_open_univ : is_open univ) @@ -220,7 +205,7 @@ lemma closure_eq_compl_interior_compl {s : set α} : closure s = - interior (- s begin simp [interior, closure], rw [compl_sUnion, compl_image_set_of], - simp [neg_subset_neg_iff_subset] + simp [compl_subset_compl_iff_subset] end @[simp] lemma interior_compl_eq {s : set α} : interior (- s) = - closure s := @@ -422,9 +407,9 @@ classical.by_contradiction $ assume h, (assume ⟨c₁, hc₁, hc'₁⟩ ⟨c₂, hc₂, hc'₂⟩, ⟨⟨c₁ ∪ c₂, union_subset hc₁ hc₂, finite_union hc'₁ hc'₂⟩, principal_mono.mpr $ diff_right_antimono $ sUnion_mono $ subset_union_left _ _, principal_mono.mpr $ diff_right_antimono $ sUnion_mono $ subset_union_right _ _⟩) - (assume ⟨c', hc'₁, hc'₂⟩, by simp [diff_neq_empty]; exact h hc'₁ hc'₂), + (assume ⟨c', hc'₁, hc'₂⟩, show principal (s \ _) ≠ ⊥, by simp [diff_neq_empty]; exact h hc'₁ hc'₂), have f ≤ principal s, from infi_le_of_le ⟨∅, empty_subset _, finite.empty⟩ $ - show principal (s - ⋃₀∅) ≤ principal s, by simp; exact subset.refl s, + show principal (s \ ⋃₀∅) ≤ principal s, by simp; exact subset.refl s, let ⟨a, ha, (h : f ⊓ nhds a ≠ ⊥)⟩ := hs f ‹f ≠ ⊥› this, ⟨t, ht₁, (ht₂ : a ∈ t)⟩ := hc₂ ha diff --git a/topology/uniform_space.lean b/topology/uniform_space.lean index efdb1a59746b8..4cae19a7d5a47 100644 --- a/topology/uniform_space.lean +++ b/topology/uniform_space.lean @@ -677,10 +677,10 @@ lemma totally_bounded_iff_filter {s : set α} : assume h : ∀f, f ≠ ⊥ → f ≤ principal s → ∃c ≤ f, cauchy c, assume d hd, classical.by_contradiction $ assume hs, have hd_cover : ∀{t:set α}, finite t → ¬ s ⊆ (⋃y∈t, {x | (x,y) ∈ d}), - by simp [not_exists_iff, not_and_iff, not_or_iff_implies] at hs; - assumption, + by simp [not_exists_iff, not_and_iff] at hs; + simp [implies_iff_not_or, hs], let - f := ⨅t:{t : set α // finite t}, principal (s - (⋃y∈t.val, {x | (x,y) ∈ d})), + f := ⨅t:{t : set α // finite t}, principal (s \ (⋃y∈t.val, {x | (x,y) ∈ d})), ⟨a, ha⟩ := @exists_mem_of_ne_empty α s (assume h, hd_cover finite.empty $ h.symm ▸ empty_subset _) in