Sam Estep

Stream: new members

[Sam Estep]

Hi everyone! I've been wanting to learn Lean for a while and now I finally have the time to do so :) I have a noob question: is there a way to do a rw in only part of something? For instance, in Advanced Addition world Level 8/13 of the Natural Number Game, I used this proof:

intro h,
rw ← add_zero a at h,
rw add_assoc at h,
rw zero_add at h,
exact add_left_cancel _ _ _ h,

But I'd like to just write something like this:

intro h,
rw_rhs ← add_zero a at h,
exact add_left_cancel _ _ _ h,

Is there a tactic that I could use for what I'm calling rw_rhs here?

[Bryan Gin-ge Chen]

There is conv, but I don't know if it works in the NNG: https://leanprover-community.github.io/extras/conv.html

[Sam Estep]

@Bryan Gin-ge Chen Ah thanks! That seems to be exactly what I was looking for; can I use that from my locally-downloaded Lean installation, or do I need to also install something else?

[Bryan Gin-ge Chen]

It's part of Lean's core library, so it should work out of the box, I think.

[Bryan Gin-ge Chen]

OK, this works in the level you're looking at:

intro h,
conv at h { to_rhs, rw ← add_zero a, },
exact add_left_cancel _ _ _ h,

[Sam Estep]

Oh awesome, thanks @Bryan Gin-ge Chen!

[Dan Stanescu]

@Sam Estep I don't have that level in front of me right now, but something like this may also help: rw [← add_zero a] {occs := occurrences.pos [1]}

[Bryan Gin-ge Chen]

Wow, I didn't know about occs / occurrences. We should add this info to the docs somewhere...

[Johan Commelin]

In theory mathlib's nth_rewrite tactic should also help here. But I recently tried it, and got an error. I haven't yet looked into why...

[Scott Morrison]

occs has pretty strange behaviour: if a rule can match multiple times, but with different arguments, rw {occs:=...} will not find the alternative matches. nth_rewrite was written to solve this problem.

[Wojtek Wawrów]

Dan Stanescu said:

Sam Estep I don't have that level in front of me right now, but something like this may also help: rw [← add_zero a] {occs := occurrences.pos [1]}

I've tried using your code but it just gives me an error. Could it be that it just doesn't work in NNG? Same goes for the nth_rewrite thing, it doesn't seem to be recognized in NNG (and I wouldn't know how to use it anyways)

[Kevin Buzzard]

rofl I think that code has very little chance of working in NNG; I use a hacked rw. Try using rewrite [← add_zero a] {occs := occurrences.pos [1]} in NNG? I didn't hack that, so NNG rewrite should be the same as Lean rw.

[Kevin Buzzard]

Lean rw closes goals which can be closed by rfl (i.e. it tries refl after every rewrite, and if it works it just closes the goal). I thought this was confusing for NNG beginners so i turned it off (and probably turned off a bunch of other things too).

[Kevin Buzzard]

Similarly I doubt I am importing enough in NNG to make nth_rewrite work. If you want to play it "properly" you can just download and install the repo -- it would be a much less painful experience!

[Wojtek Wawrów]

Using rewrite worked! Here's then a short solution which works in NNG:

rewrite [← add_zero a] {occs := occurrences.pos [2]},
exact add_left_cancel _ _ _,

I will have to get around to installing the repo, hopefully later this weekend.

[Kevin Buzzard]

One unfortunate consequence of the hacked rw decision in NNG is that we get people here complaining that rw works differently in real Lean than in NNG. I could have hacked rewrite instead, because then users might expect rw to behave differently, but this would have caused so many extra key presses for my users :-/

[ROCKY KAMEN-RUBIO]

My (somewhat clunky) approach if rw isn't cooperating is to use a have statement for the thing I wanted rw to give me, and then prove that. I'm forgetting whether NNG has discussed them at this point. This isn't much more concise, but maybe it feels a little less redundant?

intro h,
have h2 : a + b = a + 0,
rw add_zero,
exact h,
exact add_left_cancel _ _ _ h,

[Yakov Pechersky]

Can you put the larger #mwe?