From 6549940c6321e31d836ae90bf4fdfa8ae69904ee Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 17 May 2015 17:50:32 +1000 Subject: [PATCH] feat(library/data/finset/bigops.lean): add Union for finsets --- library/algebra/group_bigops.lean | 11 ++++ library/data/finset/bigops.lean | 98 +++++++++++++++++++++++++++++++ library/data/finset/default.lean | 2 +- library/data/finset/finset.md | 1 + library/data/nat/bigops.lean | 4 ++ 5 files changed, 115 insertions(+), 1 deletion(-) create mode 100644 library/data/finset/bigops.lean diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index edaac182e..978225cde 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -61,6 +61,10 @@ section monoid Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := by rewrite [union_eq_append d, Prodl_append] end deceqA + + theorem Prodl_one : ∀(l : list A), Prodl l (λ x, 1) = 1 + | [] := rfl + | (a::l) := by rewrite [Prodl_cons, Prodl_one, mul_one] end monoid section comm_monoid @@ -134,6 +138,9 @@ section comm_monoid assert H4 : f x = g x, from H2 !mem_insert, by rewrite [Prod_insert_of_not_mem f H1, Prod_insert_of_not_mem g H1, IH H3, H4]) end deceqA + + theorem Prod_one (s : finset A) : Prod s (λ x, 1) = 1 := + quot.induction_on s (take u, !Prodl_one) end comm_monoid section add_monoid @@ -161,6 +168,8 @@ section add_monoid theorem Suml_union {l₁ l₂ : list A} (f : A → B) (d : disjoint l₁ l₂) : Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := Prodl_union f d end deceqA + + theorem Suml_zero (l : list A) : Suml l (λ x, 0) = 0 := Prodl_one l end add_monoid section add_comm_monoid @@ -199,6 +208,8 @@ section add_comm_monoid theorem Sum_ext {s : finset A} {f g : A → B} (H : ∀x, x ∈ s → f x = g x) : Sum s f = Sum s g := Prod_ext H end deceqA + + theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = 0 := Prod_one s end add_comm_monoid end algebra diff --git a/library/data/finset/bigops.lean b/library/data/finset/bigops.lean new file mode 100644 index 000000000..f31a8aed4 --- /dev/null +++ b/library/data/finset/bigops.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jeremy Avigad + +Finite unions and intersections on finsets. + +Note: for the moment we only do unions. We need to generalize bigops for intersections. +-/ +import data.finset.comb algebra.group_bigops +open list + +namespace finset + +variables {A B : Type} [deceqA : decidable_eq A] [deceqB : decidable_eq B] + +/- Unionl and Union -/ + +section union + +definition to_comm_monoid_Union (B : Type) [deceqB : decidable_eq B] : + algebra.comm_monoid (finset B) := +⦃ algebra.comm_monoid, + mul := union, + mul_assoc := union.assoc, + one := empty, + mul_one := union_empty, + one_mul := empty_union, + mul_comm := union.comm +⦄ + +open [classes] algebra +local attribute finset.to_comm_monoid_Union [instance] + +include deceqB + +definition Unionl (l : list A) (f : A → finset B) : finset B := algebra.Prodl l f +notation `⋃` binders `←` l, r:(scoped f, Unionl l f) := r +definition Union (s : finset A) (f : A → finset B) : finset B := algebra.Prod s f +notation `⋃` binders `∈` s, r:(scoped f, finset.Union s f) := r + +theorem Unionl_nil (f : A → finset B) : Unionl [] f = ∅ := algebra.Prodl_nil f +theorem Unionl_cons (f : A → finset B) (a : A) (l : list A) : + Unionl (a::l) f = f a ∪ Unionl l f := algebra.Prodl_cons f a l +theorem Unionl_append (l₁ l₂ : list A) (f : A → finset B) : + Unionl (l₁++l₂) f = Unionl l₁ f ∪ Unionl l₂ f := algebra.Prodl_append l₁ l₂ f +theorem Unionl_mul (l : list A) (f g : A → finset B) : + Unionl l (λx, f x ∪ g x) = Unionl l f ∪ Unionl l g := algebra.Prodl_mul l f g +section deceqA + include deceqA + theorem Unionl_insert_of_mem (f : A → finset B) {a : A} {l : list A} (H : a ∈ l) : + Unionl (list.insert a l) f = Unionl l f := algebra.Prodl_insert_of_mem f H + theorem Unionl_insert_of_not_mem (f : A → finset B) {a : A} {l : list A} (H : a ∉ l) : + Unionl (list.insert a l) f = f a ∪ Unionl l f := algebra.Prodl_insert_of_not_mem f H + theorem Unionl_union {l₁ l₂ : list A} (f : A → finset B) (d : list.disjoint l₁ l₂) : + Unionl (list.union l₁ l₂) f = Unionl l₁ f ∪ Unionl l₂ f := algebra.Prodl_union f d + theorem Unionl_empty (l : list A) : Unionl l (λ x, ∅) = ∅ := algebra.Prodl_one l +end deceqA + +theorem Union_empty (f : A → finset B) : Union ∅ f = ∅ := algebra.Prod_empty f +theorem Union_mul (s : finset A) (f g : A → finset B) : + Union s (λx, f x ∪ g x) = Union s f ∪ Union s g := algebra.Prod_mul s f g +section deceqA + include deceqA + theorem Union_insert_of_mem (f : A → finset B) {a : A} {s : finset A} (H : a ∈ s) : + Union (insert a s) f = Union s f := algebra.Prod_insert_of_mem f H + theorem Union_insert_of_not_mem (f : A → finset B) {a : A} {s : finset A} (H : a ∉ s) : + Union (insert a s) f = f a ∪ Union s f := algebra.Prod_insert_of_not_mem f H + theorem Union_union (f : A → finset B) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) : + Union (s₁ ∪ s₂) f = Union s₁ f ∪ Union s₂ f := algebra.Prod_union f disj + theorem Union_ext {s : finset A} {f g : A → finset B} (H : ∀x, x ∈ s → f x = g x) : + Union s f = Union s g := algebra.Prod_ext H + theorem Union_empty' (s : finset A) : Union s (λ x, ∅) = ∅ := algebra.Prod_one s + + -- this will eventually be an instance of something more general + theorem inter_Union (s : finset B) (t : finset A) (f : A → finset B) : + s ∩ (⋃ x ∈ t, f x) = (⋃ x ∈ t, s ∩ f x) := + finset.induction_on t + (by rewrite [*Union_empty, inter_empty]) + (take s' x, assume H : x ∉ s', + assume IH, + by rewrite [*Union_insert_of_not_mem _ H, inter.distrib_left, IH]) + + theorem mem_Union_iff (s : finset A) (f : A → finset B) (b : B) : + b ∈ (⋃ x ∈ s, f x) ↔ (∃ x, x ∈ s ∧ b ∈ f x ) := + finset.induction_on s + (by rewrite [exists_mem_empty_eq]) + (take s' a, assume H : a ∉ s', assume IH, + by rewrite [Union_insert_of_not_mem _ H, mem_union_eq, IH, exists_mem_insert_eq]) + + theorem mem_Union_eq (s : finset A) (f : A → finset B) (b : B) : + b ∈ (⋃ x ∈ s, f x) = (∃ x, x ∈ s ∧ b ∈ f x ) := + propext !mem_Union_iff +end deceqA + +end union + +end finset diff --git a/library/data/finset/default.lean b/library/data/finset/default.lean index e674f993d..d3a4ecc9c 100644 --- a/library/data/finset/default.lean +++ b/library/data/finset/default.lean @@ -5,4 +5,4 @@ Author: Leonardo de Moura Finite sets. -/ -import .basic .comb .to_set .card +import .basic .comb .to_set .card .bigops diff --git a/library/data/finset/finset.md b/library/data/finset/finset.md index 744a37c1f..96ede67ae 100644 --- a/library/data/finset/finset.md +++ b/library/data/finset/finset.md @@ -7,3 +7,4 @@ Finite sets. By default, `import list` imports everything here. [comb](comb.lean) : combinators and list constructions [to_set](to_set.lean) : interactions with sets [card](card.lean) : cardinality +[bigops](bigops.lean) : finite unions and intersections diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean index c1de0b381..58e90b234 100644 --- a/library/data/nat/bigops.lean +++ b/library/data/nat/bigops.lean @@ -33,6 +33,7 @@ section deceqA Prodl (insert a l) f = f a * Prodl l f := algebra.Prodl_insert_of_not_mem f H theorem Prodl_union {l₁ l₂ : list A} (f : A → nat) (d : disjoint l₁ l₂) : Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d + theorem Prodl_one (l : list A) : Prodl l (λ x, nat.succ 0) = 1 := algebra.Prodl_one l end deceqA /- Prod -/ @@ -53,6 +54,7 @@ section deceqA Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.Prod_union f disj theorem Prod_ext {s : finset A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) : Prod s f = Prod s g := algebra.Prod_ext H + theorem Prod_one (s : finset A) : Prod s (λ x, nat.succ 0) = 1 := algebra.Prod_one s end deceqA /- Suml -/ @@ -75,6 +77,7 @@ section deceqA Suml (insert a l) f = f a + Suml l f := algebra.Suml_insert_of_not_mem f H theorem Suml_union {l₁ l₂ : list A} (f : A → nat) (d : disjoint l₁ l₂) : Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d + theorem Suml_zero (l : list A) : Suml l (λ x, zero) = 0 := algebra.Suml_zero l end deceqA /- Sum -/ @@ -95,6 +98,7 @@ section deceqA Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.Sum_union f disj theorem Sum_ext {s : finset A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) : Sum s f = Sum s g := algebra.Sum_ext H + theorem Sum_zero (s : finset A) : Sum s (λ x, zero) = 0 := algebra.Sum_zero s end deceqA end nat