## Stream: maths

### Topic: basic complex number computations

#### Kevin Buzzard (Jul 11 2018 at 15:19):

@VeraZZ is doing basic computations with complex numbers and I'm still not 100% sure that we're doing it right.

If the goal looks like this:

z₁ z₂ : ℂ
⊢ ↑(z₁.re * z₂.re + z₁.im * z₂.im) + ↑(z₁.re * z₂.re + z₁.im * z₂.im) =
z₁ * conj z₂ + z₂ * conj z₁


then currently our strategy is the (probably rather inefficient)

   apply complex.ext,
simp,ring,simp,ring,


After Chris' complex number PR I realised that I am not at all sure how I'm supposed to be working with complex numbers. The strategy above is to check that two complex numbers are equal it suffices to check their real and imag parts are equal, and then use a dangerous non-finishing simp to unravel all the real and imaginary stuff followed by ring. Are there better approaches?

#### Chris Hughes (Jul 11 2018 at 15:27):

I think a non-finishing simp is not dangerous here, since ring is not sensitive to the precise state of the goal.

#### Patrick Massot (Jul 11 2018 at 15:28):

you could also define a tactic doing apply complex.ext ; {simp, ring}, and you wouldn't see simp :wink:

#### Patrick Massot (Jul 11 2018 at 15:29):

By the way, if ext cannot replace apply complex.ext then the extensionality attribute needs to be added somewhere

#### Patrick Massot (Jul 11 2018 at 15:30):

and, as usual with non finishing simp, you can use suffices : stuff := by simp,, where stuff is what you currently see as after simp

#### Chris Hughes (Jul 11 2018 at 15:32):

That sounds like a tactic I might be able to write.

#### Patrick Massot (Jul 11 2018 at 15:33):

sure: meta def cplx_ring : tactic unit := [apply complex.ext ; {simp, ring}]`

Last updated: May 19 2021 at 02:10 UTC