[Merged by Bors] - feat(data/list/join): add list.append_join_append and list.reverse_join

src/data/list/join.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sébastien Gouëzel, Floris van Doorn, Mario Carneiro
+Authors: Sébastien Gouëzel, Floris van Doorn, Mario Carneiro, Martin Dvorak
 -/
 import data.list.big_operators
 
@@ -148,4 +148,28 @@ begin
   { simp },
 end
 
+/-- We can rebracket `x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x)` to
+`(x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x` where `L = [l₁, l₂, ..., lₙ]`. -/
+lemma append_join_map_append (L : list (list α)) (x : list α) :
+  x ++ (list.map (λ l, l ++ x) L).join = (list.map (λ l, x ++ l) L).join ++ x :=
+begin
+  induction L,
+  { rw [map_nil, join, append_nil, map_nil, join, nil_append] },
+  { rw [map_cons, join, map_cons, join, append_assoc, L_ih, append_assoc, append_assoc] },
+end
+
+/-- Reversing a join is the same as reversing the order of parts and reversing all parts. -/
+lemma reverse_join (L : list (list α)) :
+  L.join.reverse = (list.map list.reverse L).reverse.join :=
+begin
+  induction L,
+  { refl },
+  { rw [join, reverse_append, L_ih, map_cons, reverse_cons', join_concat] },
+end
+
+/-- Joining a reverse is the same as reversing all parts and reversing the joined result. -/
+lemma join_reverse (L : list (list α)) :
+  L.reverse.join = (list.map list.reverse L).join.reverse :=
+by simpa [reverse_reverse] using congr_arg list.reverse (reverse_join L.reverse)
+
 end list