Some simple structs and arithmetic in Lean4

StructsAndArith.lean

instance HasPowFloatNat : HasPow Float Nat := ⟨λ x y => x ^ (y.toFloat)⟩


structure Cartesian :=
(x : Float)
(y : Float)

structure Polar :=
(r : Float)
(θ : Float)



namespace Cartesian

def distance (p1 p2 : Cartesian) : Float :=
((p1.x - p2.x) ^ 2 + (p1.y - p2.y) ^ 2).sqrt

def toPolar (p : Cartesian) : Polar :=
{r := (p.x ^ 2 + p.y ^ 2).sqrt,
 θ := if p.x == 0 then 90 else (p.y / p.x).atan
}

end Cartesian

namespace Polar

def distance (p1 p2 : Polar) : Float :=
(p1.r ^ 2 + p2.r ^ 2 - (2 * p1.r * p2.r * (p2.θ - p1.θ).cos)).sqrt

def toCartesian (p : Polar) : Cartesian :=
{x := p.r * p.θ.cos, 
 y := p.r * p.θ.sin
}

end Polar

def main : IO Unit := do
let p1 : Cartesian := {x := 3, y := 4};
let p2 : Polar := p1.toPolar;
IO.println $ "(3,4) in cartesian is (" ++ p2.r.toString ++ ", " ++ p2.θ.toString ++ ") in polar";
pure ()