PartialOrder and StarOrderedRing on IsROrC

Stream: general

[MohanadAhmed]

In a previous discussion Here on using the rank_conjTranspose_mul_self and its sister lemma rank_conjTranspose_mul_self @Kevin Buzzard stated that I cannot just require IsROrC to have a PartialOrder and then StarOrderedRing. That will place two Star operations on the field!! Thus to be able to have StarOrderedRing and hence use the above theorems I must create instances inside IsROrC PartialOrder and then for `StarOrderedRing.

My attempt at doing that is below. It seems to work and I am able to successfully use the theorems. However my understanding of the Typeclass system is not that good. So my question are:

1. Is this the "right" way to make IsROrC a StarOrderedRing?
2. IsROrC applies to ℝ and ℂ . Would the instance of PartialOrder I created interfere with PartialOrder already inside the Complex ℂ for example?
3. Assume I am to submit this to Mathlib any gotchas I need to pay attention to?

Thanks

import Mathlib

variable {K} [IsROrC K]

namespace IsROrC

instance toPartialOrder : PartialOrder K :=
{
  le := fun w z => (IsROrC.re w ≤ IsROrC.re z) ∧ (IsROrC.im w = IsROrC.im z)
  le_refl := by
    intros a
    dsimp
    simp only [le_refl, and_self]
  le_trans := by
    intros a b c hab hbc
    dsimp at *
    exact ⟨ hab.1.trans hbc.1, hab.2.trans hbc.2 ⟩
  le_antisymm := by
    intros a b hab hba
    dsimp at *
    rw [IsROrC.ext_iff]
    exact ⟨ hab.1.antisymm hba.1, hab.2 ⟩ }

lemma le_def {w z: K}: w ≤ z ↔ (IsROrC.re w ≤ IsROrC.re z) ∧ (IsROrC.im w = IsROrC.im z) := by
  unfold LE.le Preorder.toLE PartialOrder.toPreorder toPartialOrder LE.le
  simp only [and_congr_left_iff]

instance toStarOrderedRing : StarOrderedRing K := by
  apply StarOrderedRing.ofNonnegIff'
  intros x y h z
  rw [le_def] at *
  simp only [map_add, add_le_add_iff_left, add_right_inj, h.1, h.2]
  intros z
  constructor
  intros h
  use Real.sqrt (IsROrC.re z)
  rw [IsROrC.ext_iff, le_def, star_def, map_zero, map_zero, conj_ofReal] at *
  simp only [mul_re, ofReal_re, ofReal_im, mul_zero, sub_zero, mul_im, zero_mul, add_zero,
    Real.mul_self_sqrt h.1, true_and, h.2.symm]
  intros h
  cases' h with s hs
  rw [hs, star_def, le_def, map_zero, map_zero]
  simp only [mul_re, conj_re, conj_im, neg_mul,
    sub_neg_eq_add, sub_neg_eq_add, ←sub_eq_add_neg, mul_im,
    ← IsROrC.norm_sq_eq_def, ← IsROrC.normSq_eq_def', IsROrC.normSq_nonneg s,
    mul_comm (im s) (re s), sub_self, eq_self ]

end IsROrC

[Yury G. Kudryashov]

Note that docs#IsROrC already extends docs#StarRing, so you can reuse star operation from there.

[Yury G. Kudryashov]

However, if you add a generic instance IsROrC.toPartialOrder, then you'll get 2 partial orders on Reals and Complex.

[Yury G. Kudryashov]

So, if you want the order to be a part of the signature, then you need to extend, e.g., PartialOrder (or LT and LE) and an axiom saying that z ≤ w ↔ re z ≤ re w ∧ im z = im w (and similarly for < if you only extend LT and LE).

[Yury G. Kudryashov]

In fact, you have 1 more option: just extend docs#StarOrderedRing and reuse existing instances for Real and Complex.

[MohanadAhmed]

Yury G. Kudryashov said:

In fact, you have 1 more option: just extend docs#StarOrderedRing and reuse existing instances for Real and Complex.

Can you point me towards an example of extending StarOrderedRing which I can try to emulate. What I did above was to a large extent emulating the Complex.partialOrder and StarOrderedRing codes?

Also what is your preferred learning resource for learning about how to deal with classes/structures?

[Yury G. Kudryashov]

I was learning by looking at mathlib code...

[Yury G. Kudryashov]

I see 3 different options.

Option 1

• Add PartialOrder K to the list of extends, replace StarRing K with StarOrderedRing K.
• Deduce from the definition of StarOrderedRing that z ≤ w ↔ re z ≤ re w ∧ im z = im w and similarly for <.
• Prove that complex numbers is a star ordred ring.
• Reuse this instance and the existing instance for real numbers in the IsROrC instances for real and complex numbers.

With this approach, you will need to relate the StarOrderedRing axiom to z ≤ w ↔ re z ≤ re w ∧ im z = im w twice (one implication for an IsROrC field, the reversed implication for complex numbers.

Option 2 (I recommend this one)

• Add PartialOrder K to the list of extends and add le_iff_re_im : z ≤ w ↔ re z ≤ re w ∧ im z = im w to the list of axioms.
• Prove StarOrderedRing instance for any IsROrC. Important: reuse existing data (PartialOrder), don't define a new one.
• Add (almost trivial) le_iff_re_im proofs to IsROrC instances for real and complex numbers.

Option 3

• Add LE K and LT K to the list of extends and add le_iff_re_im and lt_iff_re_im to the list of axioms.
• Define IsROrC.toPartialOrder reusing given LT and LE instances.
• Prove StarOrderedRing instance for any IsROrC. Important: reuse existing data (PartialOrder), don't define a new one.
• Add (almost trivial) le_iff_re_im and lt_iff_re_im proofs to IsROrC instances for real and complex numbers.

[Jireh Loreaux]

None of this (actually, I think option 3 does?) works because Real has a partial order, but Complex doesn't have one that is activated globally. Unless we want Complex to have a globally activated partial order instance, we can't make IsROrC extend PartialOrder

[Yury G. Kudryashov]

Unless we activate this instance globally, we can't turn IsROrC into a StarOrderedRing.

[Yury G. Kudryashov]

Because either way you need the [PartialOrder] argument to the class.

[Yury G. Kudryashov]

So, I suggest that we turn this instance on globally.

[Yury G. Kudryashov]

BTW, docs#StarOrderedRing.ofLeIff looks like a nice constructor. Why does it need h_add? UPD: read the source. UPD2: proved without this assumption.

[Yury G. Kudryashov]

#5639

[Jireh Loreaux]

@Yury G. Kudryashov please see my open PR about refactoring StarOrderedRing

[Jireh Loreaux]

#4871

[Jireh Loreaux]

Wait, sorry, I forgot what happened. That's a different PR. Nevermind.

[Yaël Dillies]

Personally, I like and need the order on the complexes (I'm convoluting complex-valued functions and getting a (morally) real-valued result), so I'm happy to see the instance go global.

[Alex J. Best]

I'm curious which order that induces the ordinary one on the reals has better properties though, using the real part alone, or letting complexes with nonzero imaginary part be incomparable with any other (the push forward of the nice order).

[Yaël Dillies]

Your second one is quite weak, since it's not even an ordered_add_comm_monoid! $0 ≤ 1$ but $i \not≤ i + 1$

[Jireh Loreaux]

(deleted)

[MohanadAhmed]

Hello @Yaël Dillies @Yury G. Kudryashov and @Jireh Loreaux . Just submitted PR #6210 which implements @Yury G. Kudryashov suggestion number 2 above. Any review welcome

[Eric Wieser]

It looks like you didn't actually implement the thing in the title of this thread!

[Yury G. Kudryashov]

Also, you should delete the scope that contains PartialOrder instance on Complex and turn it into a global instance.

[MohanadAhmed]

Eric Wieser said:

It looks like you didn't actually implement the thing in the title of this thread!

Yeah my bad!

[MohanadAhmed]

It seems I thought I included the code from the top of this thread but I didn't

[MohanadAhmed]

When I add PartialOrder to the extends list and a field le_iff_re_im it seems the le used on the right is from the IsROrC class not the Real numbers which is not what I want.

The error message below is

unsolved goals
K : Type ?u.1086422
E : Type ?u.1086425
inst✝ : IsROrC K
a b c : K
⊢ ↑IsROrC.re a ≤ ↑IsROrC.re b ∧ ↑IsROrC.im a = ↑IsROrC.im b → True

The arrows behind IsROrC shows that it is being sent back to K instead of staying as Real numbers!!

In the file Data.IsROrC.Basic:

open BigOperators

section

local notation "𝓚" => algebraMap ℝ _

open ComplexConjugate

variable {n: Type _}[Fintype n]
/--
This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ.
-/
class IsROrC (K : semiOutParam (Type _)) extends DenselyNormedField K, StarRing K, PartialOrder K,
    NormedAlgebra ℝ K, CompleteSpace K where
  re : K →+ ℝ
  im : K →+ ℝ
  /-- Imaginary unit in `K`. Meant to be set to `0` for `K = ℝ`. -/
  I : K
  I_re_ax : re I = 0
  I_mul_I_ax : I = 0 ∨ I * I = -1
  re_add_im_ax : ∀ z : K, 𝓚 (re z) + 𝓚 (im z) * I = z
  ofReal_re_ax : ∀ r : ℝ, re (𝓚 r) = r
  ofReal_im_ax : ∀ r : ℝ, im (𝓚 r) = 0
  mul_re_ax : ∀ z w : K, re (z * w) = re z * re w - im z * im w
  mul_im_ax : ∀ z w : K, im (z * w) = re z * im w + im z * re w
  conj_re_ax : ∀ z : K, re (conj z) = re z
  conj_im_ax : ∀ z : K, im (conj z) = -im z
  conj_I_ax : conj I = -I
  norm_sq_eq_def_ax : ∀ z : K, ‖z‖ ^ 2 = re z * re z + im z * im z
  mul_im_I_ax : ∀ z : K, im z * im I = im z
  le_iff_re_im : z ≤ w ↔ ((re z) ≤ (re w)) ∧ ((im z) = (im w))
  -- le_iff_re_im : z ≤ w ↔ (((re z):ℝ) ≤ ((re w):ℝ)) ∧ (im z) = ((im w):ℝ)
#align is_R_or_C IsROrC
end

variable {K E : Type _} [IsROrC K]

example {a b c: K} : a ≤ b → True := by
  rw [IsROrC.le_iff_re_im]
  -- unfold LE.le Preorder.toLE  PartialOrder.toPreorder IsROrC.toPartialOrder at h

#exit

[Eric Wieser]

The arrows behind IsROrC shows that it is being sent back to K instead of staying as Real numbers!!

No they don't; did you hover over them?

[MohanadAhmed]

Hopefully fixed now

[MohanadAhmed]

spoke two minutes too soon
getting failed to synthesize maxHeartbeats errors

[Jireh Loreaux]

@Eric Wieser , we want those scoped instances on ℂ to be global now, right?

[Eric Wieser]

In the interest of keeping changes small, I'd argue that the IsROrC instance should be in the same scope

[Eric Wieser]

I think making the instance global for Complex is sort of orthogonal to generalizing it to IsROrC

[Jireh Loreaux]

I don't follow. We need the following:

1. A global IsROrC ℂ instance.
2. With the change in this PR, a global PartialOrder ℂ instance (because IsROrC now extends PartialOrder)

At that point, all the data is in global instances, so why should instances that only add proofs be scoped?

[Eric Wieser]

because IsROrC now extends PartialOrder

It could instead have a toPartialOrder field that is only attribute [instance]d in a scope

[Eric Wieser]

I agree that if the PartialOrder instance is global then the rest should be too

[Anatole Dedecker]

The more I think about it the more docs#Complex.partialOrder is a reasonable order to put as a global instance (!): it's also the order coming from the star algebra structure...

[Jireh Loreaux]

I agree (but of course I'm biased about this!), especially since we know there doesn't exist an order on ℂ making it into a LinearOrderedField (by the way, do we have this result stated anywhere, maybe in counterexamples?). We should probably have a poll before we turn it on globally though. (I'll make it now)

[Jireh Loreaux]

Here is the poll

[MohanadAhmed]

@Eric Wieser
If we go with the measured approach will the IsROrC instance for Complex have to be in whole inside the ComplexOrder locale? Meaning IsROrC would not apply to Complex unless the person is willing to take the order with it right?

[Eric Wieser]

No, that's not what it would mean

[Eric Wieser]

It would mean that IsROrC.toPartialOrder and IsROrC.toStarOrderedRing would be in the ComplexOrder locale

[Jireh Loreaux]

Oh, right, Eric that's bad then. It would mean that ℝ doesn't have a globally enabled StarOrderedRing instance.

[Eric Wieser]

We could add a shortcut for R, I don't see that being an issue

[MohanadAhmed]

Probably a stupid question. But what happens Real gets two instances of StarOrderedRing?

[Eric Rodriguez]

Not much if they're definitional equal

[Eric Wieser]

Note that discussions about global orders aside, this PR is not passing CI due to timeouts

[Eric Wieser]

#6391 passes CI and leaves things in the ComplexOrder locale for now