[Merged by Bors] - feat (data/multiset/powerset): add bind_powerset_len

src/algebra/big_operators/basic.lean

@@ -1706,6 +1706,14 @@ begin
     exact add_eq_union_left_of_le (finset.sup_le (λ x hx, le_sum_of_mem (mem_map_of_mem f hx))), },
 end
 
+lemma sup_powerset_len {α : Type*} [decidable_eq α] (x : multiset α) :
+  finset.sup (finset.range (x.card + 1)) (λ k, x.powerset_len k) = x.powerset :=
+ begin
+  convert bind_powerset_len x,
+  rw [multiset.bind, multiset.join, ←finset.range_coe, ←finset.sum_eq_multiset_sum],
+  exact eq_comm.mp (finset_sum_eq_sup_iff_disjoint.mpr (λ _ _ _ _ h, disjoint_powerset_len x h)),
+end
+
 @[simp] lemma to_finset_sum_count_eq (s : multiset α) :
   (∑ a in s.to_finset, s.count a) = s.card :=
 multiset.induction_on s rfl

src/data/list/perm.lean

@@ -7,6 +7,7 @@ import data.list.dedup
 import data.list.lattice
 import data.list.permutation
 import data.list.zip
+import data.list.range
 import logic.relation
 
 /-!
@@ -924,6 +925,10 @@ begin
   exact perm_append_comm.append_right _
 end
 
+theorem map_append_bind_perm (l : list α) (f : α → β) (g : α → list β) :
+  l.map f ++ l.bind g ~ l.bind (λ x, f x :: g x) :=
+by simpa [←map_eq_bind] using bind_append_perm l (λ x, [f x]) g
+
 theorem perm.product_right {l₁ l₂ : list α} (t₁ : list β) (p : l₁ ~ l₂) :
   product l₁ t₁ ~ product l₂ t₁ :=
 p.bind_right _
@@ -983,6 +988,24 @@ begin
     { exact (IH _ _ h).cons _ } }
 end
 
+lemma range_bind_sublists_len {α : Type*} (l : list α) :
+  (list.range (l.length + 1)).bind (λ n, sublists_len n l) ~ sublists' l :=
+begin
+  induction l with h tl,
+  { simp [range_succ] },
+  { simp_rw [range_succ_eq_map, length, cons_bind, map_bind, sublists_len_succ_cons,
+      sublists'_cons, list.sublists_len_zero, list.singleton_append],
+    refine ((bind_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans _,
+    simp_rw [←list.bind_map, ←cons_append],
+    rw [←list.singleton_append, ←list.sublists_len_zero tl],
+    refine perm.append _ (l_ih.map _),
+    rw [list.range_succ, append_bind, bind_singleton,
+      sublists_len_of_length_lt (nat.lt_succ_self _), append_nil,
+      ←list.map_bind (λ n, sublists_len n tl) nat.succ, ←cons_bind 0 _ (λ n, sublists_len n tl),
+      ←range_succ_eq_map],
+    exact l_ih }
+end
+
 theorem perm_lookmap (f : α → option α) {l₁ l₂ : list α}
   (H : pairwise (λ a b, ∀ (c ∈ f a) (d ∈ f b), a = b ∧ c = d) l₁)
   (p : l₁ ~ l₂) : lookmap f l₁ ~ lookmap f l₂ :=

src/data/list/sublists.lean

@@ -282,4 +282,13 @@ end
   length_of_sublists_len h⟩,
 λ ⟨h₁, h₂⟩, h₂ ▸ mem_sublists_len_self h₁⟩
 
+lemma sublists_len_of_length_lt {n} {l : list α} (h : l.length < n) : sublists_len n l = [] :=
+eq_nil_iff_forall_not_mem.mpr $ λ x, mem_sublists_len.not.mpr $ λ ⟨hs, hl⟩,
+  (h.trans_eq hl.symm).not_le (length_le_of_sublist hs)
+
+@[simp] lemma sublists_len_length : ∀ (l : list α), sublists_len l.length l = [l]
+| [] := rfl
+| (a::l) := by rw [length, sublists_len_succ_cons, sublists_len_length, map_singleton,
+                   sublists_len_of_length_lt (lt_succ_self _), nil_append]
+
 end list

src/data/multiset/antidiagonal.lean

@@ -67,10 +67,23 @@ quotient.induction_on s $ λ l, begin
   {congr; simp}, {simp}
 end
 
+theorem antidiagonal_eq_map_powerset [decidable_eq α] (s : multiset α) :
+  s.antidiagonal = s.powerset.map (λ t, (s - t, t)) :=
+begin
+  induction s using multiset.induction_on with a s hs,
+  { simp only [antidiagonal_zero, powerset_zero, zero_tsub, map_singleton] },
+  { simp_rw [antidiagonal_cons, powerset_cons, map_add, hs, map_map, function.comp, prod.map_mk,
+      id.def, sub_cons, erase_cons_head],
+    rw add_comm,
+    congr' 1,
+    refine multiset.map_congr rfl (λ x hx, _),
+    rw cons_sub_of_le _ (mem_powerset.mp hx) }
+end
+
 @[simp] theorem card_antidiagonal (s : multiset α) :
   card (antidiagonal s) = 2 ^ card s :=
 by have := card_powerset s;
-   rwa [← antidiagonal_map_fst, card_map] at this
+  rwa [← antidiagonal_map_fst, card_map] at this
 
 lemma prod_map_add [comm_semiring β] {s : multiset α} {f g : α → β} :
   prod (s.map (λa, f a + g a)) =

src/data/multiset/basic.lean

@@ -1159,6 +1159,10 @@ multiset.induction_on t (by simp [multiset.sub_zero])
 instance : has_ordered_sub (multiset α) :=
 ⟨λ n m k, multiset.sub_le_iff_le_add⟩
 
+lemma cons_sub_of_le (a : α) {s t : multiset α} (h : t ≤ s) :
+  a ::ₘ s - t = a ::ₘ (s - t) :=
+by rw [←singleton_add, ←singleton_add, add_tsub_assoc_of_le h]
+
 theorem sub_eq_fold_erase (s t : multiset α) : s - t = foldl erase erase_comm s t :=
 quotient.induction_on₂ s t $ λ l₁ l₂,
 show ↑(l₁.diff l₂) = foldl erase erase_comm ↑l₁ ↑l₂,

src/data/multiset/powerset.lean

@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import data.multiset.basic
-
+import data.multiset.range
+import data.multiset.bind
 /-!
 # The powerset of a multiset
 -/
@@ -253,4 +254,18 @@ begin
   { cases n; simp [ih, map_comp_cons], },
 end
 
+lemma disjoint_powerset_len (s : multiset α) {i j : ℕ} (h : i ≠ j) :
+  multiset.disjoint (s.powerset_len i) (s.powerset_len j) :=
+λ x hi hj, h (eq.trans (multiset.mem_powerset_len.mp hi).right.symm
+  (multiset.mem_powerset_len.mp hj).right)
+
+lemma bind_powerset_len {α : Type*} (S : multiset α) :
+  bind (multiset.range (S.card + 1)) (λ k, S.powerset_len k) = S.powerset :=
+begin
+  induction S using quotient.induction_on,
+  simp_rw [quot_mk_to_coe, powerset_coe', powerset_len_coe, ←coe_range, coe_bind, ←list.bind_map,
+    coe_card],
+  exact coe_eq_coe.mpr (list.perm.map _ (list.range_bind_sublists_len S)),
+end
+
 end multiset

src/tactic/wlog.lean

@@ -162,13 +162,13 @@ perms ← parse_permutations perms,
   | some pat := do
     pat ← to_expr pat,
     let vars' := vars.filter $ λv, v.occurs pat,
-    case_pat ← mk_pattern [] vars' pat [] vars',
+    case_pat ← tactic.mk_pattern [] vars' pat [] vars',
     perms' ← match_perms case_pat cases,
     return (pat, perms')
   | none := do
     (p :: ps) ← dest_or cases,
     let vars' := vars.filter $ λv, v.occurs p,
-    case_pat ← mk_pattern [] vars' p [] vars',
+    case_pat ← tactic.mk_pattern [] vars' p [] vars',
     perms' ← (p :: ps).mmap (λp, do m ← match_pattern case_pat p, return m.2),
     return (p, perms')
   end,