Zulip Chat Archive

Stream: new members

Topic: Rewriting in just one place (newbie)

Cris Perdue (Jan 02 2023 at 19:34):

I am playing around with the natural numbers game online, trying out variations on some proofs.
I want to rewrite a hypothesis

ab : b + a = a

using zero_add, to get ab: b + a = 0 + a

with the step: rw ← zero_add a at ab,

I get: ab : b + (0 + a) = 0 + a (rewriting both occurrences of "a")

Is there a nice idiom that would give the desired result?

Martin Dvořák (Jan 02 2023 at 19:47):

You might try change for definitional equivalence or convert_to for other other. The latter might create additional goals.

Martin Dvořák (Jan 02 2023 at 19:50):

There is also nth_rewrite which first takes a zero-based index and then a rewrite lemma.

Kevin Buzzard (Jan 02 2023 at 19:50):

zero_add isn't definitional and NNG is running on a very old Lean so might well not have convert_to or nth_rewrite

Kevin Buzzard (Jan 02 2023 at 19:51):

The way I usually solve this sort of thing in NNG is have ab' : b + a = 0 + a, and prove this with rw zero_add, exact ab.

Patrick Johnson (Jan 02 2023 at 19:53):

NNG has tactic#conv

conv at ab {to_rhs, rw zero_add a}

Kevin Buzzard (Jan 02 2023 at 20:02):

indeed conv was in core Lean 3.4.1

Cris Perdue (Jan 02 2023 at 22:29):

Thanks much!

Last updated: Dec 20 2023 at 11:08 UTC