algebra/lattice/filter: cleanup move theorems to appropriate places

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 = ⊤)

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

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

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
+