# Zulip Chat Archive

## Stream: general

### Topic: Ntural number game advanced addition world / 13

#### Daniel Papp (Jan 10 2021 at 17:19):

So the problem is the following: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=8&level=13 And this proof works:

```
symmetry,
intro p,
induction n with d hd,
exact succ_ne_zero(0)(p),
exact hd(succ_inj(p)),
```

My question is if I want to introduce a new variable for `succ_inj(p)`

before the last line how should I parametrize the `succ_inj`

function/theorem to make this work. I tried something like `have tmp := (succ_inj (succ d) d)(p)`

but that didn't seem to work. Not sure if such lisp-like syntax is allowed here or not.

#### Daniel Papp (Jan 10 2021 at 17:20):

Note that I would like to be explicit about the parameters for the theorem I know `have tmp := succ_inj(p)`

would work just fine.

#### Yakov Pechersky (Jan 10 2021 at 17:38):

Because the definition of `succ_inj`

is:

```
succ_inj {a b : mynat} :
succ(a) = succ(b) → a = b
```

those curly braces mean that the arguments are implicit. To prove arguments explicitly to `succ_inj`

for the `a b`

, you can use `@`

like so:

```
have := @succ_inj (succ d) d p,
```

But in any case, a proper `p`

hypothesis will always allow both `a b`

to be inferred.

#### Daniel Papp (Jan 10 2021 at 18:00):

I see. so does this also mean that the above case I can use `hd(succ_inj (succ d) d p)`

as well?

What do you mean by proper hypothesis? Also could you give me some link on how lean infers this?

Thanks for your help btw!

#### Yakov Pechersky (Jan 10 2021 at 18:45):

You can read this section of TPIL: https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html and TPIL in general is a good resource.

#### Yakov Pechersky (Jan 10 2021 at 18:45):

You would have to say `hd (@succ_inj (succ d) d p)`

if you really wanted to be explicit

#### Yakov Pechersky (Jan 10 2021 at 18:48):

Your `p`

is a hypothesis that says `p : succ (succ d) = succ d`

. And you have a theorem that says that for any `a b`

such that `succ a = succ b`

then `a = b`

.

What does that look like?

```
succ_inj {a b : mynat} :
succ(a) = succ(b) → a = b
```

The implicit arguments mean -- infer which `a`

and `b`

I'm talking about from the hypothesis given. So, when you say `succ_inj p`

, that is `succ_inj`

over a hypothesis that `succ (succ d) = succ d`

, then of course it is obvious that the only `a`

and `b`

being discussed here are `succ d`

and `d`

, respectively.

#### Daniel Papp (Jan 10 2021 at 19:07):

Thanks Yakov!

I think I more or less understand it. I mean I was going through the exercises in the natural number game. Sometimes it feels a bit like magic. I have to get used to this language I guess.

Thanks for the link too!

#### Kevin Buzzard (Jan 10 2021 at 19:21):

Lean does not do magic. After a while you can start asking yourself how it just did what it did, and finding the logical explanation.

#### Daniel Papp (Jan 11 2021 at 10:55):

Yes, I get that. I really like this tool. I hope it will be more widespread in the future. It would be interesting to see sites similar to math.stackexchange.com to use lean or having competition sites like codeforces but for math.

#### Alex Peattie (Jan 11 2021 at 12:10):

Daniel Papp said:

Yes, I get that. I really like this tool. I hope it will be more widespread in the future. It would be interesting to see sites similar to math.stackexchange.com to use lean or having competition sites like codeforces but for math.

In case it's of interest there are some Lean challenges on Codewars :smile: - https://www.codewars.com/kata?language=lean

#### Daniel Papp (Jan 11 2021 at 12:19):

Thanks Alex! I check that out in the evening.

Last updated: Dec 20 2023 at 11:08 UTC