List lemmas

Stream: Is there code for X?

[Chris Wong]

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]

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]

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]

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]

Maybe a reducible setting for library_search would be useful?

[Scott Morrison]

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

[Scott Morrison]

 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]

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

[Scott Morrison]

I'll fix that bug.

[Scott Morrison]

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

[Scott Morrison]

#2648

[Reid Barton]

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]

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]

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.