Better automation for manipulating complex numbers?

Stream: mathlib4

[Jonathan Laurent]

I have found the norm_num and simp tactics disappointing when dealing with complex numbers. For example, consider proving the following property:

example: (1 + Complex.I) / (1 - Complex.I) = Complex.I := by sorry

One would expect norm_num or something like simp +arith [Complex.ext_iff, Complex.div_im, Complex.div_re] to just work but it does not. My current solution is:

example: (1 + Complex.I) / (1 - Complex.I) = Complex.I := by
  have: (1 - Complex.I) ≠ 0 := by
    by_contra h
    apply_fun Complex.re at h
    simp at *
  field_simp
  ring_nf ; simp ; ring

Can we do better? Am I missing some idioms/tactics for manipulating complex numbers?

[Aaron Liu]

You can write a norm_num extension

[Eric Wieser]

Complex numbers are not numerals according to norm_num, so that doesn't really sound possible

[Eric Wieser]

You'd have to fundamentally rewrite norm_num itself

[Kevin Buzzard]

@Sidharth Hariharan does your extension of norm_num do this?

[Jireh Loreaux]

This is how I would do it. Note that we seem to be honestly missing the lemma Complex.I_ne_one.

import Mathlib

@[simp]
lemma Complex.I_ne_one : I ≠ 1 :=
  fun h ↦ by simp [Complex.ext_iff] at h

lemma Complex.one_add_I_div_one_sub_I : (1 + I) / (1 - I) = I := by
  have : (1 - I) ≠ 0 := by simp [sub_ne_zero, ne_comm (b := I)]
  field_simp [Complex.ext_iff]

[Sidharth Hariharan]

Kevin Buzzard said:

Sidharth Hariharan does your extension of norm_num do this?

Apologies for the late response, I must've missed this message! Yes, our tactic does do this.

[Sidharth Hariharan]

For context, @Heather Macbeth, @Edison Xie and I have been working on a tactic called norm_numI that performs norm_num-like simplifications in $\mathbb{C}$. Roughly speaking, it works by splitting into real and imaginary parts and performing component-wise simplifications using component-wise formulae for addition, multiplication, inversion, negation and conjugation.

[Edison Xie]

Sidharth Hariharan said:

For context, Heather Macbeth, Edison Xie and I have been working on a tactic called norm_numI that performs norm_num-like simplifications in $\mathbb{C}$. Roughly speaking, it works by splitting into real and imaginary parts and performing component-wise simplifications using component-wise formulae for addition, multiplication, inversion, negation and conjugation.

It could also do powers :))

[Sidharth Hariharan]

Our tactic currently handles a lot of expressions. The following all work:

-- @**Jonathan Laurent**'s example
example : (1 + I) / (1 - I) = I := by norm_numI
-- Misc examples
example : (1:ℂ) = 1 + 0 * I := by norm_numI
example : (1.5:ℂ) = 3 / 2 + 0 * I := by norm_numI
example : (1.0:ℂ) + 0.5 = 3/2 := by norm_numI
example : (conj (3 + 4 * I) : ℂ) * (3 + 4 * I) = 25 := by norm_numI
example : (1 + 2 * I) - (1 + 2 * I) = 0 := by norm_numI
example : (3 + I : ℂ)^2 = 8 + 6 * I := by norm_numI
example : (3 + 4 * I)⁻¹ * (3 + 4 * I) = 1 := by norm_numI

We have more examples.

There are, however, a few things that don't quite work yet:

example : I ≠ 1 := by norm_numI -- doesn't work because goal is not an equality
example : I ^ (-1) = - I := by norm_numI -- can't handle -1 in the exponent
example : I ^ (3 + 4) = 1 := by norm_numI -- isn't adding up 3 and 4 in the exponent

Edison and I are currently a bit busy preparing for exams and writing our Master's theses, but we're working on this tactic on the side

[Edison Xie]

I think Zpow is on its way but it just takes a bit of time :(

[Edison Xie]

and it's not impossible for norm_numI to handle inequalities as well we'll see where we can get and the basic stuff should soon (within 2 months) be an PR to mathlib

[Sabbir Rahman]

Would norm_numI be a completely new tactic? I think similar need for a tactic/norm_num expansion will happen if someone tries to work with quaternions. Just a thought.

[Sidharth Hariharan]

At the moment, it is a completely new tactic.

We have been discussing the sort of generality in which we’d want such automation to exist: quaternions are one setting, number fields are another—eg. in $\mathbb{Q}\!\left[\sqrt{2}\right]$ we’d want to treat $\sqrt{2}$ as a symbol with the added relation that its square is $2$. I think we can adapt the design of our tactic to a more general framework for such automation, but I personally have no idea how to do this/whether this would become another tactic entirely (“extension_simp” maybe?) or an extension of norm_num/norm_numI