Stuck on Natural Numbers Game: mul_pos

Stream: new members

[Joe Lambourne]

Hi,
I'm stuck on the first level of Advanced Multiplication World in the Natural Numbers Game. I've tried all kinds of approaches, but I can't make progress. There must be some tactic which I'm missing.

My basic strategy is

• Use the induction tactic
• Solve for the easy zero case
• Look for a way to use trick (2) given in the hints. i.e. I want the goal to be false and to have a hypothesis succ(something)=0

Could anyone give me a hint? If possible, don't post the solution but give me just enough to allow me make progress

[Kevin Buzzard]

Do you know the maths proof?

[Kevin Buzzard]

PS the website seems to be down again :-/ Here's a mirror https://cbirkbeck.github.io/natural_number_game . I've reported the issue, no doubt someone will read the report on Wednesday when the university opens again :-/

[Joe Lambourne]

I think the maths proof is something like this. From the state

hd : d ≠ 0 → b ≠ 0 → d * b ≠ 0,
m : b ≠ 0
⊢ succ d * b ≠ 0

We know that the successor of a number can never be zero. succ_ne_zero should take care of that.
We have a hypothesis that b ≠ 0.
We need the fact that multiplying two non-zero numbers results in a non-zero number. hd looks to cover that, but I'm not sure what tactic would use hdto get the goal into the right state for succ_ne_zero

[Ruben Van de Velde]

Joe Lambourne said:

We need the fact that multiplying two non-zero numbers results in a non-zero number.

Note that this fact is exactly what you need to prove in the first place

[Ruben Van de Velde]

From the state you posted, it looks like you've already made a wrong turn. Your induction hypothesis hd is not strong enough to make progress, because it's about fixed d and you need it for all d. I think you should have encountered that situation a few times before getting to advanced multiplication

[Joe Lambourne]

Ah. Yes. So it looks like I don't know the maths proof.
Also it looks like starting with induction was a wrong move. cases b with n, and solving the easy case got me to

a n : mynat
⊢ a ≠ 0 → succ n ≠ 0 → a * succ n ≠ 0

[Arthur Paulino]

Notice that using cases instead of induction usually gives you less resources to work with (no induction hypothesis)

[Kevin Buzzard]

I think you should have encountered that situation a few times before getting to advanced multiplication

@Ruben Van de Velde this is not true! In fact I never explain this issue properly, which is why everyone gets stuck on advanced mult world level 4, which is the first time you really need it (I now spell out what to do in the hints).

@Joe Lambourne it's getting to the point in the game where you need to know the maths proofs, you can't follow your nose any more. So I would try to figure out a maths proof before trying to leanify it.

[Joe Lambourne]

OK. Proof by contradiction feels like a sensible strategy.
Let's imagine that we have two numbers a ≠ 0 and b ≠ 0 but a*b=0.
Now a*succ(b)=a*b + a
but as a*b=0we have
a*succ(b)=a
Then with something like mul_one we see that succ(b)=1
but then b=0

Trying to follow this strategy I can get to

h : a ≠ 0,
i : b ≠ 0,
h : a * b = 0
⊢ false

[Ruben Van de Velde]

Kevin Buzzard said:

I think you should have encountered that situation a few times before getting to advanced multiplication

Ruben Van de Velde this is not true! In fact I never explain this issue properly, which is why everyone gets stuck on advanced mult world level 4, which is the first time you really need it (I now spell out what to do in the hints).

Oh huh, I was convinced it came up in addition somewhere. Thanks for the correction

[Joe Lambourne]

I was able to solve this, but I'm trying to understand quite how the tactics worked. The solution was a proof by contradiction implemented into lean using exact succ_ne_zero _ hab with a goal of false as recommended in the tricks section.

However the expressions in hypothesis hab which worked are not at all what I expected. It feels like the exact tactic is doing multiple extra steps for me. Is there a way to see what lean has replaced _ with to help extend my understanding?

[Patrick Johnson]

What is your proof? Tactics apply and exact can unfold terms up to definitional equality. So, for example, in this proof:

intros ha hb,
cases a, exact (ha rfl).elim,
cases b, exact (hb rfl).elim,
apply succ_ne_zero,

Before apply succ_ne_zero, the goal was succ a * succ b ≠ 0, but the apply tactic unfolds it to succ a * b + succ a ≠ 0 and then to succ (succ a * b + a) ≠ 0, so it figures out that the argument for succ_ne_zero must be succ a * b + a

[Kevin Buzzard]

You could fill in the hole with a random thing like 37 or hab and read the error to find out what it was expecting.

[Kevin Buzzard]

Note that add_succ is true by definition (under the hood its proof is rfl, just like add_zero), but the same does not apply to succ_add or zero_add (under the hood their proofs use the induction axiom).