## Stream: new members

### Topic: ne_succ_self

#### Claus-Peter Becke (Aug 17 2020 at 10:26):

I tried different ways to solve the problem. I used the induction, the cases-tactic or the way to produce via intro h as a hypothesis 0=succ 0 . Going the way via cases or induction I supposed that at the end it should be possible to proof at least the first goal 0 not equal succ 0 with the lemma zero_ne_succ when a had been substituted by 0. But unfortunately this doesn't work and I don't understand why.

#### Kenny Lau (Aug 17 2020 at 10:30):

Claus-Peter Becke said:

this doesn't work and I don't understand why.

what does the error message say?

#### Kevin Buzzard (Aug 17 2020 at 10:32):

zero_ne_succ should solve this fine

#### Claus-Peter Becke (Aug 17 2020 at 10:34):

I'm so sorry. I should have been a little more patient. That goal could be solved with apply zero_ne_succ. But the next one concerning the successor made some problems. I will evaluate it again and post the result.

#### Kenny Lau (Aug 17 2020 at 10:35):

don't just say "this doesn't work"; post the error

#### Claus-Peter Becke (Aug 17 2020 at 10:54):

To solve the next goal succ n not equal succ(succ n) I used the tactic rw

repeat {rw one_eq_succ_zero},

to get the following result: n + (0 + 1) ≠ n + (0 + 1) + (0 + 1). This inequation is obviously true. So, as I did successfully before, I tried to apply the cc- or the simp-tactic, but that didn't succeed with the following error_messages:

cc tactic failed
state:
case mynat.succ
n : mynat
⊢ n + (0 + 1) ≠ n + (0 + 1) + (0 + 1)

tactic failed, there are unsolved goals
state:
case mynat.succ
n : mynat
⊢ ¬n + 1 = n + (1 + 1)

Unfortuantely I don't find a way to continue at that point if this is a way that could be gone at all.

#### Johan Commelin (Aug 17 2020 at 10:56):

Tip: use #backticks for formatting code

#### Kevin Buzzard (Aug 17 2020 at 11:00):

I'm not sure it's "obviously true" -- isn't it precisely what you're supposed to be proving?

#### Kevin Buzzard (Aug 17 2020 at 11:00):

you surely need to prove this by induction

#### Johan Commelin (Aug 17 2020 at 11:06):

@Kevin Buzzard This is the induction step, right?

#### Johan Commelin (Aug 17 2020 at 11:06):

So rather, @Claus-Peter Becke you need to use the induction hypothesis somewhere

#### Johan Commelin (Aug 17 2020 at 11:06):

Remember that \not P is shorthand for P → false

#### Claus-Peter Becke (Aug 17 2020 at 11:08):

These are very helpful hints. I'm just trying to prove the goal using the induction-tactic.

#### Kevin Buzzard (Aug 17 2020 at 11:09):

if you're trying to prove a != b then you can intro h

#### Kevin Buzzard (Aug 17 2020 at 11:09):

(because of what Johan said)

#### Kevin Buzzard (Aug 17 2020 at 11:09):

ooh -- you'll need succ_inj right?

#### Claus-Peter Becke (Aug 17 2020 at 11:28):

After having used the following steps

'induction n with m,
intro h,
repeat {rw ← add_assoc at h},

I end up with the following goal:
2 goals
h : 1 = 1 + 1
⊢ false'

And at that point I don't know of how to apply Johan's hint. As far as I see h corresponds to P (in Johan's hint). If this is true I don't find a way to apply it in this context. The apply- or exact-tactics don't work as far as I see. If I would have succeeded in showing that what h maintains is false I should be able to use exact h to finish the proof of this goal.

#### Johan Commelin (Aug 17 2020 at 11:35):

Well, your h is very close to succ_ne_zero

#### Claus-Peter Becke (Aug 17 2020 at 12:06):

I don't find an appropriate tactic to apply the succ_ne_zero- lemma. My h has the following shape at present: h : succ 0 = succ (succ 0)

#### Kevin Buzzard (Aug 17 2020 at 12:13):

you can probably just do cases on h to close the goal

#### Claus-Peter Becke (Aug 17 2020 at 12:17):

That works. I don't know why up tp now, but I will have again a closer look at the explanations of the tactics in the NNG.

#### Kevin Buzzard (Aug 17 2020 at 12:23):

if you want to do it more carefully you can apply succ_inj and then zero_ne_succ

#### Claus-Peter Becke (Aug 17 2020 at 12:33):

Using apply succ_injinstead of cases hdoesn't work unfortunately It generates the following error messages:
Invalid apply tactic, failed to unify
false
with
?m_1 = ?m_2
state:
2 goals
h : succ 0 = succ (succ 0)
⊢ false

case mynat.succ
m : mynat,
n_ih : m + (0 + 1) ≠ m + (0 + 1) + (0 + 1)
⊢ succ m + (0 + 1) ≠ succ m + (0 + 1) + (0 + 1)

#### Kevin Buzzard (Aug 17 2020 at 12:33):

you need to apply it to h, not to the goal

#### Kevin Buzzard (Aug 17 2020 at 12:33):

e.g. have h2 := succ_inj h

#### Kevin Buzzard (Aug 17 2020 at 12:34):

apply only works on goals

#### Kevin Buzzard (Aug 17 2020 at 12:35):

Your inductive hypothesis is horrible. What are all these zeros? I suspect that you messed around with your goal and introduced them before you applied the induction tactic, and now they're everywhere

#### Kevin Buzzard (Aug 17 2020 at 12:36):

All that repeat stuff you quoted above has just made the goal mathematically equivalent but harder to work with

#backticks

#### Claus-Peter Becke (Aug 17 2020 at 12:51):

@Kevin Buzzard Which tactic can I use to apply the zero_ne_succ-lemma on h2?

#### Yakov Pechersky (Aug 17 2020 at 12:54):

If you're trying to prove false, then you can just directly do exact zero_ne_succ h2

#### Claus-Peter Becke (Aug 17 2020 at 13:09):

That doesn't work unfortunately. It produces the following error messages after having generated h2 with the have-tactic.

type mismatch at application
zero_ne_succ h2
term
h2
has type
0 = succ 0 : Prop
but is expected to have type
mynat : Type
/Natural number game-1.3.3-library.lean:28:6: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
type mismatch, term
zero_ne_succ ?m_1
has type
0 ≠ succ ?m_1
but is expected to have type
false
state:
2 goals
h : succ 0 = succ (succ 0),
h2 : 0 = succ 0
⊢ false


#### Chris Wong (Aug 17 2020 at 13:27):

but is expected to have type
mynat : Type


That means it expects a number instead

#### Chris Wong (Aug 17 2020 at 13:28):

Try exact zero_ne_succ 0 h2

#### Claus-Peter Becke (Aug 17 2020 at 13:31):

@Chris Wong: That worked. Thank you.

#### Claus-Peter Becke (Aug 17 2020 at 14:16):

Finally I found a solution:

cases n,
apply zero_ne_succ,
intro h,
induction n with m,
have h2 := succ_inj h,
exact zero_ne_succ 0 h2,
have h3 := succ_succ_inj h,
rw ← h3 at h,
rw ← h3 at n_ih,
rw ← h3 at n_ih,
apply n_ih,
refl,


#### Kevin Buzzard (Aug 17 2020 at 14:17):

why do you do cases n and then induction n? It would be quicker to just do induction n from the outset

#### Claus-Peter Becke (Aug 17 2020 at 14:20):

Ok, I will keep it in my mind. Now in the beginning of working with lean prover I followed every hint I could get. Next I will try to be more concise.

#### Kevin Buzzard (Aug 17 2020 at 14:22):

this is a straight induction, you don't need to do the initial case split.

#### Kevin Buzzard (Aug 17 2020 at 14:24):

induction n with d hd,
{ exact zero_ne_succ 0 },
{ intro h,
apply hd,
apply succ_inj,
exact h }


#### Kevin Buzzard (Aug 17 2020 at 14:26):

You can always take a peek at the "official solutions" too e.g. https://github.com/ImperialCollegeLondon/natural_number_game/blob/master/src/game/world8/level13.lean

#### Claus-Peter Becke (Aug 17 2020 at 14:27):

Next time ( in the Advanced Multiplication World) I will try to improve it. And you remember, you made me aware of the need to use the induction to prove what I expected to be self-evident. Because I'm not very experienced in dealing with mathematical subjects I will have to learn a lot.

#### Kevin Buzzard (Aug 17 2020 at 14:30):

natural numbers are a really cool mathematical object to learn about :-) They are in some sense the simplest infinite object.

#### Claus-Peter Becke (Aug 17 2020 at 14:34):

With respect to the link you posted. That's great. I didn't know that there is a collection of solutions.
And with respect to your comment on the natural numbers. Yes, I agree with you completely. That's a fascinating story. I regret that I start as late as I do becoming familiar with these subjects.

#### Kevin Buzzard (Aug 17 2020 at 14:35):

The way the game works is that that it needs to know that all the levels are solvable, so the solutions have to be in there somewhere :-) The link is to the source code.

#### Claus-Peter Becke (Aug 17 2020 at 14:40):

I would like to say thank you and bye-bye for today. Tomorrow in the morning I will start the next session. Irt was a great pleasure to be here and to benefit from your great support.

Last updated: May 15 2021 at 23:13 UTC