basic complex number computations

Stream: maths

[Kevin Buzzard]

@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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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