I am new to Lean 4, and I was doing the exercises from Functional Programming in Lean, in particular the one about defining a length function for a custom Segment type. Here is what I came up with, for reference:
structure Point where
x : Float
y : Float
deriving Repr
structure Segment where
a : Point
b : Point
deriving Repr
def length (s : Segment) : Float :=
Float.sqrt (Float.pow dx 2 + Float.pow dy 2) where
dx := s.b.x - s.a.x
dy := s.b.y - s.a.y
def origin : Point := {x := 0, y := 0}
def p : Point := {x := 3, y := 5}
def s : Segment := Segment.mk origin p
#eval length s -- 5.830952
#eval Float.pow 5.830952 2
I would like to know how to idiomatically generalize this so Point is the type of any point in R^n for any n, and then write corresponding Segment and length definitions that make sense.
No doubt some analogue of this exists in mathlib4, but I'd like to write this basic version from scratch.
No doubt we need a type class here, perhaps something like
class Point (n : Nat) where
components : Vector Float n
deriving Repr
but I'm not sure how to then use this to define the generalizations of Segment and length.
No doubt we need a type class here
A multi-dimensional point is as much a concrete value of a data structure as a two-dimensional point. There is no canonical point per n. So keep structure here (or make it a def/abbrev).
abbrev Point (n : Nat) := Vector Float n -- no need for `deriving` this way