如何在Lean 4递归函数中用head替代head!

问题核心 #

你当前实现的suffixes函数通过递归生成列表的所有后缀，但依赖不安全的head!操作。要替换它，必须证明任意列表xs传入suffixes后返回的结果永远非空，但直接先定义函数再证定理会陷入循环依赖——证明需要用到函数的递归逻辑，而函数又需要定理来去掉head!。

两种可行解决方案 #

方案1：用NonEmpty类型约束递归结果 #

先定义一个带非空保证的辅助函数，利用Lean的类型系统提前约束结果，避免不安全操作：

def suffixesAux : (xs : List α) → NonEmpty (List (List α))
  | [] => ⟨[[]]⟩  -- 空列表的后缀只有自身，天然非空
  | x::xs =>
    let sfx := suffixesAux xs
    -- 借助NonEmpty的类型保证，直接安全调用head
    let next_sfx := x :: sfx.val.head
    ⟨next_sfx :: sfx.val⟩

def suffixes (xs : List α) : List (List α) := (suffixesAux xs).val

NonEmpty T是Lean内置类型，用于标记T至少包含一个元素，.val可提取对应的非空值，.head在此处是完全安全的。

方案2：相互递归定义函数与定理 #

Lean 4支持mutual块同时定义函数和定理，打破循环依赖：

mutual
  def suffixes : List α → List (List α)
    | [] => [[]]
    | x::xs =>
      let sfx := suffixes xs
      -- 引入定理证明sfx非空，安全调用head
      have : sfx ≠ [] := suffixes_nonempty xs
      (x :: sfx.head) :: sfx

  theorem suffixes_nonempty : ∀ xs : List α, suffixes xs ≠ []
    | [] => by simp [suffixes]
    | x::xs => by
      simp [suffixes]
      apply Ne.suffix (suffixes_nonempty xs)
end

这里suffixes_nonempty通过归纳法证明所有suffixes的返回结果非空，函数中用have引入该定理，即可安全使用.head替代head!。

验证效果 #

两种方案的执行结果一致，且完全消除了不安全操作：

#eval suffixes [1, 2, 3, 4]  -- 输出 [[1,2,3,4], [2,3,4], [3,4], [4], []]

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