# Zulip Chat Archive

## 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