list append append

Stream: general

[Martin Dvořák]

Am I the only one who uses the following lemmata?

lemma length_append_append :
  list.length (x ++ y ++ z) = x.length + y.length + z.length :=
by rw [list.length_append, list.length_append]

lemma map_append_append {f : α → β} :
  list.map f (x ++ y ++ z) = list.map f x ++ list.map f y ++ list.map f z :=
by rw [list.map_append, list.map_append]

lemma filter_map_append_append {f : α → option β} :
  list.filter_map f (x ++ y ++ z) = list.filter_map f x ++ list.filter_map f y ++ list.filter_map f z :=
by rw [list.filter_map_append, list.filter_map_append]

lemma reverse_append_append :
  list.reverse (x ++ y ++ z) = z.reverse ++ y.reverse ++ x.reverse :=
by rw [list.reverse_append, list.reverse_append, list.append_assoc]

lemma forall_mem_append_append {p : α → Prop} :
  (∀ a ∈ x ++ y ++ z, p a)  ↔  (∀ a ∈ x, p a) ∧ (∀ a ∈ y, p a) ∧ (∀ a ∈ z, p a)  :=
by rw [list.forall_mem_append, list.forall_mem_append, and_assoc]

lemma join_append_append {X Y Z : list (list α)} :
  list.join (X ++ Y ++ Z) = X.join ++ Y.join ++ Z.join :=
by rw [list.join_append, list.join_append]

They look like a pointless exercise, but they declutter my code.

[Floris van Doorn]

simp_rw [list.length_append] rewrites with list.length_append any number of times, and can probably be used instead of proving this new lemma.

[Martin Dvořák]

Sometimes I specifically want to rewrite "that triplet" and not just all places list.length_append matches.
Of course list.length_append_append is not the only solution, but it is the easiest solution for me.

[Martin Dvořák]

That said, I don't want to convert you to my faith. I am just curious whether other lean users have tiny lemmata of this kind in their code.

[Floris van Doorn]

We regularly add small lemmas like this in various places of mathlib. I can see that they can be useful sometimes.

[Eric Wieser]

I would say mathlib does not want these lemmas unless you also contribute a proof where they're used

[Eric Wieser]

Martin Dvořák said:

Sometimes I specifically want to rewrite "that triplet" and not just all places list.length_append matches.
Of course list.length_append_append is not the only solution, but it is the easiest solution for me.

This is usually a good excuse to use a have statement