Natural Number Game

Stream: lean4

[Kreijstal]

image.png
there's a natural number game here https://adam.math.hhu.de/#/g/hhu-adam/NNG4/world/AdvAddition/level/6
surely the tactic tauto solves the problem, but I feel like it is cheating, how are you supposed to solve this level?

[Luigi Massacci]

You might use apply False.elim (which I’m not sure was shown in NNG though) and zero_ne_succ if you want all the intermediate steps I guess

[Leo Shine]

Why's it cheating? The panel on the left suggests using it

[David Méndez]

contradiction solved it for me, but I'm also not convinced that that was the way in which we are supposed to solve this level.

[Kevin Buzzard]

Thank you for this discussion. There are often many ways that you can solve a level and I don't think I have a "right" or a "wrong" way in my mind when I'm writing worlds, I just have a route through to a solution which uses only tactics which I have introduced so far. I will take a closer look at this thread and see if I can tidy things up, but please bear in mind that right now game development is very active (I have advanced multiplication world ready to go, I am moving where tauto is introduced and encouraging people to use it more) and things are still likely to be shifting around.

[Kreijstal]

image.png
like this, lol

[Kreijstal]

image.png
yay

[James Sully]

Hiya, I'm working through the natural number game, I'm up to less than equal world level 5:
theorem le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by

The hint says

It's "intuitively obvious" that there are no numbers less than zero, but to prove it you will need a result which you showed in advanced addition world.

The theorems from that world are:

n ≠ succ n
a + n = b + n → a = b
n + a = n + b → a = b
x + y = y → x = 0
x + y = x → y = 0
a + b = 0 → a = 0
a + b = 0 → b = 0

I'm a bit stuck on this, can I get another hint? It feels like it's probably referring to the last two but I'm not sure how to start.

[Mario Carneiro]

from the link above it seems like level 6 is a + b = 0 -> a = 0 which looks like the right lemma to use here

[Mario Carneiro]

how is less-equal defined?

[James Sully]

a <= b if exists c such that b = a + c

[James Sully]

so it introduced me to use in earlier exercises

[Mario Carneiro]

okay, so you should use that definition to get a + b = 0 from the assumption

[Mario Carneiro]

do you know how to unpack an existence assumption? use is for constructing one

[James Sully]

I'm assuming I use cases?

[James Sully]

I'm pretty fuzzy on what it means though

[Mario Carneiro]

the basic idea is that if you are trying to prove goal P and you have an assumption h that says there exists an x such that Q x holds, then cases h will give you such an x and the fact that Q x holds, and your goal is still to prove P

[James Sully]

the lean server on the website keeps crashing unfortunately

[James Sully]

got it, thanks!

cases hx with a
symm at h
apply eq_zero_of_add_right_eq_zero at h
exact h

[James Sully]

where hx was x <= 0

[James Sully]

I guess I don't need the with, I had thought that was a required part of the syntax

[Mac Malone]

@Mario Carneiro I was thinking of suggesting using induction on n. Is that unadvised?

[Mario Carneiro]

The way this game is structured you generally only have to do one induction per level

[Mario Carneiro]

and you don't need to write your own inductive hypotheses

[Mario Carneiro]

in this case the lemma to prove by induction is a + b = 0 -> a = 0 by induction on b, and this was done already in a previous level (which is the reason for the hint)

[Mac Malone]

@Mario Carneiro What is the motivation behind avoiding induction? Typing induction x in the level autogenerates the case split for you, so there isn't much overhead there.

[Mario Carneiro]

induction is the "creative" step when it comes to these kind of problems

[Mario Carneiro]

so it is helpful to control when it is done when teaching

[Mac Malone]

What is a "creative" step?

[Mario Carneiro]

It's well known in ATPs that the hardest step when reasoning about inductive types like Nat is coming up with the right inductive hypothesis or loop invariant, everything else is just "follow your nose"

[Mario Carneiro]

In this case, you might be tempted to prove a <= 0 -> a = 0 by induction on a, but this is the wrong move and you will get stuck

[Mac Malone]

@Mario Carneiro I did that and it worked. (I passed the level via induction on exactly that).

[Mario Carneiro]

if you have the right other lemmas you can still do it

[Mario Carneiro]

it's true after all

[Mario Carneiro]

so you can never really get stuck when applying induction with the wrong IH, but the induction might not do you any good

[Mac Malone]

That's certainly fair and true. In this case, though, induction does help.

[Mac Malone]

But I presume your point is that the goal is to avoid cases were it could hurt. However, isn't that true of other theorems as well (i.e., le_trans and the like can be applied ad nauseum to little effect as well if you don't have a plan).

[Mario Carneiro]

not exactly, there is a precise sense in which those are easier from an ATP perspective (and to some extent when hand proving too): you can enumerate all the consequences of what you know until you don't get any new things, and this can handle le_trans reasoning

[Mac Malone]

@Mario Carneiro I assume this applies when the strategy is strictly to apply one of the possible theorems to the current goal. Because you could continue building infinite have s by le_trans/le_succ from 0 upwards in the Nats (in a manner similar to inducitng up them). (iirc, one of these is forward reasoning and one is backwards reasoning?)

[Mario Carneiro]

I think the trick that makes saturation work is the subformula property: (under some conditions) if there is a proof then there is a proof which only uses subterms of what you already have

[Mario Carneiro]

so you know that just building up big terms doesn't help

[James Sully]

Ok, now I'm stuck on one that definitely does involve induction:
https://adam.math.hhu.de/#/g/hhu-adam/NNG4/world/LessOrEqual/level/8

Here's what I have so far:

theorem le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by

induction y with d hd
-- base
right
exact zero_le x

-- inductive
cases hd with x_le_d d_le_x
-- x_le_d case
left
apply le_trans x d (succ d) x_le_d (le_succ_self d)

Now my goal is:

Current Goal
Objects:
xd: ℕ
Assumptions:
d_le_x: d ≤ x
Goal:
x ≤ succ d ∨ succ d ≤ x

but the goal doesn't seem to me to follow from the assumption? It's difficult for me to keep track of what's going on haha

[James Sully]

presumably it must and I'm mistaken. But i'm not sure where to go next

[Ruben Van de Velde]

Maybe you should have started with induction y with d hd generalizing x

[James Sully]

hmm, that may be a better approach, but I haven't been introduced to generalizing yet and don't know what it is, and the hint says

Start with induction y with d hd.

So presumably it's not the intended solution

[Kevin Buzzard]

Generalizing won't help you here, I think. Do I not offer some hints with this level? It's one of the hardest ones. How do you get over the line with generalizing? Am I pushing people the wrong way?

[Kevin Buzzard]

My idea was: cases on d_le_x with a and then cases on a

[Ruben Van de Velde]

I didn't actually manage to finish it with generalizing either :)

[Thomas Murrills]

The key for me was realizing how to use numbers to make progress on ≤ goals, then working backwards. Without the usual things accessible, it took a bit to figure out which of the very few tools available were suitable! :P

[James Sully]

Kevin Buzzard said:

My idea was: cases on d_le_x with a and then cases on a

it seems very simple and obvious and mechanical when you put it like that haha. I guess I just lost faith

induction y with d hd
-- base
right
exact zero_le x
-- inductive
cases hd with x_le_d d_le_x
-- x_le_d case
left
apply le_trans x d (succ d) x_le_d (le_succ_self d)
cases d_le_x with a
cases a
rw [add_zero] at h
rw [h]
left
exact le_succ_self d

rw [add_succ, ← succ_add] at h
right
use a_1
exact h

[Thomas Murrills]

(Btw, @Kevin Buzzard, typo at the end: "remarks that with you've")

[James Sully]

thanks for the help!

[Mac Malone]

Mario Carneiro said:

In this case, you might be tempted to prove a <= 0 -> a = 0 by induction on a, but this is the wrong move and you will get stuck

As an FYI, here is how I solved LE world level 5 via induciton:

theorem le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by

induction x
rfl
rw [n_ih $ le_trans _ _ _ (le_succ_self n) hx] at hx
cases hx
rw [add_comm, add_succ, add_zero] at h
exact False.elim <| zero_ne_succ _ h

Noting this here in case @Kevin Buzzard desires to forbid such an inductive solution.

[Mac Malone]

(One worry is that my use of cases on the ≤ term may be an unintentional leakage of the underlying definition.)

[Ruben Van de Velde]

Level 4 explicitly teaches using cases like this

[Mario Carneiro]

I doubt Kevin actually wants to forbid proofs off the beaten track; finding a solution via an unexpected strategy is one of the joys of gaming

[James Sully]

I finished the game!

[James Sully]

that was fun

[learnreal]

For one of my goals

Objects:
abn_1: ℕ
Assumptions:
n_ih: (a * b) ^ n_1 = a ^ n_1 * b ^ n_1
Goal:
(a * b) ^ n_1 * (a * b) = a ^ n_1 * (a * b ^ n_1 * b)

I am tring rw [mul_comm a b^n_1] but getting the following error:

tactic 'rewrite' failed, equality or iff proof expected
  ?m.39929
case succ
abn_1: ℕ
n_ih: (a * b) ^ n_1 = a ^ n_1 * b ^ n_1
⊢ (a * b) ^ n_1 * (a * b) = a ^ n_1 * (a * b ^ n_1 * b)

can someone please explain the error to me and how to apply mul_comm here?

[Riccardo Brasca]

rw [mul_comm a (b^n_1)] should work.

[Kevin Buzzard]

You're not the first person who has run into this and I don't know what to do about it :-/

[learnreal]

Explicitly add example in documenttion? May be it's there but I missed it!

[Alexander Bentkamp]

Maybe we could add a custom elaborator that would catch equalities raised to the power of something and then throw a sensible error message?