Lean 4能否定义循环长度为N的循环列表类型？

当然可以。在依赖类型论的框架下，Lean 4支持依赖归纳类型，我们可以直接将循环列表的长度N作为类型的一部分，同时通过构造子确保结构的循环性（无空列表选项）。

实现思路 #

核心是定义一个以自然数n为参数的归纳类型CycleList α n，其中α是元素类型，n是循环列表的长度。通过构造子限制所有实例都是非空的循环结构，且长度严格匹配n。

具体代码示例 #

-- 定义长度为 n 的循环列表，n ≥ 1
inductive CycleList (α : Type) : Nat → Type where
  | single : α → CycleList α 1  -- 单元素循环，长度为1
  | insert : α → CycleList α n → CycleList α (n + 1)  -- 向循环中插入元素，长度+1

代码解释 #

• single a：构造一个仅包含元素a的长度为1的循环列表，这是最基础的循环结构。
• insert a c：在长度为n的循环列表c中插入元素a，得到长度为n+1的新循环列表。由于循环列表没有固定起点，插入操作不依赖具体位置，完全符合循环的特性。

使用示例 #

-- 构造一个包含1、2、3的长度为3的循环列表
def my_cycle : CycleList Nat 3 := CycleList.insert 1 (CycleList.insert 2 (CycleList.single 3))

扩展说明 #

如果需要更贴近“循环等价”的语义（即旋转同一个循环列表得到的实例视为等价），也可以基于Vector α n（带长度的线性列表）定义等价类，但上述归纳定义已经满足“将长度N作为类型一部分”的核心需求，且结构更直观。

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