ne_succ_self

Stream: new members

[Claus-Peter Becke]

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]

Claus-Peter Becke said:

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

what does the error message say?

[Kevin Buzzard]

zero_ne_succ should solve this fine

[Claus-Peter Becke]

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]

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

[Claus-Peter Becke]

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

repeat {rw succ_eq_add_one},
repeat {rw one_eq_succ_zero},
repeat {rw succ_eq_add_one},

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]

Tip: use #backticks for formatting code

[Kevin Buzzard]

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

[Kevin Buzzard]

you surely need to prove this by induction

[Johan Commelin]

@Kevin Buzzard This is the induction step, right?

[Johan Commelin]

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

[Johan Commelin]

Remember that \not P is shorthand for P → false

[Claus-Peter Becke]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

(because of what Johan said)

[Kevin Buzzard]

ooh -- you'll need succ_inj right?

[Claus-Peter Becke]

After having used the following steps

'induction n with m,
intro h,
repeat {rw ← add_assoc at h},
repeat {rw zero_add at h},
rw add_zero 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]

Well, your h is very close to succ_ne_zero

[Claus-Peter Becke]

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]

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

[Claus-Peter Becke]

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]

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

[Claus-Peter Becke]

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]

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

[Kevin Buzzard]

e.g. have h2 := succ_inj h

[Kevin Buzzard]

apply only works on goals

[Kevin Buzzard]

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]

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

[Kenny Lau]

#backticks

[Claus-Peter Becke]

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

[Yakov Pechersky]

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

[Claus-Peter Becke]

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
Additional information:
/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]

but is expected to have type
  mynat : Type

That means it expects a number instead

[Chris Wong]

Try exact zero_ne_succ 0 h2

[Claus-Peter Becke]

@Chris Wong: That worked. Thank you.

[Claus-Peter Becke]

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,

Some comments could helpful, I suppose.

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Claus-Peter Becke]

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]

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]

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.