From 9c28552afbd5da45c593675ce1155ce8d19c8467 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Mon, 4 Jan 2016 22:03:47 +0100 Subject: [PATCH] feat(library/algebra): add lattice instances for Prop, fun, and set Adds weak_order, lattice and complete_lattice instances for Prop, fun, and set. Adds supporting theorems to various other places. --- library/algebra/complete_lattice.lean | 89 +++++++++++++++++++++++ library/algebra/lattice.lean | 32 ++++++++ library/algebra/order.lean | 32 ++++++++ library/data/set/basic.lean | 101 ++++++++++++++++++++++++++ library/init/classical.lean | 12 +++ library/init/logic.lean | 10 +++ 6 files changed, 276 insertions(+) diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean index e10e094f0..4b4120452 100644 --- a/library/algebra/complete_lattice.lean +++ b/library/algebra/complete_lattice.lean @@ -270,3 +270,92 @@ have le₂ : ⨅ univ ≤ ⨆ (∅ : set A), from le.antisymm le₁ le₂ end complete_lattice + +/- complete lattice instances -/ + +section +open eq.ops complete_lattice + +definition complete_lattice_fun [instance] {A B : Type} [complete_lattice B] : + complete_lattice (A → B) := +⦃ complete_lattice, lattice_fun, + Inf := λS x, Inf ((λf, f x) ' S), + le_Inf := take f S H x, + le_Inf (take y Hy, obtain g `g ∈ S` `g x = y`, from Hy, `g x = y` ▸ H g `g ∈ S` x), + Inf_le := take f S `f ∈ S` x, + Inf_le (exists.intro f (and.intro `f ∈ S` rfl)), + Sup := λS x, Sup ((λf, f x) ' S), + le_Sup := take f S `f ∈ S` x, + le_Sup (exists.intro f (and.intro `f ∈ S` rfl)), + Sup_le := take f S H x, + Sup_le (take y Hy, obtain g `g ∈ S` `g x = y`, from Hy, `g x = y` ▸ H g `g ∈ S` x) +⦄ + +section +open classical -- Prop and set are only in the classical setting a complete lattice + +definition complete_lattice_Prop [instance] : complete_lattice Prop := +⦃ complete_lattice, lattice_Prop, + Inf := λS, false ∉ S, + le_Inf := take x S H Hx Hf, + H _ Hf Hx, + Inf_le := take x S Hx Hf, + (classical.cases_on x (take x, true.intro) Hf) Hx, + Sup := λS, true ∈ S, + le_Sup := take x S Hx H, + iff_subst (iff.intro (take H, true.intro) (take H', H)) Hx, + Sup_le := take x S H Ht, + H _ Ht true.intro +⦄ + +lemma sInter_eq_fun_Inf {A : Type} (S : set (set A)) : ⋂₀ S = @Inf (A → Prop) _ S := +funext (take x, + calc + (⋂₀ S) x = ∀₀ P ∈ S, P x : rfl + ... = ¬ (∃₀ P ∈ S, P x = false) : + begin + rewrite not_bounded_exists, + apply bounded_forall_congr, + intros, + rewrite eq_false, + rewrite not_not_iff + end + ... = @Inf (A → Prop) _ S x : rfl) + +lemma sUnion_eq_fun_Sup {A : Type} (S : set (set A)) : ⋃₀ S = @Sup (A → Prop) _ S := +funext (take x, + calc + (⋃₀ S) x = ∃₀ P ∈ S, P x : rfl + ... = (∃₀ P ∈ S, P x = true) : + begin + apply bounded_exists_congr, + intros, + rewrite eq_true + end + ... = @Sup (A → Prop) _ S x : rfl) + +definition complete_lattice_set [instance] {A : Type} : complete_lattice (set A) := +⦃ complete_lattice, + le := subset, + le_refl := @le_refl (A → Prop) _, + le_trans := @le_trans (A → Prop) _, + le_antisymm := @le_antisymm (A → Prop) _, + inf := inter, + sup := union, + inf_le_left := @inf_le_left (A → Prop) _, + inf_le_right := @inf_le_right (A → Prop) _, + le_inf := @le_inf (A → Prop) _, + le_sup_left := @le_sup_left (A → Prop) _, + le_sup_right := @le_sup_right (A → Prop) _, + sup_le := @sup_le (A → Prop) _, + Inf := sInter, + Sup := sUnion, + le_Inf := begin intros X S H, rewrite sInter_eq_fun_Inf, apply (@le_Inf (A → Prop) _), exact H end, + Inf_le := begin intros X S H, rewrite sInter_eq_fun_Inf, apply (@Inf_le (A → Prop) _), exact H end, + le_Sup := begin intros X S H, rewrite sUnion_eq_fun_Sup, apply (@le_Sup (A → Prop) _), exact H end, + Sup_le := begin intros X S H, rewrite sUnion_eq_fun_Sup, apply (@Sup_le (A → Prop) _), exact H end +⦄ + +end + +end diff --git a/library/algebra/lattice.lean b/library/algebra/lattice.lean index c01980753..ad18c1d65 100644 --- a/library/algebra/lattice.lean +++ b/library/algebra/lattice.lean @@ -106,3 +106,35 @@ section theorem sup_eq_right {a b : A} (H : a ≤ b) : a ⊔ b = b := eq.subst !sup.comm (sup_eq_left H) end + +/- lattice instances -/ + +definition lattice_Prop [instance] : lattice Prop := +⦃ lattice, weak_order_Prop, + inf := and, + le_inf := take a b c Ha Hb Hc, and.intro (Ha Hc) (Hb Hc), + inf_le_left := @and.elim_left, + inf_le_right := @and.elim_right, + sup := or, + sup_le := @or.rec, + le_sup_left := @or.intro_left, + le_sup_right := @or.intro_right +⦄ + +definition lattice_fun [instance] {A B : Type} [lattice B] : lattice (A → B) := +⦃ lattice, weak_order_fun, + inf := λf g x, inf (f x) (g x), + le_inf := take f g h Hf Hg x, le_inf (Hf x) (Hg x), + inf_le_left := take f g x, !inf_le_left, + inf_le_right := take f g x, !inf_le_right, + sup := λf g x, sup (f x) (g x), + sup_le := take f g h Hf Hg x, sup_le (Hf x) (Hg x), + le_sup_left := take f g x, !le_sup_left, + le_sup_right := take t g x, !le_sup_right +⦄ + +/- + Should we add a trans-instance from total orders to lattices? + If we added we should add it with lower priority: + Prop is added as a lattice, but in the classical case it is a total order! +-/ diff --git a/library/algebra/order.lean b/library/algebra/order.lean index 33cd557dc..8161ba764 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -434,3 +434,35 @@ section (assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂) (assume H : a > b, by rewrite (max_eq_left_of_lt H); apply H₁) end + +/- order instances -/ + +definition weak_order_Prop [instance] : weak_order Prop := +⦃ weak_order, + le := λx y, x → y, + le_refl := λx, id, + le_trans := λa b c H1 H2 x, H2 (H1 x), + le_antisymm := λf g H1 H2, propext (and.intro H1 H2) +⦄ + +definition weak_order_fun [instance] {A B : Type} [weak_order B] : weak_order (A → B) := +⦃ weak_order, + le := λx y, ∀b, x b ≤ y b, + le_refl := λf b, !le.refl, + le_trans := λf g h H1 H2 b, !le.trans (H1 b) (H2 b), + le_antisymm := λf g H1 H2, funext (λb, !le.antisymm (H1 b) (H2 b)) +⦄ + +definition weak_order_dual {A : Type} (wo : weak_order A) : weak_order A := +⦃ weak_order, + le := λx y, y ≤ x, + le_refl := le.refl, + le_trans := take a b c `b ≤ a` `c ≤ b`, le.trans `c ≤ b` `b ≤ a`, + le_antisymm := take a b `b ≤ a` `a ≤ b`, le.antisymm `a ≤ b` `b ≤ a` ⦄ + +lemma dual {A : Type} (wo : weak_order A) (a b : A) : + @le _ (@weak_order.to_has_le _ (weak_order_dual wo)) a b = + @le _ (@weak_order.to_has_le _ wo) b a := +rfl + +-- what to do with the strict variants? diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 45ee59ff3..a6f8669e7 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -64,6 +64,54 @@ theorem bounded_exists.intro {P : X → Prop} {s : set X} {x : X} (xs : x ∈ s) ∃₀ x ∈ s, P x := exists.intro x (and.intro xs Px) +lemma bounded_forall_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x∈S, P x ↔ Q x) : + (∀₀ x ∈ S, P x) = (∀₀ x ∈ S, Q x) := +begin + apply propext, + apply forall_congr, + intros x, + apply imp_congr_right, + apply H +end + +lemma bounded_exists_congr {A : Type} {S : set A} {P Q : A → Prop} (H : ∀₀ x∈S, P x ↔ Q x) : + (∃₀ x ∈ S, P x) = (∃₀ x ∈ S, Q x) := +begin + apply propext, + apply exists_congr, + intros x, + apply and_congr_right, + apply H +end + +section + open classical + + lemma not_bounded_exists {A : Type} {S : set A} {P : A → Prop} : + (¬ (∃₀ x ∈ S, P x)) = (∀₀ x ∈ S, ¬ P x) := + begin + rewrite forall_iff_not_exists, + apply propext, + apply forall_congr, + intro x, + rewrite not_and_iff_not_or_not, + rewrite imp_iff_not_or + end + + lemma not_bounded_forall {A : Type} {S : set A} {P : A → Prop} : + (¬ (∀₀ x ∈ S, P x)) = (∃₀ x ∈ S, ¬ P x) := + calc (¬ (∀₀ x ∈ S, P x)) = ¬ ¬ (∃₀ x ∈ S, ¬ P x) : + begin + rewrite not_bounded_exists, + apply (congr_arg not), + apply bounded_forall_congr, + intros x H, + rewrite not_not_iff + end + ... = (∃₀ x ∈ S, ¬ P x) : by (rewrite not_not_iff) + +end + /- empty set -/ definition empty : set X := λx, false @@ -95,6 +143,10 @@ subset.antisymm H (empty_subset s) theorem subset_empty_iff (s : set X) : s ⊆ ∅ ↔ s = ∅ := iff.intro eq_empty_of_subset_empty (take xeq, by rewrite xeq; apply subset.refl ∅) +lemma bounded_forall_empty_iff {P : X → Prop} : + (∀₀x∈∅, P x) ↔ true := +iff.intro (take H, true.intro) (take H, by contradiction) + /- universal set -/ definition univ : set X := λx, true @@ -287,6 +339,18 @@ theorem forall_of_forall_insert {P : X → Prop} {a : X} {s : set X} ∀ x, x ∈ s → P x := λ x xs, H x (!mem_insert_of_mem xs) +lemma forall_insert_iff {P : X → Prop} {a : X} {s : set X} : + (∀₀x ∈ insert a s, P x) ↔ P a ∧ (∀₀x ∈ s, P x) := +begin + apply iff.intro, all_goals (intro H), + { apply and.intro, + { apply H, apply mem_insert }, + { intro x Hx, apply H, apply mem_insert_of_mem, assumption } }, + { intro x Hx, cases Hx with eq Hx, + { cases eq, apply (and.elim_left H) }, + { apply (and.elim_right H), assumption } } +end + /- singleton -/ theorem mem_singleton_iff (a b : X) : a ∈ '{b} ↔ a = b := @@ -521,8 +585,45 @@ theorem complement_complement_image (S : set (set X)) : complement ' (complement ' S) = S := by rewrite [-image_compose, complement_compose_complement, image_id] +lemma forall_image_implies_forall {f : X → Y} {S : set X} {P : Y → Prop} (H : ∀₀ x ∈ S, P (f x)) : + ∀₀ y ∈ f ' S, P y := +begin + intro x' Hx; + cases Hx with x Hx; + cases Hx with Hx eq; + rewrite (eq⁻¹); + apply H; + assumption +end + +lemma forall_image_iff {f : X → Y} {S : set X} {P : Y → Prop} : + (∀₀ y ∈ f ' S, P y) ↔ (∀₀ x ∈ S, P (f x)) := +iff.intro (take H x Hx, H _ (!mem_image_of_mem `x ∈ S`)) forall_image_implies_forall + +lemma image_insert_eq {f : X → Y} {a : X} {S : set X} : + f ' insert a S = insert (f a) (f ' S) := +begin + apply set.ext, + intro x, apply iff.intro, all_goals (intros H), + { cases H with y Hy, cases Hy with Hy eq, rewrite (eq⁻¹), cases Hy with y_eq, + { rewrite y_eq, apply mem_insert }, + { apply mem_insert_of_mem, apply mem_image_of_mem, assumption } }, + { cases H with eq Hx, + { rewrite eq, apply mem_image_of_mem, apply mem_insert }, + { cases Hx with y Hy, cases Hy with Hy eq, + rewrite (eq⁻¹), apply mem_image_of_mem, apply mem_insert_of_mem, assumption } } +end + end image +/- function pre image -/ + +definition preimage {A B:Type} (f : A → B) (Y : set B) : set A := { x | f x ∈ Y } + +lemma image_subset_iff {A B : Type} {f : A → B} {X : set A} {Y : set B} : + f ' X ⊆ Y ↔ X ⊆ preimage f Y := +@forall_image_iff A B f X Y + /- collections of disjoint sets -/ definition disjoint_sets (S : set (set X)) : Prop := ∀ a b, a ∈ S → b ∈ S → a ≠ b → a ∩ b = ∅ diff --git a/library/init/classical.lean b/library/init/classical.lean index cbc4e1115..8099f7e50 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -159,6 +159,18 @@ propext (iff.intro (assume H, eq.of_iff H) (assume H, iff.of_eq H)) +lemma eq_false {a : Prop} : (a = false) = (¬ a) := +begin + rewrite ((@iff_eq_eq a false)⁻¹), + rewrite iff_false +end + +lemma eq_true {a : Prop} : (a = true) = a := +begin + rewrite ((@iff_eq_eq a true)⁻¹), + rewrite iff_true +end + end aux /- All propositions are decidable -/ diff --git a/library/init/logic.lean b/library/init/logic.lean index 7cdc23c15..5476c1559 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -342,6 +342,11 @@ iff.intro (λHab Hc, iff.mp H2 (Hab (iff.mpr H1 Hc))) (λHcd Ha, iff.mpr H2 (Hcd (iff.mp H1 Ha))) +theorem imp_congr_right (H : a → (b ↔ c)) : (a → b) ↔ (a → c) := +iff.intro + (take Hab Ha, iff.elim_left (H Ha) (Hab Ha)) + (take Hab Ha, iff.elim_right (H Ha) (Hab Ha)) + theorem not_not_intro (Ha : a) : ¬¬a := assume Hna : ¬a, Hna Ha @@ -392,6 +397,11 @@ and.rec (λHa Hb, and.intro (H₂ Ha) (H₃ Hb)) theorem and_congr [congr] (H1 : a ↔ c) (H2 : b ↔ d) : (a ∧ b) ↔ (c ∧ d) := iff.intro (and.imp (iff.mp H1) (iff.mp H2)) (and.imp (iff.mpr H1) (iff.mpr H2)) +theorem and_congr_right (H : a → (b ↔ c)) : (a ∧ b) ↔ (a ∧ c) := +iff.intro + (take Hab, obtain `a` `b`, from Hab, and.intro `a` (iff.elim_left (H `a`) `b`)) + (take Hac, obtain `a` `c`, from Hac, and.intro `a` (iff.elim_right (H `a`) `c`)) + theorem and.comm [simp] : a ∧ b ↔ b ∧ a := iff.intro and.swap and.swap