rw only replaces first occurrence

Stream: new members

[Lucy M]

Hello, I just came across this game thing called the natural number game, which teaches you lean (I never heard of it before today). I was going through it, and I came across a situation that doesn't feel right - but I have no idea how you would do this differently.

I have this situation (mynat is just the natural numbers defined by the lesson - I did not make it).

a b : mynat
⊢ a + b + 0 = a + (b + 0)

I also have this definition:

add_zero (a : mynat) :
a + 0 = a

now here is my question: when I type rw add_zero, it replaces the first b + 0 - but why I type rw add_zero b, it get rids of the second. Why is this? And why does it not get rid of both? Is there a way to replace all instances at once? Is there a way to replace a specific instance

[Lucy M]

Online it says rw rewites all terms simultaneously - so what am I doing wrong?

[Junyan Xu]

a + b + 0 is actually (a + b) + 0, so "the first b + 0" doesn't exist, and what rewrite does there is rw add_zero (a + b). If there were actually two b + 0s, they would be both replaced, but here it's not the case.

@maintainers These should be moved to another thread.

[Mario Carneiro]

anyone can move posts to another thread

[Junyan Xu]

It seems I cannot
https://zulip.com/help/move-content-to-another-topic
image.png

[Mario Carneiro]

oh, I guess that got changed to mod-only

[Junyan Xu]

I mean I can presumably move my own post by Edit the title, but not @Lucy M's posts.

[Lucy M]

I apologise, I did not mean to make the post here. i clicked on 'new members' so I thought it would create a new thread. I tried to move it after I posted it but I can't.

[Matt Diamond]

it's all good!

[Lucy M]

I have one more question if that is alright

my solution was this:

induction c with d hd,
rw add_zero (a + b),
rw add_zero b,
refl,

rw add_succ b d,
rw add_succ a (b + d),
rw add_succ (a+b),
rw ← hd,
refl,

and the 'offical' solution was this

induction c with d hd,
{ -- ⊢ a + b + 0 = a + (b + 0)
rw add_zero,
rw add_zero,
refl
},
{ -- ⊢ (a + b) + succ d = a + (b + succ d)
rw add_succ,
rw add_succ,
rw add_succ,
rw hd,
refl,
}

my question is what are the braces for? I tried again to search on google - but I could only get results about the braces being used in different contexts

[Mario Carneiro]

(#backticks)

[Mario Carneiro]

The braces denote subgoals. They ensure that the subgoal is closed at the close brace, so they provide better structuring of the proof

[Mario Carneiro]

you simulated that with an extra newline, but the braces are checked by lean

[Lucy M]

Ah, thank you - I understand, and thank you for letting me know ``` works as well!

[Lucy M]

Is there a way to put a lemma inside a lemma. There is a small theorem I want to make in order to make the puzzle easier but I get lots of errors when I try it

[Mario Carneiro]

have my_lemma : statement, { proof },

[Lucy M]

thank you, but I think I've done it wrong

have add_succ_zero (a : mynat) : a + succ(0) = succ a,
  {
    induction a with d hd,
    {
      rw zero_add (succ 0),
    },
    {
    rw add_succ (succ d) 0,
    rw add_zero (succ d),
    },
  },

This is what I've wrote but I get an "unexpected identifier a" error on line 35 and "sync" on line 36

[Reid Barton]

"my_lemma : statement" needs to be an ordinary type signature, not the syntax found in a top-level lemma. So

  have add_succ_zero : \all (a : mynat), a + succ(0) = succ a,

then you will need to intro a in the proof

[Lucy M]

Thank you, I'm having a lot of trouble googling for this language - do you have any online resources I can use to learn the syntax?

[Reid Barton]

Have you read #tpil?

[Mario Carneiro]

note that you might want to leave NNG and use lean proper if you are going to learn the syntax

[Mario Carneiro]

NNG is designed so that you don't have to really interact with the syntax of the language except for the small tactic vocabulary it teaches. I don't think it even teaches braces

[Kevin Buzzard]

No, I sometimes regret not teaching braces but students seemed to be happy with the idea that tactics just worked on the top goal so what the heck. I just feel a bit guilty that in some sense it's actively teaching bad style.

[Patrick Massot]

I never teach braces because students are so confused when they get braces wrong. Error messages in Lean 3 are not very helpful when your braces aren't balanced or when you forget a comma after a closing brace.