Zulip Chat Archive

Stream: general

Topic: rw vs simp_rw


view this post on Zulip Johan Commelin (Jul 10 2020 at 03:55):

Are there downsides to using simp_rw vs rw? Is simp_rw going to be (much) slower? Otherwise I wonder if they should be merged.

view this post on Zulip Anne Baanen (Jul 10 2020 at 08:44):

There are things that simp_rw can't do by default: if your rewrite equation looks like x = some_function_of x then simp_rw is going to loop

view this post on Zulip Anne Baanen (Jul 10 2020 at 08:44):

There is presumably some fancy configuration that we can pass to simp to prevent this

view this post on Zulip Patrick Massot (Jul 10 2020 at 08:46):

Even without looping you sometimes want to rewrite only one occurence of a pattern.

view this post on Zulip Gabriel Ebner (Jul 10 2020 at 08:47):

Anne Baanen said:

There is presumably some fancy configuration that we can pass to simp to prevent this

{single_pass:=tt}

view this post on Zulip Scott Morrison (Jul 10 2020 at 11:07):

Could we turn on single_pass by default in simp_rw? This often trips me up, and I don't ever rely on the current behaviour (although presumably places in mathlib do at this point)

view this post on Zulip Kenny Lau (Jul 10 2020 at 11:20):

maybe rw_simp can be singlepass and simp_rw multiple pass

view this post on Zulip Kenny Lau (Jul 10 2020 at 11:20):

or better, make rw able to rewrite inside binders


Last updated: May 08 2021 at 10:12 UTC