complex/real coercion nightmare

Stream: Is there code for X?

[Alex Kontorovich]

In math, we regularly write (imprecise) things like: $z + \bar z = 2 \Re z$, where $$ z \in \C $$. It's imprecise because do I want this equation to be interpreted over $$\C$$, or am I implicitly applying some coercion to $\R$ on the left, with a proof that the imaginary part is zero, etc. What's the "right" way in mathlib to deal with such issues? For example, one can show:

example (z : ℂ) : z + conj z = 2 * z.re := by
  -- simp -- does nothing
  -- exact? -- fails
  ext
  · simp only [Complex.add_re, Complex.conj_re]
    ring_nf
    simp
  · simp only [Complex.add_im, Complex.conj_im]
    ring_nf
    simp

This of course coerces the right side to $$\C$$, so it can be compared with the left side. Note that simp and exact? fail (but copilot completes the proof by itself!... after suggesting the ugly ext...)

Similarly, one can write:

example (z : ℂ) : (z + conj z).re = 2 * z.re := by
  -- exact? -- fails
  simp only [Complex.add_re, Complex.conj_re]
  ring

but this is not the "spirit" of the math version, because I shouldn't be taking real parts on the left, I should be doing some coercion together with a proof that the imaginary part is zero. What's the "right" way to express such ideas, and what tactics make it all work?... Thanks!

[Jireh Loreaux]

I'm not necessarily saying this is the "best" way, but if you wanted, you can use docs#realPart instead of docs#Complex.re. This is (z + conj z) / 2 : ℝ (modulo fiddly details).

[Kyle Miller]

Maybe z + conj z = (2 * z.re :) (which should be the same as z + conj z = (2 * z.re : ℝ) here) captures the idea better than z + conj z = 2 * z.re? This is saying that z + conj z lies in the image of the coercion from ℝ by giving an explicit witness.

[Jireh Loreaux]

For example, this works:

import Mathlib.Data.Complex.Module

open ComplexStarModule ComplexConjugate

example (z : ℂ) : z + conj z = 2 * ℜ z := by
  simp [mul_add]

[Kyle Miller]

The norm_cast tactic by the way should be able to "real-ize" expressions and equalities that are morally real, by pushing the cast outward as far as possible. (I think I don't really understand the question actually. Maybe Jireh's suggestion gets at it better.)

[Anatole Dedecker]

I have no good solution but this is definitely something we need to think about, it makes working with Hilbert spaces quite annoying for bad reasons sometimes

[Jireh Loreaux]

Sorry, I realized what I said was kind of stupid, but I'll try to have a better answer later.

[Yaël Dillies]

Not sure how relevant this is to your case, but I recently had to formalise a bunch of inequalities between real numbers, whose intermediate steps involved manipulating complex number expressions. The only way I've found to formalise those is by talking about the norm of the coercion of the LHS being smaller than some sum of norms being equal to the RHS.

[Jireh Loreaux]

Obviously this isn't simpler than what you had, but I think these additional declarations are things we would probably want, and once we have those, the original result is quite simple.

import Mathlib.Data.Complex.Module

open ComplexStarModule Complex ComplexConjugate

/-- The natural `ℝ`-linear equivalence between `selfAdjoint ℂ` and `ℝ`. -/
@[simps apply symm_apply]
def Complex.selfAdjointEquiv : selfAdjoint ℂ ≃ₗ[ℝ] ℝ where
  toFun := fun z ↦ (z : ℂ).re
  invFun := fun x ↦ ⟨x, conj_ofReal x⟩
  left_inv := fun z ↦ Subtype.ext <| conj_eq_iff_re.mp z.property.star_eq
  right_inv := fun x ↦ rfl
  map_add' := by simp
  map_smul' := by simp

lemma Complex.coe_selfAdjointEquiv (z : selfAdjoint ℂ) :
    (selfAdjointEquiv z : ℂ) = z := by
  simpa [-realPart_apply_coe, selfAdjointEquiv_symm_apply]
    using (congr_arg Subtype.val <| Complex.selfAdjointEquiv.left_inv z)

@[simp]
lemma realPart_ofReal (r : ℝ) : (ℜ (r : ℂ) : ℂ) = r := by
  simp only [realPart_apply_coe, conj_ofReal, star_def, ←two_smul ℝ (r : ℂ)]
  simp

@[simp]
lemma imaginaryPart_ofReal (r : ℝ) : ℑ (r : ℂ) = 0 := by
  ext1; simp [conj_ofReal]

lemma Complex.coe_realPart (z : ℂ) : (ℜ z : ℂ) = z.re := by
  nth_rw 1 [←re_add_im z]
  rw [map_add, AddSubmonoid.coe_add, mul_comm, ←smul_eq_mul, realPart_I_smul]
  simp [-realPart_apply_coe]

example (z : ℂ) : z + conj z = 2 * z.re := calc
  z + conj z = 2 * ℜ z := by simp [mul_add]
  _          = 2 * z.re := by rw [Complex.coe_realPart]

Note that docs#realPart and docs#imaginaryPart are relatively new, so the API is lacking. I have just written some additional bits which may be useful for other things that are not included above; I will PR them sometime soon.

As for what is the appropriate way to phrase things. I think the first way is correct (z + conj z = z.re) although it takes place in ℂ. If you want it to take place in ℝ, then using ℜ z is at least one way to do it. For example, you can write with the above:

example (z : ℂ) : selfAdjointEquiv (ℜ z) = z.re :=
  ofReal_injective <| by
    simp only [selfAdjointEquiv_apply, Complex.coe_realPart, ofReal_re]

[Jireh Loreaux]

@Anatole Dedecker what exactly are the issues you have encountered with Hilbert spaces?

[Jireh Loreaux]

@Alex Kontorovich personally, I would probably stick with the first version you had. However, if you want an elementary proof that is close to what you might do on paper, consider this:

example (z : ℂ) : z + conj z = 2 * z.re := calc
  z + conj z = (z.re + z.im * I) + conj (z.re + z.im * I) := by simp
  _          = 2 * z.re                                   := by simp [-re_add_im, conj_ofReal]; ring

or, if you prefer to make Lean infer different things:

example (z : ℂ) : z + conj z = 2 * z.re := calc
  z + conj z = _        := let h := (re_add_im z).symm; by congrm($h + conj $h)
  _          = 2 * z.re := by simp [-re_add_im, conj_ofReal]; ring

Note the use of the features of the new congrm tactic, which is super useful for things like this.

[Jireh Loreaux]

And no ext required!

[Kevin Buzzard]

Nobody has posted a thought-free proof (i.e. only use tactics, don't need to know any lemma names):

import Mathlib.Data.Complex.Module

open ComplexStarModule ComplexConjugate

example (z : ℂ) : z + conj z = 2 * z.re := by
  ext <;> simp; ring

[Alex Kontorovich]

That's already much better, thanks! But I guess my question is more of a philosophical one, closer in spririt to @Jireh Loreaux's Complex.selfAdjointEquiv. That is, when my mind sees $z + \bar z$, it sees it as a real number... Anyway, moving on. Thanks all

[MohanadAhmed]

Does the following code look like what you want?
Basically the idea is to:

1. Define a type class of Complexes that can become reals RealizableComlpex.
2. Then define a coercion from this class to the Reals.
3. Finally for the particular case I am interested in I provide the instance of the RealizableComplex class in this case it was called instRealizable_C_add_conj

In principle all these intsances can be hidden inside a library somewhere, the use just writes the last three lines.

import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.Module

open ComplexConjugate

theorem old_conj_sumx (z : ℂ) : z + conj z = 2 * z.re := by
  ext <;> simp ; ring;
  done

class RealizableComplex (z : ℂ) : Prop where
  im_zero : z.im = 0

instance (z : ℂ) [RealizableComplex z] : CoeDep ℂ z ℝ where
  coe := z.re

def instRealizable_C_add_conj (z : ℂ) : RealizableComplex (z + conj z) where
  im_zero := by simp

theorem good_conj_sumx (z : ℂ) :  letI := instRealizable_C_add_conj z
  2 * z.re = ↑(z + conj z) := by
  simp
  ring

-- Should be hidden inside the library somewhere.
instance (z : ℂ) : RealizableComplex (z + conj z) := instRealizable_C_add_conj z

theorem better_conj_sumx (z : ℂ) : ↑(z + conj z) = 2 * z.re := by
  simp
  ring

My use case was getting the determinant of hermitian matrices to act like a real number, so I needed one instance. But if you want this to be every case where some operation on complex numbers leads to a real number this might require a lot of instances.

One point worth mentioning here. I still have to add the small arrow to nudge lean in the direction of using real numbers. I am sure someone with a bit more expertise can get rid of the need for the small arrow.

[Alex Kontorovich]

This is quite nice, thanks! Yes I suppose I'll need to make a list of things that should be "Realizable"... Or alternatively, give up on the philosophy and just apply .re... (Might be less painful...)

[Jireh Loreaux]

I don't want to rain on Mohanad's parade, but unfortunately I need to point out some issues with this approach. This isn't going to be well-behaved since the class depends on a term z : ℂ. if you have a RealizableComplex z instance, you won't get a RealizableComplex w instance for free if z = w, unless they happen to be (reducibly, I think?) defeq. What that means in practice is that wherever you see something like ↑(z + conj z) where ↑ is the CoeDep coercion above, you won't be able to rewrite the z + conj z to something else without losing the ↑, so yeah ... that sucks.

Another issue: as written, the CoeDep instance only allows Lean to find the coercion automatically (if it can find a RealizableComplex instance), but it won't pretty print the ↑ in the infoview unless we add the @[coe] attribute to Complex.re. But (I think, I'm not sure about this) I don't think we can apply it selectively, so then I think we would see ↑z for z.re for any z : ℂ. And without the coe attribute, this is just a feature of input syntax. The theorems would still be (z + conj z).re = 2 * z.re.

Then there's potential issues surrounding coercions back and forth between ℝ and ℂ. This is probably pretty minor and not actually a problem though.

[Jireh Loreaux]

@MohanadAhmed if you need a real-valued determinant for Hermitian matrices, you can always just define one. And also, do both of you know about the lift tactic? For z : ℂ, you can lift z to ℝ using hz where hz : z.im = 0. This is pretty handy, and I think may do a lot of what you might want, but maybe I'm wrong.

[MohanadAhmed]

No I didn't know about the lift tactic. So thanks for that.
But I guess since it is a tactic I cannot use it in the lemma statement right?

[Jireh Loreaux]

I mean, technically you can, but you shouldn't.

[Kevin Buzzard]

I remember noticing years ago that when defining norms on the complexes it was useful to have a bespoke function norm_sq from the complexes to the reals sending a+bi to a^2+b^2. Similarly there will be a trace function nowadays from the complexes to the reals sending a+bi to 2a (this will be defined in some huge generality). Then you just need the lemma that trace, coerced, is z + conj z and things should be fine.

[Yaël Dillies]

Kevin, I cannot understate how much I hate norm_sq :sweat_smile:

[Eric Wieser]

I'm sure the real reason that Kevin likes it is that it's computable /s

[Jireh Loreaux]

Kevin, I claim that the canonical way to spell that map is what I wrote above: selfAdjointEquiv (\Re z). Do you disagree? It sounds like you have something else in mind.

[MohanadAhmed]

Jireh Loreaux said:

Another issue: as written, the CoeDep instance only allows Lean to find the coercion automatically (if it can find a RealizableComplex instance), but it won't pretty print the ↑ in the infoview unless we add the @[coe] attribute to Complex.re. But (I think, I'm not sure about this) I don't think we can apply it selectively, so then I think we would see ↑z for z.re for any z : ℂ. And without the coe attribute, this is just a feature of input syntax. The theorems would still be (z + conj z).re = 2 * z.re.

Well I learned something new on this one. I didn't know about @[coe]. If I understood this correctly the issue you mention can be mitigated by adding an intermediary between Complex.re and CoeDep. In the code below I called it hidden_re. Now the pretty printer the coercion arrow shows up behind the z + conj z.

import Mathlib.Data.Complex.Basic
import Mathlib.Data.Complex.Module

open ComplexConjugate

class RealizableComplex (z : ℂ) : Prop where
  im_zero : z.im = 0

@[coe]
def hidden_re (z : ℂ) : ℝ := Complex.re z

@[simp] lemma hidden_re_is_re (z : ℂ) : hidden_re z = z.re := rfl

instance (z : ℂ) [RealizableComplex z] : CoeDep ℂ z ℝ where
  coe := hidden_re z

def instRealizable_C_add_conj (z : ℂ) : RealizableComplex (z + conj z) where
  im_zero := by simp

instance (z : ℂ) : RealizableComplex (z + conj z) := instRealizable_C_add_conj z

-- All above Should be hidden inside the library somewhere.

theorem better_conj_sumx (z : ℂ) : ↑(z + conj z) = 2 * z.re := by
  simp
  ring

image.png

[Jireh Loreaux]

Yes, that would solve that particular problem, but it introduces new ones. Now you either need to duplicate lemmas or else pass from hidden_re to re all the time. This would be mitigated by making it an abbrev. However, no matter what you'll always end up with hidden_re littered throughout your theorem statements, it will just be displayed as an up arrow.

[Kevin Buzzard]

Jireh Loreaux said:

Kevin, I claim that the canonical way to spell that map is what I wrote above: selfAdjointEquiv (\Re z). Do you disagree? It sounds like you have something else in mind.

I've been travelling all day and I couldn't even read your solution because of the stupid android font bug. But now I've seen it and yes it's not what I had in mind but maybe it works here. Part of the set-up fills me with dread because we'll need all of this stuff when we do the theory of CM number fields and these are not $\R$-modules so everything will need to be refactored/generalised. A CM field is a field like $\mathbb{Q}(\sqrt{2},i)$ which has a well-defined star, and a "real part" / "imaginary part" function etc etc. For a general number field there can be more than one "complex conjugation" (coming from different embeddings into the complexes) but for a CM field there is a unique one.

[Jireh Loreaux]

Kevin, for those can't you just use docs#selfAdjointPart and docs#skewAdjointPart ?

[Kevin Buzzard]

Yes! I see, the point of RealPart is registering that it's a linear map. I guess I'd want some analogue one day but not today :-)

[Jireh Loreaux]

no, they're both linear maps (in fact, probably docs#realPart should be reducible, whoops!), and in your case you would probably choose R := ℚ. The point is that in a ℂ-module we can get z = x + I • y where y is also selfAdjoint, as opposed to just considering I • y as skewAdjoint. In particular, the module is span (over ℂ) of the selfadjoint elements. Many arguments in C⋆-algebra theory first reduce to the selfadjoint case.

It's possible this is just unnecessary overhead though. I haven't determined that yet.

[Anatole Dedecker]

No, it's defined as selfAdjointPart Real, it's just a wrapper for this common case. selfAdjointPart is already linear.

[Kevin Buzzard]

Thanks for the explanations!