advanced addition world level 7

Stream: new members

[Nam]

what is wrong with this solution that it keeps saying , is expected?

  split,
  exact add_right_cancel _ _ _,
  induction t on d hd,
  repeat {rw add_zero},
  exact id,
  intro h,
  rw succ_eq_add_one,
  repeat {rw ← add_assoc},
  rw t_ih,
  refl,
  rw h,
  refl,

[Kevin Buzzard]

Please post a MWE

[Kevin Buzzard]

Oh I just saw the title. Hang on.

[Nam]

sorry, the context is http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

[Kevin Buzzard]

induction t on d hd this line is bad.

[Kevin Buzzard]

induction t with d hd,

[Kevin Buzzard]

(and then you won't get a t_ih)

[Kevin Buzzard]

If you just change it to induction t, it works

[Kevin Buzzard]

In VS Code you clearly see the error on on.

[Nam]

that's useful! thanks.

[Kevin Buzzard]

But NNG is most easily played via the website.

[Nam]

it is kinda upsetting too that we need an IDE to spot the error.

[Kevin Buzzard]

The interface is very primitive really. It was written by mathematicians ;-)

[Kevin Buzzard]

But it's just about good enough to make it playable.

[PV]

what's the "on" actually doing in that case? I've made that typo a few times.

[Kevin Buzzard]

In VS Code it just says "I don't know what you're talking about with the on"

[Kevin Buzzard]

The induction tactic succeeds, Lean finds "on" and doesn't know what to do because it was expecting , or with, so it gives an error saying it was expecting ,, and then just proceeds as normal with the induction having succeeded.

[Kevin Buzzard]

The error I get with the original code is

27:14: error:
invalid 'begin-end' expression, ',' expected

and indeed it is the 14th character on the 27th line which is the problem, which is the o in on

[Nam]

what does exact succ_ne_zero(a + b) H, mean? does succ_ne_zero(a + b) return a lambda, and then it applies to H?

[Kevin Buzzard]

Probably succ_ne_zero (a + b) is a proof that succ(a + b) \ne 0, and in Lean X \ne Y is defined to mean (X = Y) -> False, so maybe H is a proof of succ(a + b) = 0

[Kevin Buzzard]

and the goal was false?

[Nam]

yes. my question was about the syntactic meaning of that clause.

[Kevin Buzzard]

The answer to your question is yes.

[Kevin Buzzard]

succ_ne_zero (a + b) : (succ (a + b) = 0) -> false

[Kevin Buzzard]

(I just fixed several missing succ errors)

[Nam]

ah, i think i've got it now. thanks Kevin.