Zulip Chat Archive

Stream: new members

Topic: Using @add_right_inj


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 16:40):

Can you post a MWE with the error?

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 16:43):

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

view this post on Zulip 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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 13 2018 at 16:50):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 13 2018 at 16:51):

so the first argument is the type

view this post on Zulip 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 @

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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
  apply nat.sub_eq_of_eq_add,
  apply nat.sub_eq_of_eq_add,
  rw Hrs,
  simp,
end

view this post on Zulip 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.

view this post on Zulip 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 :=
by simp [nat.sub_sub, nat.add_sub_cancel, Hrs]

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 18:43):

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

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 18:43):

I was surprised rw Hrs;ring didn't work

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 18:55):

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

view this post on Zulip 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 :=
by rw [nat.sub_sub, Hrs, nat.add_sub_cancel_left]

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Oct 13 2018 at 20:58):

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

view this post on Zulip 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"

view this post on Zulip 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