feat(data/finset): powerset_len (subsets of a given size) (#899)

* feat(data/finset): powerset_len (subsets of a given size)

* fix build

src/algebra/char_p.lean

@@ -59,7 +59,7 @@ theorem ring_char.eq (α : Type u) [semiring α] {p : ℕ} (C : char_p α p) : p
 theorem add_pow_char (α : Type u) [comm_ring α] {p : ℕ} (hp : nat.prime p)
   [char_p α p] (x y : α) : (x + y)^p = x^p + y^p :=
 begin
-  rw [add_pow, finset.sum_range_succ, nat.sub_self, pow_zero, choose_self],
+  rw [add_pow, finset.sum_range_succ, nat.sub_self, pow_zero, nat.choose_self],
   rw [nat.cast_one, mul_one, mul_one, add_left_inj],
   transitivity,
   { refine finset.sum_eq_single 0 _ _,
@@ -68,7 +68,7 @@ begin
       rw [← nat.div_mul_cancel this, nat.cast_mul, char_p.cast_eq_zero α p],
       simp only [mul_zero] },
     { intro H, exfalso, apply H, exact finset.mem_range.2 hp.pos } },
-  rw [pow_zero, nat.sub_zero, one_mul, choose_zero_right, nat.cast_one, mul_one]
+  rw [pow_zero, nat.sub_zero, one_mul, nat.choose_zero_right, nat.cast_one, mul_one]
 end
 
 /-- The frobenius map that sends x to x^p -/

src/data/complex/exponential.lean

@@ -381,12 +381,12 @@ have hj : ∀ j : ℕ, (range j).sum
     finset.sum_congr rfl (λ m hm, begin
       rw [add_pow, div_eq_mul_inv, sum_mul],
       refine finset.sum_congr rfl (λ i hi, _),
-      have h₁ : (choose m i : ℂ) ≠ 0 := nat.cast_ne_zero.2
-        (nat.pos_iff_ne_zero.1 (choose_pos (nat.le_of_lt_succ (mem_range.1 hi)))),
-      have h₂ := choose_mul_fact_mul_fact (nat.le_of_lt_succ $ finset.mem_range.1 hi),
+      have h₁ : (nat.choose m i : ℂ) ≠ 0 := nat.cast_ne_zero.2
+        (nat.pos_iff_ne_zero.1 (nat.choose_pos (nat.le_of_lt_succ (mem_range.1 hi)))),
+      have h₂ := nat.choose_mul_fact_mul_fact (nat.le_of_lt_succ $ finset.mem_range.1 hi),
       rw [← h₂, nat.cast_mul, nat.cast_mul, mul_inv', mul_inv'],
-      simp only [mul_left_comm (choose m i : ℂ), mul_assoc, mul_left_comm (choose m i : ℂ)⁻¹,
-        mul_comm (choose m i : ℂ)],
+      simp only [mul_left_comm (nat.choose m i : ℂ), mul_assoc, mul_left_comm (nat.choose m i : ℂ)⁻¹,
+        mul_comm (nat.choose m i : ℂ)],
       rw inv_mul_cancel h₁,
       simp [div_eq_mul_inv, mul_comm, mul_assoc, mul_left_comm]
     end),

src/data/finset.lean

@@ -1240,6 +1240,29 @@ mem_powerset.2 (subset.refl _)
 
 end powerset
 
+section powerset_len
+
+def powerset_len (n : ℕ) (s : finset α) : finset (finset α) :=
+⟨(s.1.powerset_len n).pmap finset.mk
+  (λ t h, nodup_of_le (mem_powerset_len.1 h).1 s.2),
+ nodup_pmap (λ a ha b hb, congr_arg finset.val)
+   (nodup_powerset_len s.2)⟩
+
+theorem mem_powerset_len {n} {s t : finset α} :
+  s ∈ powerset_len n t ↔ s ⊆ t ∧ card s = n :=
+by cases s; simp [powerset_len, val_le_iff.symm]; refl
+
+@[simp] theorem powerset_len_mono {n} {s t : finset α} (h : s ⊆ t) :
+  powerset_len n s ⊆ powerset_len n t :=
+λ u h', mem_powerset_len.2 $
+  and.imp (λ h₂, subset.trans h₂ h) id (mem_powerset_len.1 h')
+
+@[simp] theorem card_powerset_len (n : ℕ) (s : finset α) :
+  card (powerset_len n s) = nat.choose (card s) n :=
+(card_pmap _ _ _).trans (card_powerset_len n s.1)
+
+end powerset_len
+
 section fold
 variables (op : β → β → β) [hc : is_commutative β op] [ha : is_associative β op]
 local notation a * b := op a b

src/data/list/basic.lean

@@ -659,6 +659,11 @@ end
 ⟨λ h, by have := reverse_sublist h; simp only [reverse_append, append_sublist_append_left, reverse_sublist_iff] at this; assumption,
  λ h, append_sublist_append_of_sublist_right h l⟩
 
+theorem append_sublist_append {α} {l₁ l₂ r₁ r₂ : list α}
+  (hl : l₁ <+ l₂) (hr : r₁ <+ r₂) : l₁ ++ r₁ <+ l₂ ++ r₂ :=
+(append_sublist_append_of_sublist_right hl _).trans
+  ((append_sublist_append_left _).2 hr)
+
 theorem subset_of_sublist : Π {l₁ l₂ : list α}, l₁ <+ l₂ → l₁ ⊆ l₂
 | ._ ._ sublist.slnil             b h := h
 | ._ ._ (sublist.cons  l₁ l₂ a s) b h := mem_cons_of_mem _ (subset_of_sublist s h)
@@ -2271,6 +2276,107 @@ reverse_rec_on l (nil_sublist _) $
   mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by refl⟩).trans
 ((append_sublist_append_right _).2 IH)
 
+/- sublists_len -/
+
+def sublists_len_aux {α β : Type*} : ℕ → list α → (list α → β) → list β → list β
+| 0     l      f r := f [] :: r
+| (n+1) []     f r := r
+| (n+1) (a::l) f r := sublists_len_aux (n + 1) l f
+  (sublists_len_aux n l (f ∘ list.cons a) r)
+
+def sublists_len {α : Type*} (n : ℕ) (l : list α) : list (list α) :=
+sublists_len_aux n l id []
+
+lemma sublists_len_aux_append {α β γ : Type*} :
+  ∀ (n : ℕ) (l : list α) (f : list α → β) (g : β → γ) (r : list β) (s : list γ),
+  sublists_len_aux n l (g ∘ f) (r.map g ++ s) =
+  (sublists_len_aux n l f r).map g ++ s
+| 0     l      f g r s := rfl
+| (n+1) []     f g r s := rfl
+| (n+1) (a::l) f g r s := begin
+  unfold sublists_len_aux,
+  rw [show ((g ∘ f) ∘ list.cons a) = (g ∘ f ∘ list.cons a), by refl,
+    sublists_len_aux_append, sublists_len_aux_append]
+end
+
+lemma sublists_len_aux_eq {α β : Type*} (l : list α) (n) (f : list α → β) (r) :
+  sublists_len_aux n l f r = (sublists_len n l).map f ++ r :=
+by rw [sublists_len, ← sublists_len_aux_append]; refl
+
+lemma sublists_len_aux_zero {α : Type*} (l : list α) (f : list α → β) (r) :
+  sublists_len_aux 0 l f r = f [] :: r := by cases l; refl
+
+@[simp] lemma sublists_len_zero {α : Type*} (l : list α) :
+  sublists_len 0 l = [[]] := sublists_len_aux_zero _ _ _
+
+@[simp] lemma sublists_len_succ_nil {α : Type*} (n) :
+  sublists_len (n+1) (@nil α) = [] := rfl
+
+@[simp] lemma sublists_len_succ_cons {α : Type*} (n) (a : α) (l) :
+  sublists_len (n + 1) (a::l) =
+  sublists_len (n + 1) l ++ (sublists_len n l).map (cons a) :=
+by rw [sublists_len, sublists_len_aux, sublists_len_aux_eq,
+  sublists_len_aux_eq, map_id, append_nil]; refl
+
+@[simp] lemma length_sublists_len {α : Type*} : ∀ n (l : list α),
+  length (sublists_len n l) = nat.choose (length l) n
+| 0     l      := by simp
+| (n+1) []     := by simp
+| (n+1) (a::l) := by simp [-add_comm, nat.choose, *]; apply add_comm
+
+lemma sublists_len_sublist_sublists' {α : Type*} : ∀ n (l : list α),
+  sublists_len n l <+ sublists' l
+| 0     l      := singleton_sublist.2 (mem_sublists'.2 (nil_sublist _))
+| (n+1) []     := nil_sublist _
+| (n+1) (a::l) := begin
+  rw [sublists_len_succ_cons, sublists'_cons],
+  exact append_sublist_append
+    (sublists_len_sublist_sublists' _ _)
+    (map_sublist_map _ (sublists_len_sublist_sublists' _ _))
+end
+
+lemma sublists_len_sublist_of_sublist
+  {α : Type*} (n) {l₁ l₂ : list α} (h : l₁ <+ l₂) : sublists_len n l₁ <+ sublists_len n l₂ :=
+begin
+  induction n with n IHn generalizing l₁ l₂, {simp},
+  induction h with l₁ l₂ a s IH l₁ l₂ a s IH, {refl},
+  { refine IH.trans _,
+    rw sublists_len_succ_cons,
+    apply sublist_append_left },
+  { simp [sublists_len_succ_cons],
+    exact append_sublist_append IH (map_sublist_map _ (IHn s)) }
+end
+
+lemma length_of_sublists_len {α : Type*} : ∀ {n} {l l' : list α},
+  l' ∈ sublists_len n l → length l' = n
+| 0     l      l' (or.inl rfl) := rfl
+| (n+1) (a::l) l' h := begin
+  rw [sublists_len_succ_cons, mem_append, mem_map] at h,
+  rcases h with h | ⟨l', h, rfl⟩,
+  { exact length_of_sublists_len h },
+  { exact congr_arg (+1) (length_of_sublists_len h) },
+end
+
+lemma mem_sublists_len_self {α : Type*} {l l' : list α}
+  (h : l' <+ l) : l' ∈ sublists_len (length l') l :=
+begin
+  induction h with l₁ l₂ a s IH l₁ l₂ a s IH,
+  { exact or.inl rfl },
+  { cases l₁ with b l₁,
+    { exact or.inl rfl },
+    { rw [length, sublists_len_succ_cons],
+      exact mem_append_left _ IH } },
+  { rw [length, sublists_len_succ_cons],
+    exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩) }
+end
+
+@[simp] lemma mem_sublists_len {α : Type*} {n} {l l' : list α} :
+  l' ∈ sublists_len n l ↔ l' <+ l ∧ length l' = n :=
+⟨λ h, ⟨mem_sublists'.1
+    (subset_of_sublist (sublists_len_sublist_sublists' _ _) h),
+  length_of_sublists_len h⟩,
+λ ⟨h₁, h₂⟩, h₂ ▸ mem_sublists_len_self h₁⟩
+
 /- forall₂ -/
 
 section forall₂
@@ -3885,6 +3991,10 @@ nodup_filter _
 by rw [sublists'_eq_sublists, nodup_map_iff reverse_injective,
        nodup_sublists, nodup_reverse]
 
+lemma nodup_sublists_len {α : Type*} (n) {l : list α}
+  (nd : nodup l) : (sublists_len n l).nodup :=
+nodup_of_sublist (sublists_len_sublist_sublists' _ _) (nodup_sublists'.2 nd)
+
 end nodup
 
 /- erase duplicates function -/

src/data/multiset.lean

@@ -1690,6 +1690,91 @@ begin
   { assume a s ih, simp [ih, add_mul, mul_comm, mul_left_comm, mul_assoc, sum_map_mul_left.symm] },
 end
 
+/- powerset_len -/
+
+def powerset_len_aux (n : ℕ) (l : list α) : list (multiset α) :=
+sublists_len_aux n l coe []
+
+theorem powerset_len_aux_eq_map_coe {n} {l : list α} :
+  powerset_len_aux n l = (sublists_len n l).map coe :=
+by rw [powerset_len_aux, sublists_len_aux_eq, append_nil]
+
+@[simp] theorem mem_powerset_len_aux {n} {l : list α} {s} :
+  s ∈ powerset_len_aux n l ↔ s ≤ ↑l ∧ card s = n :=
+quotient.induction_on s $
+by simp [powerset_len_aux_eq_map_coe, subperm]; exact
+  λ l₁, ⟨λ ⟨l₂, ⟨s, e⟩, p⟩, ⟨⟨_, p, s⟩, (perm_length p.symm).trans e⟩,
+    λ ⟨⟨l₂, p, s⟩, e⟩, ⟨_, ⟨s, (perm_length p).trans e⟩, p⟩⟩
+
+@[simp] theorem powerset_len_aux_zero (l : list α) :
+  powerset_len_aux 0 l = [0] :=
+by simp [powerset_len_aux_eq_map_coe]
+
+@[simp] theorem powerset_len_aux_nil (n : ℕ) :
+  powerset_len_aux (n+1) (@nil α) = [] := rfl
+
+@[simp] theorem powerset_len_aux_cons (n : ℕ) (a : α) (l : list α) :
+  powerset_len_aux (n+1) (a::l) =
+  powerset_len_aux (n+1) l ++ list.map (cons a) (powerset_len_aux n l) :=
+by simp [powerset_len_aux_eq_map_coe]; refl
+
+theorem powerset_len_aux_perm {n} {l₁ l₂ : list α} (p : l₁ ~ l₂) :
+  powerset_len_aux n l₁ ~ powerset_len_aux n l₂ :=
+begin
+  induction n with n IHn generalizing l₁ l₂, {simp},
+  induction p with a l₁ l₂ p IH a b l l₁ l₂ l₃ p₁ p₂ IH₁ IH₂, {refl},
+  { simp, exact perm_app IH (perm_map _ (IHn p)) },
+  { simp, apply perm_app_right,
+    cases n, {simp, apply perm.swap},
+    simp,
+    rw [← append_assoc, ← append_assoc,
+        (by funext s; simp [cons_swap] : cons b ∘ cons a = cons a ∘ cons b)],
+    exact perm_app_left _ perm_app_comm },
+  { exact IH₁.trans IH₂ }
+end
+
+def powerset_len (n : ℕ) (s : multiset α) : multiset (multiset α) :=
+quot.lift_on s
+  (λ l, (powerset_len_aux n l : multiset (multiset α)))
+  (λ l₁ l₂ h, quot.sound (powerset_len_aux_perm h))
+
+theorem powerset_len_coe' (n) (l : list α) :
+  @powerset_len α n l = powerset_len_aux n l := rfl
+
+theorem powerset_len_coe (n) (l : list α) :
+  @powerset_len α n l = ((sublists_len n l).map coe : list (multiset α)) :=
+congr_arg coe powerset_len_aux_eq_map_coe
+
+@[simp] theorem powerset_len_zero_left (s : multiset α) :
+  powerset_len 0 s = 0::0 :=
+quotient.induction_on s $ λ l, by simp [powerset_len_coe']; refl
+
+@[simp] theorem powerset_len_zero_right (n : ℕ) :
+  @powerset_len α (n + 1) 0 = 0 := rfl
+
+@[simp] theorem powerset_len_cons (n : ℕ) (a : α) (s) :
+  powerset_len (n + 1) (a::s) =
+  powerset_len (n + 1) s + map (cons a) (powerset_len n s) :=
+quotient.induction_on s $ λ l, by simp [powerset_len_coe']; refl
+
+@[simp] theorem mem_powerset_len {n : ℕ} {s t : multiset α} :
+  s ∈ powerset_len n t ↔ s ≤ t ∧ card s = n :=
+quotient.induction_on t $ λ l, by simp [powerset_len_coe']
+
+@[simp] theorem card_powerset_len (n : ℕ) (s : multiset α) :
+  card (powerset_len n s) = nat.choose (card s) n :=
+quotient.induction_on s $ by simp [powerset_len_coe]
+
+theorem powerset_len_le_powerset (n : ℕ) (s : multiset α) :
+  powerset_len n s ≤ powerset s :=
+quotient.induction_on s $ λ l, by simp [powerset_len_coe]; exact
+  subperm_of_sublist (map_sublist_map _ (sublists_len_sublist_sublists' _ _))
+
+theorem powerset_len_mono (n : ℕ) {s t : multiset α} (h : s ≤ t) :
+  powerset_len n s ≤ powerset_len n t :=
+le_induction_on h $ λ l₁ l₂ h, by simp [powerset_len_coe]; exact
+  subperm_of_sublist (map_sublist_map _ (sublists_len_sublist_of_sublist _ h))
+
 /- countp -/
 
 /-- `countp p s` counts the number of elements of `s` (with multiplicity) that
@@ -2249,6 +2334,10 @@ nodup_of_le $ inter_le_right _ _
     (perm_ext_sublist_nodup h (mem_sublists'.1 sx) (mem_sublists'.1 sy)).1
       (quotient.exact e)⟩
 
+theorem nodup_powerset_len {n : ℕ} {s : multiset α}
+  (h : nodup s) : nodup (powerset_len n s) :=
+nodup_of_le (powerset_len_le_powerset _ _) (nodup_powerset.2 h)
+
 @[simp] lemma nodup_bind {s : multiset α} {t : α → multiset β} :
   nodup (bind s t) ↔ ((∀a∈s, nodup (t a)) ∧ (s.pairwise (λa b, disjoint (t a) (t b)))) :=
 have h₁ : ∀a, ∃l:list β, t a = l, from

src/data/nat/basic.lean

@@ -833,6 +833,80 @@ by  rw [← add_assoc, nat.fact_succ, mul_comm (nat.succ _), nat.pow_succ, ← m
   exact mul_le_mul fact_mul_pow_le_fact
     (nat.succ_le_succ (nat.le_add_right _ _)) (nat.zero_le _) (nat.zero_le _)
 
+/- choose -/
+
+def choose : ℕ → ℕ → ℕ
+| _             0 := 1
+| 0       (k + 1) := 0
+| (n + 1) (k + 1) := choose n k + choose n (succ k)
+
+@[simp] lemma choose_zero_right (n : ℕ) : choose n 0 = 1 := by cases n; refl
+
+@[simp] lemma choose_zero_succ (k : ℕ) : choose 0 (succ k) = 0 := rfl
+
+lemma choose_succ_succ (n k : ℕ) : choose (succ n) (succ k) = choose n k + choose n (succ k) := rfl
+
+lemma choose_eq_zero_of_lt : ∀ {n k}, n < k → choose n k = 0
+| _             0 hk := absurd hk dec_trivial
+| 0       (k + 1) hk := choose_zero_succ _
+| (n + 1) (k + 1) hk :=
+  have hnk : n < k, from lt_of_succ_lt_succ hk,
+  have hnk1 : n < k + 1, from lt_of_succ_lt hk,
+  by rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]
+
+@[simp] lemma choose_self (n : ℕ) : choose n n = 1 :=
+by induction n; simp [*, choose, choose_eq_zero_of_lt (lt_succ_self _)]
+
+@[simp] lemma choose_succ_self (n : ℕ) : choose n (succ n) = 0 :=
+choose_eq_zero_of_lt (lt_succ_self _)
+
+@[simp] lemma choose_one_right (n : ℕ) : choose n 1 = n :=
+by induction n; simp [*, choose]
+
+lemma choose_pos : ∀ {n k}, k ≤ n → 0 < choose n k
+| 0             _ hk := by rw [eq_zero_of_le_zero hk]; exact dec_trivial
+| (n + 1)       0 hk := by simp; exact dec_trivial
+| (n + 1) (k + 1) hk := by rw choose_succ_succ;
+    exact add_pos_of_pos_of_nonneg (choose_pos (le_of_succ_le_succ hk)) (nat.zero_le _)
+
+lemma succ_mul_choose_eq : ∀ n k, succ n * choose n k = choose (succ n) (succ k) * succ k
+| 0             0 := dec_trivial
+| 0       (k + 1) := by simp [choose]
+| (n + 1)       0 := by simp
+| (n + 1) (k + 1) :=
+  by rw [choose_succ_succ (succ n) (succ k), add_mul, ←succ_mul_choose_eq, mul_succ,
+  ←succ_mul_choose_eq, add_right_comm, ←mul_add, ←choose_succ_succ, ←succ_mul]
+
+lemma choose_mul_fact_mul_fact : ∀ {n k}, k ≤ n → choose n k * fact k * fact (n - k) = fact n
+| 0              _ hk := by simp [eq_zero_of_le_zero hk]
+| (n + 1)        0 hk := by simp
+| (n + 1) (succ k) hk :=
+begin
+  cases lt_or_eq_of_le hk with hk₁ hk₁,
+  { have h : choose n k * fact (succ k) * fact (n - k) = succ k * fact n :=
+      by rw ← choose_mul_fact_mul_fact (le_of_succ_le_succ hk);
+      simp [fact_succ, mul_comm, mul_left_comm],
+    have h₁ : fact (n - k) = (n - k) * fact (n - succ k) :=
+      by rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), fact_succ],
+    have h₂ : choose n (succ k) * fact (succ k) * ((n - k) * fact (n - succ k)) = (n - k) * fact n :=
+      by rw ← choose_mul_fact_mul_fact (le_of_lt_succ hk₁);
+      simp [fact_succ, mul_comm, mul_left_comm, mul_assoc],
+    have h₃ : k * fact n ≤ n * fact n := mul_le_mul_right _ (le_of_succ_le_succ hk),
+  rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, ← add_one, add_mul, nat.mul_sub_right_distrib,
+      fact_succ, ← nat.add_sub_assoc h₃, add_assoc, ← add_mul, nat.add_sub_cancel_left, add_comm] },
+  { simp [hk₁, mul_comm, choose, nat.sub_self] }
+end
+
+theorem choose_eq_fact_div_fact {n k : ℕ} (hk : k ≤ n) : choose n k = fact n / (fact k * fact (n - k)) :=
+begin
+  have : fact n = choose n k * (fact k * fact (n - k)) :=
+    by rw ← mul_assoc; exact (choose_mul_fact_mul_fact hk).symm,
+  exact (nat.div_eq_of_eq_mul_left (mul_pos (fact_pos _) (fact_pos _)) this).symm
+end
+
+theorem fact_mul_fact_dvd_fact {n k : ℕ} (hk : k ≤ n) : fact k * fact (n - k) ∣ fact n :=
+by rw [←choose_mul_fact_mul_fact hk, mul_assoc]; exact dvd_mul_left _ _
+
 section find_greatest
 
 /-- `find_greatest P b` is the largest `i ≤ bound` such that `P i` holds, or `0` if no such `i`