feat(library/data/{set,finset}): add more cardinality facts, rename, and add a lemma from Haitao

library/data/finset/basic.lean

@@ -47,6 +47,17 @@ definition to_finset_of_nodup (l : list A) (n : nodup l) : finset A :=
 definition to_finset [h : decidable_eq A] (l : list A) : finset A :=
 ⟦to_nodup_list l⟧
 
+lemma to_finset_eq_of_nodup [h : decidable_eq A] {l : list A} (n : nodup l) :
+  to_finset_of_nodup l n = to_finset l :=
+assert P : to_nodup_list_of_nodup n = to_nodup_list l, from
+  begin
+    rewrite [↑to_nodup_list, ↑to_nodup_list_of_nodup],
+    generalize (@nodup_erase_dup A h l),
+    rewrite [erase_dup_eq_of_nodup n], intro x, apply congr_arg (subtype.tag l),
+    apply proof_irrel
+  end,
+quot.sound (eq.subst P !setoid.refl)
+
 definition has_decidable_eq [instance] [h : decidable_eq A] : decidable_eq (finset A) :=
 λ s₁ s₂, quot.rec_on_subsingleton₂ s₁ s₂
   (λ l₁ l₂,
@@ -194,6 +205,12 @@ theorem card_insert_of_not_mem {a : A} {s : finset A} : a ∉ s → card (insert
 quot.induction_on s
   (λ (l : nodup_list A) (nainl : a ∉ ⟦l⟧), list.length_insert_of_not_mem nainl)
 
+theorem card_insert_le (a : A) (s : finset A) :
+  card (insert a s) ≤ card s + 1 :=
+decidable.by_cases
+  (assume H : a ∈ s, by rewrite [card_insert_of_mem H]; apply le_succ)
+  (assume H : a ∉ s, by rewrite [card_insert_of_not_mem H])
+
 protected theorem induction [recursor 6] {P : finset A → Prop}
     (H1 : P empty)
     (H2 : ∀ ⦃a : A⦄, ∀{s : finset A}, a ∉ s → P s → P (insert a s)) :

library/data/finset/card.lean

@@ -91,6 +91,65 @@ assert Psub : _, from and.right Pinj,
 assert Ple : card (image f a) ≤ card b, from card_le_card_of_subset Psub,
 by rewrite [(card_image_eq_of_inj_on (and.left Pinj))⁻¹]; exact Ple
 
+theorem card_image_le (f : A → B) (s : finset A) : card (image f s) ≤ card s :=
+finset.induction_on s
+  (by rewrite finset.image_empty)
+  (take a s',
+    assume Ha : a ∉ s',
+    assume IH : card (image f s') ≤ card s',
+    begin
+      rewrite [image_insert, card_insert_of_not_mem Ha],
+      apply le.trans !card_insert_le,
+      apply add_le_add_right IH
+    end)
+
+theorem inj_on_of_card_image_eq {f : A → B} {s : finset A} :
+  card (image f s) = card s → inj_on f (ts s) :=
+finset.induction_on s
+  (by intro H; xrewrite to_set_empty; apply inj_on_empty)
+  (begin
+    intro a s' Ha IH,
+    rewrite [image_insert, card_insert_of_not_mem Ha],
+    xrewrite [to_set_insert],
+    assume H1 : card (insert (f a) (image f s')) = card s' + 1,
+    show inj_on f (set.insert a (ts s')), from
+      decidable.by_cases
+        (assume Hfa : f a ∈ image f s',
+           have H2 : card (image f s') = card s' + 1,
+             by rewrite [card_insert_of_mem Hfa at H1]; assumption,
+           absurd
+             (calc
+               card (image f s') ≤ card s'           : !card_image_le
+                             ... < card s' + 1       : lt_succ_self
+                             ... = card (image f s') : H2)
+             !lt.irrefl)
+        (assume Hnfa : f a ∉ image f s',
+           have H2 : card (image f s') + 1 = card s' + 1,
+             by rewrite [card_insert_of_not_mem Hnfa at H1]; assumption,
+           have H3 : card (image f s') = card s', from add.cancel_right H2,
+           have injf : inj_on f (ts s'), from IH H3,
+           show inj_on f (set.insert a (ts s')), from
+             take x1 x2,
+             assume Hx1 : x1 ∈ set.insert a (ts s'),
+             assume Hx2 : x2 ∈ set.insert a (ts s'),
+             assume feq : f x1 = f x2,
+             or.elim Hx1
+               (assume Hx1' : x1 = a,
+                 or.elim Hx2
+                   (assume Hx2' : x2 = a, by rewrite [Hx1', Hx2'])
+                   (assume Hx2' : x2 ∈ ts s',
+                     have Hfa : f a ∈ image f s',
+                       by rewrite [-Hx1', feq]; apply mem_image_of_mem f Hx2',
+                     absurd Hfa Hnfa))
+               (assume Hx1' : x1 ∈ ts s',
+                 or.elim Hx2
+                   (assume Hx2' : x2 = a,
+                     have Hfa : f a ∈ image f s',
+                       by rewrite [-Hx2', -feq]; apply mem_image_of_mem f Hx1',
+                     absurd Hfa Hnfa)
+                   (assume Hx2' : x2 ∈ ts s', injf Hx1' Hx2' feq)))
+    end)
+
 end card_image
 
 theorem Sum_const_eq_card_mul (s : finset A) (n : nat) : (∑ x ∈ s, n) = card s * n :=

library/data/finset/to_set.lean

@@ -16,7 +16,7 @@ variable [deceq : decidable_eq A]
 definition to_set (s : finset A) : set A := λx, x ∈ s
 abbreviation ts := @to_set A
 
-variables (s t : finset A) (x : A)
+variables (s t : finset A) (x y : A)
 
 theorem mem_eq_mem_to_set : (x ∈ s) = (x ∈ ts s) := rfl
 
@@ -37,13 +37,16 @@ theorem to_set_univ [h : fintype A] : ts univ = (set.univ : set A) := funext (λ
 
 include deceq
 
-theorem mem_to_set_union : (x ∈ ts (s ∪ t)) = (x ∈ ts s ∪ ts t) := !finset.mem_union_eq
+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_union : x ∈ ts (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 ∈ ts (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 ∈ ts (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] :

library/data/set/function.lean

@@ -35,26 +35,29 @@ setext (take y, iff.intro
     have H5 : f1 x = y, from (H1 H4) ⬝ and.right H3,
     exists.intro x (and.intro H4 H5)))
 
-theorem in_image {f : X → Y} {a : set X} {x : X} {y : Y}
+theorem mem_image {f : X → Y} {a : set X} {x : X} {y : Y}
   (H1 : x ∈ a) (H2 : f x = y) : y ∈ f '[a] :=
 exists.intro x (and.intro H1 H2)
 
+theorem mem_image_of_mem (f : X → Y) {x : X} {a : set X} (H : x ∈ a) : f x ∈ image f a :=
+mem_image H rfl
+
 lemma image_compose (f : Y → Z) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
 setext (take z,
   iff.intro
     (assume Hz : z ∈ (f ∘ g) '[a],
       obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
-      have Hgx : g x ∈ g '[a], from in_image Hx₁ rfl,
-      show z ∈ f '[g '[a]], from in_image Hgx Hx₂)
+      have Hgx : g x ∈ g '[a], from mem_image Hx₁ rfl,
+      show z ∈ f '[g '[a]], from mem_image Hgx Hx₂)
     (assume Hz : z ∈ f '[g '[a]],
       obtain y (Hy₁ : y ∈ g '[a]) (Hy₂ : f y = z), from Hz,
       obtain x (Hz₁ : x ∈ a) (Hz₂ : g x = y),      from Hy₁,
-      show z ∈ (f ∘ g) '[a], from in_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
+      show z ∈ (f ∘ g) '[a], from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
 
 lemma image_subset {a b : set X} (f : X → Y) (H : a ⊆ b) : f '[a] ⊆ f '[b] :=
 take y, assume Hy : y ∈ f '[a],
 obtain x (Hx₁ : x ∈ a) (Hx₂ : f x = y), from Hy,
-in_image (H Hx₁) Hx₂
+mem_image (H Hx₁) Hx₂
 
 /- maps to -/
 
@@ -80,6 +83,9 @@ take x, assume H, trivial
 definition inj_on [reducible] (f : X → Y) (a : set X) : Prop :=
 ∀⦃x1 x2 : X⦄, x1 ∈ a → x2 ∈ a → f x1 = f x2 → x1 = x2
 
+theorem inj_on_empty (f : X → Y) : inj_on f ∅ :=
+  take x₁ x₂, assume H₁ H₂ H₃, false.elim H₁
+
 theorem inj_on_of_eq_on {f1 f2 : X → Y} {a : set X} (eq_f1_f2 : eq_on f1 f2 a)
     (inj_f1 : inj_on f1 a) :
   inj_on f2 a :=
@@ -147,7 +153,7 @@ lemma surjective_iff_surj_on_univ {f : X → Y} : surjective f ↔ surj_on f uni
 iff.intro
   (assume H, take y, assume Hy,
     obtain x Hx, from H y,
-    in_image trivial Hx)
+    mem_image trivial Hx)
   (assume H, take y,
     obtain x H1x H2x, from H y trivial,
     exists.intro x H2x)