From 471c9058eb689254bb0bef289f38711442db860e Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 27 Jul 2015 06:22:05 +0300 Subject: [PATCH] fix/feat(library/logic/connectives,library/data/{finset,set}): fix names or.left_distrib etc., fix implicit arguments, and make small additions --- library/data/finset/basic.lean | 10 +++++----- library/data/finset/comb.lean | 14 ++++++++++++++ library/data/set/basic.lean | 8 ++++---- library/logic/connectives.lean | 16 ++++++++-------- 4 files changed, 31 insertions(+), 17 deletions(-) diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index d2a991af4..31eff6177 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -297,7 +297,7 @@ theorem mem_erase_eq (a b : A) (s : finset A) : a ∈ erase b s = (a ∈ s ∧ a propext !mem_erase_iff open decidable -theorem erase_insert (a : A) (s : finset A) : a ∉ s → erase a (insert a s) = s := +theorem erase_insert {a : A} {s : finset A} : a ∉ s → erase a (insert a s) = s := λ anins, finset.ext (λ b, by_cases (λ beqa : b = a, iff.intro (λ bin, by subst b; exact absurd bin !mem_erase) @@ -481,16 +481,16 @@ variable [h : decidable_eq A] include h theorem inter.distrib_left (s t u : finset A) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) := -ext (take x, by rewrite [mem_inter_eq, *mem_union_eq, *mem_inter_eq]; apply and.distrib_left) +ext (take x, by rewrite [mem_inter_eq, *mem_union_eq, *mem_inter_eq]; apply and.left_distrib) theorem inter.distrib_right (s t u : finset A) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) := -ext (take x, by rewrite [mem_inter_eq, *mem_union_eq, *mem_inter_eq]; apply and.distrib_right) +ext (take x, by rewrite [mem_inter_eq, *mem_union_eq, *mem_inter_eq]; apply and.right_distrib) theorem union.distrib_left (s t u : finset A) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) := -ext (take x, by rewrite [mem_union_eq, *mem_inter_eq, *mem_union_eq]; apply or.distrib_left) +ext (take x, by rewrite [mem_union_eq, *mem_inter_eq, *mem_union_eq]; apply or.left_distrib) theorem union.distrib_right (s t u : finset A) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) := -ext (take x, by rewrite [mem_union_eq, *mem_inter_eq, *mem_union_eq]; apply or.distrib_right) +ext (take x, by rewrite [mem_union_eq, *mem_inter_eq, *mem_union_eq]; apply or.right_distrib) end inter /- disjoint -/ diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean index 260d09204..5a4a9b2b0 100644 --- a/library/data/finset/comb.lean +++ b/library/data/finset/comb.lean @@ -150,6 +150,11 @@ iff.intro theorem mem_filter_eq : x ∈ filter p s = (x ∈ s ∧ p x) := propext !mem_filter_iff +variable t : finset A + +theorem mem_filter_union_iff : x ∈ filter p (s ∪ t) ↔ x ∈ filter p s ∨ x ∈ filter p t := +by rewrite [*mem_filter_iff, mem_union_iff, and.right_distrib] + end filter theorem mem_singleton_eq' {A : Type} [deceq : decidable_eq A] (x a : A) : x ∈ '{a} = (x = a) := @@ -423,6 +428,15 @@ begin (show x ⊆ s, by rewrite [(erase_eq_of_not_mem this) at H']; apply H')))) end +theorem subset_of_mem_powerset {s t : finset A} (H : s ∈ powerset t) : s ⊆ t := +by rewrite mem_powerset_iff_subset at H; exact H + +theorem mem_powerset_of_subset {s t : finset A} (H : s ⊆ t) : s ∈ powerset t := +by rewrite -mem_powerset_iff_subset at H; exact H + +theorem empty_mem_powerset (s : finset A) : ∅ ∈ powerset s := +by rewrite mem_powerset_iff_subset; apply empty_subset + end powerset end finset diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 461587fa6..d868be40c 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -157,16 +157,16 @@ setext (take x, !true_and) /- distributivity laws -/ theorem inter.distrib_left (s t u : set X) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) := -setext (take x, !and.distrib_left) +setext (take x, !and.left_distrib) theorem inter.distrib_right (s t u : set X) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) := -setext (take x, !and.distrib_right) +setext (take x, !and.right_distrib) theorem union.distrib_left (s t u : set X) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) := -setext (take x, !or.distrib_left) +setext (take x, !or.left_distrib) theorem union.distrib_right (s t u : set X) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) := -setext (take x, !or.distrib_right) +setext (take x, !or.right_distrib) /- set-builder notation -/ diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean index 2b9599aaf..b7ce97139 100644 --- a/library/logic/connectives.lean +++ b/library/logic/connectives.lean @@ -152,7 +152,7 @@ theorem and_imp_eq (a b c : Prop) : (a ∧ b → c) = (a → b → c) := propext !and_imp_iff theorem and_iff_and (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)) +iff.intro (and.imp (iff.mp H1) (iff.mp H2)) (and.imp (iff.mpr H1) (iff.mpr H2)) /- or -/ @@ -221,25 +221,25 @@ theorem or_self (a : Prop) : a ∨ a ↔ a := iff.intro (or.rec imp.id imp.id) or.inl theorem or_iff_or (H1 : a ↔ c) (H2 : b ↔ d) : (a ∨ b) ↔ (c ∨ d) := -iff.intro (or.imp (iff.mp H1) (iff.mp H2)) (or.imp (iff.mpr H1) (iff.mpr H2)) +iff.intro (or.imp (iff.mp H1) (iff.mp H2)) (or.imp (iff.mpr H1) (iff.mpr H2)) /- distributivity -/ -theorem and.distrib_left (a b c : Prop) : a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c) := +theorem and.left_distrib (a b c : Prop) : a ∧ (b ∨ c) ↔ (a ∧ b) ∨ (a ∧ c) := iff.intro (and.rec (λH, or.imp (and.intro H) (and.intro H))) (or.rec (and.imp_right or.inl) (and.imp_right or.inr)) -theorem and.distrib_right (a b c : Prop) : (a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c) := -iff.trans (iff.trans !and.comm !and.distrib_left) (or_iff_or !and.comm !and.comm) +theorem and.right_distrib (a b c : Prop) : (a ∨ b) ∧ c ↔ (a ∧ c) ∨ (b ∧ c) := +iff.trans (iff.trans !and.comm !and.left_distrib) (or_iff_or !and.comm !and.comm) -theorem or.distrib_left (a b c : Prop) : a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c) := +theorem or.left_distrib (a b c : Prop) : a ∨ (b ∧ c) ↔ (a ∨ b) ∧ (a ∨ c) := iff.intro (or.rec (λH, and.intro (or.inl H) (or.inl H)) (and.imp or.inr or.inr)) (and.rec (or.rec (imp.syl imp.intro or.inl) (imp.syl or.imp_right and.intro))) -theorem or.distrib_right (a b c : Prop) : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := -iff.trans (iff.trans !or.comm !or.distrib_left) (and_iff_and !or.comm !or.comm) +theorem or.right_distrib (a b c : Prop) : (a ∧ b) ∨ c ↔ (a ∨ c) ∧ (b ∨ c) := +iff.trans (iff.trans !or.comm !or.left_distrib) (and_iff_and !or.comm !or.comm) /- iff -/