Arithmetic in ℂ

Stream: new members

[Leo Mayer]

I'm working through exercises in "Linear Algebra done right" with @Vasily Ilin, and one of them was "verify this expression is a third root of unity." I have a solution which works but is pretty awful:

import tactic
import data.complex.basic

open complex

example : ((-1 + (real.sqrt 3 : ℂ)*I)/2)^3 = 1 :=
begin
  have h : (real.sqrt(3) : ℂ)*(real.sqrt(3) : ℂ) = 3,
  norm_cast,
  apply real.mul_self_sqrt,
  norm_cast,
  exact nat.zero_le 3,
  calc
      ((-1 + (real.sqrt 3 : ℂ)*I)/2)^3 =
      (1 / 8)*(-1 + 3*(real.sqrt(3)*I) + ((I*I)*(real.sqrt(3)*real.sqrt(3)))*(-3+(real.sqrt(3)*I))) : by ring
      ... = (1 / 8)*(-1 + 3*(real.sqrt(3)*I) + (I*I*3)*(-3+(real.sqrt(3)*I))) : by rw h
      ... = (1 / 8)*(-1 + 3*(real.sqrt(3)*I) + (-1*3)*(-3+(real.sqrt(3)*I))) : by rw I_mul_I
      ... = 1 : by ring,
end

Is there a more pleasant way to do this?

[Alex J. Best]

Slightly random looking, but this works without any by hand calculation:

import tactic
import data.complex.basic

open complex

example : ((-1 + (real.sqrt 3 : ℂ)*I)/2)^3 = 1 :=
begin
  field_simp,
  ring_nf,
  norm_num,
  ring_nf,
  norm_cast,
  norm_num,
end

[Leo Mayer]

Thanks! Good to know that norm_num knows about squaring square roots!
So does norm_cast move the coercions as high up the syntax tree as possible, so that we can, eg, use lemmas about arithmetic in ℕ, ℤ, ℝ, etc before having to reason in ℂ?

[Alex J. Best]

Exactly, this lets norm num apply what it/simp knows about squaring real square roots, rather than squares of coercions

[Leo Mayer]

It's sad that this doesn't work:

example : (real.sqrt 3)^3 = 3*(real.sqrt 3) :=
begin
  norm_num,
end

or else the proof could maybe be shorter using ring_nf SOP?

[Alex J. Best]

Might be worth adding the norm_num lemma that (real.sqrt a) ^ n = a ^ (n / 2) * (real.sqrt a) ^ (n % 2) then

[Mario Carneiro]

that's not how norm_num works, it doesn't have lemmas like that

[Mario Carneiro]

norm_num evaluates things to a normal form, so you would need to define what normal form means for sqrt expressions

[Mario Carneiro]

this kind of reasoning is closest to what ring could do

[Mario Carneiro]

you need to know some facts about sqrt, and I think linear_combination can handle it

[Mario Carneiro]

example : (real.sqrt 3)^3 = 3*(real.sqrt 3) :=
begin
  have := @real.sq_sqrt 3 (by norm_num),
  linear_combination (this, real.sqrt 3),
end

[Mario Carneiro]

when #14229 lands it can be written by linear_combination real.sqrt 3 * @real.sq_sqrt 3 (by norm_num)

[Alex J. Best]

A lemma like that could be a simp lemma under the side condition that n is at least 2, which norm num could then discharge is what I'm thinking. Or would that also not happen the way I hope?

[Alex J. Best]

The normal form would then naturally be no natural powers on sqrts?

[Mario Carneiro]

And here's a proof of your original problem

example : ((-1 + (real.sqrt 3 : ℂ)*I)/2)^3 = 1 :=
begin
  have : (real.sqrt 3 : ℂ)^2 * I^2 = -3,
  { simp, exact_mod_cast @real.sq_sqrt 3 (by norm_num) },
  linear_combination (this, (-3+(real.sqrt(3)*I))/8),
end

[Mario Carneiro]

@Alex J. Best norm_num calls simp, which is why it was able to solve some simple questions about sqrt, but it doesn't really understand sqrt at all. norm_num normal form is not like simp normal form, in that the latter is defined simply as "whatever is not modified by simp" and the former has an explicit definition per type (for example, a normal form for nat is a numeral expression like 37). If you allow sqrts, then the normal form is something like "arbitrary + * ^ combinations of sqrt operations" and it sounds like a nightmare to decide equality on that grammar

[Mario Carneiro]

sqrt 2 * sqrt 3 = sqrt 6 has no natural powers on sqrts but they are distinct normal forms by your definition