Beginner Question (Lean Natural Number Game Level)

Stream: new members

[jakub]

Hello, I'm just getting into lean, and I wanted to ask how to prove

theorem add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by

this is part of this level
I'm using the cases tactic and so far I've gotten the case b=0 proven by entering

cases b with d

and then

apply add_left_eq_self

How do I prove the other case?

[Luigi Massacci]

This is the wrong channel for these kinds of questions

[Luigi Massacci]

You should ask this in #new members

[jakub]

Sorry, where can I post my question

[jakub]

okay, thanks

[Luigi Massacci]

Don't double post though, maybe @Kim Morrison can move it there?

[Ruben Van de Velde]

They're probably offline for the weekend

[Luigi Massacci]

I forgot it's Saturday :sob:

[Luigi Massacci]

Time flies

[Ruben Van de Velde]

Anyway, the first step is: what's the pen-and-paper proof?

[jakub]

Ruben Van de Velde said:

Anyway, the first step is: what's the pen-and-paper proof?

Well you change a + succ d to succ (a + d) and then use the theorem that the successor of anything is not equal to zero, and if the left side of the implication is false then the implication is said to be true

[jakub]

jakub said:

Ruben Van de Velde said:

Anyway, the first step is: what's the pen-and-paper proof?

Well you change a + succ d to succ (a + d) and then use the theorem that the successor of anything is not equal to zero, and if the left side of the implication is false then the implication is said to be true

Not sure how to transfer this into code though

[Ruben Van de Velde]

Can you do the first step?

[jakub]

Ruben Van de Velde said:

Can you do the first step?

Yes, I just type

rw [add_succ]

But then when I try to apply succ_ne_zero it gives me an error so I'm not sure what commands I need to do next to make this work

[Ruben Van de Velde]

First, you assume that succ (a + d) = 0 with intro h

[jakub]

Alright, what comes next?

[Ruben Van de Velde]

So you've got hypothesis succ (a + d) = 0 and a theorem 0 ≠ succ x, so you want to swap around the sides of the equation in h. Have you seen a tactic for that?

[jakub]

Yeah, I can use symm, though I'm not sure why I would since both succ_ne_zero and zero_ne_succ exist

[Ruben Van de Velde]

Oh, if you've unlocked that, you can use that with apply succ_ne_zero at h

[jakub]

That works, and then?

[jakub]

Ruben Van de Velde said:

Oh, if you've unlocked that, you can use that with apply succ_ne_zero at h

How do I do something with the False that remains

[Ruben Van de Velde]

Read the left hand bar again :)

[jakub]

Ohhhh okay I had to read it a couple times to see what it actually meant. Thank you very much

[Tom]

Hi @jakub

(Take my advice with a big pinch of salt because I am also just a learner) I found the following very useful:

https://plfa.github.io/

It's an online book about theorem proving in Agda, and the first two chapters on naturals and induction cover proofs very similar to what you're asking about. While the syntax is a little different, it's similar enough to make it easy to learn the concepts and transfer them to Lean, so I've been working through it while learning Lean side-by-side. (I don't know if there are any major differences in the theoretical underpinnings of Agda vs Lean, but as far as I can tell at my level of understanding of dependent types, they seem identical).

HTH,

Tom

[Notification Bot]

This topic was moved here from #lean4 > Beginner Question (Lean Natural Number Game Level) by Kim Morrison.