feat,refactor(library/data/finset/*): add priorities for finset notation, add some theorems

library/data/finset/basic.lean

@@ -41,6 +41,9 @@ quot (finset.nodup_list_setoid A)
 
 namespace finset
 
+-- give finset notation higher priority than set notation, so that it is tried first
+protected definition prio : num := num.succ std.priority.default
+
 definition to_finset_of_nodup (l : list A) (n : nodup l) : finset A :=
 ⟦to_nodup_list_of_nodup n⟧
 
@@ -71,8 +74,8 @@ quot.lift_on s (λ l, a ∈ elt_of l)
    (λ ainl₁, mem_perm e ainl₁)
    (λ ainl₂, mem_perm (perm.symm e) ainl₂)))
 
-infix `∈` := mem
-notation a ∉ b := ¬ mem a b
+infix [priority finset.prio] `∈` := mem
+notation [priority finset.prio] a ∉ b := ¬ mem a b
 
 theorem mem_of_mem_list {a : A} {l : nodup_list A} : a ∈ elt_of l → a ∈ ⟦l⟧ :=
 λ ainl, ainl
@@ -117,7 +120,7 @@ quot.induction_on₂ s₁ s₂ (λ l₁ l₂ e, quot.sound (perm_ext (has_proper
 definition empty : finset A :=
 to_finset_of_nodup [] nodup_nil
 
-notation `∅` := !empty
+notation [priority finset.prio] `∅` := !empty
 
 theorem not_mem_empty [simp] (a : A) : a ∉ ∅ :=
 λ aine : a ∈ ∅, aine
@@ -166,8 +169,7 @@ quot.lift_on s
   (λ (l₁ l₂ : nodup_list A) (p : l₁ ~ l₂), quot.sound (perm_insert a p))
 
 -- set builder notation
-notation `'{`:max a:(foldr `,` (x b, insert x b) ∅) `}`:0 := a
--- notation `⦃` a:(foldr `,` (x b, insert x b) ∅) `⦄` := a
+notation [priority finset.prio] `'{`:max a:(foldr `,` (x b, insert x b) ∅) `}`:0 := a
 
 theorem mem_insert (a : A) (s : finset A) : a ∈ insert a s :=
 quot.induction_on s
@@ -338,7 +340,7 @@ quot.lift_on₂ s₁ s₂
                        (nodup_union_of_nodup_of_nodup (has_property l₁) (has_property l₂)))
   (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_union p₁ p₂))
 
-notation s₁ ∪ s₂ := union s₁ s₂
+infix [priority finset.prio] ∪ := union
 
 theorem mem_union_left {a : A} {s₁ : finset A} (s₂ : finset A) : a ∈ s₁ → a ∈ s₁ ∪ s₂ :=
 quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁, list.mem_union_left _ ainl₁)
@@ -415,7 +417,7 @@ quot.lift_on₂ s₁ s₂
                        (nodup_inter_of_nodup _ (has_property l₁)))
   (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_inter p₁ p₂))
 
-notation s₁ ∩ s₂ := inter s₁ s₂
+infix [priority finset.prio] ∩ := inter
 
 theorem mem_of_mem_inter_left {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₁ :=
 quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_inter_left ainl₁l₂)
@@ -544,7 +546,7 @@ quot.lift_on₂ s₁ s₂
     (λ s₁ a i, mem_perm p₂ (s₁ a (mem_perm (perm.symm p₁) i)))
     (λ s₂ a i, mem_perm (perm.symm p₂) (s₂ a (mem_perm p₁ i)))))
 
-infix `⊆` := subset
+infix [priority finset.prio] `⊆` := subset
 
 theorem empty_subset (s : finset A) : ∅ ⊆ s :=
 quot.induction_on s (λ l, list.nil_sub (elt_of l))

library/data/finset/comb.lean

@@ -20,7 +20,7 @@ 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)))
-notation f `'[`:max a `]` := image f a
+notation [priority finset.prio] f `'[`:max a `]` := image f a
 
 theorem image_empty (f : A → B) : image f ∅ = ∅ :=
 rfl
@@ -125,7 +125,7 @@ quot.lift_on s
     (list.nodup_filter p (subtype.has_property l)))
   (λ l₁ l₂ u, quot.sound (perm.perm_filter u))
 
-notation `{` binder ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
+notation [priority finset.prio] `{` binder ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
 
 theorem filter_empty : filter p ∅ = ∅ := rfl
 
@@ -157,16 +157,28 @@ 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) :=
+section
+
+variables {A : Type} [deceqA : decidable_eq A]
+include deceqA
+
+theorem eq_filter_of_subset {s t : finset A} (ssubt : s ⊆ t) : s = {x ∈ t | x ∈ s} :=
+ext (take x, iff.intro
+  (suppose x ∈ s, mem_filter_of_mem (mem_of_subset_of_mem ssubt this) this)
+  (suppose x ∈ {x ∈ t | x ∈ s}, of_mem_filter this))
+
+theorem mem_singleton_eq' (x a : A) : x ∈ '{a} = (x = a) :=
 by rewrite [mem_insert_eq, mem_empty_eq, or_false]
 
+end
+
 /- set difference -/
 section diff
 variables {A : Type} [deceq : decidable_eq A]
 include deceq
 
 definition diff (s t : finset A) : finset A := {x ∈ s | x ∉ t}
-infix `\`:70 := diff
+infix [priority finset.prio] `\`:70 := diff
 
 theorem mem_of_mem_diff {s t : finset A} {x : A} (H : x ∈ s \ t) : x ∈ s :=
 mem_of_mem_filter H
@@ -309,7 +321,7 @@ quot.lift_on₂ s₁ s₂
                        (nodup_product (has_property l₁) (has_property l₂)))
   (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_product p₁ p₂))
 
-infix * := product
+infix [priority finset.prio] * := product
 
 theorem empty_product (s : finset B) : @empty A * s = ∅ :=
 quot.induction_on s (λ l, rfl)

library/data/finset/to_set.lean

@@ -13,7 +13,7 @@ namespace finset
 variable {A : Type}
 variable [deceq : decidable_eq A]
 
-definition to_set (s : finset A) : set A := λx, x ∈ s
+definition to_set [coercion] (s : finset A) : set A := λx, x ∈ s
 abbreviation ts := @to_set A
 
 variables (s t : finset A) (x y : A)
@@ -37,27 +37,27 @@ theorem to_set_univ [h : fintype A] : ts univ = (set.univ : set A) := funext (λ
 
 include deceq
 
-theorem mem_to_set_insert : x ∈ ts (insert y s) = (x ∈ set.insert y (ts s)) := !finset.mem_insert_eq
-theorem to_set_insert : ts (insert y s) = set.insert y (ts s) := funext (λ x, !mem_to_set_insert)
+theorem mem_to_set_insert : x ∈ insert y s = (x ∈ set.insert y s) := !finset.mem_insert_eq
+theorem to_set_insert : insert y s = set.insert y s := funext (λ x, !mem_to_set_insert)
 
-theorem mem_to_set_union : x ∈ ts (s ∪ t) = (x ∈ ts s ∪ ts t) := !finset.mem_union_eq
+theorem mem_to_set_union : x ∈ s ∪ t = (x ∈ ts s ∪ ts t) := !finset.mem_union_eq
 theorem to_set_union : ts (s ∪ t) = ts s ∪ ts t := funext (λ x, !mem_to_set_union)
 
-theorem mem_to_set_inter : x ∈ ts (s ∩ t) = (x ∈ ts s ∩ ts t) := !finset.mem_inter_eq
+theorem mem_to_set_inter : x ∈ s ∩ t = (x ∈ ts s ∩ ts t) := !finset.mem_inter_eq
 theorem to_set_inter : ts (s ∩ t) = ts s ∩ ts t := funext (λ x, !mem_to_set_inter)
 
-theorem mem_to_set_diff : x ∈ ts (s \ t) = (x ∈ ts s \ ts t) := !finset.mem_diff_eq
+theorem mem_to_set_diff : x ∈ s \ t = (x ∈ ts s \ ts t) := !finset.mem_diff_eq
 theorem to_set_diff : ts (s \ t) = ts s \ ts t := funext (λ x, !mem_to_set_diff)
 
-theorem mem_to_set_filter (p : A → Prop) [h : decidable_pred p] :
-  (x ∈ ts (finset.filter p s)) = (x ∈ set.filter p (ts s)) := !finset.mem_filter_eq
-theorem to_set_filter (p : A → Prop) [h : decidable_pred p] :
-  ts (finset.filter p s) = set.filter p (ts s) := funext (λ x, !mem_to_set_filter)
+theorem mem_to_set_filter (p : A → Prop) [h : decidable_pred p] : x ∈ filter p s = (x ∈ set.filter p s) := 
+  !finset.mem_filter_eq
+theorem to_set_filter (p : A → Prop) [h : decidable_pred p] : filter p s = set.filter p s := 
+  funext (λ x, !mem_to_set_filter)
 
 theorem mem_to_set_image {B : Type} [h : decidable_eq B] (f : A → B) {s : finset A} {y : B} :
-  (y ∈ ts (finset.image f s)) = (y ∈ set.image f (ts s)) := !finset.mem_image_eq
+  y ∈ image f s = (y ∈ set.image f s) := !finset.mem_image_eq
 theorem to_set_image {B : Type} [h : decidable_eq B] (f : A → B) (s : finset A) :
-  ts (finset.image f s) = set.image f (ts s) := funext (λ x, !mem_to_set_image)
+  image f s = set.image f s := funext (λ x, !mem_to_set_image)
 
 /- relations -/
 

library/data/set/basic.lean

@@ -182,6 +182,13 @@ notation `{` binder ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
 definition insert (x : X) (a : set X) : set X := {y : X | y = x ∨ y ∈ a}
 notation `'{`:max a:(foldr `,` (x b, insert x b) ∅) `}`:0 := a
 
+/- filter -/
+
+theorem eq_filter_of_subset {s t : set X} (ssubt : s ⊆ t) : s = {x ∈ t | x ∈ s} :=
+setext (take x, iff.intro
+  (suppose x ∈ s, and.intro (ssubt this) this)
+  (suppose x ∈ {x ∈ t | x ∈ s}, and.right this))
+
 /- set difference -/
 
 definition diff (s t : set X) : set X := {x ∈ s | x ∉ t}
@@ -196,6 +203,8 @@ and.right H
 theorem mem_diff {s t : set X} {x : X} (H1 : x ∈ s) (H2 : x ∉ t) : x ∈ s \ t :=
 and.intro H1 H2
 
+theorem diff_eq (s t : set X) : s \ t = {x ∈ s | x ∉ t} := rfl
+
 theorem mem_diff_iff (s t : set X) (x : X) : x ∈ s \ t ↔ x ∈ s ∧ x ∉ t := !iff.refl
 
 theorem mem_diff_eq (s t : set X) (x : X) : x ∈ s \ t = (x ∈ s ∧ x ∉ t) := rfl