rw docs

Stream: new members

[Jeff Wu]

i'm brand new so this is surely a stupid question. I'm doing the natural number game and in the documentation for rw it says:

Exercise: think about why rw [add_zero] changes the term (0 + 0) + (x + 0) + (0 + 0) + (x + 0) to 0 + (x + 0) + 0 + (x + 0)

but why doesn't it become 0 + x + 0 + x? the docs don't make this clear to me (but I am likely missing something!)

[Notification Bot]

A message was moved here from #new members > proof aeval with calc by Jeff Wu.

[Kyle Miller]

rw finds the first place where add_zero would apply, specializes the arguments to the lemma, and then rewrites using that one specialization everywhere. Here, it specializes to add_zero 0. If it would rewrite x + 0 to 0, it would also have to use add_zero x simultaneously somehow.

This is sort of a side effect to how rw actually performs its rewrites. It can do a single concrete rewrite at any number of positions simultaneously. (There are options you can pass rw to say which occurrences you want to actually rewrite.)

[Nicholas Wilson]

(It might not be available in NNG, but) simp only [add_zero] will do multiple matches.