Natural Numbers Game Level No Solution?

Stream: new members

[Jared Cosulich]

Hi all, apologies for what is likely a silly question, but I can't seem to figure out what I believe is intended to be a relatively easy level:

≤ World, Level 2 / 11, 0 ≤ x

I don't seem to have the tools available to get passed x = 0 as the goal:

**Theorem** `zero_le`: If x is a number, then 0≤x.
`theorem zero_le (x : ℕ) : 0 ≤ x := by`

use 0
rw [add_zero]

Current Goal
Objects:
**x**: ℕ

Goal:
x = 0

Am I missing something?

[Kevin Buzzard]

Think about what claim you're making when you write use 0.

[Jared Cosulich]

My understanding is the "use" statement is to provide a c such that :

b = a + c

In this case a = 0, b = x so the statement becomes x = 0 + c

but there is no additional information about x, so it would seem that any positive number could be an answer. This doesn't seem like much of a proof though.

Alternatively if I use cases then I can get it down to pred d = 1 but again there's no additional context for d to work with.

cases x with d
use 0
rw [add_zero]
rfl
use 1
rw [zero_add]

Current Goal
Objects:
d: ℕ
Goal:
succ d = 1

If I use induction then I can create additional context for d, but I can't figure out how to leverage the assumption hd: 0 ≤ d (e.g. use 1 at hd throws an error)

induction x with d hd
use 0
rw [add_zero]
rfl
use 2
rw [zero_add]

Current Goal
Objects:
d: ℕ
Assumptions:
hd: 0 ≤ d
Goal:
succ d = 1

I'm sure I am missing something here, but I'm not sure what. For context, I'm not a mathematician (learning this all as an experiment in learning more mathematical concepts in a format I'm comfortable with - I'm a software developer)

[Mark Fischer]

You're trying to find a c such that x = 0 + c. In the case where, for example, x has the value 5, you'd want a c such that

5 = 0 + c

If I try use 0, I'd be trying to prove the following:

5 = 0 + 0

and I can use any positive number. Say use 271:

5 = 0 + 271

I don't think those are statements I can prove.
If I try use 5, I get

5 = 0 + 5

Which is something I think I can actually prove.

[Jared Cosulich]

Ok, I didn't realize that you could call use with a variable. That is what I was missing.

[Mark Fischer]

Ah. Any expression with the right type! :) So things like use x * x + x + 1 don't throw a syntax error.

[Jared Cosulich]

Yes, makes sense. Feel silly for not recognizing that sooner. Thank you for the help!

[Jared Cosulich]

I think it might help to add an example with a variable to the definition of use (I just found it confusing because every example provided that I saw used an explicit natural number). Would an addition to the use "documentation" in the game be welcome? I'm happy to open a PR for it in GitHub. Maybe something like:

use can accept a variety of arguments, such as 37, x, x * x + 1 as long as the variable is of the correct type

[Mark Fischer]

-deleted-