Natural Number Game

Stream: general

[Olonbayar Temuulen]

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]

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

[Mario Carneiro]

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]

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

omg, this explains alot. thank you very much!

[Olonbayar Temuulen]

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]

assumption essentially tries calling exact h with each hypotheses h.

[Bryan Gin-ge Chen]

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]

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

[Scott Morrison]

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

[Kyle Miller]

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]

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]

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]

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

[Kyle Miller]

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]

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]

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]

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]

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

[Kyle Miller]

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]

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]

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]

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

[Olonbayar Temuulen]

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]

image.png

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Joseph O]

I know I have to use induction

[Joseph O]

aha, I think induction on b will work

[Joseph O]

yeah I solved it

[Joseph O]

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]

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

[Johan Commelin]

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

[Joseph O]

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]

Why is nng freezing here? image.png

[Julian Berman]

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]

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]

I thought so to

[Joseph O]

I made a different proof

[Joseph O]

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]

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]

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

[Kevin Buzzard]

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]

Thanks again.

[Joseph O]

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

[Joseph O]

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

[Patrick Johnson]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

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]

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]

@Kevin Buzzard it's down again

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

[Verone Kadriu]

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

[Ruben Van de Velde]

See, Alex is always faster than me :)

[Jencel Panic]

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]

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]

Shouldn't the last step be exact m_ih?

[Jencel Panic]

Ah, of course, sorry

[Damiano Testa]

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

[Kevin Buzzard]

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

[Jencel Panic]

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]

Great tutorial, btw @Kevin Buzzard !

[Kevin Buzzard]

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

[Damiano Testa]

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

[Jencel Panic]

And I find Lean pretty easy to use too.

[Jencel Panic]

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

[Jencel Panic]

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]

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

[Jencel Panic]

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

[Kevin Buzzard]

Sure, we already have docs#id

[Shreyas Srinivas]

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]

(deleted)