如何在Lean 4中为任意n维欧几里得空间Rⁿ定义点类型并泛化线段与长度函数？

作为Lean 4新手，你想从零开始把2维点和线段泛化到任意n维的思路非常棒！你一开始尝试用类型类的方向有点偏——其实对于n维点这种本身依赖维度参数的类型，用带Nat参数的structure会更直接地道。下面一步步带你实现这个泛化版本：

1. 定义n维Point结构 #

首先我们用Nat参数n表示维度，内部用Lean自带的Vector Float n存储分量（固定长度数组刚好符合n维点的需求）：

structure Point (n : Nat) where
  components : Vector Float n
  deriving Repr  -- 自动生成打印用的Repr实例，方便调试

2. 定义同维度的Segment结构 #

线段是两个同维度的点，所以Segment也带n参数，确保两个点维度严格一致：

structure Segment (n : Nat) where
  a : Point n
  b : Point n
  deriving Repr

3. 实现n维线段的长度计算 #

欧几里得距离的计算逻辑对任意维度都通用：先算每个维度分量差的平方和，再开根号。我们可以拆分两步实现：

辅助函数：计算差的平方和

用Vector.zipWith把两个点的分量一一配对，再用foldl累加所有平方值：

def squaredDistanceSum {n : Nat} (p q : Point n) : Float :=
  (Vector.zipWith (fun x y => Float.pow (x - y) 2) p.components q.components)
  |>.foldl (· + ·) 0.0

核心length函数

基于平方和结果开根号即可：

def length {n : Nat} (s : Segment n) : Float :=
  Float.sqrt (squaredDistanceSum s.a s.b)

4. 测试用例验证 #

我们可以测试2维（和你原代码对齐）、3维的情况，确保结果符合预期：

-- 2维测试：和原代码结果一致
def origin2D : Point 2 := ⟨Vector.mk [0.0, 0.0]⟩
def p2D : Point 2 := ⟨Vector.mk [3.0, 5.0]⟩
def s2D : Segment 2 := ⟨origin2D, p2D⟩

#eval length s2D  -- 输出 5.830952，和原代码结果匹配

-- 3维测试：计算(0,0,0)到(1,2,3)的距离
def origin3D : Point 3 := ⟨Vector.mk [0.0, 0.0, 0.0]⟩
def p3D : Point 3 := ⟨Vector.mk [1.0, 2.0, 3.0]⟩
def s3D : Segment 3 := ⟨origin3D, p3D⟩

#eval length s3D  -- 输出≈3.7416575，对应√(1²+2²+3²)=√14

额外优化：添加便捷构造函数 #

为了更方便创建Point，我们可以加一些辅助构造函数，比如从数组创建（需要保证数组长度等于n）：

-- 从数组创建Point（需要证明数组长度等于n）
def Point.ofArray {n : Nat} (arr : Array Float) (h : arr.size = n) : Point n :=
  ⟨Vector.ofArray arr h⟩

-- 1维点的快捷构造
def Point.scalar (x : Float) : Point 1 :=
  ⟨Vector.mk [x]⟩

-- 用便捷构造函数创建2维点
def q2D : Point 2 := Point.ofArray #[4.0, 3.0] rfl
def s2D' : Segment 2 := ⟨origin2D, q2D⟩
#eval length s2D'  -- 输出5.0，符合预期

为什么不用类型类？ #

你一开始尝试的class Point (n : Nat)其实不太适合这里：类型类的核心是给已有类型添加行为（比如给Float加一个"可以作为标量"的约束），而我们的Point是一个全新的、依赖维度的类型，用带参数的structure是更自然的选择——它清晰表达了"n维点是一个包含n个Float分量的结构"这个语义。

内容的提问来源于stack exchange，提问作者Brendan Langfield