## Stream: Is there code for X?

### Topic: List lemmas

#### Chris Wong (May 10 2020 at 10:05):

Do we have either of these in mathlib?

lemma singleton_append {α} (x : α) (l : list α) : [x] ++ l = x :: l :=
by rw [list.cons_append, list.nil_append]

lemma bind_singleton {α β} (x : α) (f : α → list β) : list.bind [x] f = f x :=
by rw [list.cons_bind, list.nil_bind, list.append_nil]


I did find the latter in terms of monads, but it would still be nice to have a version specialized to lists.

#### Shing Tak Lam (May 10 2020 at 11:13):

library_search is helpful here and finds solution to both.

lemma singleton_append {α} (x : α) (l : list α) : [x] ++ l = x :: l :=
rfl

lemma bind_singleton {α β} (x : α) (f : α → list β) : list.bind [x] f = f x :=
list.append_nil (f x)


#### Scott Morrison (May 10 2020 at 12:34):

Even if the first is true by rfl, it might not hurt to have the lemma, so that one can rewrite using it.

#### Scott Morrison (May 10 2020 at 12:35):

Similarly the second can still be useful, as the solution found by library_search is unfolding some definitions, and it might be helpful to have the syntactical statement too.

#### Reid Barton (May 10 2020 at 12:35):

Maybe a reducible setting for library_search would be useful?

#### Scott Morrison (May 10 2020 at 12:36):

Moreover, potentially both of these lemmas could be @[simp] lemmas?

#### Scott Morrison (May 10 2020 at 12:42):

 library_search { apply := λ e, tactic.apply e { md := tactic.transparency.reducible } }


should do this (i.e. only unfold reducible things), but there is a small bug preventing it from working.

#### Scott Morrison (May 10 2020 at 12:42):

(the custom apply tactic is only used by solve_by_elim discharging subgoals, not for actually applying library lemmas)

#### Scott Morrison (May 10 2020 at 12:44):

I'll fix that bug.

#### Scott Morrison (May 10 2020 at 12:45):

@Reid Barton, if you have an idea for a shortcut syntax for the reducibility setting, I can do that.

#2648

#### Reid Barton (May 10 2020 at 12:54):

Well, hmm... the best option would be not to have an option, and have library_search try with the reducible setting first. Would this be too slow?

#### Scott Morrison (May 11 2020 at 02:23):

I'll try to do some experiments. I don't know what to expect: pessimistically, it will take twice as long, optimistically, running with md := reducible could be be much faster (and so potentially even faster overall in cases where it finds something in the first pass).

#### Chris Wong (May 12 2020 at 10:40):

What an interesting discussion!

Indeed I was using these for rw. With palindromes, there's a lot of x :: (l ++ [x]) constructions that take some effort to manipulate.

I think I'll send a PR then, if at least so they're there next time I reach for them.

Last updated: May 16 2021 at 05:21 UTC