Avoid one `have`

Stream: new members

[Riccardo Brasca]

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]

I think you need ()

[Johan Commelin]

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

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

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]

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

[Kevin Buzzard]

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]

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]

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]

Now it is very clear :)

[Kevin Buzzard]

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]

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]

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.