natural numbers world ... advanced addition world

Stream: new members

[Robert Watson]

Hi there, I'm working through the natural numbers game and am stuck on advanced addition world 13 that asks for a tactics proof of n \ne succ n. I think I'm stuck because I keep thinking of it in terms of recursion, and I'm pretty sure I can't do recursive proofs with tactics. Some pointers would be great. (also I'm doing something wrong with the code formatting here, where I tried to use backticks but it didn't display \ne correctly?)

[Daniel Packer]

I'm not sure what you mean by recursion, but at least when I did this proof I didn't use induction. That said, the main idea was to reduce the problem to a state where I could use zero_ne_succ. I'm happy to give more hints if you'd like--I don't want to ruin your fun, though!
Re: code formatting, I generally just copy and paste the unicode into the backticks: n ≠ succ n. Maybe someone else has a better way?

[Robert Watson]

Yeah, I need one more hint. I was already doing that. The trouble is I was ending up with a sort of loop as I was using induction.

[Daniel Packer]

Ahh, the other lemma that was "key" was rw add_right_cancel_iff at g,

[Robert Watson]

great thanks.

[Arthur Paulino]

Daniel Packer said:

Re: code formatting, I generally just copy and paste the unicode into the backticks: n ≠ succ n. Maybe someone else has a better way?

• If you want a system wide unicode typing method on Linux, you can try m17n-lean
• A cross platform and system-wide solution: Espanso (will require a manual configuration)
• An extension that works on Chrome or Chromium: chrome-lean-unicode
• A solution for Android
• A solution that turns browser text inputs into neovim input buffers

[Robert Watson]

´
intro g,
rw succ_eq_add_one at g,
rw (add_right_cancel_iff 0 n (n + 1)).1 at g,
rw add_assoc at g,
rw (add_left_cancel n 1 2) at g,
´

I don't think my problem here is which tactic to use in principle. It's something more fundamental to do with the hidden details of the tactics. In the above code when I apply cancel the number of required goals increases. But the idea of the cancelation is to decrease the number of goals! I just end up increasing the number of goals with each cancelation. This is essentially what I was also doing before when I was trying to solve it with the induction tactic.

[Kevin Buzzard]

#backticks

[Robert Watson]

I have an italian keyboard. It has no backticks!

[Kevin Buzzard]

Oh no!

If I do what you did above, I end up with three goals, two of which look fine, and one of which is to prove that n + 2 ≠ n + 4, which seems harder than the original question, making me think that you're going in the wrong direction.

[Kevin Buzzard]

Sure the number of goals you get increases with your method: you are rewriting a theorem of the form X -> (a = b) so it will rewrite the a's to b's but it won't forget the promise that you're making, namely that X is true; it will add it as a new goal.

[Robert Watson]

intro g, rw succ_eq_add_one at g, rw (add_right_cancel_iff 0 n (n + 1)).1 at g, rw (add_right_cancel n 1 (n + 1)) at g,

[Kevin Buzzard]

#backticks

[Robert Watson]

This is worse of course. (By the way the above is formatted with alt-96,. backtick...it isn't working for me)

[Kevin Buzzard]

As the link explains, you need to use three backticks on a single line by itself. Click on the three dots for this message and then "view source":

intro g,
rw succ_eq_add_one at g,
rw (add_right_cancel_iff 0 n (n + 1)).1 at g,
rw (add_right_cancel n 1 (n + 1)) at g,

[Robert Watson]

Ah, sorry, thought it wasthe same link! Got it. Thanks.