feat(data/list/perm): perm.permutations (#8587)

This proves the theorem from [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/perm.20of.20permutations):

```lean
theorem perm.permutations {s t : list α} (h : s ~ t) : permutations s ~ permutations t := ...
```
It also introduces a `permutations'` function which has simpler equations (and indeed, this function is used to prove the theorem, because it is relatively easier to prove `perm.permutations'` first).

src/data/list/basic.lean

@@ -528,6 +528,15 @@ append_bind _ _ _
 @[simp] theorem bind_singleton (f : α → list β) (x : α) : [x].bind f = f x :=
 append_nil (f x)
 
+@[simp] theorem bind_singleton' (l : list α) : l.bind (λ x, [x]) = l := bind_pure l
+
+theorem map_eq_bind {α β} (f : α → β) (l : list α) : map f l = l.bind (λ x, [f x]) :=
+by { transitivity, rw [← bind_singleton' l, bind_map], refl }
+
+theorem bind_assoc {α β} (l : list α) (f : α → list β) (g : β → list γ) :
+  (l.bind f).bind g = l.bind (λ x, (f x).bind g) :=
+by induction l; simp *
+
 /-! ### concat -/
 
 theorem concat_nil (a : α) : concat [] a = [a] := rfl
@@ -2230,12 +2239,12 @@ end
 @[simp] theorem mfoldl_append {f : β → α → m β} : ∀ {b l₁ l₂},
   mfoldl f b (l₁ ++ l₂) = mfoldl f b l₁ >>= λ x, mfoldl f x l₂
 | _ []     _ := by simp only [nil_append, mfoldl_nil, pure_bind]
-| _ (_::_) _ := by simp only [cons_append, mfoldl_cons, mfoldl_append, bind_assoc]
+| _ (_::_) _ := by simp only [cons_append, mfoldl_cons, mfoldl_append, is_lawful_monad.bind_assoc]
 
 @[simp] theorem mfoldr_append {f : α → β → m β} : ∀ {b l₁ l₂},
   mfoldr f b (l₁ ++ l₂) = mfoldr f b l₂ >>= λ x, mfoldr f x l₁
 | _ []     _ := by simp only [nil_append, mfoldr_nil, bind_pure]
-| _ (_::_) _ := by simp only [mfoldr_cons, cons_append, mfoldr_append, bind_assoc]
+| _ (_::_) _ := by simp only [mfoldr_cons, cons_append, mfoldr_append, is_lawful_monad.bind_assoc]
 
 end mfoldl_mfoldr
 
@@ -3848,13 +3857,26 @@ produced by inserting `t` into every non-terminal position of `ys` in order. As
 lemma permutations_aux2_snd_eq (t : α) (ts : list α) (r : list β) (ys : list α) (f : list α → β) :
   (permutations_aux2 t ts r ys f).2 =
     (permutations_aux2 t [] [] ys id).2.map (λ x, f (x ++ ts)) ++ r :=
-by rw [←permutations_aux2_append, map_permutations_aux2, permutations_aux2_comp_append]
+by rw [← permutations_aux2_append, map_permutations_aux2, permutations_aux2_comp_append]
 
 theorem map_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_map_permutations'_aux (f : α → β) (t : α) (ts : list α) :
+  map (map f) (permutations'_aux t ts) = permutations'_aux (f t) (map f ts) :=
+by induction ts with a ts ih; [refl, {simp [← ih], refl}]
+
+theorem permutations'_aux_eq_permutations_aux2 (t : α) (ts : list α) :
+  permutations'_aux t ts = (permutations_aux2 t [] [ts ++ [t]] ts id).2 :=
+begin
+  induction ts with a ts ih, {refl},
+  simp [permutations'_aux, permutations_aux2_snd_cons, ih],
+  simp only [← permutations_aux2_append] {single_pass := tt},
+  simp [map_permutations_aux2],
+end
+
 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 :=
@@ -3921,6 +3943,9 @@ by rw [permutations_aux, permutations_aux.rec]
     (permutations_aux ts (t::is)) (permutations is) :=
 by rw [permutations_aux, permutations_aux.rec]; refl
 
+@[simp] theorem permutations_nil : permutations ([] : list α) = [[]] :=
+by rw [permutations, permutations_aux_nil]
+
 theorem map_permutations_aux (f : α → β) : ∀ (ts is : list α),
   map (map f) (permutations_aux ts is) = permutations_aux (map f ts) (map f is) :=
 begin
@@ -3934,6 +3959,25 @@ theorem map_permutations (f : α → β) (ts : list α) :
   map (map f) (permutations ts) = permutations (map f ts) :=
 by rw [permutations, permutations, map, map_permutations_aux, map]
 
+theorem map_permutations' (f : α → β) (ts : list α) :
+  map (map f) (permutations' ts) = permutations' (map f ts) :=
+by induction ts with t ts ih; [refl, simp [← ih, map_bind, ← map_map_permutations'_aux, bind_map]]
+
+theorem permutations_aux_append (is is' ts : list α) :
+  permutations_aux (is ++ ts) is' =
+  (permutations_aux is is').map (++ ts) ++ permutations_aux ts (is.reverse ++ is') :=
+begin
+  induction is with t is ih generalizing is', {simp},
+  simp [foldr_permutations_aux2, ih, bind_map],
+  congr' 2, funext ys, rw [map_permutations_aux2],
+  simp only [← permutations_aux2_comp_append] {single_pass := tt},
+  simp only [id, append_assoc],
+end
+
+theorem permutations_append (is ts : list α) :
+  permutations (is ++ ts) = (permutations is).map (++ ts) ++ permutations_aux ts is.reverse :=
+by simp [permutations, permutations_aux_append]
+
 end permutations
 
 /-! ### insert -/

src/data/list/defs.lean

@@ -421,6 +421,15 @@ def sections : list (list α) → list (list α)
 
 section permutations
 
+/-- An auxiliary function for defining `permutations`. `permutations_aux2 t ts r ys f` is equal to
+`(ys ++ ts, (insert_left ys t ts).map f ++ r)`, where `insert_left ys t ts` (not explicitly
+defined) is the list of lists of the form `insert_nth n t (ys ++ ts)` for `0 ≤ n < length ys`.
+
+    permutations_aux2 10 [4, 5, 6] [] [1, 2, 3] id =
+      ([1, 2, 3, 4, 5, 6],
+       [[10, 1, 2, 3, 4, 5, 6],
+        [1, 10, 2, 3, 4, 5, 6],
+        [1, 2, 10, 3, 4, 5, 6]]) -/
 def permutations_aux2 (t : α) (ts : list α) (r : list β) : list α → (list α → β) → list α × list β
 | []      f := (ts, r)
 | (y::ys) f := let (us, zs) := permutations_aux2 ys (λx : list α, f (y::x)) in
@@ -445,6 +454,8 @@ using_well_founded {
   dec_tac := tactic.assumption,
   rel_tac := λ _ _, `[exact ⟨(≺), @inv_image.wf _ _ _ meas (prod.lex_wf lt_wf lt_wf)⟩] }
 
+/-- An auxiliary function for defining `permutations`. `permutations_aux ts is` is the set of all
+permutations of `is ++ ts` that do not fix `ts`. -/
 def permutations_aux : list α → list α → list (list α) :=
 @@permutations_aux.rec (λ _ _, list (list α)) (λ is, [])
   (λ t ts is IH1 IH2, foldr (λy r, (permutations_aux2 t ts r y id).2) IH1 (is :: IH2))
@@ -457,6 +468,32 @@ def permutations_aux : list α → list α → list (list α) :=
 def permutations (l : list α) : list (list α) :=
 l :: permutations_aux l []
 
+/-- `permutations'_aux t ts` inserts `t` into every position in `ts`, including the last.
+This function is intended for use in specifications, so it is simpler than `permutations_aux2`,
+which plays roughly the same role in `permutations`.
+
+Note that `(permutations_aux2 t [] [] ts id).2` is similar to this function, but skips the last
+position:
+
+    permutations'_aux 10 [1, 2, 3] =
+      [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3], [1, 2, 3, 10]]
+    (permutations_aux2 10 [] [] [1, 2, 3] id).2 =
+      [[10, 1, 2, 3], [1, 10, 2, 3], [1, 2, 10, 3]] -/
+@[simp] def permutations'_aux (t : α) : list α → list (list α)
+| []      := [[t]]
+| (y::ys) := (t :: y :: ys) :: (permutations'_aux ys).map (cons y)
+
+/-- List of all permutations of `l`. This version of `permutations` is less efficient but has
+simpler definitional equations. The permutations are in a different order,
+but are equal up to permutation, as shown by `list.permutations_perm_permutations'`.
+
+     permutations [1, 2, 3] =
+       [[1, 2, 3], [2, 1, 3], [2, 3, 1],
+        [1, 3, 2], [3, 1, 2], [3, 2, 1]] -/
+@[simp] def permutations' : list α → list (list α)
+| [] := [[]]
+| (t::ts) := (permutations' ts).bind $ permutations'_aux t
+
 end permutations
 
 /-- `erasep p l` removes the first element of `l` satisfying the predicate `p`. -/

src/data/list/perm.lean

@@ -811,6 +811,15 @@ theorem perm.bind_left (l : list α) {f g : α → list β} (h : ∀ a, f a ~ g
   l.bind f ~ l.bind g :=
 by induction l with a l IH; simp; exact (h a).append IH
 
+theorem bind_append_perm (l : list α) (f g : α → list β) :
+  l.bind f ++ l.bind g ~ l.bind (λ x, f x ++ g x) :=
+begin
+  induction l with a l IH; simp,
+  refine (perm.trans _ (IH.append_left _)).append_left _,
+  rw [← append_assoc, ← append_assoc],
+  exact perm_append_comm.append_right _
+end
+
 theorem perm.product_right {l₁ l₂ : list α} (t₁ : list β) (p : l₁ ~ l₂) :
   product l₁ t₁ ~ product l₂ t₁ :=
 p.bind_right _
@@ -1049,9 +1058,67 @@ begin
   { exact or.inr (or.inl m) }
 end
 
-@[simp] theorem mem_permutations (s t : list α) : s ∈ permutations t ↔ s ~ t :=
+@[simp] theorem mem_permutations {s t : list α} : s ∈ permutations t ↔ s ~ t :=
 ⟨perm_of_mem_permutations, mem_permutations_of_perm_lemma mem_permutations_aux_of_perm⟩
 
+theorem perm_permutations'_aux_comm (a b : α) (l : list α) :
+  (permutations'_aux a l).bind (permutations'_aux b) ~
+  (permutations'_aux b l).bind (permutations'_aux a) :=
+begin
+  induction l with c l ih, {simp [swap]},
+  simp [permutations'_aux], apply perm.swap',
+  have : ∀ a b,
+    (map (cons c) (permutations'_aux a l)).bind (permutations'_aux b) ~
+    map (cons b ∘ cons c) (permutations'_aux a l) ++
+    map (cons c) ((permutations'_aux a l).bind (permutations'_aux b)),
+  { intros,
+    simp only [map_bind, permutations'_aux],
+    refine (bind_append_perm _ (λ x, [_]) _).symm.trans _,
+    rw [← map_eq_bind, ← bind_map] },
+  refine (((this _ _).append_left _).trans _).trans ((this _ _).append_left _).symm,
+  rw [← append_assoc, ← append_assoc],
+  exact perm_append_comm.append (ih.map _),
+end
+
+theorem perm.permutations' {s t : list α} (p : s ~ t) :
+  permutations' s ~ permutations' t :=
+begin
+  induction p with a s t p IH a b l s t u p₁ p₂ IH₁ IH₂, {simp},
+  { simp only [permutations'], exact IH.bind_right _ },
+  { simp only [permutations'],
+    rw [bind_assoc, bind_assoc], apply perm.bind_left, apply perm_permutations'_aux_comm },
+  { exact IH₁.trans IH₂ }
+end
+
+theorem permutations_perm_permutations' (ts : list α) : ts.permutations ~ ts.permutations' :=
+begin
+  obtain ⟨n, h⟩ : ∃ n, length ts < n := ⟨_, nat.lt_succ_self _⟩,
+  induction n with n IH generalizing ts, {cases h},
+  refine list.reverse_rec_on ts (λ h, _) (λ ts t _ h, _) h, {simp [permutations]},
+  rw [← concat_eq_append, length_concat, nat.succ_lt_succ_iff] at h,
+  have IH₂ := (IH ts.reverse (by rwa [length_reverse])).trans (reverse_perm _).permutations',
+  simp only [permutations_append, foldr_permutations_aux2,
+    permutations_aux_nil, permutations_aux_cons, append_nil],
+  refine (perm_append_comm.trans ((IH₂.bind_right _).append ((IH _ h).map _))).trans
+    (perm.trans _ perm_append_comm.permutations'),
+  rw [map_eq_bind, singleton_append, permutations'],
+  convert bind_append_perm _ _ _, funext ys,
+  rw [permutations'_aux_eq_permutations_aux2, permutations_aux2_append]
+end
+
+@[simp] theorem mem_permutations' {s t : list α} : s ∈ permutations' t ↔ s ~ t :=
+(permutations_perm_permutations' _).symm.mem_iff.trans mem_permutations
+
+theorem perm.permutations {s t : list α} (h : s ~ t) : permutations s ~ permutations t :=
+(permutations_perm_permutations' _).trans $ h.permutations'.trans
+(permutations_perm_permutations' _).symm
+
+@[simp] theorem perm_permutations_iff {s t : list α} : permutations s ~ permutations t ↔ s ~ t :=
+⟨λ h, mem_permutations.1 $ h.mem_iff.1 $ mem_permutations.2 (perm.refl _), perm.permutations⟩
+
+@[simp] theorem perm_permutations'_iff {s t : list α} : permutations' s ~ permutations' t ↔ s ~ t :=
+⟨λ h, mem_permutations'.1 $ h.mem_iff.1 $ mem_permutations'.2 (perm.refl _), perm.permutations'⟩
+
 end permutations
 
 end list