Zulip Chat Archive

Stream: general

Topic: Natural Number Game


Olonbayar Temuulen (Apr 19 2022 at 03:35):

I noticed that sometimes my goal closes even without me having to use the "exact" tactic, after using the "apply" tactic? Under what circumstances does the "apply" tactic finish the proof as well?

Scott Morrison (Apr 19 2022 at 03:38):

If there are no "unknown" hypotheses required for the lemma you are applying, then apply will solve the goal.

Mario Carneiro (Apr 19 2022 at 03:38):

if there are no subgoals in the theorem, then apply will finish the goal. That means that usually you can use apply in place of exact and it will work the same

Scott Morrison (Apr 19 2022 at 03:38):

(Essentially, apply tries to unify the conclusion of the lemma with the current goal. If that completely determines all the arguments of the lemma, we're done. Otherwise, apply creates a new goal for each undetermined argument.)

Olonbayar Temuulen (Apr 19 2022 at 03:46):

omg, this explains alot. thank you very much!

Olonbayar Temuulen (Apr 19 2022 at 04:52):

What is the difference between the "exact" and the "assumption" tactic?
And in general from where can one find all the documentations for the tactics in Lean?

Scott Morrison (Apr 19 2022 at 04:57):

assumption essentially tries calling exact h with each hypotheses h.

Bryan Gin-ge Chen (Apr 19 2022 at 04:57):

Quoting from our tactic documentation page:

assumption: This tactic looks in the local context for a hypothesis whose type is equal to the goal target. If it finds one, it uses it to prove the goal, and otherwise it fails.

exact : This tactic provides an exact proof term to solve the main goal. If t is the goal and p is a term of type u then exact p succeeds if and only if t and u can be unified.

Kyle Miller (Apr 19 2022 at 04:58):

tactic#assumption and tactic#exact are the main mathlib documentation for the tactics (beyond books like #tpil)

Scott Morrison (Apr 19 2022 at 04:58):

With exact, you have to specify the term you want to use!

Kyle Miller (Apr 19 2022 at 05:03):

Something I forget about using is the special notation for by assumption, which can be convenient when you want to pass extra arguments to something. Here's an example that's equivalent do doing assumption:

example {p : Prop} (h : p) : p :=
begin
  exact _
end

Another example:

example {p q : Prop} (h : p) (f : p  q) : q :=
begin
  exact f _
end

The underscore can be replaced with the type of the assumption you're wanting to get, like ‹p› for both of these examples.

Olonbayar Temuulen (Apr 19 2022 at 06:18):

When I write "exact succ_ne_zero _ h" for what exactly does the "_" before "h" in the end stand for?

Source: Taken from the solution of the Level 2 of the Advanced Multiplication World.

*PS: I feel like i've encountered a similar notation once in the game before, but cannot recall where exactly and at the time failed to address my gap in the knowledge and question why was it so.

Olonbayar Temuulen (Apr 19 2022 at 06:27):

To put my question into a bit more detailed beginners perspective:

From my current level of understanding the "exact" tactic simply unifies the goal with the hypothesis, if the hypothesis is a term of the goal.
But in the level 2 of Advanced Multiplication World, after the neccesary steps just before using the exact tactic we arrive at the state of:

image.png

And here we only have the "h" hypothesis and the goal, which we close through "exact succ_ne_zero _ h", in which case my questions is what is the "_" underscore that we are using to close the goal in the exact tactic?

Olonbayar Temuulen (Apr 19 2022 at 06:29):

I understand that "underscore _" is a placeholder, but for what exactly is it placeholding for?

Kyle Miller (Apr 19 2022 at 06:38):

The _ placeholder represents a fresh metavariable, and Lean will try to solve for what this metavariable should be through unification.

The type of succ_ne_zero is ∀ (n : ℕ), succ n ≠ 0, so when you do succ_ne_zero _ h, since h has type succ (succ d * e + d) = 0 (and since succ n ≠ 0 means succ n = 0 → false), then both _ and succ d * e + d are unified with the "n" of the lemma, so it's as if you wrote succ_ne_zero (succ d * e + d) h.

Kyle Miller (Apr 19 2022 at 06:39):

By the way, the apply tactic is sort of like doing exact foo _ _ _ with the right number of placeholders, but with the twist where each of those placeholders that don't get unified with anything end up being turned into additional goals.

Olonbayar Temuulen (Apr 19 2022 at 06:41):

Kyle Miller said:

The _ placeholder represents a fresh metavariable, and Lean will try to solve for what this metavariable should be through unification.

The type of succ_ne_zero is ∀ (n : ℕ), succ n ≠ 0, so when you do succ_ne_zero _ h, since h has type succ (succ d * e + d) = 0 (and since succ n ≠ 0 means succ n = 0 → false), then both _ and succ d * e + d are unified with the "n" of the lemma, so it's as if you wrote succ_ne_zero (succ d * e + d) h.

thank you for your kind response.
I understand it now, but just for the purpose of a little bit of more clarification can you explain what you mean by metavariable a bit more in depth?

Kyle Miller (Apr 19 2022 at 06:43):

A metavariable is a "hole" in an expression that can be filled in with another expression. They are exactly what the unification algorithm solves for.

Kyle Miller (Apr 19 2022 at 06:45):

Have you seen those ?m_1 things in expressions in tactic states yet? Those are how Lean displays metavariables.

Kyle Miller (Apr 19 2022 at 06:46):

In fact, what the goal in the tactic state is showing you is the type of the metavariable that you are trying to fill yourself using tactics. The metavariable itself isn't shown, just its type.

Olonbayar Temuulen (Apr 19 2022 at 06:47):

Kyle Miller said:

Have you seen those ?m_1 things in expressions in tactic states yet? Those are how Lean displays metavariables.

Ah....! yes, indeed.

Kyle Miller (Apr 19 2022 at 06:48):

lemma foo : bar = baz := begin ... end is creating a metavariable at the exact point of the begin ... end block, and through tactics you're trying to solve for it.

Olonbayar Temuulen (Apr 19 2022 at 06:52):

Thank you again, will think a bit more and digest this by taking a small walk outside.

Olonbayar Temuulen (Apr 19 2022 at 07:08):

Just realized I can use the "contradiction" tactic to close succ.case at the end in the level 1 of the advanced multiplication world, awesome!
Feel like this is much more intuitive, compared to trying to rw, then exfalso and then "exact succ_ne_zero _ hab".
Or does this kill the educational value of doing it the latter "proper" way?

Olonbayar Temuulen (Apr 19 2022 at 07:13):

image.png

Kevin Buzzard (Apr 19 2022 at 07:19):

I have no idea about the educational value of proving any theorem in any way -- I just wrote things which I thought people might understand. The game is very rough around the edges.

David Chanin (Apr 19 2022 at 09:55):

Is the natural number game open source? I was thinking it might be fun to try adding modules for more concepts, ex working with matrices, etc..

Kevin Buzzard (Apr 19 2022 at 10:04):

Sure, although I am unlikely to ever push an update.

Kevin Buzzard (Apr 19 2022 at 10:05):

The way I see NNG is that it does the job it's supposed to do, and in under a year we'll all be using Lean 4 and then we'll have to wait until someone writes Lean 4 game maker and then redo stuff in that.

Alex J. Best (Apr 19 2022 at 21:19):

Using the same lean_game_maker you are free to create your own game though. I know @Marc Masdeu has for a course and i have for my own teaching at https://GitHub.com/alexjbest/cap-game that's probably a better way to go than forking nng if you have good ideas for follow ups you want to share

Joseph O (Apr 22 2022 at 01:19):

can i get a hint for level 4 in multiplication world?

Joseph O (Apr 22 2022 at 01:20):

I know I have to use induction

Joseph O (Apr 22 2022 at 01:20):

aha, I think induction on b will work

Joseph O (Apr 22 2022 at 01:25):

yeah I solved it

Joseph O (Apr 22 2022 at 12:39):

how is this proof for level 6 of world 3?

induction b with d hd,
{
  simp,
  repeat {rw mul_zero},
},
{
  simp,
  repeat {rw mul_succ},
  rw hd,
  simp,
  repeat {rw [add_assoc, add_succ]},
  simp,
},

Johan Commelin (Apr 22 2022 at 12:43):

Note that you can write simp [my_lemma_1, my_lemma_2].

Johan Commelin (Apr 22 2022 at 12:43):

So simp [mul_zero] would probably close the first goal in one line.

Joseph O (Apr 22 2022 at 13:21):

Johan Commelin said:

So simp [mul_zero] would probably close the first goal in one line.

Ah nng didn't cover that, but that's good to know

Joseph O (Apr 23 2022 at 00:12):

Why is nng freezing here? image.png

Julian Berman (Apr 23 2022 at 00:29):

Does it unfreeze if you do a refresh? Or a full refresh (cmd+shift+r or the equivalent for your OS+browser)? I don't know why Javascript does what it does but it does (I've seen the above fix a frozen weblean)

Julian Berman (Apr 23 2022 at 00:30):

Ah sorry, I didn't glance at the actual code, it may be Lean is going round and round in circles with the repeats

Joseph O (Apr 23 2022 at 01:07):

I thought so to

Joseph O (Apr 23 2022 at 01:07):

I made a different proof

Joseph O (Apr 23 2022 at 12:28):

For level 8 of power world, I beat it in 17 rewrites (i counted)

rw [two_eq_succ_one, one_eq_succ_zero],
repeat {rw pow_succ},
repeat {rw pow_zero},
repeat {rw one_mul},
repeat {rw succ_mul},
rw [zero_mul, zero_add],
repeat {rw add_mul},
repeat {rw mul_add},
simp,

but I still don't exactly understand the ring proof, even after reading the docs

Joseph O (Apr 23 2022 at 12:42):

This being the ring proof:

rw [two_eq_succ_one, one_eq_succ_zero],
repeat {rw pow_succ},
repeat {rw pow_zero},
ring,

Joseph O (Apr 23 2022 at 12:42):

Ring seems really powerful, I would like to know where to use them.

Kevin Buzzard (Apr 23 2022 at 14:16):

ring will prove identities in systems where there is addition and multiplication which satisfy the usual axioms. At this point in the game you've proved all the axioms required so we can register the relevant instance on mynat and then all of a sudden you don't have to do 17 rewrites any more. I wrote a blog post with some details about how the tactic works here.

Joseph O (Apr 23 2022 at 15:14):

Thanks again.

Joseph O (Apr 24 2022 at 01:51):

I tried the apply easter egg, but I can't really explain it.
image.png

Joseph O (Apr 24 2022 at 01:52):

An explanation on why and how this happens would be nice. Thanks in advance.

Patrick Johnson (Apr 24 2022 at 03:52):

The goal was R. Function f takes a term of type P and a term of type Q and produces a term of type R. When you say apply f, you tell Lean that you want to construct a term of type R using function f, so Lean asks you to provide arguments for f (that is, terms of types P and Q).

Niv Sarig (Apr 24 2022 at 07:16):

Hi, that is agreat game and a wonderful way to teach formal proofs. Way to go :-)

I finished all 8 levels in the Power world, used the hiden ring tactics or without and still the power world is colored with blue and not green... what do I miss?

Thanks

Kevin Buzzard (Apr 24 2022 at 07:18):

Check each level has a tick and for any that don't, hit enter a couple of times at the end of the proof

Niv Sarig (Apr 24 2022 at 07:25):

Thanks Kevin for your fast reply, did all of that and yet... :-)

Kevin Buzzard (Apr 24 2022 at 07:59):

Sorry. My co-author had a hard time getting this to work, I don't know any of the details here (I just wrote the lean code, not any of the other infrastructure)

Olonbayar Temuulen (Apr 24 2022 at 08:52):

Kyle Miller said:

The _ placeholder represents a fresh metavariable, and Lean will try to solve for what this metavariable should be through unification.

The type of succ_ne_zero is ∀ (n : ℕ), succ n ≠ 0, so when you do succ_ne_zero _ h, since h has type succ (succ d * e + d) = 0 (and since succ n ≠ 0 means succ n = 0 → false), then both _ and succ d * e + d are unified with the "n" of the lemma, so it's as if you wrote succ_ne_zero (succ d * e + d) h.

Hello, thank you for your time again.
I wanted to settle the understanding of a definition of a metavariable once and for all, and have been reading documentation.
But what does one mean in this "system description", when they say a "construction"? image.png Can anyone give me an example of what makes a "construction" and what are particular constituents of it? Is it simply any proof, theorem or a lemma? Or am I failing to capture certain nuances, when I label it simply as such?
(Source taken from: https://leanprover.github.io/papers/system.pdf)

Yaël Dillies (Apr 24 2022 at 08:55):

What's meant is a term. A term is simply a "member" of a type, so for example if x is a real number, then x is a term of type (note that a type is itself a term, which might be confusing at first). "Partial constructions" then refer to terms with underscores in them. For example, if f : ℕ → ℕ, then f _ : ℕ is a "partial construction, because we haven't determined what should go in place of the _.

Joseph O (Apr 24 2022 at 12:13):

Patrick Johnson said:

The goal was R. Function f takes a term of type P and a term of type Q and produces a term of type R. When you say apply f, you tell Lean that you want to construct a term of type R using function f, so Lean asks you to provide arguments for f (that is, terms of types P and Q).

An this makes sense

Kyle Miller (Apr 24 2022 at 17:26):

@Olonbayar Temuulen When the paper says "construction," I think it's referring to a "construction" in the Calculus of Inductive Constructions, a type theory that Lean is based on. I'm not an expert in type theory, and, in my limited reading, as far as I can tell a "construction" is a representation of a term of a type (i.e., a term constructed using lambda abstractions, match statements, pi types, applications, and so on). To prove/calculate things in Lean, you have to construct a proof/algorithm, but as part of the user interface you are able to manipulate partially constructed proofs/algorithms.

Concretely, Lean expressions are an inductive type (defined here, at least on the Lean side -- Lean is also written in C++). An expression that still has mvar constructors seems like it should correspond to what they mean by a "partial construction." When two expressions are unified, mvar expressions unified with any other expression get replaced by that other expression immediately, there and at all occurrences (at least, it's as if it did this -- the algorithm does something more efficient). Presence of metavariables after a certain point in the typechecking process triggers the "don't know how to synthesize placeholder" error message.

There's some more complexity with metavariables that I'm aware of, but don't fully understand, and those are "delayed abstractions": metavariables that are allowed to depend on a list of local variables.

Verone Kadriu (Jun 01 2022 at 18:43):

Hi all,
I am trying to find the Natural Number Game but the link doesn't work. Is it erased? Where can I find it. Thanks!

Alex J. Best (Jun 01 2022 at 18:45):

I don't think it has been intentionally taken down, hopefully it is just a temporary bug, in the meantime there is another copy hosted at https://cbirkbeck.github.io/natural_number_game/

Ruben Van de Velde (Jun 01 2022 at 18:45):

@Kevin Buzzard it's down again

@Verone Kadriu there's a mirror at https://cbirkbeck.github.io/natural_number_game

Verone Kadriu (Jun 01 2022 at 18:46):

@Alex J. Best @Ruben Van de Velde Thank you very much! I hope they will fix soon!

Ruben Van de Velde (Jun 01 2022 at 18:46):

See, Alex is always faster than me :)

Jencel Panic (Sep 13 2023 at 11:00):

Hello,

I am "playing" the natural numbers game and it's been good so far, but at the first level of multiplication world I got this very weird message:

image.png

Jencel Panic (Sep 13 2023 at 11:01):

The lemma is:
zero_mul (m : mynat) : 0 * m = 0
My proof is

induction m,
rw mul_zero,
refl,
rw mul_succ 0 m_n,
rw add_zero (0 * m_n),
refl,

Damiano Testa (Sep 13 2023 at 11:02):

Shouldn't the last step be exact m_ih?

Jencel Panic (Sep 13 2023 at 11:03):

Ah, of course, sorry

Damiano Testa (Sep 13 2023 at 11:03):

The error message is telling you that the goal is not an equality between equal things.

Kevin Buzzard (Sep 13 2023 at 11:03):

BTW if you write induction m with d hd then you won't have this funny m_n variable.

Jencel Panic (Sep 13 2023 at 11:04):

OK, sorry, I am new to Lean, I even didn't know the exact tactic existed (although I vaguely remember I've seen it in Cog)

Jencel Panic (Sep 13 2023 at 11:05):

Great tutorial, btw @Kevin Buzzard !

Kevin Buzzard (Sep 13 2023 at 11:06):

I probably didn't teach it yet. You can do rw m_ih and then rfl.

Damiano Testa (Sep 13 2023 at 11:06):

If exact is not "allowed", then rw [m_ih]; refl should work!

Jencel Panic (Sep 13 2023 at 11:06):

And I find Lean pretty easy to use too.

Jencel Panic (Sep 13 2023 at 11:06):

I tried to learn Agda before, but it was much hader

Jencel Panic (Sep 13 2023 at 11:10):

One side question, is there a way to prove a general statement of the type "everything follows from itself", something like:

lemma id: (a: set) a ⊢ a

And then use it in such occasions?

Kevin Buzzard (Sep 13 2023 at 11:50):

NNG is not extensible but the exact tactic already does this.

Jencel Panic (Sep 13 2023 at 12:52):

I mean is it possible to to it in Lean in general, just curious.

Kevin Buzzard (Sep 13 2023 at 12:54):

Sure, we already have docs#id

Shreyas Srinivas (Sep 13 2023 at 14:09):

Jencel Panic said:

I mean is it possible to to it in Lean in general, just curious.

If you mean reflexivity, that's the rfl tactic. Also @Kevin Buzzard you probably mean docs3#id

Shreyas Srinivas (Sep 13 2023 at 14:09):

(deleted)

Arihant Gadgade (Mar 01 2024 at 03:20):

Does anyone know why the natural number game in lean4 is down?

Kevin Buzzard (Mar 01 2024 at 08:32):

No

Kevin Buzzard (Mar 01 2024 at 08:32):

But the relevant person knows that it's down

Egbert Rijke (Mar 01 2024 at 08:47):

It is down for me as well. It's at a very unfortunate moment for me, because I wanted to play the natural numbers game with my students today at our tutorial session on Lean

Egbert Rijke (Mar 01 2024 at 08:58):

It seems to be back up. Just in time for my class :tada:

Jon Eugster (Mar 01 2024 at 10:11):

Sorry for that! Apparently the server rebooted and some reboot script didn't work :(

Alex Kontorovich (Apr 19 2024 at 17:51):

Stupid question. I was giving a demo of the Natural Number Game yesterday (at Wesleyan), and I didn't know why the following happens. We went over the fact that if the goal is: a + (b + 0) + (c + 0) = a + b + c, and you rw [add_zero], it will do the first one it finds. We spent a little time going over the fact that you could alternatively do rw [add_zero c] to rewrite the other instance; then we learned how to use nth_rewrite, repeat, etc.

But then we got to the "big boss" of 2 + 2 = 4; and if you do a single rw [two_eq_succ_one], it applies it to both instances of 2! Naturally someone asked why it did that, and I mumbled something to move us along ("nothing to see here"). Of course it's not a big deal, but pedagogically, is this what we want? (Or is there something better I could/should have said about the change in behavior?) Thanks!

Johan Commelin (Apr 19 2024 at 17:59):

If you have a + (b + 0) + (c + 0) + (b + 0) = a + b + c + b and you do rw [add_zero] then it will also rewrite both occurences of b + 0 (but do nothing with the c + 0).

Johan Commelin (Apr 19 2024 at 18:00):

Lean latches on to the first subexpression for which it can fill in the metavariables, and then rewrites that subexpression everywhere.

Richard Osborn (Apr 19 2024 at 18:04):

This hopefully gives some intuition as to what rw is doing.

import Mathlib

example {b c : }: (b + 0) + (b + 0) + (c + 0) = b + b + c := by
  rw [add_zero] -- ⊢ b + b + (c + 0) = b + b + c
  rw [add_zero]

Mark Fischer (Apr 19 2024 at 20:44):

Here's how I've explained this to my counsin and their friend (they're in highschool)

I think it's pretty natural to imagine a version of rw that only works with equalities and bi-conditionals. In which case, rw [add_zero] simply wouldn't work as it's a function and not either an equality or a bi-conditional.

(add_zero 5) on the other hand is an equality - specifically (5 + 0) = 5.

This version of rw replaces all instances of 5 + 0 with 5.

Lean's actual rw tactic is a bit more powerful than this though. It will accept functions so long as they eventually return an equality and it can find a values for the parameters along the way. It doesn't exhaustively look for these values though, it'll just go with the first ones it finds.

Kim Morrison (Apr 20 2024 at 07:00):

Note that you can ask it to rewrite using later occurrences than the first one, e.g. using the rw (config := {occs := .pos [2]}) [w] syntax.

Jawad Ali (Apr 24 2024 at 07:33):

Hi, I am new here and I want to learn LEAN 4, I have completed first 4 lessons of natural number game but its not working for furthers level. how can I tackle this issue ?

Kevin Buzzard (Apr 24 2024 at 07:34):

:-( . Reload the page?

Jawad Ali (Apr 24 2024 at 07:37):

image.png
I tried but its not working...

Kevin Buzzard (Apr 24 2024 at 07:43):

That looks fine to me. What's "not working"? This is quite a vague big report...

Bernardo Borges (May 11 2024 at 18:43):

Jawad Ali said:

image.png
I tried but its not working...

You still need to close the proof with rfl


Last updated: May 02 2025 at 03:31 UTC