# Zulip Chat Archive

## Stream: new members

### Topic: Natural number game

#### Rei (Apr 02 2021 at 04:11):

Hi :) I just finished the natural number game, it was really fun! The levels are well designed and explanations are sufficient to understand the material but not spoil the solutions.

A few questions

- I noticed in Proposition World, many of the levels are very similar to Function world. I assume this is to instill the "moral" that propositions and functions can be thought of as similar? Level 7 proposition world still says "Function world" though, and there are few more typos. Should I submit a PR for these, or is this intended?
- I'm not much of a mathematician but I can probably help out on the more programming aspects, are the issues in https://github.com/ImperialCollegeLondon/natural_number_game/issues good to start with if I wanted to help out?
- I'm a little fuzzy on the concept of "fixed" variables (as introduced in Adv Mult 4/4). If there's a declaration
`a: mynat`

, does that mean`a`

is fixed in this context? If I'm doing an induction (for example) on`b`

in`a+b>a`

and my inductive hypothesis ends up being`a+k>a`

, are both`a`

and`k`

the same "kinds" of variables in this context? Fixed? It seems a bit weird because I should be able to substitute anything I want for`a`

in the inductive hypothesis and still have the proof be correct, but of course I cannot substitute`succ k`

for`k`

. Are there other kinds of variables? For example, in`\exists z.z \geq 0`

, is z thought of as "fixed"?

#### Johan Commelin (Apr 02 2021 at 04:39):

cc @Kevin Buzzard

#### Kevin Buzzard (Apr 02 2021 at 09:31):

Oh yeah proposition world and function world are a kind of joke way of teaching mathematicians about the Curry Howard correspondence. I did it like that because at the time I was convinced that mathematicians would better understand intro and apply in the context of functions and I thought that this was quite an amusing way to teach it. Since then I've discovered that mathematicians are just fine with the whole intro apply thing applied directly to propositions and proofs (see for example workshop 1 of my recent course where I just dive straight in) so if I were to write the game again then probably function world would not be in there. I would happily look at PRs, maybe it's about time I added less than world

#### Kalle Kytölä (Apr 02 2021 at 10:28):

As a mathematician with no logic background, I can confirm that Kevin's joke landed, and "amusing" is an understatement.

I was wondering, however, if it is worth avoiding explicit spoilers about that. At least I personally really appreciated sitting back and enjoying the NNG show.

#### n Simplex Pachinko (Apr 02 2021 at 15:23):

In Power World, I noticed that the first two (at least) can be solved using only "refl,". I don't think that should be a valid strategy for either, as they are not literally equal.

#### Kevin Buzzard (Apr 02 2021 at 18:07):

They are definitionally equal though, and that's what refl tests for, and I can't change the behaviour of lean there. I guess I could make a bunch of stuff irreducible, but in practice the one big change to lean I did make (disabling refl after rw) has caused some confusion when people come from NNG to proper lean so I'm reluctant to make any more changes such as breaking refl

#### Jukka Kohonen (Aug 17 2021 at 21:32):

Can I ask a question about the Natural number game here? It looks like if I close a proof by "simp", the game does not acknowledge that the proof is complete. For example in Power World, Level 2, there is a very short proof like "rw pow_succ, rw mul_zero, simp," but all I get is "no goals". However, if instead of "simp" I say "refl" it says "Proof complete". What am I missing here?

#### Ruben Van de Velde (Aug 17 2021 at 21:35):

Weird. Just `simp [pow_succ]`

also shows "Proof complete"

#### Eric Rodriguez (Aug 17 2021 at 21:35):

it's just a bug (an annoying one tbf); don't worry about it!

#### Eric Rodriguez (Aug 17 2021 at 21:35):

it can happen with `refl`

and with other things too, it's very unpredictable in my experience

#### Jukka Kohonen (Aug 17 2021 at 21:37):

Ok thanks :) It's just confusing that even if I complete all levels, the world stays blue in the Main Menu (because some of the levels were not "really" completed). I get the feeling that I missed something. Now that I know, I won't worry

#### Kevin Buzzard (Aug 18 2021 at 08:22):

Just hit enter a few times

#### Lucas (Aug 18 2021 at 20:21):

Where is the definition of prime numbers in lean? I tried data.nat.prime and init.data.nat.prime and many close variants thereof. It seems to have moved from where the online tutorials say they are, and I am having trouble finding it.

#### Bryan Gin-ge Chen (Aug 18 2021 at 20:22):

Is docs#nat.prime what you're looking for?

#### Lucas (Aug 18 2021 at 20:24):

it looks like it is, how do you set it up to be imported?

#### Bryan Gin-ge Chen (Aug 18 2021 at 20:29):

Make sure your Lean project depends on mathlib and add the line `import data.nat.prime`

at the top of your file.

#### Patrick Massot (Aug 18 2021 at 20:30):

Which online tutorial are you talking about?

#### Lucas (Aug 18 2021 at 20:31):

I'm going to look at what Bryan mentioned, I didn't know you needed this extra setup. Thanks for the help!

#### Lucas (Aug 18 2021 at 20:32):

Also, it was on youtube tutorials, lean for the curious mathematician

#### Lucas (Aug 18 2021 at 20:32):

they gave the example of proving the infinitude of primes

#### Patrick Massot (Aug 18 2021 at 20:34):

The videos are unfortunately impossible to keep updated. However you can download an updated version of all the Lean files from those lectures as described here.

#### Lucas (Aug 18 2021 at 20:35):

are they already outdated?

#### Patrick Massot (Aug 18 2021 at 20:37):

Anything about Lean + mathlib which is more than one day old is outdated: https://leanprover-community.github.io/mathlib_stats.html

#### Patrick Massot (Aug 18 2021 at 20:37):

You can still learn a lot from those talks, but you can't expect the details to be accurate.

#### Lucas (Aug 18 2021 at 20:40):

alright, good to know for the future

#### Ayush Agrawal (Sep 30 2021 at 19:33):

Hi guys! I have recently started exploring Lean. I am not able to access the Natural Number Game link today. Few days ago it was just working fine. (https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/ ) . Can anyone advise please?

#### Horatiu Cheval (Sep 30 2021 at 19:42):

The issue is also being discussed in this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/natural.20numbers.20game

#### Kevin Buzzard (Sep 30 2021 at 22:21):

I don't know what's going on. I've opened a ticket with the people who maintain the site but I've not heard back from them

#### Galen Selligman (Jul 22 2022 at 15:05):

I found the natural number game recently and I am still working on finishing it, but I am getting an error with the website.

"403 Forbidden

You don't have permission to access this resource."

#### Kalle Kytölä (Jul 22 2022 at 15:22):

The NNG is also available at <https://cbirkbeck.github.io/natural_number_game/> .

#### Kevin Buzzard (Jul 22 2022 at 19:36):

Thanks. I've put in the usual complaint. Basically all of www.ma.imperial.ac.uk is down right now and the issue is that there are some people high up in the system who would like it to be down always.

#### King Crawford (Aug 27 2022 at 16:26):

Hello, I've been really enjoying the Natural Number Game for the past few days. I was wondering if there is a way to solve Advanced Proposition world lvl 10 using tactics in a way that might be more intuitive to someone who might approach the proof "by hand" like this:

lemma contrapositive2 (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := sorry

assume (¬ Q → ¬ P):

__assume P:

____assume ¬ Q:

______¬ P

____ ¬¬ Q

____Q

__P → Q

(¬ Q → ¬ P) → (P → Q)

Thanks!

#### Junyan Xu (Aug 27 2022 at 17:37):

Maybe this is close enough?

```
intro nqinp,
intro p,
by_contra nq,
have np := nqinp nq,
exact np p,
```

#### King Crawford (Aug 27 2022 at 17:41):

This is exactly what I was looking for. Appreciate it!

#### Arien Malec (Sep 11 2022 at 15:37):

I'm working through NNG and stuck on `eq_zero_or_eq_zero_of_mul_eq_zero`

.

I have

```
case mynat.succ
a c : mynat,
hd : a * c = 0 → a = 0 ∨ c = 0,
h : a * succ c = 0
⊢ a = 0 ∨ succ c = 0
```

which gets me `a=0`

either through `succ_ne_zero`

(assume right, leads to contradiction), or more directly by rewriting via `mul_succ`

then `add_left_eq_zero`

which gets me the left branch.

But the latter rewrite fails due to "metavariable" issues, and I don't now how to get Lean to assume right.... I guess I could also get there through `hd`

applied to `h`

, but that also fails due to "metavariable" issues...

#### Ruben Van de Velde (Sep 11 2022 at 16:37):

Do you need to generalise `c`

?

#### Ruben Van de Velde (Sep 11 2022 at 16:40):

Because the goal doesn't seem provable from your induction hypothesis

#### Kevin Buzzard (Sep 11 2022 at 16:50):

Right now your inductive hypothesis `hd`

is unusable because it needs as input a proof that `a*c=0`

and you only have a hypothesis that `a*(c+1)=0`

.

#### Arien Malec (Sep 11 2022 at 18:25):

the issue is the same if I use `cases`

-- agree that `hd`

doesn't do much here. (If I understand the logic of cases, it splits the proof into a proof for zero `n`

and a proof for non-zero (`succ n`

) at which point I should be done with the disjunction but I can't tell that to Lean. With `cases`

I get to:

```
case mynat.succ
a c : mynat,
h : a * succ c = 0
⊢ a = 0 ∨ succ c = 0
```

and since I know `succ_ne_zero`

I should be done.

#### Kevin Buzzard (Sep 11 2022 at 18:26):

No you're not at all done -- all you've managed to do is to reduce the question to the question you started with!

#### Kevin Buzzard (Sep 11 2022 at 18:27):

Or maybe I'm not understanding your logic. Sure you know `succ c \ne 0`

. But how do you deduce a = 0 without assuming the thing you're supposed to be proving?

#### Kevin Buzzard (Sep 11 2022 at 18:28):

Maybe you can show me an explicit example of the "metavariable" issues? Can you post some code which you think should work and doesn't?

#### Arien Malec (Sep 11 2022 at 18:36):

here are the moves that get the metavariable issue -- from the above:

```
rw mul_succ at h,
rw add_left_eq_zero at h,
```

```
rewrite tactic failed, lemma lhs is a metavariable
state:
case mynat.succ
a c : mynat,
h : a * c + a = 0
⊢ a = 0 ∨ succ c = 0
```

There's an implicit assumption that `a*c`

: `mynat`

...

#### Arien Malec (Sep 11 2022 at 18:44):

yeesh I got it with `left`

+ `exact add_left_eq_zero h`

#### Kevin Buzzard (Sep 11 2022 at 18:45):

Nice! Sorry, I'm just doing several other things at the same time. Let me try and figure out the error

#### Kevin Buzzard (Sep 11 2022 at 18:46):

#### Kevin Buzzard (Sep 11 2022 at 18:47):

OK after firing up NNG it appears that `add_left_eq_zero : a + b = 0 -> b = 0`

#### Kevin Buzzard (Sep 11 2022 at 18:49):

so your error about metavariables is a very unhelpful error message which should instead say "hey! You cannot `rw add_left_eq_zero`

because `rw X`

*only* works for lemmas `X`

which are of the form `P = Q`

or `P <-> Q`

"

#### Kevin Buzzard (Sep 11 2022 at 18:50):

In fact `add_left_eq_zero`

is a *function* which eats as input a proof that `X + Y = 0`

for some X and Y, and returns a proof that `Y = 0`

.

#### Kevin Buzzard (Sep 11 2022 at 18:51):

And indeed `exact add_left_eq_zero h`

works because this means "feed `h`

into the `add_left_eq_zero`

function and the goal is exactly the output". Sorry about the obscure error messages but hopefully that explains your problem!

#### Kevin Buzzard (Sep 11 2022 at 18:51):

I also now understand that the inductive hypo was irrelevant -- I had imagined that one needed to do this by induction but as you point out you don't need the inductive hypothesis at all! It's been a while since I played through the game :-)

#### Arien Malec (Sep 11 2022 at 20:55):

super helpful! Bitten by the rw vs apply conceptual issue.

#### Arien Malec (Sep 14 2022 at 15:54):

Another issue here with inequality level 14 (`add_le_add_left`

).

My first thought was that `t + a ≤ t + b`

is just `a + t ≤ b + t`

by commutativity, but there's a quantification issue with how `add_le_add_right`

is defined relative to `add_le_add_left`

. Signature of right is `{a b : mynat} : a ≤ b → ∀ t, (a + t) ≤ (b + t)`

and left is `add_le_add_left {a b : mynat} (h : a ≤ b) (t : mynat) : t + a ≤ t + b`

which leads to an error:

```
invalid type ascription, term has type
∀ (t : mynat), a + t ≤ b + t
but is expected to have type
t + a ≤ t + b
```

Is there a trick to address the quantification mismatch?

#### Arien Malec (Sep 14 2022 at 15:56):

Oh nevermind, `add_comm`

applied to wrong side & I didn't read the error message well enough. :flushed:

#### Arien Malec (Sep 14 2022 at 15:57):

But once I fixed that bonehead error, I still have the type error:

```
invalid type ascription, term has type
∀ (t : mynat), a + t ≤ b + t
but is expected to have type
a + t ≤ b + t
```

#### Ruben Van de Velde (Sep 14 2022 at 16:06):

Something like this?

```
rw [add_comm t a, add_comm t b],
exact add_le_add_right h t,
```

#### Ryan Duan (Sep 14 2022 at 16:49):

Quck question, how would this expression be simplified |x - y + z| + w ^ 2 ≤ 10 + 5 + 4 + 3 ^ 2? I've tried combinations of abs_sub/abs_add and it always says it cannot find expressions of type |a+b| to get the inequality of <= |a| + |b| or something of that sort. and le_trans doesn't do anything

#### Ruben Van de Velde (Sep 14 2022 at 16:51):

Probably you need the fact that a \le b and c \le d implies a+c \le b+d

#### Ryan Duan (Sep 14 2022 at 16:57):

I see, there's no way to just evaluate away an abs value expression with three elements with just abs_sub/add?

#### Arien Malec (Sep 14 2022 at 17:12):

adding `t`

as a parameter worked -- collapses `∀ t`

to my `t : mynat`

?

#### Arien Malec (Sep 14 2022 at 17:15):

It now occurs to me that Lean does currying...

#### Ruben Van de Velde (Sep 14 2022 at 17:25):

Yeah, that's right

#### Alex J. Best (Sep 14 2022 at 17:32):

@Ryan Duan if you ask your question in a new thread it'll be much clearer whats going on here. Also check out the #mwe guide, this will make your questions easier to answer

#### Arien Malec (Sep 14 2022 at 23:30):

As feedback to the NNG maintainers, the biggest issues in NNG were often the syntax of function calls - when I can call `foo_bar_baz h`

and when I have to call `foo_bar_baz a b h`

, etc., as well as the mental table I had to construct of when I have to `cases h`

vs `split`

vs etc. depending on if I'm in hypothesis space or goal space, etc.

If I hadn't "cheated" and found some examples of how to do all this stuff, I'd still be in a maze working through `mul_left_cancel`

...)

#### Arien Malec (Sep 14 2022 at 23:35):

But generally kudos -- have been interested in this space since I discovered OCaml and heard about this thing called Coq, but getting my arms around what automated theory provers did and how they worked was a bit overwhelming. NNG is an amazing intro to the curious computer scientist.

#### Kevin Buzzard (Sep 15 2022 at 07:04):

Yeah I definitely could have said something about implicit and explicit inputs to functions. If you look at the type of a function, the inputs it can implicitly infer are those in `{}`

brackets, but I'm not sure this is ever explicitly mentioned

#### Alberto Navarro Garmendia (Sep 19 2022 at 11:52):

Advanced Addition world level 1/13 It says 'You should know a couple of ways to prove the below -- one directly using an exact' But I don't see how to prove directly and it without using apply. Any suggestion? Thanks!

#### Riccardo Brasca (Sep 19 2022 at 11:54):

If you can prove something in one line using `apply`

you should be able to prove the same using `exact`

, using the same lemma. The difference is that with `exact`

you can specify all the arguments, that are "guessed" by Lean using `apply`

. (You can also just use `_`

as an argument.)

#### Kevin Buzzard (Sep 19 2022 at 12:15):

#### Alberto Navarro Garmendia (Sep 20 2022 at 11:26):

Advanced Addition World, level 8/13. Typing

```
intro h,
rw ← add_left_cancel a b 0,
```

produces two goals. Why??

Second question: it is a little weird to always work *backwards*. For example, here, after `intro h`

the goal is `b=0`

while the hypothesis is `h:a+b=a`

. The way to think *forward* would be that somehow `add_zero`

should produce somehow `p: a+b=a+0`

and `add_left_cancel`

should produce `q:b=0`

. Is there a way to do so?

Thanks in advance

#### Kevin Buzzard (Sep 20 2022 at 11:39):

`add_left_cancel a b 0`

has type `a + b = a + 0 -> b = 0`

. This is not an equality or an iff statement, so you cannot rewrite it. You attempt to use the `rw`

tactic anyway, so Lean has to make a decision about what you could mean, and it decides that probably you're going to give a proof of `a + b = a + 0`

later on (and creates this as a new goal) and then it tries to rewrite the new conclusion `b = 0`

(which *is* an equality, so is rewritable) backwards, so it changes the 0 to a `b`

giving you the first goal you see.

#### Kevin Buzzard (Sep 20 2022 at 11:43):

Sure you can argue forwards in Lean, using repeated `have`

statements, but it almost always takes longer. Here's a Lean version of your sketch proof:

```
intro h,
have h2 : a + b = a + 0,
rw add_zero,
exact h,
exact add_left_cancel _ _ _ h2,
```

#### Kevin Buzzard (Sep 20 2022 at 11:49):

The general structure of a formal proof is that you have multiple hypotheses but only one goal. The hypotheses tend to stick around, even when you've finished with them. The goal is fluid, it can change during a proof, and previous goals can be thrown away as the proof moves on. If you want to argue via "we know this stuff, so we can deduce this, and now we can deduce this, and now this, and now we're done" then you are constantly adding to the list of hypotheses. If you are instead arguing backwards, saying "reduce the problem to this, and then to this, and then to this, and now we're done" then you don't have to keep adding hypotheses to the local context and you can throw away previous goals. So from the point of view of formalisation it's less clutter.

Under the hood, a proof is a function. What a tactic proof is really doing is building that function in an extremely flexible way, adding in parts of the function in funny places and leaving "holes" which become new goals. Thought of in this way, a forwards ("normal for mathematician") proof can be thought of as building other functions along the way which you plug into the definition of the function you actually want. Arguing backwards is building the function you actually want directly, by building the "end part" of it first (you build a function from A to C by directly plugging in the function from B to C and reducing the question to building the function from A to B -- this is the `apply`

tactic). If instead you want to build the function from A to B first, you can't plug it in directly, you need to give it a new name and then apply it to the input (a term of type A) to get the term of type B which as mathematicians we're trained to think we want to have.

#### Will Midwood (Sep 20 2022 at 14:49):

Advanced Multiplication World 4/4. Hi all, I'm not too sure how to solve the first goal of this proof:

```
a : mynat,
ha : a ≠ 0,
b : mynat
⊢ a * b = 0 → b = 0
```

I assume the use of `eq_zero_or_eq_zero_of_mul_eq_zero`

or `mul_eq_zero_iff`

is necassary but I'm unsure what tactics I can use with them. Thanks!

#### Kevin Buzzard (Sep 20 2022 at 15:16):

If you `intro hab`

then you'll be able to feed `hab`

into `eq_zero_or_eq_zero_of_mul_eq_zero`

and you'll be able to `rw mul_eq_zero_iff at hab`

.

#### Alberto Navarro Garmendia (Sep 21 2022 at 10:51):

Multiplication World 1/13: Question about syntaxis . Writing

```
induction m on n,
exact mul_zero 0,
rw mul_succ,
rw m_ih,
rw zero_add,
refl,
```

Lean says "no goals" but no "Proof complete!" The console writes

```
60:12: error:
invalid 'begin-end' expression, ',' expected
61:0: error:
sync
```

I usually find that several times Lean says 'no goals`but no `

Proof complete!`. Usually, when this happens I erase and write again the last line few times until it says `

Proof complete!`, but this time it does not work. Surely I am writing something wrong, but I don't see it...

Thanks in advance.

#### Anne Baanen (Sep 21 2022 at 11:06):

Pro-tip: you can surround a longer quotation by three #backticks on their own line

#### Anne Baanen (Sep 21 2022 at 11:07):

The error you're encountering means there's some syntax error like forgetting to close a parenthesis but I don't see any in your code...

#### Ruben Van de Velde (Sep 21 2022 at 11:48):

I see `induction m on n`

, which is not valid syntax

#### Alberto Navarro Garmendia (Sep 21 2022 at 12:33):

Ruben Van de Velde ha dicho:

I see

`induction m on n`

, which is not valid syntax

Thanx a lot, that was it. Although it is surprising, while using `induction m on n`

doesn't display any error at that moment and the proof goes all the way correctly (only that it does not say `Proof complete`

at the end). Now, with `induction m with n`

every step works the same, except the final one wich says `Proof complete `

. Anyway. Thank you very much!

#### Will Midwood (Sep 22 2022 at 14:06):

Me again, struggling with Advanced Multiplication world Level 4/4 again, I'm just not sure how to proceed? Here is my Goal

```
case mynat.succ
a : mynat,
ha : a ≠ 0,
d : mynat,
hd : ∀ (b : mynat), a * b = a * d → b = d,
b : mynat,
h : a * b = a * succ d
⊢ b = succ d
```

I'm not sure if I should be manipulating the hypotheses or the goal or if I need to retry my tactics. Any help would be much appreciated!

#### Will Midwood (Sep 22 2022 at 14:07):

I tried `cases a with n`

but couldn't get anything more solvable

#### Arien Malec (Sep 22 2022 at 16:32):

Alberto Navarro Garmendia said:

```
I usually find that several times Lean says ```no goals``` but no ```Proof complete!```. Usually, when this happens I erase and write again the last line few times until it says ```Proof complete!``` , but this time it does not work. Surely I am writing something wrong, but I don't see it...
```

I didn't see a reply here -- when I was doing NNG, adding a newline after the last line in the proof usually triggered the transition between `no goals`

and `Proof complete!`

.

#### Alberto Navarro Garmendia (Sep 22 2022 at 17:01):

Two questions:

First: I am having troubles with the syntaxis of `add_left_equal_zero`

, `eq_zero_or_eq_zero_of_mul_eq_zero`

and similar statements.

More concretely, let `p: 0=succ a * succ b `

. I want to produce `q : succ a =0 ∨ succ b =0 `

out of `p`

, but I fail to do so. The command `have q:= eq_zero_or_eq_zero_of_mul_eq_zero (p)`

does not work.

Second, very stupid: is there a quick command to switch `p: P=Q`

into some `q:Q=P`

, where `P`

and `Q`

are different expressions?

Thanks in advance.

#### Ruben Van de Velde (Sep 22 2022 at 17:22):

2/ `rw eq_comm at p`

or `have q := p.symm`

#### Ruben Van de Velde (Sep 22 2022 at 17:22):

1/ what's the error?

#### Kevin Buzzard (Sep 22 2022 at 19:55):

Will Midwood said:

Me again, struggling with Advanced Multiplication world Level 4/4 again, I'm just not sure how to proceed? Here is my Goal

`case mynat.succ a : mynat, ha : a ≠ 0, d : mynat, hd : ∀ (b : mynat), a * b = a * d → b = d, b : mynat, h : a * b = a * succ d ⊢ b = succ d`

I'm not sure if I should be manipulating the hypotheses or the goal or if I need to retry my tactics. Any help would be much appreciated!

Do you know the maths proof from where you have got to, to the goal, or are you just kind of trying things at random? Before embarking on this Lean proof you might want to plan your route on paper.

#### Alberto Navarro Garmendia (Sep 22 2022 at 23:10):

Ruben Van de Velde ha dicho:

1/ what's the error?

The console sais

```
type mismatch at application
eq_zero_or_eq_zero_of_mul_eq_zero p
term
p
has type
0 = succ a * succ c_n : Prop
but is expected to have type
mynat : Type
```

Note that `p: 0=succ a * succ c_n `

because i was inside an induction.

#### Will Midwood (Sep 23 2022 at 09:48):

Kevin Buzzard said:

Do you know the maths proof from where you have got to, to the goal, or are you just kind of trying things at random? Before embarking on this Lean proof you might want to plan your route on paper.

You make an excellent point. Without the use of division I actually do not not how to prove this statement from here anyways. I guess back to the drawing board!

#### Kevin Buzzard (Sep 23 2022 at 11:28):

I'm not "being cruel" not giving you access to division -- you don't get to division until you've built the rationals and to build the rationals you need all the theorems about naturals first!

#### Kevin Buzzard (Sep 23 2022 at 11:30):

Alberto Navarro Garmendia said:

Ruben Van de Velde ha dicho:

1/ what's the error?

I solved the problem. For the sake of completeness: the console said

`type mismatch at application eq_zero_or_eq_zero_of_mul_eq_zero p term p has type 0 = succ a * succ c_n : Prop but is expected to have type mynat : Type`

Right -- so `eq_zero_or_eq_zero_of_mul_eq_zero`

seems to want to eat a natural number next, not `p`

. You could try `eq_zero_or_eq_zero_of_mul_eq_zero _ _ p`

or something (the number of `_`

s is the number of natural numbers which you don't want to give but which the system wants before `p`

).

#### Arien Malec (Sep 24 2022 at 00:20):

Kevin Buzzard said:

I'm not "being cruel" not giving you access to division -- you don't get to division until you've built the rationals and to build the rationals you need all the theorems about naturals first!

I'm getting a bit nerdsniped by what we are actually proving --- something like the natural numbers under multiplication are a cancellable semigroup?

Is there a way in Lean to do induction starting at a different base case? The paper outline of the proof here is far easier if we can start `a`

with 1, which is sort of what my now rewritten proof does, just inside out... (induction over `b`

then sorta induction by `case`

over `c`

).

#### Newell Jensen (Sep 24 2022 at 00:22):

Arien Malec said:

Is there a way in Lean to do induction starting at a different base case? The paper outline of the proof here is far easier if we can start

`a`

with 1, which is sort of what my now rewritten proof does, just inside out... (induction over`b`

then sorta induction by`case`

over`c`

).

#### Newell Jensen (Sep 24 2022 at 00:22):

but you probably don't have access to that in the game...not sure

#### Kyle Miller (Sep 24 2022 at 00:53):

@Arien Malec If you want to start at `1`

without additional library lemmas, you can do `cases a, { ... proof for 0 ... }, induction a`

#### Arien Malec (Sep 24 2022 at 03:04):

Kyle Miller said:

Arien Malec If you want to start at

`1`

without additional library lemmas, you can do`cases a, { ... proof for 0 ... }, induction a`

Sadly I think that leads to a dead end...

#### Kevin Buzzard (Sep 24 2022 at 08:23):

No that's exactly the right way to do induction on a>=1.

#### Arien Malec (Sep 24 2022 at 15:36):

Kevin Buzzard said:

No that's exactly the right way to do induction on a>=1.

It works, but it's not shorter, simpler or easier to understand than the original proof...

#### Alberto Navarro Garmendia (Sep 28 2022 at 08:50):

I have a syntaxis doubt. Having `h : a * c + a = a * d + a `

and the goal being `a * c = a * d `

my question is: why does `apply add_right_cancel _ _ _ h, `

solves the goal?

As far as I know, the `apply`

tactic with `add_right_cancel _ a _ `

transforms the goal precisely into ` a * c + a = a * d + a `

, Why can I just simply write h after the apply tactic in the same line? I don't understand the syntaxis and the description of the apply tactic does not explain this use.

Thanks in advance.

#### Johan Commelin (Sep 28 2022 at 09:11):

@Alberto Navarro Garmendia docs#add_right_cancel is a function that takes (some elements and) a proof that `X + a = Y + a`

and returns a proof that `X = Y`

.

So you can either

`apply add_right_cancel`

which will require you to provide`h`

afterwards. In particular that is the new goal that you are seeing; or`apply (add_right_cancel _ _ _ h)`

which applies the function immediately to`h`

and closes the goal with the resulting proof of`X = Y`

. (I added the parentheses after the`apply`

for some clarity. They aren't needed.)

#### Alberto Navarro Garmendia (Sep 28 2022 at 09:23):

Thanks @Johan Commelin I see .

I still have a doubt: it seems to me that the `apply`

tactic can also work on hypothesis, not only on the goal as I learnt. More concretely, If I understand correctly, having a theorem (let's denote it theorem_1) saying `P → Q`

and having `p : P`

then `apply (theorem_1 p)`

would solve a goal `Q`

. But, , is there a way to simply get `q : Q`

out of `apply (Theorem_1 p)`

or a similar syntaxis? Thanks in advance

#### Johan Commelin (Sep 28 2022 at 09:24):

You could do

```
have q : Q := theorem_1 p
-- or
apply_fun theorem_1 at p
```

#### Johan Commelin (Sep 28 2022 at 09:25):

Probably `apply_fun`

is closest to what you want. But the downside is that it doesn't update the name. So now you will suddenly have `p : Q`

, which looks a bit odd.

#### Ruizhe Wan (Oct 08 2022 at 21:54):

I am currently trying to use the add_left_cancel theorem to get from h2 to the goal, it says that the type of h2 should be mynat instead of Prop, which I think is problematic? I have also tried to just repeat again the proofs of all the theorems I need, but at the end I could not use induction on (a * d), so this doesn't work either, does anyone have some hint of it?

SharedScreenshot.jpg

#### Kevin Buzzard (Oct 08 2022 at 21:56):

The reason is that `add_left_cancel`

wants to eat three numbers before it eats `h2`

. You can see on the left it says `add_left_cancel (t a b : mynat) : ...`

, which means "I want to eat t, a and b, before I eat the proof that t+a=t+b and then I'll spit out the proof that a = b". You can probably write `have h3 := add_left_cancel _ _ _ h2`

.

#### Ruizhe Wan (Oct 08 2022 at 22:01):

It still doesn't seem to work, and I have also tried writing explicitly (a * d) 0 a out, but there is still error SharedScreenshot.jpg

#### Ruben Van de Velde (Oct 08 2022 at 22:04):

You've got two `d`

s

#### Ruizhe Wan (Oct 08 2022 at 22:06):

Oh I see, I will try to fix that. Thanks a lot.

#### Kevin Buzzard (Oct 08 2022 at 22:49):

Yeah, sorry the error message is confusing, the reason it's talking about d and d_1 is that you've called two things d

#### Mike Shulman (Oct 08 2022 at 23:28):

Did you consider making the infix notations `+`

and `*`

nonassociative in the NNG? I have some students working through it as part of a class in formalization, and they frequently have trouble remembering that `a + b + c`

actually means `(a + b) + c`

. (To be honest, I have trouble remembering that myself!)

#### Mario Carneiro (Oct 09 2022 at 00:28):

I don't think lean 3 supports nonassociative operators

#### Mario Carneiro (Oct 09 2022 at 00:28):

actually that's not true, you can do it with `notation`

if you set all the precedences manually

#### Kevin Buzzard (Oct 09 2022 at 00:43):

@Mike Shulman (btw you seem to have two active accounts here which makes you harder to @) I agree that the lack of brackets causes confusion. I think @Kyle Miller made some pp.bracket option which you can now switch on to see where they are. At the time people convinced me that it was important to learn lean's conventions for associativity and I didn't know anything about how to make the brackets appear so I just went with what we have

#### Mike Shulman (Oct 09 2022 at 01:50):

(Huh, I had no idea I had a second account. I wonder how that happened, let's see if I can delete it.)

#### Mike Shulman (Oct 09 2022 at 01:52):

Is there an important reason to use Lean's `has_add`

? In another proof assistant I would just declare `+`

directly to be an infix notation without associativity. I presume that going through `has_add`

forces you to use the same associativity as all other "add"s in the library.

#### Mario Carneiro (Oct 09 2022 at 02:00):

You can do that, but you either have to shadow the original notation (meaning that your new add can't be used along with the old one), or you have to use lean's type-based disambiguation mechanism which is largely avoided in mathlib because it doesn't play well with typeclasses

#### Mario Carneiro (Oct 09 2022 at 02:00):

for teaching purposes the former approach is often reasonable

#### Mike Shulman (Oct 09 2022 at 02:52):

Personally, I almost wish proof assistants would *always* include the brackets. I can never remember the default associativity of any binary operation and am always failing to rewrite because I got it wrong.

#### Mike Shulman (Oct 09 2022 at 02:57):

Mario Carneiro said:

I don't think lean 3 supports nonassociative operators

I would be very disappointed in any proof assistant that doesn't support nonassociative operators. I can think of oodles of infix binary operators that I think should be nonassociative, starting with `=`

.

#### Mike Shulman (Oct 09 2022 at 03:02):

I see that in Lean 3, `=`

is left-associative.

```
variables x y : ℕ
variable P : Prop
#check x = y = P
```

Ugh.

#### Mario Carneiro (Oct 09 2022 at 03:50):

lean 4 has nonassociative operators, although I'm not so sure about using them because I noticed that the parse failure can sometimes trigger a surprising fallback behavior

#### Mario Carneiro (Oct 09 2022 at 03:52):

The way to write them in lean 3 is `notation:p x:p+1 `foo` y:p+1 := foo x y`

for some choice of `p`

#### Mike Shulman (Oct 09 2022 at 05:43):

How do I parse that?

#### Kevin Buzzard (Oct 09 2022 at 09:03):

@Mike Shulman you can just hover over a + or any other infix operator in the infoview to see how it's associating, you have instant visual feedback in VS Code

#### Jeremy Avigad (Oct 09 2022 at 16:33):

@Mike Shulman You can tell Lean to print parentheses always:`set_option pp.parens true`

.

#### Mike Shulman (Oct 11 2022 at 08:59):

Kevin Buzzard said:

Mike Shulman you can just hover over a + or any other infix operator in the infoview to see how it's associating, you have instant visual feedback in VS Code

When I hover over `+`

I see

```
has_add.add : Π {α : Type} [self : has_add α], α → α → α
```

#### Patrick Massot (Oct 11 2022 at 09:00):

He means in the info view.

#### Patrick Massot (Oct 11 2022 at 09:02):

#### Patrick Massot (Oct 11 2022 at 09:03):

Observe how part of the expression turns blue, indicating that addition is left-associative.

#### Mike Shulman (Oct 11 2022 at 09:14):

My infoview doesn't do that.

#### Patrick Massot (Oct 11 2022 at 09:36):

That's probably because the natural number game uses an ancient version of Lean and mathlib.

#### Patrick Massot (Oct 11 2022 at 09:36):

At least you know that when working on a real project you won't have this issue.

#### Mike Shulman (Oct 11 2022 at 09:37):

I'm not talking about the NNG now, I actually have vs code running locally.

#### Mike Shulman (Oct 11 2022 at 09:51):

(Although I would much prefer to use Emacs...)

#### Johan Commelin (Oct 11 2022 at 10:29):

@Mike Shulman Which version of the Lean extension do you have in VScode?

#### Johan Commelin (Oct 11 2022 at 10:29):

And which version of Lean are you running in that project? `#eval lean.version`

#### Mike Shulman (Oct 11 2022 at 10:31):

Lean extension is 0.16.55, Lean version is `(3, (46, 0))`

.

#### Johan Commelin (Oct 11 2022 at 10:31):

Ooh, maybe you need something like `import tactic`

at the top? I'm just guessing.

#### Johan Commelin (Oct 11 2022 at 10:32):

Because those version numbers seem pretty up to date

#### Johan Commelin (Oct 11 2022 at 10:32):

I don't know exactly which part of mathlib you need to import to make the widget stuff work...

#### Mike Shulman (Oct 11 2022 at 10:33):

At the moment I'm not using any of mathlib.

#### Johan Commelin (Oct 11 2022 at 10:34):

Understood. I'm afraid it might not work without mathlib.

#### Mike Shulman (Oct 11 2022 at 10:34):

The libraries that I import in my code can affect what sort of information my editor can display?

#### Mike Shulman (Oct 11 2022 at 10:34):

That seems like a weird sort of level-mixing.

#### Johan Commelin (Oct 11 2022 at 10:35):

Sure, if you import a library about Young tableaus, you might want to explain to your editor how to display them.

#### Johan Commelin (Oct 11 2022 at 10:35):

Or if you setup category theory, you might want to implement a widget for diagram chasing.

#### Mike Shulman (Oct 11 2022 at 10:36):

Sure, but those are domain-specific. Bracketing is something that applies to all infix operators in the world.

#### Alex J. Best (Oct 11 2022 at 10:36):

https://leanprover-community.github.io/mathlib_docs/tactic/interactive_expr.html#widgets-used-for-tactic-state-and-term-mode-goal-display is the relevant file I believe.

#### Alex J. Best (Oct 11 2022 at 10:37):

The default tactic state is pure text, the widgets override it with the additional nested expression information

#### Alex J. Best (Oct 11 2022 at 10:37):

One could definitely make the argument that this should be in core now though!

#### Johan Commelin (Oct 11 2022 at 10:37):

Mike Shulman said:

Sure, but those are domain-specific. Bracketing is something that applies to all infix operators in the world.

Agreed. So you would expect it to be implemented in the standard library. But in the case of Lean 3, by historical accident, mathlib is the standard library. In Lean 4 this will all be done with more modular packages.

#### Alex J. Best (Oct 11 2022 at 10:38):

Seeing as that file imports none of mathlib, you could simply copy it to your project I guess

#### Patrick Massot (Oct 11 2022 at 11:12):

Yes, https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive_expr.lean is the file that Mike wants. It is extremely convenient to be able to override what is that file, and I use this possibility in my teaching or in the sphere eversion project. But indeed the basic version could be in the core library now that is stabilized (in the beginning it was convenient to have that file in mathlib for fast iteration).

#### Adam Kurkiewicz (Aug 03 2023 at 10:19):

(deleted)

#### Adam Kurkiewicz (Aug 03 2023 at 10:36):

Hi all,

I'm playing through Kevin's Natural Number game. In the advanced addition world, level 1 introduces

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

I just wanted to clarify, that this is just a trick to make things more understandable, right? It is not in any way an additional axiom that needs to be defined to get natural numbers to work?

In practice the foundation of lean is sufficiently smart to actually prove that "axiom" from the definition of natural numbers as an inductive type?

I've checked in the standard library, and there is a proof of this here:

https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean#L1504

It uses reflexivity to prove this.

So if I decided to define my own natural numbers in a separate file, I could just prove the `succ_inj`

from the reflexivity skipping the "intermediate" Bool type?

#### Zach Battleman (Aug 03 2023 at 10:49):

Yep! That’s all exactly right. I can’t remember if you prove it in NNG, but succ_inj is a theorem that you get access to. You can prove it directly from the inductive definition of the natural numbers.

The theorem you pointed out in the Lean Prelude is not succ inj. That theorem is saying that for natural numbers, Boolean equality implies propositional equality.

The theorem succ_inj can be found here https://github.com/leanprover/std4/blob/e3c2be331da9ddeef7f82ca363f072a68d7210b3/Std/Data/Nat/Lemmas.lean#L123-L124

#### Riccardo Brasca (Aug 03 2023 at 10:51):

It's indeed not a new axiom. You can try to prove it yourself, and see if you need `bool`

, or something else!

#### Riccardo Brasca (Aug 03 2023 at 10:51):

You can start by proving that 1 is different from 0

#### Adam Kurkiewicz (Aug 03 2023 at 11:35):

Thanks @Zach Battleman and @Riccardo Brasca

So, I've been able to prove this (not really, chatGPT was able to prove this), like this:

```
inductive xnat : Type
| zero : xnat
| succ : xnat -> xnat
theorem inj_succ (n m : xnat) (h : n.succ = m.succ) : n = m :=
by
injection h
```

I don't really know what the `injection`

tactic does, so still a bit of magic, but it works :). I think I will re-read the Inductive Types chapter in Proving Theorems with Lean 4 book, and this should be able to help me provide a proof by directly constructing the term without using tactics.

#### Kevin Buzzard (Aug 03 2023 at 11:39):

I think the nicest proof of this is to define `pred`

recursively (with `pred 0 = 37`

)), prove `pred (succ n) = n`

and then apply `pred`

to `h`

.

I think it's interesting that in Peano's original work he added `succ_inj`

and `succ_ne_zero`

as axioms but in Lean's type theory they can both be proved, however in both cases the proof involves recursion not induction.

#### Riccardo Brasca (Aug 03 2023 at 11:41):

Well, `injection`

essentially already knows the result, so it's not really useful if you want to understand how this is proved. I really suggest you to do it by yourself (without asking to ChatGPT). Do you have a mathematical proof?

#### Adam Kurkiewicz (Aug 03 2023 at 12:17):

@Riccardo Brasca , started working on the non-formal proof. I'm getting stuck in the first inductive step -- it's kind of hard to do that without having access to the "Lean Infoview" box:

By induction on n:

Base case n = 0:

succ(0) = succ(m) => 0 = m

1 = m + 1 => 0 = m

By induction on m:

Base case m = 0:

1 = 0 + 1 => 0 = 0, by reflexivity

Inductive case:

h: 1 = m_d + 1 => 0 = m_d

goal: 1 = succ(m_d) + 1 => 0 = succ(m_d)

#### Adam Kurkiewicz (Aug 03 2023 at 12:18):

I realised, I will probably need `eq_implies_succ_eq`

, which is luckily easy to prove:

```
theorem eq_implies_succ_eq (n m : xnat) (h : n = m) : xnat.succ n = xnat.succ m :=
by
rw [h]
```

#### Riccardo Brasca (Aug 03 2023 at 12:18):

Why can't you use the infoview?

#### Kevin Buzzard (Aug 03 2023 at 12:18):

As I already said, I am not sure if you can do these by induction; I think you need recursion. I might be wrong.

#### Riccardo Brasca (Aug 03 2023 at 12:19):

But, as Kevin is saying, have you a math proof?

#### Riccardo Brasca (Aug 03 2023 at 12:19):

These questions are both trivial and tricky at the same time, since we usually don't think we need to prove them.

#### Adam Kurkiewicz (Aug 03 2023 at 12:21):

I'm getting stuck in the informal math proof -- message above is the attempt.

#### Adam Kurkiewicz (Aug 03 2023 at 12:21):

Proving that 1 != 0 is easy and I think I understand it -- it should flow directly from the type system like this:

```
theorem one_neq_zero : xnat.zero ≠ xnat.succ xnat.zero :=
xnat.noConfusion
```

#### Adam Kurkiewicz (Aug 03 2023 at 12:22):

Kevin has a blog post about this here

#### Adam Kurkiewicz (Aug 03 2023 at 12:23):

@Kevin Buzzard I think I will re-read the Inductive Types chapter in Proving Theorems with Lean 4 book, and construct a proof term using xnat.recOn -- that should work, right?

#### Riccardo Brasca (Aug 03 2023 at 12:24):

Yes, but again, in this way you're using something it seems you don't understand completely. `noConfusion`

is no magic, it is just a theorem autogenerated by Lean, but it has it's own proof of course. I suggest to prove ` 0 \neq 1`

without any tactics or built in results, and you will probably understand things mich better.

#### Riccardo Brasca (Aug 03 2023 at 12:27):

I am deliberately not giving hints, but if you want help I can of course suggest a strategy.

#### Adam Kurkiewicz (Aug 03 2023 at 12:38):

Yes, a hint would be great!

I somehow can't imagine there would be a simpler proof -- it seems like the kernel should be able to distinguish two terms as being equal or not if they are constructed explicitly. If they are equal, refl should be the only proof. If they are not equal, noConfusion should be the only proof. No?

#### Adam Kurkiewicz (Aug 03 2023 at 12:40):

I'm probably missing something @Riccardo Brasca -- any help would be greatly appreciated

#### Riccardo Brasca (Aug 03 2023 at 12:40):

The idea is the following: using `xnat.rec`

(that is the only axiom really added by Lean when you define a new type), you can define functions on `xnat`

by choosing (freely!) the value on `zero`

and on `n.succ`

(using the value on `n`

). Now, if `zero = zero.succ`

, than `f zero = f zero.succ`

for all `f`

...

#### Riccardo Brasca (Aug 03 2023 at 12:41):

Can you see a function that gives a contradiction?

#### Adam Kurkiewicz (Aug 03 2023 at 12:47):

Hmm, if we go with the obious f n = succ n, then we can get zero = succ(succ(zero)) -- that's not a contradiction though

#### Adam Kurkiewicz (Aug 03 2023 at 12:47):

I don't actually know what f should be

#### Riccardo Brasca (Aug 03 2023 at 13:05):

`f`

can take values everywhere! You need to find two "things" `a`

and `b`

such that you are able to prove that `a ≠ b`

, then you can define `f 0 = a`

and `f n.succ = b`

for all `n`

, and if `0 = 0.succ`

you get `a =b`

, that is a contradiction (I am just proving that `0 ≠ 1`

, the general version is similar).

#### Riccardo Brasca (Aug 03 2023 at 13:05):

So everything boils down to find a type `T`

and two terms `a b : T`

such that `a ≠ b`

is easy to prove.

#### Riccardo Brasca (Aug 03 2023 at 13:08):

This is where `Prop`

(or `Bool`

if you prefer) enters the story: we have two terms `True : Prop`

and `False : Prop`

, and the first step is to prove that `True ≠ False`

. You can have a try, it's a nice exercice!

#### Adam Kurkiewicz (Aug 03 2023 at 13:15):

So we're actually eliminating the equality?

#### Riccardo Brasca (Aug 03 2023 at 13:22):

I am not sure what you mean by that. We can prove, rather easily, that `True ≠ False`

, and then define `f : xnat → Prop`

such that `f zero = True`

and `f n.succ = False`

#### Riccardo Brasca (Aug 03 2023 at 13:31):

Here is a full proof of `0 ≠ 1`

.

Proof

#### Adam Kurkiewicz (Aug 03 2023 at 14:58):

Thank you Riccardo! This is very clever & satisfying.

One of the reasons I'm struggling is that the syntax between visual studio code (I'm using Lean 4) and Natural Numbers Game is quite different. E.g. There isn't a begin end block and rw needs square brackets.

Is there a version of natural numbers game in lean 4? Or is natural numbers game using its own set of custom tactics?

#### Adam Kurkiewicz (Aug 03 2023 at 14:59):

Let me see if I can delete the whole file and "reinvent" it from scratch in visual studio code.

#### Riccardo Brasca (Aug 03 2023 at 15:01):

This is because you are playing the lean3 version! Here is the Lean4 version

#### Kevin Buzzard (Aug 03 2023 at 15:14):

So Riccardo's proof of Peano's axiom 0 != succ(n) uses `f`

, which is a function defined by recursion. Similarly my proof of his other axiom `succ_inj`

uses `pred`

which is also defined by recursion. @Adam Kurkiewicz yes you can definitely use `xnat.recOn`

directly, it's just a more painful way to do it. I'm just making the point that you seem to need a recursor which will eliminate into `Type`

even though you're proving a Prop.

#### Adam Kurkiewicz (Aug 03 2023 at 17:07):

Thanks guys, I can reproduce this from scratch and mostly from memory. I will try again tomorrow.

```
inductive xnat : Type
| zero : xnat
| succ : xnat -> xnat
theorem TnF : False ≠ True := by
intro h
rw [h]
exact True.intro
def f (x : xnat) : Prop := match x with
| xnat.zero => True
| xnat.succ _ => False
theorem zero_not_one : xnat.succ xnat.zero ≠ xnat.zero := by
intro h
have x: f xnat.zero = True := rfl
rw [← h] at x
apply TnF
exact x
#check zero_not_one
```

Conceptually I'm still struggling with the claim that this needs to be done this way -- it seems like the kernel (or the underlying type theory) should simply be able to distinguish between two terms once they are fully expanded/evaluated (not sure what the lambda calculus terminology is here). I definitely need to read up more about this, but it will be tomorrow -- my brain is completely fried now, and we aren't even at the stage of succ_inj yet :)

#### Arthur Adjedj (Aug 03 2023 at 17:17):

Some flavor of type theory, referred to as observational theory, does allow to distinguish terms "trivially" by reducing the equality type depending on the constructors. in your case, the type `xnat.succ xnat.zero = xnat.zero`

would reduce to `False`

, and your proof that `xnat.succ xnat.zero ≠ xnat.zero`

would simply be the identity function over `False`

. Even though Lean doesn't have such a type theory, the language constructs some helper functions to solve these things "automatically". In your case, this theorem can be solved by calling `xnat.noConfusion`

, a helper function which discriminates terms of a type by its constructors to prove things like your non-equality here "automatically" (I've just realised that this was already mentioned before in this thread, oops):

```
theorem zero_not_one : xnat.succ xnat.zero ≠ xnat.zero := xnat.noConfusion
```

If you're interested in going deeper, these helper functions are described in this paper by McBride, Goguen and McKinna.

#### Adam Kurkiewicz (Aug 03 2023 at 19:05):

Thanks Arthur, do you think there might be a more accessible source than the paper? I'd love to learn this, but I'm probably missing a couple of semesters of theoretical computer science to have the necessary background to learn from a paper like this (I don't even understand the notation with long horizontal lines).

In terms of immediate objectives, I'd like to learn how to formalise IMO problems (I'm interested in the IMO Grand Challenge). My current understanding is that I shouldn't need an in-depth understanding of typed lambda calculi for this (please let me know if you disagree).

#### Arthur Adjedj (Aug 03 2023 at 19:17):

Other than this article, and @Kevin Buzzard 's blog on the matter, the only other ressource I can think of would be Lean's source code itself, but i don't think it's be any more accessible.

You certainly don't need a deep knowledge of lambda-calculus and type theory to prove things in it, Mathlib provides a pletorha of properties already proven, as well as very powerful tactics which abstract away from lean's core theory and objects. I believe your best bet would be to get more familiar with writing tactics in general, as well as getting familiar with the additional tactics mathlib bring to the table.

#### Kevin Buzzard (Aug 03 2023 at 19:41):

@Adam Kurkiewicz you don't need to know *anything* about this type theory stuff if you want to formalise Olympiad papers. You just get on with it -- it's mathematics, not computer science. Just ask if you don't understand how to do something and people will help. I don't teach any type theory at all in my course and my students produce excellent mathematical proofs.

#### Riccardo Brasca (Aug 03 2023 at 19:44):

Well, the point is that the only new axiom added when you create a type `xnat`

is `xnat.rec`

. you can `#check`

it and see the precise statement, but this is only "magic". The fact that the constructors are injective Is a theorem, proved using `xnat.rec`

. Lean just automatically generates it since it is very useful, but it is a normal theorem, and the proof is essentially the one suggested by Kevin.

#### Riccardo Brasca (Aug 03 2023 at 19:45):

And I completely agree, you don't need to understand all this to formalize mathematics, but if you're curious we're happy to explain.

#### Adam Kurkiewicz (Aug 04 2023 at 12:13):

So, I've proven that left addition is equal to right addition for all inputs (a b : Nat). I was surprised how far the rewrite tactic can take me :)

But I'd like to prove that left addition and right addition are "extensionally" equal.

I found this bit of lean magic `funext`

, but it complains about the number of inputs -- it only seems to work on single-parameter functions.

Would I need to find a way express the theorem as a chain of single-parameter functions? Or is there some other trick to use?

The error I'm getting is:

```
application type mismatch
funext left_add_eq_right_add
argument
left_add_eq_right_add
has type
∀ (a b : Nat), left_add a b = right_add a b : Prop
but is expected to have type
∀ (x : Nat), left_add x = right_add x : PropLean 4
left_add_eq_right_add : ∀ (a b : Nat), left_add a b = right_add a b
```

It's generated by the following

```
def left_add_eq_right_add_func_level: left_add = right_add :=
funext left_add_eq_right_add
```

I already have the proof of

```
def left_add_eq_right_add (a b : Nat) : left_add a b = right_add a b
```

#### Ruben Van de Velde (Aug 04 2023 at 12:22):

```
example (f g : ℕ → ℕ → ℕ) (h : ∀ a b, f a b = g a b) :
f = g := funext fun a => funext (h a)
```

#### Johan Commelin (Aug 04 2023 at 17:28):

@Adam Kurkiewicz You might have guessed already from Ruben's post: every function in Lean is "secretly" single-valued. It's just that some single-valued functions return single-valued functions that return single-valued functions that return .....

#### Adam Kurkiewicz (Aug 04 2023 at 18:05):

Yes, I figured :) -- Thanks Johan!!!

#### Hamza Shezad (Nov 02 2023 at 00:43):

in world 1 level 8, where we have to prove `2 + 2 = 4`

;

https://adam.math.hhu.de/#/g/hhu-adam/NNG4/world/Tutorial/level/8

what is the more correction solution? initially, i wanted to "prove" (or "turn into"? not sure of the terminology here) 2+2 into 4. i wasn't able to figure that out so i went with the following;

```
example : (2 : ℕ) + 2 = 4 := by
nth_rewrite 2 [two_eq_succ_one]
rw [add_succ]
rw [succ_eq_add_one]
rw [four_eq_succ_three]
rw [three_eq_succ_two]
rw [succ_eq_add_one]
rw [succ_eq_add_one]
rfl
```

after looking at the solution i figured it out;

```
example : (2 : ℕ) + 2 = 4 := by
nth_rewrite 2 [two_eq_succ_one]
rw [add_succ]
rw [one_eq_succ_zero]
rw [add_succ]
rw [add_zero]
rw [← three_eq_succ_two]
rw [← four_eq_succ_three]
rfl
```

i am wondering which one is the more "correct" solution? admittedly the second one is more elegant and was satisfying to write.

#### Kevin Buzzard (Nov 02 2023 at 03:32):

I have no idea how to judge which solution is "correct". I have started adding comments after levels saying "here's one way to do it" but I don't really know if there is a right or wrong answer. I think `decide`

is the correct solution :-) (see algorithm world)

#### Hamza Shezad (Nov 02 2023 at 14:42):

haha, thanks Kevin

i am quite far from algorithm world :D i am on the final level of addition world

#### Hamza Shezad (Nov 02 2023 at 14:56):

but i guess solutions are subjective?

Last updated: Dec 20 2023 at 11:08 UTC