No refl?

Stream: general

[Joseph O]

How come in this proof i dont need refl. I had to write it in the Natural Number Game.

lemma add_succ_zero (a : nat) : a + succ(0) = succ(a) :=
begin
  rw add_succ,
  rw add_zero,
end

when i write refl, at the end, it tells me

tactic failed, there are no goals to be solved
state:
no goals

is it implicit now?

[Julian Berman]

The nng uses a simplified rw, essentially to make it a bit less confusing to learn

[Julian Berman]

But yes the real rw will basically automatically run refl after rewriting

[Joseph O]

Julian Berman said:

The nng uses a simplified rw, essentially to make it a bit less confusing to learn

what is the nng?

[Joseph O]

how can i use the real rw?

[Alex J. Best]

Nng= natural number game, outside of the game rw is the real rewrite and you don't need to do anything special to use it

[Joseph O]

oh right

[Joseph O]

like im surprised with real rw succ_eq_add_one is

lemma succ_eq_add_one (n : nat) : succ n = n + 1 :=
begin
  rw one_eq_succ_zero,
end

but with nng its

lemma succ_eq_add_one (n : nat) : succ n = n + 1 :=
begin
  rw one_eq_succ_zero,
  rw add_succ,
  rw add_zero,
  refl,
end

[Alex J. Best]

What happens if you try the first one in nng, just followed by refl?

[Alex J. Best]

Does it work then? If add_succ and add_zero are proved by refl in the first place then it should be basically the same to do that

[Joseph O]

Alex J. Best said:

Does it work then? If add_succ and add_zero are proved by refl in the first place then it should be basically the same to do that

it doesn't prove it without them. It also seems like nng's rwa is analogous to the real rw.