How do you use the Quaternion type?

Stream: mathlib4

[Mr Proof]

I would like to use the quaternion type to multiply (2+3i+4j+5k) by (6+7i+8j+9k). Any idea how to do this? I can't find a constructor for quaternions anywhere.

My attempt:

import Mathlib

open Quaternion

def x:ℍ := {re:= 1, imI:= 2, imJ:= 3, imK:= 4}
def y:ℍ := {re:= 5, imI:= 6, imJ:= 7, imK:= 8}

def z:ℍ := x * y

#eval z /-doesn't work-/

[Ruben Van de Velde]

That sounds correct, but I don't think you should expect #eval to work on quaternions at all

[Mr Proof]

Yeah, it doesn't seem to work with complex numbers either.
Are there any other tools inside lean that can give the answer?
Or can I override #eval to add this functionality perhaps?

[Mr Proof]

Also it is failing with Real

import Mathlib

def k:Real := 5

#eval k

Giving error:

Real.ofCauchy (sorry /- 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, ... -/)

[Paul Rowe]

Reals are represented as cauchy sequences. There is no clear way to display a real number. Notice that in your case Lean is revealing that 5 is represented by the constant cauchy sequence of all 5s.

In your code above, you should get that z = {re:= -60, imI:= 12, imJ:= 30, imK:= 24}. You can verify this works explicitly:

example : z = {re:= -60, imI:= 12, imJ:= 30, imK:= 24} := by
  ext <;> simp [z, x, y] <;> ring

But since real numbers (and hence complex and quaternions) are not, in general, computable, you will encounter friction when doing explicit computations.

[Paul Rowe]

In fact, I didn't do the multiplication by hand. I tricked Lean into revealing the constant cauchy sequences it computed for z by trying

#eval z.re
#eval z.imI
#eval z.imJ
#eval z.imK

which yield errors like you reported, but it's an informative one!

[Kevin Buzzard]

If you want to #eval you need to use a field which is evalable. Try doing stuff over the rationals instead.

[Paul Rowe]

I think the original point was to learn how to work with quaternions which are inherently tied to the reals (at least as implemented). I suppose a helpful learning project could be to define the "rational quaternions" from scratch and prove a few things about them.

[Paul Rowe]

Oh I actually see docs#Quaternion which defines quaternions over a type. So maybe the thing to do is not to use ℍ, but to use Quaternion Rat instead?

[Ruben Van de Velde]

Yeah, ℍ is Quaternion Real

[Paul Rowe]

Quaternion Rat is also missing a Repr instance so is not currently evalable. Would it be hard to define one so the result could be displayed?

[Kevin Buzzard]

I conjecture that it would be very easy, it just wouldn't be easy for me :-) Maybe go and look at how Repr is defined for types like Rat and then just copy stuff?

[Eric Wieser]

Do we have a repr for Complex? That probably makes more sense to copy

[Paul Rowe]

instance : Repr (Quaternion ℚ) :=
  { reprPrec := fun q _ => s!"{repr q.re} + {repr q.imI}i + {repr q.imJ}j + {repr q.imK}k" }

Just to pick a mathy representation. This works. And if you add this to the code above making x, y, z : Quaternion Rat then it does the eval.

[Paul Rowe]

Or a truly working example:

import Mathlib

open Quaternion

instance : Repr (Quaternion ℚ) :=
  { reprPrec := fun q _ => s!"{repr q.re} + {repr q.imI}i + {repr q.imJ}j + {repr q.imK}k" }

def x:Quaternion ℚ := {re:= 1, imI:= 2, imJ:= 3, imK:= 4}
def y:Quaternion ℚ := {re:= 5, imI:= 6, imJ:= 7, imK:= 8}
#eval x

def z:Quaternion ℚ := x * y -- -60 + 12i + 30j + 24k
#eval z

[Kevin Buzzard]

Once you're happy with it, feel free to PR! Do you have push access to non-master branches of mathlib? If not then let me know your github userid.

[Paul Rowe]

Eric Wieser said:

Do we have a repr for Complex? That probably makes more sense to copy

I think the problem is that Complex truly is tied to Real which we can't expect to have a Repr (unless I'm wrong).

[Eric Wieser]

Well, docs#Complex.instRepr exists

[Paul Rowe]

Kevin Buzzard said:

Once you're happy with it, feel free to PR! Do you have push access to non-master branches of mathlib? If not then let me know your github userid.

I don't have push access to non-master branches. This seems like a pretty safe way to test those waters. My github id is pauldavidrowe

[Eric Wieser]

It's uglier, but I think the repr should be { re := _, im_i := _, im_j := _, im_k := _ } or similar; Repr instances are expected to be roughly valid syntax

[Eric Wieser]

I've sent you an invite @Paul Rowe

[Paul Rowe]

I agree. I was being a little too cutesy.

[Eric Wieser]

Well, the other way to take this is "there ought to be matching notation", but that sounds like a problem for another time

[Eric Wieser]

You could argue that Quaternion should be built like Complex, and use r + x*I + y*J + z*K; if you want to pursue that, perhaps worth creating a new thread and pinging Yury G. Kudryashov

[Mr Proof]

Thanks, that works great:

import Mathlib
open Quaternion

instance : Repr (Quaternion ℚ) :=
  { reprPrec := fun q _ => s!"{repr q.re} + {repr q.imI}i + {repr q.imJ}j + {repr q.imK}k" }

instance : Repr (Quaternion ℤ) :=
  { reprPrec := fun q _ => s!"{repr q.re} + {repr q.imI}i + {repr q.imJ}j + {repr q.imK}k" }

/- didn't know how to do the same for complexified quaternions-/

def x:ℍ[ℤ] := {re:= 1, imI:= 2, imJ:= 3, imK:= 4}
def y:ℍ[ℤ] := {re:= 5, imI:= 6, imJ:= 7, imK:= 8}

def z:ℍ[ℤ] := x * y

#eval z

Some further points:
I wonder is it possible to also use ℂ[ℚ] and ℂ[ℤ] ? . Should there be a way to display complexified quaternions ℍ[ℂ] just for completeness?

Or if we want to go a bit crazy:

def p:ℍ[ℍ[ℤ]] := {re:=x, imI:=y, imJ:= x, imK:= y}
#eval p /-how would this be displayed?-/

[Eric Wieser]

I don't think quaternions make sense over non-commutative rings

[Eric Wieser]

We have docs#GaussianInt for ℂ[ℤ]

[Paul Rowe]

It turns out I was mistaken earlier. When the infoview shows the Cauchy sequence for a real number, it’s not an error. That’s just how real numbers are displayed.

I’m no longer at a computer, but in another thread in this stream you can see a more general way to do it that will work for reals and complex too. But it will still show you all the messy Cauchy sequence stuff.

[Mr Proof]

Yes, I just thought it was an error because it had the word "sorry" in it. I'm sure there's a good reason why reals are displayed like that. As a newcomer I'm not totally sure why it needs to display so many repeated 5's /- 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, ... -/ but I'm sure there's a good reason :thinking:

[Mario Carneiro]

it's displaying the underlying cauchy sequence, which is a converging sequence of rational numbers

[Mario Carneiro]

for rational numbers this is just the constant sequence, although of course just because you see a bunch of 5's doesn't mean it doesn't eventually converge to 6 instead

[Mr Proof]

Yes, I get the principle. And not knowing the internals I can't criticise. But I'm just wondering if there aren't some simple cases where it can tell the number is rational and then it doesn't have to write it out as a sequence.

[Paul Rowe]

The problem is that you can’t know what it converges to without considering the whole sequence which involves non-trivial reasoning.

[Paul Rowe]

That is, there’s no easy test to know if a Cauchy sequence converges to some rational number that should be displayed more simply instead.

[Mr Proof]

I guess so. If you're defining the sequence by a general algorithm then the problem is unsolvable in general. But I mean there might be simple cases, for example where I just defined z:Real = 3. In those special cases would it not be possible?
Just theoretically I mean.

[Paul Rowe]

The issue is that the display function either has to work for all reals, or else you need a decidable algorithm to determine which thing to display. It doesn’t matter that you just defined it as a constant; it immediately get represented as a Cauchy sequence and the display code doesn’t know anything else.

[Mr Proof]

OK, but presumably it's represented by a Cauchy sequence which contains an algorithm of how to get the next number. And can we not inspect that algorithm to see if the algorithm is a simple constant algorithm? Then for those special cases just write that constant?

In terms of usefulness, I think the usefullness of being able to display a shortened version in very special cases would outweigh the fact that the algorithm would not detect all rationals and default to the original sequence?

[Mario Carneiro]

but presumably it's represented by a Cauchy sequence which contains an algorithm of how to get the next number.

No, in lean functions cannot inspect the algorithms of their inputs, this would be unsound

[Mario Carneiro]

e.g. if you could do this you could prove there are countably many reals

[Mario Carneiro]

if you wanted to do this you would need to use an entirely different data structure which allows inspection. For example... Rat

[Paul Rowe]

If your goal is play with quaternions, defining (computable) functions, and inspecting results, I strongly suggest restricting to quaternions over rationals. If you really want to prove general theorems, you can use the “full” quaternions and these issues around eval are probably irrelevant.

[Mr Proof]

Yes, it seems the problem is harder than I first thought. I suppose the correct solution is not do things like z:Real=5 when you don't need to use a real.

On a different note. If I was going to format a Cauchy sequence do you think this is a good notation:

⟨ 1, 1/2, 3/4, 2/3,..⟩

Also I notice that actually you can do ℍ[Float] but the + * operations don't seem to work on it.

[Eric Wieser]

Mario Carneiro said:

but presumably it's represented by a Cauchy sequence which contains an algorithm of how to get the next number.

No, in lean functions cannot inspect the algorithms of their inputs, this would be unsound

The instance is already unsafe, so this seems totally possible

[Mr Proof]

Some more tests:

instance : Repr (Quaternion GaussianInt ) :=
  { reprPrec := fun q _ => s!"{repr q.re} + {repr q.imI}i + {repr q.imJ}j + {repr q.imK}k" }

instance : Repr (Quaternion (Quaternion ℤ) ) :=
  { reprPrec := fun q _ => s!"({repr q.re}) + ({repr q.imI})I + ({repr q.imJ})J + ({repr q.imK})K" }

def q:ℍ[ℤ]:={re:= 1, imI:= 2, imJ:= 3, imK:= 4}
def r:ℍ[ℍ[ℤ]]:={re:= q, imI:= q, imJ:= q, imK:= q}
def a:GaussianInt := {re:=3,im:=5}
def P:ℍ[GaussianInt] :={re:= a, imI:= a, imJ:= a, imK:= a}

#eval q /-1 + 2i + 3j + 4k-/
#eval r/-(1 + 2i + 3j + 4k) + (1 + 2i + 3j + 4k)I + (1 + 2i + 3j + 4k)J + (1 + 2i + 3j + 4k)K-/
#eval P /-⟨3, 5⟩ + ⟨3, 5⟩i + ⟨3, 5⟩j + ⟨3, 5⟩k-/

Not that ℍ[ℍ[ℤ]] is well defined but it's nice to know that nesting works.

[Eric Wieser]

If you want a challenge related to nested quaternion objects, you could formalize John Selig's results about exponentiation of dual quaternions (DualNumber (Quaternion R))

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

but presumably it's represented by a Cauchy sequence which contains an algorithm of how to get the next number.

No, in lean functions cannot inspect the algorithms of their inputs, this would be unsound

The instance is already unsafe, so this seems totally possible

It's also impossible difficult from a technical standpoint, there is no interface for introspecting on closure values. You could write one from scratch with a lot of care using C code. I did some work on that a while back, packaging lean objects into a lean_external object so they can be explicitly interacted with as data structures, but it's tricky to ensure that the reference counts are handled directly when the compiler is handling some but not all of the inc/dec stuff

[Mr Proof]

Eric Wieser said:

If you want a challenge related to nested quaternion objects, you could formalize John Selig's results about exponentiation of dual quaternions (DualNumber (Quaternion R))

Only thing I know about dual numbers is they're a special case of Grassmann numbers which is used in supersymmetry calculations. That would be a another nice case to formalise. The #eval for them would look like:

a + bθ₁ + cθ₂ + dθ₁θ₂

for example. Maybe this is already possible as some subset of non-commutable algebra in Lean. Then we could define superfields like φ(x,θ₁,θ₂)