Decasting and distributing to simplify

Stream: new members

[Shadman Sakib]

import data.complex.basic

open complex

example (a b: ℤ) : 2 * (-(a : ℂ) - ↑(1 / 2) + (b - ↑(1 / 2)) * I) = -2 * a - 1 + 2 * b * I - I :=
begin
  sorry,
end

[Shadman Sakib]

How can I decast the 1/2 to simply use ring to prove the goal?

[Kyle Miller]

Do you intend for that to be 1 / 2 using integer division? The norm_num tactic will reduce each 1 / 2 to 0 (and I think it's not true unless they're both an actual one-half).

[Adam Topaz]

The general strategy for such things:

import data.complex.basic

open complex

example (a b: ℤ) : 2 * (-(a : ℂ) - (1 / 2) + (b - (1 / 2)) * I) = -2 * a - 1 + 2 * b * I - I :=
begin
  field_simp,
  ring,
end

[Adam Topaz]

(Note I removed the coercions.

[Kyle Miller]

Illustrating the problem:

example : ((1 / 2 : ℤ) : ℂ) = (0 : ℂ) := rfl

[Shadman Sakib]

No the 1/2 should be coerced, but I didn't know (1 / 2 : ℤ) : ℂ) = (0 : ℂ)

[Shadman Sakib]

Thank you for your help

[Johan Commelin]

Should it be coerced from the rationals to $\mathbb C$?

[Kyle Miller]

Because in that case, this works:

example (a b: ℤ) : 2 * (-(a : ℂ) - (1 / 2 : ℚ) + (b - (1 / 2 : ℚ)) * I) = -2 * a - 1 + 2 * b * I - I :=
begin
  field_simp,
  ring,
end

[Kyle Miller]

I tend to find the way type ascriptions work to be somewhat counter-intuitive (though it has a logic to it). Since division has type a -> a -> a, by saying you want the result to be a rational, it causes 1 and 2 to be a rational as well. They say casting goes "outside-in".

[Adam Topaz]

You're subtracting 1/2 from something that lean knows is a complex number, so lean should know to coerce it to a complex number without any additional arrows