Using @add_right_inj

Stream: new members

[Abhimanyu Pallavi Sudhir]

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]

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]

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]

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]

Can you post a MWE with the error?

[Kevin Buzzard]

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]

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

[Abhimanyu Pallavi Sudhir]

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]

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

[Kenny Lau]

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]

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]

so the first argument is the type

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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
  apply nat.sub_eq_of_eq_add,
  apply nat.sub_eq_of_eq_add,
  rw Hrs,
  simp,
end

[Kevin Buzzard]

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]

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) :
  2 * r - 4 * s * s - 4 * s = 1 :=
by simp [nat.sub_sub, nat.add_sub_cancel, Hrs]

[Kevin Buzzard]

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

[Kevin Buzzard]

I was surprised rw Hrs;ring didn't work

[Chris Hughes]

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]

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

[Kevin Buzzard]

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

[Kenny Lau]

@Chris Hughes

example (r : ℕ) (s : ℕ) (Hrs : 2 * r = 4 * s * s + 4 * s + 1) :
  2 * r - 4 * s * s - 4 * s = 1 :=
by rw [nat.sub_sub, Hrs, nat.add_sub_cancel_left]

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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