Zulip Chat Archive

Stream: new members

Topic: ne_succ_self


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 10:32):

zero_ne_succ should solve this fine

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 17 2020 at 10:35):

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

view this post on Zulip 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 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.

view this post on Zulip Johan Commelin (Aug 17 2020 at 10:56):

Tip: use #backticks for formatting code

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 11:00):

you surely need to prove this by induction

view this post on Zulip Johan Commelin (Aug 17 2020 at 11:06):

@Kevin Buzzard This is the induction step, right?

view this post on Zulip Johan Commelin (Aug 17 2020 at 11:06):

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

view this post on Zulip Johan Commelin (Aug 17 2020 at 11:06):

Remember that \not P is shorthand for P → false

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 11:09):

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

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 11:09):

(because of what Johan said)

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 11:09):

ooh -- you'll need succ_inj right?

view this post on Zulip 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},
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.

view this post on Zulip Johan Commelin (Aug 17 2020 at 11:35):

Well, your h is very close to succ_ne_zero

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:13):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)`

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:33):

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

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:33):

e.g. have h2 := succ_inj h

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 12:34):

apply only works on goals

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 17 2020 at 12:46):

#backticks

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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
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

view this post on Zulip Chris Wong (Aug 17 2020 at 13:27):

but is expected to have type
  mynat : Type

That means it expects a number instead

view this post on Zulip Chris Wong (Aug 17 2020 at 13:28):

Try exact zero_ne_succ 0 h2

view this post on Zulip Claus-Peter Becke (Aug 17 2020 at 13:31):

@Chris Wong: That worked. Thank you.

view this post on Zulip 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,

Some comments could helpful, I suppose.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 14:22):

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

view this post on Zulip 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 }

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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