lean2/library/data/finset/bigops.lean

136 lines
5.4 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad, Haitao Zhang
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) [decidable_eq B] :
comm_monoid (finset B) :=
⦃ comm_monoid,
mul := union,
mul_assoc := union_assoc,
one := empty,
mul_one := union_empty,
one_mul := empty_union,
mul_comm := union_comm
local attribute finset.to_comm_monoid_Union [instance]
include deceqB
definition Unionl (l : list A) (f : A → finset B) : finset B := Prodl l f
notation `` binders `←` l, r:(scoped f, Unionl l f) := r
definition Union (s : finset A) (f : A → finset B) : finset B := finset.Prod s f
notation `` binders `∈` s, r:(scoped f, finset.Union s f) := r
theorem Unionl_nil (f : A → finset B) : Unionl [] f = ∅ := Prodl_nil f
theorem Unionl_cons (f : A → finset B) (a : A) (l : list A) :
Unionl (a::l) f = f a Unionl l f := 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 := 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 := 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 := 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 := 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 := Prodl_union f d
theorem Unionl_empty (l : list A) : Unionl l (λ x, ∅) = (∅ : finset B) := Prodl_one l
end deceqA
theorem Union_empty (f : A → finset B) : Union ∅ f = ∅ := finset.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 := finset.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 := finset.Prod_insert_of_mem f H
private 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 := finset.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 := finset.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 := finset.Prod_ext H
theorem Union_empty' (s : finset A) : Union s (λ x, ∅) = (∅ : finset B) := finset.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) :=
begin
induction t with s' x H IH,
rewrite [*Union_empty, inter_empty],
rewrite [*Union_insert_of_not_mem _ H, inter_distrib_left, IH],
end
theorem mem_Union_iff (s : finset A) (f : A → finset B) (b : B) :
b ∈ ( x ∈ s, f x) ↔ (∃ x, x ∈ s ∧ b ∈ f x ) :=
begin
induction s with s' a H IH,
rewrite [exists_mem_empty_eq],
rewrite [Union_insert_of_not_mem _ H, mem_union_eq, IH, exists_mem_insert_eq]
end
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
theorem Union_insert (f : A → finset B) {a : A} {s : finset A} :
Union (insert a s) f = f a Union s f :=
decidable.by_cases
(assume Pin : a ∈ s,
begin
rewrite [Union_insert_of_mem f Pin],
apply ext,
intro x,
apply iff.intro,
exact mem_union_r,
rewrite [mem_union_eq],
intro Por,
exact or.elim Por
(assume Pl, begin
rewrite mem_Union_eq, exact (exists.intro a (and.intro Pin Pl)) end)
(assume Pr, Pr)
end)
(assume H : a ∉ s, !Union_insert_of_not_mem H)
lemma image_eq_Union_index_image (s : finset A) (f : A → finset B) :
Union s f = Union (image f s) id :=
finset.induction_on s
(by rewrite Union_empty)
(take s1 a Pa IH, by rewrite [image_insert, *Union_insert, IH])
lemma Union_const [decidable_eq B] {f : A → finset B} {s : finset A} {t : finset B} :
s ≠ ∅ → (∀ x, x ∈ s → f x = t) → Union s f = t :=
begin
induction s with a' s' H IH,
{intros [H1, H2], exfalso, apply H1 !rfl},
intros [H1, H2],
rewrite [Union_insert, H2 _ !mem_insert],
cases (decidable.em (s' = ∅)) with [seq, sne],
{rewrite [seq, Union_empty, union_empty]},
have H3 : ∀ x, x ∈ s' → f x = t, from (λ x H', H2 x (mem_insert_of_mem _ H')),
rewrite [IH sne H3, union_self]
end
end deceqA
end union
end finset