## Stream: new members

### Topic: Avoid one have

#### Riccardo Brasca (Sep 22 2020 at 16:28):

Hello everybody. The following code works without problems.

import data.complex.basic

lemma ok (n : ℕ) (x y : ℂ) (hn : n ≠ 0) (h: ↑n*x = ↑n*y) : x = y :=
begin
have notzero : (n : ℂ) ≠ 0 := nat.cast_ne_zero.mpr hn,
exact (mul_right_inj' notzero).mp h
end


It seems to me that the introduction of the assumption notzero is useless, so I tried to do everything in one line as follows:

import data.complex.basic

lemma notok (n : ℕ) (x y : ℂ) (hn : n ≠ 0) (h: ↑n*x = ↑n*y) : x = y :=
begin
exact (mul_right_inj' nat.cast_ne_zero.mpr hn).mp h
end


But now Lean complains, with:

type mismatch at application
mul_right_inj' nat.cast_ne_zero.mpr
term
nat.cast_ne_zero.mpr
has type
?m_1 ≠ 0 → ↑?m_1 ≠ 0
but is expected to have type
?m_2 ≠ 0


I understand that the point is that I am not saying that I want to put n inside \C m but I don't see how to correct it. Or maybe the first version is just better? Thank you!

#### Johan Commelin (Sep 22 2020 at 16:32):

I think you need ()

#### Johan Commelin (Sep 22 2020 at 16:33):

@Riccardo Brasca mul_right_inj' gobbles up the next thing (separated by spaces) as its argument. But you want it to gobble up nat.cast_ne_zero.mpr hn

#### Kevin Buzzard (Sep 22 2020 at 16:33):

Functions are greedy. mul_right_inj' will just eat nat.cast_ne_zero.mpr and then complain that it didn't have the right type (which it doesn't)

#### Kevin Buzzard (Sep 22 2020 at 16:35):

If you do it backwards then you don't need to name the extra hypothesis:

import data.complex.basic

lemma ok (n : ℕ) (x y : ℂ) (hn : n ≠ 0) (h: ↑n*x = ↑n*y) : x = y :=
begin
refine (mul_right_inj' _).mp h,
exact nat.cast_ne_zero.mpr hn,
end


But there is a problem even with the brackets, right?

#### Riccardo Brasca (Sep 22 2020 at 16:36):

@Johan Commelin I tried to put () in any reasonable way, but it does not work.

#### Kevin Buzzard (Sep 22 2020 at 16:36):

The problem with your code is clear -- the problem with the bracketed version is more subtle.

#### Kevin Buzzard (Sep 22 2020 at 16:40):

import data.complex.basic

lemma ok (n : ℕ) (x y : ℂ) (hn : n ≠ 0) (h: ↑n*x = ↑n*y) : x = y :=
begin
exact (mul_right_inj' (nat.cast_ne_zero.mpr hn : (n : ℂ) ≠ 0)).mp h,
end


#### Kevin Buzzard (Sep 22 2020 at 16:41):

The problem with nat.cast_ne_zero when applied the "backwards" way is that the input is n != 0 but the output is "some casted version of n isn't zero" and Lean doesn't know where to cast it to. If you tell it explicitly with an "explicit type ascription" then it works.

#### Kevin Buzzard (Sep 22 2020 at 16:41):

Note also

import data.complex.basic

lemma ok (n : ℕ) (x y : ℂ) (hn : n ≠ 0) (h: ↑n*x = ↑n*y) : x = y :=
(mul_right_inj' (nat.cast_ne_zero.mpr hn : (n : ℂ) ≠ 0)).mp h


(you don't need begin/end, because begin/end switches from term mode to tactic mode, and then exact switches you back to term mode)

#### Riccardo Brasca (Sep 22 2020 at 16:44):

@Kevin Buzzard Yes, sure, without brackets of course it does not work. The thing I was looking for is "explicit type ascription", thank you very much!

#### Kevin Buzzard (Sep 22 2020 at 16:46):

Lean has this "elaborator" which tries to figure out the type of everything. Sometimes this is much harder than you might expect, because we don't give clues, and Lean has to remember to figure things out later. And sometimes the system demands that the elaborator answers a question it's not ready to answer, and then you get these errors. The explicit type ascriptions can fix this. Sometimes you're unlucky and you have to use an @ and then supply all fields explicitly.

#### Riccardo Brasca (Sep 22 2020 at 16:47):

I see. I guess I have to learn about @.

#### Kevin Buzzard (Sep 22 2020 at 16:47):

lemma ok (n : ℕ) (x y : ℂ) (hn : n ≠ 0) (h: ↑n*x = ↑n*y) : x = y :=
begin
exact (@mul_right_inj' ℂ _ _ _ _ (nat.cast_ne_zero.mpr hn)).mp h,
end


#### Kevin Buzzard (Sep 22 2020 at 16:48):

This also works. It avoids the type ascription because it tells mul_right_inj' that it should be a statement about complex numbers.

#### Kevin Buzzard (Sep 22 2020 at 16:52):

The output of #check @mul_right_inj' is

mul_right_inj' :
∀ {M₀ : Type u_1} [_inst_1 : cancel_monoid_with_zero M₀] {a b c : M₀}, a ≠ 0 → (a * b = a * c ↔ b = c)


and so the person who wrote that function says "You will be able to guess M_0 from other inputs; the type class inference system will find a proof that it's a cancellative monoid with zero, you'll be able to guess a,b,c from other inputs, and now if you explicitly give me a proof that a isn't zero I'll give you a proof that two things are equivalent". With the correctly bracketed version of your proof, mul_right_inj' is faced with this input "some cast isn't zero" and it's not enough to figure out that M_0 should be the complexes. The two methods I've suggested are two ways around this -- either change the proof of a != 0 so it explicitly says the type of a, or use @ and supply all inputs to the function by hand (and then just tell it that we're talking about the complex numbers and it can take care of the rest)

#### Riccardo Brasca (Sep 22 2020 at 16:54):

Now it is very clear :)

#### Kevin Buzzard (Sep 22 2020 at 16:58):

It was a big realisation for me when I realised that a lot of what is going on is extremely logical -- there is no magic involved. Learning to read the error messages was also a big breakthrough for me.

#### Riccardo Brasca (Sep 22 2020 at 17:14):

I tried the underscore, but I did not realize I had to use the version with @. I guess I should read more carefully the tutorial.

#### Kevin Buzzard (Sep 22 2020 at 17:15):

I read Theorem Proving In Lean three times, at various stages when I was learning, and each time I learnt more, but the times I learnt the most was when I was just working on projects. For example I learnt about type class inference by just trying to write the definition of a scheme.

Last updated: May 14 2021 at 21:11 UTC