diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index b2b62b903..ee8fdbf2d 100644 --- a/library/data/finset/basic.lean +++ b/library/data/finset/basic.lean @@ -460,6 +460,9 @@ quot.induction_on₃ s₁ s₂ s₃ (λ l₁ l₂ l₃ h₁ h₂, list.sub.trans theorem mem_of_subset_of_mem {s₁ s₂ : finset A} {a : A} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ := quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h₁ h₂, h₁ a h₂) +theorem subset_of_forall {s₁ s₂ : finset A} : (∀x, x ∈ s₁ → x ∈ s₂) → s₁ ⊆ s₂ := +quot.induction_on₂ s₁ s₂ (λ l₁ l₂ H, H) + /- upto -/ section upto definition upto (n : nat) : finset nat := diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean index 0a38648c4..7742349b1 100644 --- a/library/data/finset/comb.lean +++ b/library/data/finset/comb.lean @@ -10,96 +10,117 @@ open list quot subtype decidable perm function namespace finset -/- map -/ -section map +/- image (corresponds to map on list) -/ +section image variables {A B : Type} variable [h : decidable_eq B] include h -definition map (f : A → B) (s : finset A) : finset B := +definition image (f : A → B) (s : finset A) : finset B := quot.lift_on s (λ l, to_finset (list.map f (elt_of l))) (λ l₁ l₂ p, quot.sound (perm_erase_dup_of_perm (perm_map _ p))) -theorem map_empty (f : A → B) : map f ∅ = ∅ := +theorem image_empty (f : A → B) : image f ∅ = ∅ := rfl -end map + +theorem mem_image_of_mem (f : A → B) {s : finset A} {a : A} : a ∈ s → f a ∈ image f s := +quot.induction_on s (take l, assume H : a ∈ elt_of l, mem_to_finset (mem_map f H)) + +theorem exists_of_mem_image {f : A → B} {s : finset A} {b : B} : + b ∈ image f s → ∃a, a ∈ s ∧ f a = b := +quot.induction_on s + (take l, assume H : b ∈ erase_dup (list.map f (elt_of l)), + exists_of_mem_map (mem_of_mem_erase_dup H)) + +theorem mem_image_iff (f : A → B) {s : finset A} {y : B} : y ∈ image f s ↔ ∃x, x ∈ s ∧ f x = y := +iff.intro exists_of_mem_image + (assume H, + obtain x (H1 : x ∈ s ∧ f x = y), from H, + eq.subst (and.right H1) (mem_image_of_mem f (and.left H1))) + +theorem mem_image_eq (f : A → B) {s : finset A} {y : B} : y ∈ image f s = ∃x, x ∈ s ∧ f x = y := +propext (mem_image_iff f) +end image /- filter and set-builder notation -/ section filter - variables {A : Type} [deceq : decidable_eq A] - include deceq - variables (p : A → Prop) [decp : decidable_pred p] (s : finset A) {x : A} - include decp +variables {A : Type} [deceq : decidable_eq A] +include deceq +variables (p : A → Prop) [decp : decidable_pred p] (s : finset A) {x : A} +include decp - definition filter : finset A := - quot.lift_on s - (λl, to_finset_of_nodup - (list.filter p (subtype.elt_of l)) - (list.nodup_filter p (subtype.has_property l))) - (λ l₁ l₂ u, quot.sound (perm.perm_filter u)) +definition filter : finset A := +quot.lift_on s + (λl, to_finset_of_nodup + (list.filter p (subtype.elt_of l)) + (list.nodup_filter p (subtype.has_property l))) + (λ l₁ l₂ u, quot.sound (perm.perm_filter u)) - notation `{` binders ∈ s `|` r:(scoped:1 p, filter p s) `}` := r +notation `{` binders ∈ s `|` r:(scoped:1 p, filter p s) `}` := r - theorem filter_empty : filter p ∅ = ∅ := rfl +theorem filter_empty : filter p ∅ = ∅ := rfl - variables {p s} +variables {p s} - theorem of_mem_filter : x ∈ filter p s → p x := - quot.induction_on s (take l, list.of_mem_filter) +theorem of_mem_filter : x ∈ filter p s → p x := +quot.induction_on s (take l, list.of_mem_filter) - theorem mem_of_mem_filter : x ∈ filter p s → x ∈ s := - quot.induction_on s (take l, list.mem_of_mem_filter) +theorem mem_of_mem_filter : x ∈ filter p s → x ∈ s := +quot.induction_on s (take l, list.mem_of_mem_filter) - theorem mem_filter_of_mem {x : A} : x ∈ s → p x → x ∈ filter p s := - quot.induction_on s (take l, list.mem_filter_of_mem) +theorem mem_filter_of_mem {x : A} : x ∈ s → p x → x ∈ filter p s := +quot.induction_on s (take l, list.mem_filter_of_mem) - variables (p s) +variables (p s) - theorem mem_filter_eq : x ∈ filter p s = (x ∈ s ∧ p x) := - propext (iff.intro - (assume H, and.intro (mem_of_mem_filter H) (of_mem_filter H)) - (assume H, mem_filter_of_mem (and.left H) (and.right H))) +theorem mem_filter_iff : x ∈ filter p s ↔ x ∈ s ∧ p x := +iff.intro + (assume H, and.intro (mem_of_mem_filter H) (of_mem_filter H)) + (assume H, mem_filter_of_mem (and.left H) (and.right H)) + +theorem mem_filter_eq : x ∈ filter p s = (x ∈ s ∧ p x) := +propext !mem_filter_iff end filter /- set difference -/ section diff - variables {A : Type} [deceq : decidable_eq A] - include deceq +variables {A : Type} [deceq : decidable_eq A] +include deceq - definition diff (s t : finset A) : finset A := {x ∈ s | x ∉ t} - infix `\`:70 := diff +definition diff (s t : finset A) : finset A := {x ∈ s | x ∉ t} +infix `\`:70 := diff - theorem mem_of_mem_diff {s t : finset A} {x : A} (H : x ∈ s \ t) : x ∈ s := - mem_of_mem_filter H +theorem mem_of_mem_diff {s t : finset A} {x : A} (H : x ∈ s \ t) : x ∈ s := +mem_of_mem_filter H - theorem not_mem_of_mem_diff {s t : finset A} {x : A} (H : x ∈ s \ t) : x ∉ t := - of_mem_filter H +theorem not_mem_of_mem_diff {s t : finset A} {x : A} (H : x ∈ s \ t) : x ∉ t := +of_mem_filter H - theorem mem_diff {s t : finset A} {x : A} (H1 : x ∈ s) (H2 : x ∉ t) : x ∈ s \ t := - mem_filter_of_mem H1 H2 +theorem mem_diff {s t : finset A} {x : A} (H1 : x ∈ s) (H2 : x ∉ t) : x ∈ s \ t := +mem_filter_of_mem H1 H2 - theorem mem_diff_iff (s t : finset A) (x : A) : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t := - iff.intro - (assume H, and.intro (mem_of_mem_diff H) (not_mem_of_mem_diff H)) - (assume H, mem_diff (and.left H) (and.right H)) +theorem mem_diff_iff (s t : finset A) (x : A) : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t := +iff.intro + (assume H, and.intro (mem_of_mem_diff H) (not_mem_of_mem_diff H)) + (assume H, mem_diff (and.left H) (and.right H)) - theorem mem_diff_eq (s t : finset A) (x : A) : x ∈ s \ t = (x ∈ s ∧ x ∉ t) := - propext !mem_diff_iff +theorem mem_diff_eq (s t : finset A) (x : A) : x ∈ s \ t = (x ∈ s ∧ x ∉ t) := +propext !mem_diff_iff - theorem union_diff_cancel {s t : finset A} (H : s ⊆ t) : s ∪ (t \ s) = t := - ext (take x, iff.intro - (assume H1 : x ∈ s ∪ (t \ s), - or.elim (mem_or_mem_of_mem_union H1) - (assume H2 : x ∈ s, mem_of_subset_of_mem H H2) - (assume H2 : x ∈ t \ s, mem_of_mem_diff H2)) - (assume H1 : x ∈ t, - decidable.by_cases - (assume H2 : x ∈ s, mem_union_left _ H2) - (assume H2 : x ∉ s, mem_union_right _ (mem_diff H1 H2)))) +theorem union_diff_cancel {s t : finset A} (H : s ⊆ t) : s ∪ (t \ s) = t := +ext (take x, iff.intro + (assume H1 : x ∈ s ∪ (t \ s), + or.elim (mem_or_mem_of_mem_union H1) + (assume H2 : x ∈ s, mem_of_subset_of_mem H H2) + (assume H2 : x ∈ t \ s, mem_of_mem_diff H2)) + (assume H1 : x ∈ t, + decidable.by_cases + (assume H2 : x ∈ s, mem_union_left _ H2) + (assume H2 : x ∉ s, mem_union_right _ (mem_diff H1 H2)))) - theorem diff_union_cancel {s t : finset A} (H : s ⊆ t) : (t \ s) ∪ s = t := - eq.subst !union.comm (!union_diff_cancel H) +theorem diff_union_cancel {s t : finset A} (H : s ⊆ t) : (t \ s) ∪ s = t := +eq.subst !union.comm (!union_diff_cancel H) end diff /- all -/ @@ -119,7 +140,14 @@ quot.induction_on s (λ l i h, list.of_mem_of_all i h) theorem forall_of_all {p : A → Prop} {s : finset A} (H : all s p) : ∀{a}, a ∈ s → p a := λ a H', of_mem_of_all H' H -definition decidable_all (p : A → Prop) [h : decidable_pred p] (s : finset A) : decidable (all s p) := +theorem all_of_forall {p : A → Prop} {s : finset A} : (∀a, a ∈ s → p a) → all s p := +quot.induction_on s (λ l H, list.all_of_forall H) + +theorem all_iff_forall (p : A → Prop) (s : finset A) : all s p ↔ (∀a, a ∈ s → p a) := +iff.intro forall_of_all all_of_forall + +definition decidable_all [instance] (p : A → Prop) [h : decidable_pred p] (s : finset A) : + decidable (all s p) := quot.rec_on_subsingleton s (λ l, list.decidable_all p (elt_of l)) theorem all_implies {p q : A → Prop} {s : finset A} : all s p → (∀ x, p x → q x) → all s q := @@ -148,6 +176,14 @@ quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_inter_of_all_left _ h) theorem all_inter_of_all_right {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₂ p → all (s₁ ∩ s₂) p := quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_inter_of_all_right _ h) + +theorem subset_iff_all (s t : finset A) : s ⊆ t ↔ all s (λ x, x ∈ t) := +iff.intro + (assume H : s ⊆ t, all_of_forall (take x, assume H1, mem_of_subset_of_mem H H1)) + (assume H : all s (λ x, x ∈ t), subset_of_forall (take x, assume H1 : x ∈ s, of_mem_of_all H1 H)) + +definition decidable_subset [instance] (s t : finset A) : decidable (s ⊆ t) := +decidable_of_decidable_of_iff _ (iff.symm !subset_iff_all) end all /- any -/ @@ -166,6 +202,13 @@ quot.induction_on s (λ l H, list.exists_of_any H) theorem any_of_mem {p : A → Prop} {s : finset A} {a : A} : a ∈ s → p a → any s p := quot.induction_on s (λ l H1 H2, list.any_of_mem H1 H2) +theorem any_of_exists {p : A → Prop} {s : finset A} (H : ∃a, a ∈ s ∧ p a) : any s p := +obtain a H', from H, +any_of_mem (and.left H') (and.right H') + +theorem any_iff_exists (p : A → Prop) (s : finset A) : any s p ↔ (∃a, a ∈ s ∧ p a) := +iff.intro exists_of_any any_of_exists + theorem any_of_insert [h : decidable_eq A] {p : A → Prop} (s : finset A) {a : A} (H : p a) : any (insert a s) p := any_of_mem (mem_insert a s) H @@ -175,13 +218,9 @@ theorem any_of_insert_right [h : decidable_eq A] {p : A → Prop} {s : finset A} obtain b (H' : b ∈ s ∧ p b), from exists_of_any H, any_of_mem (mem_insert_of_mem a (and.left H')) (and.right H') -theorem any_of_exists {p : A → Prop} {s : finset A} (H : ∃a, a ∈ s ∧ p a) : any s p := -obtain a H', from H, -any_of_mem (and.left H') (and.right H') - -definition decidable_any (p : A → Prop) [h : decidable_pred p] (s : finset A) : decidable (any s p) := +definition decidable_any [instance] (p : A → Prop) [h : decidable_pred p] (s : finset A) : + decidable (any s p) := quot.rec_on_subsingleton s (λ l, list.decidable_any p (elt_of l)) - end any section product diff --git a/library/data/finset/finset.md b/library/data/finset/finset.md new file mode 100644 index 000000000..27f2ac2b0 --- /dev/null +++ b/library/data/finset/finset.md @@ -0,0 +1,9 @@ +data.finset +=========== + +Finite sets. By default, `import list` imports everything here. + +[basic](basic.lean) : basic operations and properties +[comb](comb.lean) : combinators and list constructions +[card](card.lean) : cardinality +[bigop](bigop.lean) : "big" operations \ No newline at end of file diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index 9f5e1b4c1..d0f3d239a 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -1,11 +1,9 @@ /- Copyright (c) 2015 Leonardo de Moura. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. - -Module: data.list.comb Authors: Leonardo de Moura -List combinators +List combinators. -/ import data.list.basic open nat prod decidable function helper_tactics @@ -43,6 +41,16 @@ theorem mem_map {A B : Type} (f : A → B) : ∀ {a l}, a ∈ l → f a ∈ map (λ aeqx : a = x, by rewrite [aeqx, map_cons]; apply mem_cons) (λ ainxs : a ∈ xs, or.inr (mem_map ainxs)) +theorem exists_of_mem_map {A B : Type} {f : A → B} {b : B} : + ∀{l}, b ∈ map f l → ∃a, a ∈ l ∧ f a = b +| [] H := false.elim H +| (c::l) H := or.elim (iff.mp !mem_cons_iff H) + (assume H1 : b = f c, + exists.intro c (and.intro !mem_cons (eq.symm H1))) + (assume H1 : b ∈ map f l, + obtain a (H : a ∈ l ∧ f a = b), from exists_of_mem_map H1, + exists.intro a (and.intro (mem_cons_of_mem _ (and.left H)) (and.right H))) + theorem eq_of_map_const {A B : Type} {b₁ b₂ : B} : ∀ {l : list A}, b₁ ∈ map (const A b₂) l → b₁ = b₂ | [] h := absurd h !not_mem_nil | (a::l) h := @@ -98,7 +106,7 @@ theorem mem_filter_of_mem {p : A → Prop} [h : decidable_pred p] {a : A} : ∀ (λ aeqb : a = b, absurd (eq.rec_on aeqb pa) npb) (λ ainl : a ∈ l, by rewrite [filter_cons_of_neg _ npb]; exact (mem_filter_of_mem ainl pa))) -theorem filter_subset {p : A → Prop} [h : decidable_pred p] (l : list A) : filter p l ⊆ l := +theorem filter_sub {p : A → Prop} [h : decidable_pred p] (l : list A) : filter p l ⊆ l := λ a ain, mem_of_mem_filter ain theorem filter_append {p : A → Prop} [h : decidable_pred p] : ∀ (l₁ l₂ : list A), filter p (l₁++l₂) = filter p l₁ ++ filter p l₂