跳转到内容

Lean可判定片段

来自代码酷

Lean可判定片段[编辑 | 编辑源代码]

介绍[编辑 | 编辑源代码]

在Lean定理证明器中，可判定片段（Decidable Fragments）指一类逻辑命题，其真值可以通过算法在有限步骤内确定。这类命题在自动化证明中尤为重要，因为Lean的类型检查器需要能够判断表达式是否属于正确的类型。理解可判定片段有助于编写高效的证明策略，并避免不可判定问题导致的类型检查失败。

可判定性通常与以下概念相关：

  • 可判定命题（Decidable Proposition）：存在算法能判定命题的真假。
  • 可计算函数（Computable Function）：函数可在有限步骤内计算出结果。
  • 类型类（Type Class）：Lean通过Decidable类型类标记可判定命题。

基本概念[编辑 | 编辑源代码]

Decidable类型类[编辑 | 编辑源代码]

Lean通过Decidable p类型类表示命题p的可判定性。其定义如下： 

class inductive Decidable (p : Prop) where
  | isTrue (h : p) : Decidable p
  | isFalse (h : ¬ p) : Decidable p
  • isTrue表示命题p为真。
  • isFalse表示命题p为假。

可判定性的作用[编辑 | 编辑源代码]

在Lean中，某些构造（如if-then-else和by decide）要求命题是可判定的。例如： 

def isEven (n : Nat) : Bool := n % 2 == 0

-- 使用`Decidable`实例自动生成证明
example : Decidable (isEven 4) := by decide

输出： 

Decidable.isTrue (isEven 4)

解释：by decide通过计算isEven 4的结果（true），自动构造了Decidable.isTrue的证明。

可判定片段的分类[编辑 | 编辑源代码]

命题逻辑片段[编辑 | 编辑源代码]

命题逻辑中的以下命题是可判定的：

  • 原子命题（如True、False）
  • 合取（∧）、析取（∨）、否定（¬）的组合

示例： 

example : Decidable (True ∨ False) := by decide

有限域上的量化[编辑 | 编辑源代码]

在有限集合上使用全称（∀）或存在（∃）量词的命题是可判定的。例如： 

def allEven (l : List Nat) : Prop := ∀ x ∈ l, isEven x

-- 对于有限列表，`allEven`是可判定的
instance (l : List Nat) : Decidable (allEven l) :=
  match l with
  | [] => Decidable.isTrue (by simp [allEven])
  | x :: xs =>
    if h : isEven x then
      match (allEven xs) with
      | Decidable.isTrue h' => Decidable.isTrue (by simp [allEven, h, h'])
      | Decidable.isFalse h' => Decidable.isFalse (by simp [allEven, h, h'])
    else
      Decidable.isFalse (by simp [allEven, h])

线性算术片段[编辑 | 编辑源代码]

线性整数算术（Linear Integer Arithmetic, LIA）是可判定的。Lean通过omega策略自动化证明此类命题： 

example (x y : Int) : Decidable (x + y = y + x) := by decide

不可判定的问题[编辑 | 编辑源代码]

并非所有命题都可判定。例如：

  • 高阶逻辑中的一般量化（如∀ f : Nat → Nat, ...）
  • 非线性算术（如x * y = 0）

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

案例1：列表排序验证[编辑 | 编辑源代码]

验证列表是否已排序是可判定的，因为只需遍历有限元素： 

def isSorted (l : List Nat) : Prop :=
  match l with
  | [] | [_] => True
  | x :: y :: xs => x ≤ y ∧ isSorted (y :: xs)

instance (l : List Nat) : Decidable (isSorted l) :=
  match l with
  | [] => Decidable.isTrue trivial
  | [x] => Decidable.isTrue trivial
  | x :: y :: xs =>
    if h : x ≤ y then
      match (isSorted (y :: xs)) with
      | Decidable.isTrue h' => Decidable.isTrue ⟨h, h'⟩
      | Decidable.isFalse h' => Decidable.isFalse (fun ⟨h1, h2⟩ => h' h2)
    else
      Decidable.isFalse (fun ⟨h1, h2⟩ => h h1)

案例2：自动证明线性不等式[编辑 | 编辑源代码]

使用omega策略自动化证明线性不等式： 

example (x y : Int) : Decidable (2 * x + 3 * y ≤ 5 * x - y) := by omega

可判定性与计算[编辑 | 编辑源代码]

可判定片段直接影响Lean的计算能力。例如，以下函数要求其终止性可判定： 

def findFirstEven (l : List Nat) : Option Nat :=
  match l with
  | [] => none
  | x :: xs => if isEven x then some x else findFirstEven xs

总结[编辑 | 编辑源代码]

片段类型 是否可判定 示例
命题逻辑组合 是 p ∧ q
有限域量化 是 ∀ x ∈ [1,2,3], p x
线性算术 是 x + y = y + x
高阶逻辑 否 ∀ f : Nat → Nat, ...

进一步阅读[编辑 | 编辑源代码]

  • Lean标准库中的Decidable类型类
  • 线性算术的omega策略
  • 有限自动机与可判定性理论
检索自“https://wiki.echo.cool/index.php?title=Lean可判定片段&oldid=22329”