English
Permutations of concatenation is ++ ts decompose into map of permutations of is followed by ts and then permutations of ts with is.reverse.
Русский
Перестановки конкатенации is ++ ts распадаются на отображение перестановок is на добавление ts, затем перестановки ts с is.reverse.
LaTeX
$$$$\operatorname{permutations}(is ++ ts) = (\operatorname{permutations} is).map (\lambda s. s ++ ts) ++ \operatorname{permutationsAux}\ ts\ (is.reverse)$$$$
Lean4
theorem permutations_perm_permutations' (ts : List α) : ts.permutations ~ ts.permutations' :=
by
obtain ⟨n, h⟩ : ∃ n, length ts < n := ⟨_, Nat.lt_succ_self _⟩
induction n generalizing ts with
| zero => cases h
| succ n IH => ?_
refine List.reverseRecOn ts (fun _ => ?_) (fun 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_permutationsAux2, permutationsAux_nil, permutationsAux_cons, append_nil]
refine
(perm_append_comm.trans ((IH₂.flatMap_right _).append ((IH _ h).map _))).trans
(Perm.trans ?_ perm_append_comm.permutations')
rw [map_eq_flatMap, singleton_append, permutations']
refine (flatMap_append_perm _ _ _).trans ?_
refine Perm.of_eq ?_
congr
funext _
rw [permutations'Aux_eq_permutationsAux2, permutationsAux2_append]
