Natural number game

Stream: new members

[Rei]

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]

cc @Kevin Buzzard

[Kevin Buzzard]

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ä]

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]

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]

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]

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]

Weird. Just simp [pow_succ] also shows "Proof complete"

[Eric Rodriguez]

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

[Eric Rodriguez]

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

[Jukka Kohonen]

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]

Just hit enter a few times

[Lucas]

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]

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

[Lucas]

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

[Bryan Gin-ge Chen]

Make sure your Lean project depends on mathlib and add the line import data.nat.prime at the top of your file.

[Patrick Massot]

Which online tutorial are you talking about?

[Lucas]

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

[Lucas]

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

[Lucas]

they gave the example of proving the infinitude of primes

[Patrick Massot]

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]

are they already outdated?

[Patrick Massot]

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

[Patrick Massot]

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

[Lucas]

alright, good to know for the future

[Ayush Agrawal]

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]

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

[Kevin Buzzard]

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]

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ä]

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

[Kevin Buzzard]

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]

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]

Maybe this is close enough?

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

[King Crawford]

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

[Arien Malec]

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]

Do you need to generalise c?

[Ruben Van de Velde]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

yeesh I got it with left + exact add_left_eq_zero h

[Kevin Buzzard]

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

[Kevin Buzzard]

docs#add_left_eq_zero

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Arien Malec]

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]

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

[Arien Malec]

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]

Something like this?

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

[Ryan Duan]

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]

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

[Ryan Duan]

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

[Arien Malec]

adding t as a parameter worked -- collapses ∀ t to my t : mynat ?

[Arien Malec]

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

[Ruben Van de Velde]

Yeah, that's right

[Alex J. Best]

@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]

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]

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]

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]

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]

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]

Spoiler from the source code

[Alberto Navarro Garmendia]

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]

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]

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]

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]

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]

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]

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 goalsbut 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]

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

[Anne Baanen]

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]

I see induction m on n, which is not valid syntax

[Alberto Navarro Garmendia]

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 ndoesn'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 nevery step works the same, except the final one wich says Proof complete . Anyway. Thank you very much!

[Will Midwood]

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]

I tried cases a with n but couldn't get anything more solvable

[Arien Malec]

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]

Two questions:

First: I am having troubles with the syntaxis of add_left_equal_zero, eq_zero_or_eq_zero_of_mul_eq_zeroand 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=Qinto some q:Q=P, where Pand Qare different expressions?

Thanks in advance.

[Ruben Van de Velde]

2/ rw eq_comm at p or have q := p.symm

[Ruben Van de Velde]

1/ what's the error?

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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).

docs#nat.le_induction

[Newell Jensen]

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

[Kyle Miller]

@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]

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]

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

[Arien Malec]

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]

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]

@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

1. apply add_right_cancel which will require you to provide h afterwards. In particular that is the new goal that you are seeing; or
2. 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]

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 : Qout of apply (Theorem_1 p)or a similar syntaxis? Thanks in advance

[Johan Commelin]

You could do

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

[Johan Commelin]

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]

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]

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]

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]

You've got two ds

[Ruizhe Wan]

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

[Kevin Buzzard]

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]

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]

I don't think lean 3 supports nonassociative operators

[Mario Carneiro]

actually that's not true, you can do it with notation if you set all the precedences manually

[Kevin Buzzard]

@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]

(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]

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]

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]

for teaching purposes the former approach is often reasonable

[Mike Shulman]

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]

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]

I see that in Lean 3, = is left-associative.

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

Ugh.

[Mario Carneiro]

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]

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]

How do I parse that?

[Kevin Buzzard]

@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]

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

[Mike Shulman]

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]

He means in the info view.

[Patrick Massot]

assoc.gif

[Patrick Massot]

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

[Mike Shulman]

My infoview doesn't do that.

[Patrick Massot]

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

[Patrick Massot]

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

[Mike Shulman]

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

[Mike Shulman]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mike Shulman]

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

[Johan Commelin]

Ooh, maybe you need something like import tactic at the top? I'm just guessing.

[Johan Commelin]

Because those version numbers seem pretty up to date

[Johan Commelin]

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

[Mike Shulman]

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

[Johan Commelin]

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

[Mike Shulman]

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

[Mike Shulman]

That seems like a weird sort of level-mixing.

[Johan Commelin]

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

[Johan Commelin]

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

[Mike Shulman]

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

[Alex J. Best]

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]

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

[Alex J. Best]

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

[Johan Commelin]

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]

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

[Patrick Massot]

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]

(deleted)

[Adam Kurkiewicz]

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]

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]

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]

You can start by proving that 1 is different from 0

[Adam Kurkiewicz]

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]

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]

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]

@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]

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]

Why can't you use the infoview?

[Kevin Buzzard]

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]

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

[Riccardo Brasca]

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

[Adam Kurkiewicz]

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

[Adam Kurkiewicz]

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]

Kevin has a blog post about this here

[Adam Kurkiewicz]

@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]

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]

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

[Adam Kurkiewicz]

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]

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

[Riccardo Brasca]

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]

Can you see a function that gives a contradiction?

[Adam Kurkiewicz]

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]

I don't actually know what f should be

[Riccardo Brasca]

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]

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]

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]

So we're actually eliminating the equality?

[Riccardo Brasca]

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]

Here is a full proof of 0 ≠ 1.

Proof

inductive xnat : Type
| zero : xnat
| succ : xnat -> xnat

theorem foo : True ≠ False := by
  intro h
  rw [← h]
  exact True.intro

def f : xnat → Prop
| xnat.zero => True
| _ => False

theorem bar : xnat.zero ≠ xnat.zero.succ := by
  intro h
  have : f xnat.zero = True := rfl
  rw [h] at this
  apply foo
  rw [← this]
  rfl

[Adam Kurkiewicz]

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]

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

[Riccardo Brasca]

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

@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]

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]

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]

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]

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

[Johan Commelin]

@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]

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

[Hamza Shezad]

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]

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]

haha, thanks Kevin
i am quite far from algorithm world :D i am on the final level of addition world

[Hamza Shezad]

but i guess solutions are subjective?