Lean列表操作与证明

Lean列表操作与证明是函数式编程和定理证明中的核心概念。在Lean语言中，列表（List）是最常用的数据结构之一，它不仅是存储数据的容器，更是构造数学证明的基础工具。本文将详细介绍Lean中列表的基本操作、高阶函数应用以及如何通过列表构造形式化证明。

列表基础[编辑 | 编辑源代码]

在Lean中，列表是递归定义的代数数据类型，其标准库定义如下：

inductive List (α : Type u) where
  | nil : List α
  | cons (head : α) (tail : List α) : List α

这表示：

空列表表示为nil
非空列表通过cons构造，包含头部元素和尾部子列表

基础操作示例[编辑 | 编辑源代码]

-- 创建列表
def emptyList : List Nat := List.nil
def singleElement := [1]  -- 语法糖，等价于 List.cons 1 List.nil
def threeElements := [1, 2, 3]

-- 获取长度
#eval [1, 2, 3].length  -- 输出: 3

-- 连接列表
#eval [1, 2] ++ [3, 4]  -- 输出: [1, 2, 3, 4]

递归与模式匹配[编辑 | 编辑源代码]

列表操作的核心是递归和模式匹配。下面演示如何实现自定义的length函数：

def myLength : List α → Nat
  | [] => 0
  | _ :: xs => 1 + myLength xs

#eval myLength [10, 20, 30]  -- 输出: 3

高阶函数应用[编辑 | 编辑源代码]

Lean提供了丰富的列表高阶函数：

-- map操作
#eval [1, 2, 3].map (fun x => x * 2)  -- 输出: [2, 4, 6]

-- filter操作
#eval [1, 2, 3, 4].filter (fun x => x % 2 == 0)  -- 输出: [2, 4]

-- fold操作
#eval [1, 2, 3].foldl (fun acc x => acc + x) 0  -- 输出: 6

列表与命题证明[编辑 | 编辑源代码]

列表在定理证明中扮演重要角色。例如，证明列表连接的结合律：

theorem append_assoc {α : Type} (xs ys zs : List α) :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
  induction xs with
  | nil => simp
  | cons x xs ih => simp [ih]

这个证明展示了： 1. 对列表xs进行结构归纳 2. 基础情况（nil）通过simp自动证明 3. 归纳步骤利用归纳假设ih完成

实际应用案例[编辑 | 编辑源代码]

案例：实现并证明列表反转函数

首先实现反转函数：

def reverse {α : Type} : List α → List α
  | [] => []
  | x :: xs => reverse xs ++ [x]

然后证明反转的反转是原列表：

theorem reverse_reverse {α : Type} (xs : List α) :
  reverse (reverse xs) = xs := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
    simp [reverse, ih]
    -- 需要辅助引理证明 (ys ++ [x]) = x :: ys
    sorry  -- 完整证明需要更多步骤