Zulip Chat Archive

Stream: Is there code for X?

Topic: List lemmas


view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 10 2020 at 12:35):

Maybe a reducible setting for library_search would be useful?

view this post on Zulip Scott Morrison (May 10 2020 at 12:36):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Scott Morrison (May 10 2020 at 12:44):

I'll fix that bug.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 10 2020 at 12:50):

#2648

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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