Representing Rational as Float (for Complex representation)

Stream: new members

[Jake Jongejans]

I'd like to introduce a small representation for the complex numbers. I have a working first version:

import Mathlib.Data.Complex.Basic

open Complex

namespace CauSeq.Completion
open CauSeq
section

variable {α : Type*} [LinearOrderedField α]
variable {β : Type*} [Ring β] (abv : β → α) [IsAbsoluteValue abv]

unsafe instance [Repr β] : Repr (Cauchy abv) where
  reprPrec r _ :=
    let seq := r.unquot
    repr (seq 100)

end
end CauSeq.Completion

namespace Real
unsafe instance : Repr ℝ where reprPrec r _ := repr r.cauchy

#eval (1 : ℝ) -- 1
end Real

namespace Complex

unsafe instance repr : Repr Complex where
  reprPrec f _p :=
    (Std.Format.bracket "⟨" · "⟩") <|
      (Std.Format.joinSep · ", ") <|
        ([f.re, f.im]).map fun i => _root_.repr i
#align complex.has_repr Complex.repr

#eval (⟨0.334534855, 0⟩ : ℂ) -- ⟨(66906971 : Rat)/200000000, 0⟩
end Complex

Why am I redefining the Real and Cauchy representations?
I do not want my representation to show me stuff like Real.ofCauchy (sorry /- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, ... -/), when I just have (1 : ℝ).

Why do I need short representations?
I am putting complex numbers in matrices, which sometimes grow beyond 4x4.

What I am trying to do (but I lack enough knowledge) is to cast the rational number (from seq 100) into a Float so the final #eval will print ⟨0.334534855, 0⟩ instead.

Is this possible? Frankly, I get kind of lost in all the cast theorems, and float is not part of Mathlib so I am having trouble finding stuff.

[Eric Wieser]

Javernus said:

Why am I redefining the Real and Cauchy representations?
I do not want my representation to show me stuff like Real.ofCauchy (sorry /- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, ... -/), when I just have (1 : ℝ).

This strategy is incorrect though; my cauchy sequence could be the number 1, repeated 101 times, followed by infinitely many zeros. This number is equal to 0, but your code prints it as 1

[Jake Jongejans]

I guess that could be the case indeed, but I am not looking for a 100% accurate strategy, only one that can net me some insights into the values I am using while using complex numbers (when I know that my complex numbers aren't a long Cauchy sequence).

I guess I posed my intentions wrong, reading back my first sentence. I suppose my complex number representation could still work, though, apart from the other alterations. Do you think it is worth it to create a PR to introduce the ⟨1, 0⟩ (or rather ⟨Real.ofCauchy (sorry /- 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, ... -/), Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/)⟩) representation? To me, it feels odd not being able to #eval any complex numbers and this would solve it.

I would still, for my own codebase and for testing, like a way to turn real or rational numbers into a float, if possible. Any pointers for that would still be much appreciated.

[Eric Wieser]

I think a PR using the long repr is fine; though I'd recommend using x + y*I as the repr

[Eric Wieser]

It's not possible to turn real numbers into a Float, but it's possible with rational numbers

[Eric Wieser]

@loogle Rat -> Float

[loogle]

:shrug: nothing found

[Jake Jongejans]

Thanks for helping out, Eric. I guess there's no Rat -> Float, but that's okay.

I'll make a PR soon to implement the imaginary number representation (with the Cauchy sequence inside). I'll edit it to show as x + y*I without any brackets. Is there anything else I should consider when making a PR? It will be my first contribution.

[Mario Carneiro]

A function for Rat -> Float is added in std4#750

[Jake Jongejans]

I have updated my code (for the imaginary number representation) to be cleaner and will be requesting access to the repository so I can put this in a PR. Thanks for the help!

unsafe instance repr : Repr Complex where
  reprPrec f _p := _root_.repr f.re ++ " + " ++ _root_.repr f.im ++ "*I"
#align complex.has_repr Complex.repr

[Eric Wieser]

I think in this case you might have to do something with the_p argument, to ensure that parentheses are added if necessary

[Jake Jongejans]

I believe I solved that now. My PR: #12427.