feat(library/data/finset/finset.md): add markdown file

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 :=

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

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

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₂