feat(data/list/perm): binding all the sublists of a given length give…

…s all the sublists (#15834)

This is essentially the defining relation between `sublists'` and `sublists_len`.

This also adds a few other trivial lemmas about `sublists_len`.

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_perm {α : 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/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,