NNG "exact" syntax / tactic arguments

Stream: new members

[Daniel K Lyons]

I am here: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=8&level=6

My question is about this line: exact add_right_cancel _ _ _. Basically, I'm not understanding why exact add_right_cancel isn't accepted, or why exact add_right_cancel _ _ isn't accepted. In general, I am fairly confused about what the real syntax is for the argument of a tactic.

Going back to world 6 level 6 for a minute: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=6&level=6

I'm also confused by the syntax for apply here. The instructions recommend trying apply (f p); in my solution I wound up with apply f(p). What's the difference between these syntaxes?

Thanks for your patience and your help!

[Adam Topaz]

exact foo does exactly what it sounds like.... it matches the goal exactly with foo. So exact add_right_cancel _ _ _ means that the goal should be matched exactly to add_right_cancel A B C where A B C are left to lean to figure out. If you don't want the underscores, use apply add_right_cancel

[Adam Topaz]

apply f p, apply f (p), apply (f p) all mean the same thing

[Adam Topaz]

I don't really see where you want to use add_right_cancel in that link, btw.. oh sorry, I clicked the wrong link :)

[Mario Carneiro]

NB: We can't see your solutions to NNG problems when you only give a link. Your solutions are stored in browser-local data

[Daniel K Lyons]

Thanks for clarifying that for me Adam! Mario, I will be sure to include the text of the proof if I get stuck, but I figured it wasn't strictly relevant to this question.

[Mario Carneiro]

exact add_right_cancel would only work if the goal was ∀ (a t b : mynat), a + t = b + t → a = b including the foralls

[Adam Topaz]

I suspect @Daniel K Lyons had some previous steps already done Mario. Here is a solution (using exact ...), if you want a spoiler (I suggest struggling a bit by yourself before looking at it :smile: )

theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b :=
begin
  intros h,
  rw [add_comm t, add_comm t] at h,
  exact add_right_cancel _ _ _ h,
end

[Daniel K Lyons]

Adam, thanks again! I actually have already solved everything up to halfway through Advanced Multiplication somewhere, and then I decided to throw everything away and go through it a second time and see if it makes more sense. It mostly does, just these little things.

I have also discovered where to find the solutions on github so I don't bother people too much with how-do-I-solve-this-one-problem type stuff.

[Adam Topaz]

Oh, it was just meant to be a demonstration of using exact for this proof, since this was your original question.

[Daniel K Lyons]

So why is apply able to suss out what to do in this case? It seems like apply is less precise about what it will accept but won't close the proof, whereas exact will? Is that right?

[Adam Topaz]

apply will try to match the goal with the conclusion of the lemma you're applying, as opposed to the exact statement of the lemma itself..

[Adam Topaz]

So if I replace exact ... in the code above with apply add_right_cancel, I get:

2 goals
t a b : mynat,
h : a + t = b + t
⊢ a + ?m_1 = b + ?m_1

t a b : mynat,
h : a + t = b + t
⊢ mynat

So you can see that lean was able to reduce the goal to proving a + ?? = b + ??, but it had no way of knowing what ?? is supposed to be.

[Adam Topaz]

On the other hand, if I tell it exactly what t is using apply add_right_cancel _ t, I get:

t a b : mynat,
h : a + t = b + t
⊢ a + t = b + t

[Daniel K Lyons]

So this seems like a really stupid question, how do you know by looking at add_right_cancel what its arity is or which placeholders are which?

[Mario Carneiro]

Count the pis and arrows in ∀ (a t b : mynat), a + t = b + t → a = b

[Mario Carneiro]

there are three variables in the forall and one hypothesis, so four arguments

[Mario Carneiro]

so you would apply it like exact add_right_cancel _ _ _ h

[Mario Carneiro]

Most of the time, those pis will be written with implicit binders like this: ∀ {a t b : mynat}, a + t = b + t → a = b. In that case, lean basically inserts the _ for you, so you would just write exact add_right_cancel h

[Daniel K Lyons]

Mario, what is a "pi"?

[Mario Carneiro]

sorry, jargon

[Patrick Massot]

pi means ∀ in this context.

[Mario Carneiro]

lean also lets you write the type as Π (a t b : mynat), a + t = b + t → a = b and so the type of dependent functions is also known as a Pi type

[Mario Carneiro]

for propositions, a Pi type is just the same as a forall

[Daniel K Lyons]

So the Pi type is more general than forall, there are other quantifications(?) that "count" for the purposes of determining the signature?

[Mario Carneiro]

they are interchangeable in lean, you can use Π for ∀ or vice versa

[Daniel K Lyons]

So a "thing" like add_right_cancel is a theorem, it has a type, the signature of that type is ∀ {a t b : mynat}, a + t = b + t → a = b which to my programmer mind means there are four parameters here, three of them are values, the fourth is a hypothesis?

[Kevin Buzzard]

Note: I can't guarantee that the mynat binder types in NNG are the same as those for nat in mathlib/lean

[Mario Carneiro]

The only thing that counts are the number of pi binders, but because of this notation you will often see pi binders written with ∀, and also A -> B is notation for ∀ (_ : A), B

[Daniel K Lyons]

It's kind of mind blowing that we can successfully compute at this high level :)

[Kevin Buzzard]

Function inputs in {} brackets are not explicitly input because their values can be read off from the types of later inputs

[Mario Carneiro]

Daniel K Lyons said:

So a "thing" like add_right_cancel is a theorem, it has a type, the signature of that type is ∀ {a t b : mynat}, a + t = b + t → a = b which to my programmer mind means there are four parameters here, three of them are values, the fourth is a hypothesis?

Yes, that's correct. The first three parameters are marked as "lean, figure it out", so even though there are actually four parameters you only need to write one of them

[Mario Carneiro]

by the way, a trick you can use in NNG to see the type of a theorem is to add have := @add_right_cancel, to the proof and look at the type of the thing that got added to the context

[Daniel K Lyons]

wow, this is incredibly sophisticated. I understand why NNG doesn't go into these depths right away, it would be terrifying.

[Daniel K Lyons]

thanks for all your help!