feat(data/list/basic): map_permutations (#8188)

As [requested on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/perm.20of.20permutations/near/244821779).

src/data/list/basic.lean

@@ -177,6 +177,11 @@ lemma bind_map {g : α → list β} {f : β → γ} :
 | [] := rfl
 | (a::l) := by simp only [cons_bind, map_append, bind_map l]
 
+lemma map_bind (g : β → list γ) (f : α → β) :
+  ∀ l : list α, (list.map f l).bind g = l.bind (λ a, g (f a))
+| [] := rfl
+| (a::l) := by simp only [cons_bind, map_cons, map_bind l]
+
 /-! ### length -/
 
 theorem length_eq_zero {l : list α} : length l = 0 ↔ l = [] :=
@@ -3783,6 +3788,88 @@ instance decidable_infix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidabl
 
 section permutations
 
+theorem permutations_aux2_fst (t : α) (ts : list α) (r : list β) : ∀ (ys : list α) (f : list α → β),
+  (permutations_aux2 t ts r ys f).1 = ys ++ ts
+| []      f := rfl
+| (y::ys) f := match _, permutations_aux2_fst ys _ : ∀ o : list α × list β, o.1 = ys ++ ts →
+      (permutations_aux2._match_1 t y f o).1 = y :: ys ++ ts with
+  | ⟨_, zs⟩, rfl := rfl
+  end
+
+@[simp] theorem permutations_aux2_snd_nil (t : α) (ts : list α) (r : list β) (f : list α → β) :
+  (permutations_aux2 t ts r [] f).2 = r := rfl
+
+@[simp] theorem permutations_aux2_snd_cons (t : α) (ts : list α) (r : list β) (y : α) (ys : list α)
+  (f : list α → β) :
+  (permutations_aux2 t ts r (y::ys) f).2 = f (t :: y :: ys ++ ts) ::
+    (permutations_aux2 t ts r ys (λx : list α, f (y::x))).2 :=
+match _, permutations_aux2_fst t ts r _ _ : ∀ o : list α × list β, o.1 = ys ++ ts →
+   (permutations_aux2._match_1 t y f o).2 = f (t :: y :: ys ++ ts) :: o.2 with
+| ⟨_, zs⟩, rfl := rfl
+end
+
+theorem permutations_aux2_append (t : α) (ts : list α) (r : list β) (ys : list α) (f : list α → β) :
+  (permutations_aux2 t ts nil ys f).2 ++ r = (permutations_aux2 t ts r ys f).2 :=
+by induction ys generalizing f; simp *
+
+theorem mem_permutations_aux2 {t : α} {ts : list α} {ys : list α} {l l' : list α} :
+    l' ∈ (permutations_aux2 t ts [] ys (append l)).2 ↔
+    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts :=
+begin
+  induction ys with y ys ih generalizing l,
+  { simp {contextual := tt} },
+  { rw [permutations_aux2_snd_cons, show (λ (x : list α), l ++ y :: x) = append (l ++ [y]),
+        by funext; simp, mem_cons_iff, ih], split; intro h,
+    { rcases h with e | ⟨l₁, l₂, l0, ye, _⟩,
+      { subst l', exact ⟨[], y::ys, by simp⟩ },
+      { substs l' ys, exact ⟨y::l₁, l₂, l0, by simp⟩ } },
+    { rcases h with ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩,
+      { simp [ye] },
+      { simp at ye, rcases ye with ⟨rfl, rfl⟩,
+        exact or.inr ⟨l₁, l₂, l0, by simp⟩ } } }
+end
+
+theorem mem_permutations_aux2' {t : α} {ts : list α} {ys : list α} {l : list α} :
+    l ∈ (permutations_aux2 t ts [] ys id).2 ↔
+    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts :=
+by rw [show @id (list α) = append nil, by funext; refl]; apply mem_permutations_aux2
+
+theorem length_permutations_aux2 (t : α) (ts : list α) (ys : list α) (f : list α → β) :
+  length (permutations_aux2 t ts [] ys f).2 = length ys :=
+by induction ys generalizing f; simp *
+
+theorem foldr_permutations_aux2 (t : α) (ts : list α) (r L : list (list α)) :
+  foldr (λy r, (permutations_aux2 t ts r y id).2) r L =
+    L.bind (λ y, (permutations_aux2 t ts [] y id).2) ++ r :=
+by induction L with l L ih; [refl, {simp [ih], rw ← permutations_aux2_append}]
+
+theorem mem_foldr_permutations_aux2 {t : α} {ts : list α} {r L : list (list α)} {l' : list α} :
+  l' ∈ foldr (λy r, (permutations_aux2 t ts r y id).2) r L ↔ l' ∈ r ∨
+  ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts :=
+have (∃ (a : list α), a ∈ L ∧
+    ∃ (l₁ l₂ : list α), ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
+    ∃ (l₁ l₂ : list α), ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts),
+from ⟨λ ⟨a, aL, l₁, l₂, l0, e, h⟩, ⟨l₁, l₂, l0, e ▸ aL, h⟩,
+      λ ⟨l₁, l₂, l0, aL, h⟩, ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩,
+by rw foldr_permutations_aux2; simp [mem_permutations_aux2', this,
+  or.comm, or.left_comm, or.assoc, and.comm, and.left_comm, and.assoc]
+
+theorem length_foldr_permutations_aux2 (t : α) (ts : list α) (r L : list (list α)) :
+  length (foldr (λy r, (permutations_aux2 t ts r y id).2) r L) = sum (map length L) + length r :=
+by simp [foldr_permutations_aux2, (∘), length_permutations_aux2]
+
+theorem length_foldr_permutations_aux2' (t : α) (ts : list α) (r L : list (list α))
+  (n) (H : ∀ l ∈ L, length l = n) :
+  length (foldr (λy r, (permutations_aux2 t ts r y id).2) r L) = n * length L + length r :=
+begin
+  rw [length_foldr_permutations_aux2, (_ : sum (map length L) = n * length L)],
+  induction L with l L ih, {simp},
+  have sum_map : sum (map length L) = n * length L :=
+    ih (λ l m, H l (mem_cons_of_mem _ m)),
+  have length_l : length l = n := H _ (mem_cons_self _ _),
+  simp [sum_map, length_l, mul_add, add_comm]
+end
+
 @[simp] theorem permutations_aux_nil (is : list α) : permutations_aux [] is = [] :=
 by rw [permutations_aux, permutations_aux.rec]
 
@@ -3791,6 +3878,34 @@ by rw [permutations_aux, permutations_aux.rec]
     (permutations_aux ts (t::is)) (permutations is) :=
 by rw [permutations_aux, permutations_aux.rec]; refl
 
+theorem map_permutations_aux2' {α β α' β'} (g : α → α') (g' : β → β')
+  (t : α) (ts ys : list α) (r : list β) (f : list α → β) (f' : list α' → β')
+  (H : ∀ a, g' (f a) = f' (map g a)) :
+  map g' (permutations_aux2 t ts r ys f).2 =
+  (permutations_aux2 (g t) (map g ts) (map g' r) (map g ys) f').2 :=
+begin
+  induction ys generalizing f f'; simp *,
+  apply ys_ih, simp [H],
+end
+
+theorem map_permutations_aux2 {α α'} (g : α → α') (t : α) (ts ys : list α) :
+  map (map g) (permutations_aux2 t ts [] ys id).2 =
+  (permutations_aux2 (g t) (map g ts) [] (map g ys) id).2 :=
+map_permutations_aux2' _ _ _ _ _ _ _ _ (λ _, rfl)
+
+theorem map_permutations_aux (f : α → β) : ∀ (ts is : list α),
+  map (map f) (permutations_aux ts is) = permutations_aux (map f ts) (map f is) :=
+begin
+  refine permutations_aux.rec (by simp) _,
+  introv IH1 IH2, rw map at IH2,
+  simp only [foldr_permutations_aux2, map_append, map, map_permutations_aux2, permutations,
+    bind_map, IH1, append_assoc, permutations_aux_cons, cons_bind, ← IH2, map_bind],
+end
+
+theorem map_permutations (f : α → β) (ts : list α) :
+  map (map f) (permutations ts) = permutations (map f ts) :=
+by rw [permutations, permutations, map, map_permutations_aux, map]
+
 end permutations
 
 /-! ### insert -/

src/data/list/perm.lean

@@ -981,88 +981,6 @@ end
 
 section permutations
 
-theorem permutations_aux2_fst (t : α) (ts : list α) (r : list β) : ∀ (ys : list α) (f : list α → β),
-  (permutations_aux2 t ts r ys f).1 = ys ++ ts
-| []      f := rfl
-| (y::ys) f := match _, permutations_aux2_fst ys _ : ∀ o : list α × list β, o.1 = ys ++ ts →
-      (permutations_aux2._match_1 t y f o).1 = y :: ys ++ ts with
-  | ⟨_, zs⟩, rfl := rfl
-  end
-
-@[simp] theorem permutations_aux2_snd_nil (t : α) (ts : list α) (r : list β) (f : list α → β) :
-  (permutations_aux2 t ts r [] f).2 = r := rfl
-
-@[simp] theorem permutations_aux2_snd_cons (t : α) (ts : list α) (r : list β) (y : α) (ys : list α)
-  (f : list α → β) :
-  (permutations_aux2 t ts r (y::ys) f).2 = f (t :: y :: ys ++ ts) ::
-    (permutations_aux2 t ts r ys (λx : list α, f (y::x))).2 :=
-match _, permutations_aux2_fst t ts r _ _ : ∀ o : list α × list β, o.1 = ys ++ ts →
-   (permutations_aux2._match_1 t y f o).2 = f (t :: y :: ys ++ ts) :: o.2 with
-| ⟨_, zs⟩, rfl := rfl
-end
-
-theorem permutations_aux2_append (t : α) (ts : list α) (r : list β) (ys : list α) (f : list α → β) :
-  (permutations_aux2 t ts nil ys f).2 ++ r = (permutations_aux2 t ts r ys f).2 :=
-by induction ys generalizing f; simp *
-
-theorem mem_permutations_aux2 {t : α} {ts : list α} {ys : list α} {l l' : list α} :
-    l' ∈ (permutations_aux2 t ts [] ys (append l)).2 ↔
-    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts :=
-begin
-  induction ys with y ys ih generalizing l,
-  { simp {contextual := tt} },
-  { rw [permutations_aux2_snd_cons, show (λ (x : list α), l ++ y :: x) = append (l ++ [y]),
-        by funext; simp, mem_cons_iff, ih], split; intro h,
-    { rcases h with e | ⟨l₁, l₂, l0, ye, _⟩,
-      { subst l', exact ⟨[], y::ys, by simp⟩ },
-      { substs l' ys, exact ⟨y::l₁, l₂, l0, by simp⟩ } },
-    { rcases h with ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩,
-      { simp [ye] },
-      { simp at ye, rcases ye with ⟨rfl, rfl⟩,
-        exact or.inr ⟨l₁, l₂, l0, by simp⟩ } } }
-end
-
-theorem mem_permutations_aux2' {t : α} {ts : list α} {ys : list α} {l : list α} :
-    l ∈ (permutations_aux2 t ts [] ys id).2 ↔
-    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts :=
-by rw [show @id (list α) = append nil, by funext; refl]; apply mem_permutations_aux2
-
-theorem length_permutations_aux2 (t : α) (ts : list α) (ys : list α) (f : list α → β) :
-  length (permutations_aux2 t ts [] ys f).2 = length ys :=
-by induction ys generalizing f; simp *
-
-theorem foldr_permutations_aux2 (t : α) (ts : list α) (r L : list (list α)) :
-  foldr (λy r, (permutations_aux2 t ts r y id).2) r L =
-    L.bind (λ y, (permutations_aux2 t ts [] y id).2) ++ r :=
-by induction L with l L ih; [refl, {simp [ih], rw ← permutations_aux2_append}]
-
-theorem mem_foldr_permutations_aux2 {t : α} {ts : list α} {r L : list (list α)} {l' : list α} :
-  l' ∈ foldr (λy r, (permutations_aux2 t ts r y id).2) r L ↔ l' ∈ r ∨
-  ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts :=
-have (∃ (a : list α), a ∈ L ∧
-    ∃ (l₁ l₂ : list α), ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
-    ∃ (l₁ l₂ : list α), ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts),
-from ⟨λ ⟨a, aL, l₁, l₂, l0, e, h⟩, ⟨l₁, l₂, l0, e ▸ aL, h⟩,
-      λ ⟨l₁, l₂, l0, aL, h⟩, ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩,
-by rw foldr_permutations_aux2; simp [mem_permutations_aux2', this,
-  or.comm, or.left_comm, or.assoc, and.comm, and.left_comm, and.assoc]
-
-theorem length_foldr_permutations_aux2 (t : α) (ts : list α) (r L : list (list α)) :
-  length (foldr (λy r, (permutations_aux2 t ts r y id).2) r L) = sum (map length L) + length r :=
-by simp [foldr_permutations_aux2, (∘), length_permutations_aux2]
-
-theorem length_foldr_permutations_aux2' (t : α) (ts : list α) (r L : list (list α))
-  (n) (H : ∀ l ∈ L, length l = n) :
-  length (foldr (λy r, (permutations_aux2 t ts r y id).2) r L) = n * length L + length r :=
-begin
-  rw [length_foldr_permutations_aux2, (_ : sum (map length L) = n * length L)],
-  induction L with l L ih, {simp},
-  have sum_map : sum (map length L) = n * length L :=
-    ih (λ l m, H l (mem_cons_of_mem _ m)),
-  have length_l : length l = n := H _ (mem_cons_self _ _),
-  simp [sum_map, length_l, mul_add, add_comm]
-end
-
 theorem perm_of_mem_permutations_aux :
   ∀ {ts is l : list α}, l ∈ permutations_aux ts is → l ~ ts ++ is :=
 begin