## 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:

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?

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

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,
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

I thought so to

#### 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},
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.

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

Last updated: Aug 03 2023 at 10:10 UTC