## Stream: new members

#### Abhimanyu Pallavi Sudhir (Oct 13 2018 at 16:16):

How many parameters do I need to specify to use ←@add_right_inj? I'm trying to understand how to use tactics with implicit parameters, but can't seem to get it right. I keep getting failed to synthesize type class instance

#### Chris Hughes (Oct 13 2018 at 16:24):

rw ← add_right_inj x should be good enough depending on the type that you're using. What type are the variables in your equality?

#### Abhimanyu Pallavi Sudhir (Oct 13 2018 at 16:35):

rw ← add_right_inj x should be good enough depending on the type that you're using. What type are the variables in your equality?

Yeah, that works, but I'm trying to understand how exactly the @ syntax works. Do we not need to use it for things in normal parantheses?

#### Chris Hughes (Oct 13 2018 at 16:40):

No. @ is for specifying the arguments in {} or [], which are usually inferred, but sometimes Lean can't infer them so they have to be given explicitly. You can put underscores in place of arguments to you want to leave implicit, if you only want to give some of the implicit arguments explicitly.

#### Kevin Buzzard (Oct 13 2018 at 16:40):

Can you post a MWE with the error?

#### Kevin Buzzard (Oct 13 2018 at 16:42):

I gave a lecture on type class inference over the summer. Abhi if you log into Imperial's Panopto and search for Xena then you should be able to find all of them.

#### Kevin Buzzard (Oct 13 2018 at 16:43):

The rule of thumb is that you should not be using @ in general

#### Abhimanyu Pallavi Sudhir (Oct 13 2018 at 16:49):

import tactic.norm_num

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) : 2 * r - 4 * s * s - 4 * s = 1 :=
begin
rw ←@add_right_inj (4 * s + 4 * s * s) (2 * r - 4 * s * s - 4 * s) 1,
sorry,
end


#### Abhimanyu Pallavi Sudhir (Oct 13 2018 at 16:50):

(Something like that -- don't mind the sorry, I created the MWE from another project)

#### Kenny Lau (Oct 13 2018 at 16:51):

import algebra.group

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) : 2 * r - 4 * s * s - 4 * s = 1 :=
begin
rw ←@add_right_inj ℕ _ (4 * s + 4 * s * s) (2 * r - 4 * s * s - 4 * s) 1,
sorry,
end


#### Kenny Lau (Oct 13 2018 at 16:51):

If you do #check @add_right_inj, then you get ∀ {α : Type u_1} [_inst_1 : add_right_cancel_semigroup α] (a : α) {b c : α}, b + a = c + a ↔ b = c

#### Kenny Lau (Oct 13 2018 at 16:51):

so the first argument is the type

#### Kevin Buzzard (Oct 13 2018 at 17:58):

Here's a crash course in how it works. If you type #check @add_right_inj as Kenny says, you'll see the full definition of the function. Stuff in round brackets you are expected to supply (although if you are lazy you can write _ which means "try to guess). Stuff in square brackets or curly brackets { } Lean is going to try to guess for you, so your first instinct should be to leave it out. If you leave that stuff out you just pretend it isn't there and don't use @

#### Kevin Buzzard (Oct 13 2018 at 17:59):

Kenny wrote the output of the #check and you see that there's only one thing in round brackets, so it only wants the value of a

#### Kevin Buzzard (Oct 13 2018 at 18:00):

So this works:

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) : 2 * r - 4 * s * s - 4 * s = 1 :=
begin
rw ←add_right_inj (4 * s + 4 * s * s),
sorry,
end


#### Kevin Buzzard (Oct 13 2018 at 18:01):

although I'm not sure it's what you want, because  2 * r - 4 * s * s - 4 * s is parsed as  (2 * r - 4 * s * s) - 4 * s so you might want to worry about the 4 * s first.

#### Kevin Buzzard (Oct 13 2018 at 18:03):

But let's talk about this later. First let me show you how @ works. With the @ you need to supply _everything_, including the stuff which might not make much sense to you like the proof and all the data about the fact that the naturals are an additive right cancellative semigroup. Lean knows this already and without the @ it uses an algorithm called type class inference to find the proof in a database. That's what's going on with the square brackets.

#### Kevin Buzzard (Oct 13 2018 at 18:05):

The squiggly brackets -- Lean is saying "I'll guess these from the context". For example your goal was 2 * r - 4 * s * s - 4 * s = 1 just before the rewrite, so Lean can guess b and c because they must be the left and right hand side. And once it's guessed them, it can guess α as well, because that's the type of b and c

#### Kevin Buzzard (Oct 13 2018 at 18:06):

If you want to go with the @ you can try this:

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) : 2 * r - 4 * s * s - 4 * s = 1 :=
begin
rw ←@add_right_inj _ _ (4 * s + 4 * s * s) _ _,
sorry,
end


which says to Lean "OK I am using @ so I am going to fill in everything myself...actually why don't you fill in those four things"

#### Kevin Buzzard (Oct 13 2018 at 18:08):

This works too:

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) : 2 * r - 4 * s * s - 4 * s = 1 :=
begin
rw ←@add_right_inj ℕ _ (4 * s + 4 * s * s) (2 * r - 4 * s * s - 4 * s) 1,
sorry,
end


and here I filled in the three squiggly bracket things but I didn't do the square bracket.

#### Kevin Buzzard (Oct 13 2018 at 18:11):

Finally here is the example with everything filled in, including the term which Lean can generate automatically:

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) : 2 * r - 4 * s * s - 4 * s = 1 :=
begin
let abcde : add_right_cancel_semigroup ℕ, -- two goals now
apply_instance, -- the new one just got closed
rw ←@add_right_inj ℕ abcde (4 * s + 4 * s * s) (2 * r - 4 * s * s - 4 * s) 1,
sorry,
end


The weird  apply_instance line means "explicitly apply the type class inference machine to solve this goal". It's the explicit tactic which means "run the square bracket machine to produce the term of this type"

#### Kevin Buzzard (Oct 13 2018 at 18:17):

So that's the story of @ in a nutshell. But what you might need advice on is how to solve your goal. If you let me cheat and work over the integers then here is the easiest way for a mathematician:

import tactic.ring

example (r : ℤ) (s : ℤ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) : 2 * r - 4 * s * s - 4 * s = 1 :=
begin
rw Hrs,
ring,
end


However subtraction on the naturals is not so well-behaved (did anyone point out to you that 2-3=0? ) and ring can't handle it (the naturals aren't a ring, and ring isn't always so clever in the naturals case)

#### Kevin Buzzard (Oct 13 2018 at 18:18):

But something you have to learn about Lean is that almost every lemma you want is already there (e.g. a+b=c -> a=c-b and all the variants will be there).

#### Kevin Buzzard (Oct 13 2018 at 18:25):

So here's a more low-level proof:

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) :
2 * r - 4 * s * s - 4 * s = 1 :=
begin
rw Hrs,
simp,
end


#### Kevin Buzzard (Oct 13 2018 at 18:26):

The strategy is to get rid of all the subtractions and then use simp, which is good at proving some equalities. Subtraction on naturals is a bit hairy though, that's why this was an effort. It would not surprise me if Kenny Chris or Mario could come up with a shorter proof.

#### Chris Hughes (Oct 13 2018 at 18:40):

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) :
2 * r - 4 * s * s - 4 * s = 1 :=


#### Kevin Buzzard (Oct 13 2018 at 18:43):

How do you find a proof like that @Chris Hughes ?

#### Kevin Buzzard (Oct 13 2018 at 18:43):

I was surprised rw Hrs;ring didn't work

#### Chris Hughes (Oct 13 2018 at 18:53):

First try to substitute in Hrs as quickly as possible. Then simp, look at the goal and see what else needs to be done.

#### Kevin Buzzard (Oct 13 2018 at 18:54):

I did that and got the horrible 1 + (4 * s + 4 * s * s) - 4 * s * s - 4 * s = 1

#### Kevin Buzzard (Oct 13 2018 at 18:55):

((1 + (4 * s + 4 * s * s)) - 4 * s * s) - 4 * s = 1

#### Kenny Lau (Oct 13 2018 at 19:29):

@Chris Hughes

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) :
2 * r - 4 * s * s - 4 * s = 1 :=


#### Kevin Buzzard (Oct 13 2018 at 19:41):

@Abhimanyu Pallavi Sudhir Kenny managed to do it in three rewrites; you can click around in the middle of his rewrite line to see what's going on.

#### Abhimanyu Pallavi Sudhir (Oct 13 2018 at 19:46):

Oh, I know how to do the proof -- I just wanted to learn about @, __inst, etc. Your crash course is helpful, thanks!

#### Kevin Buzzard (Oct 13 2018 at 20:58):

The weird _inst_ variables are the ones which are generated by the type class inference machine

#### Kevin Buzzard (Oct 13 2018 at 21:11):

If you ever see the word "instance" in Lean code it just means "definition, and add it to the type class inference machine too"

#### Kevin Buzzard (Oct 13 2018 at 21:12):

So for example the construction of the ring structure on the integers will be defined as an instance rather than a definition, and then any lemmas about rings will automatically apply to the integers

Last updated: May 13 2021 at 00:41 UTC