编辑“︁Lean可判定片段”︁

= Lean可判定片段 =

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

可判定性通常与以下概念相关：
* '''可判定命题'''（Decidable Proposition）：存在算法能判定命题的真假。
* '''可计算函数'''（Computable Function）：函数可在有限步骤内计算出结果。
* '''类型类'''（Type Class）：Lean通过<code>Decidable</code>类型类标记可判定命题。

== 基本概念 ==

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

<syntaxhighlight lang="lean">
class inductive Decidable (p : Prop) where
  | isTrue (h : p) : Decidable p
  | isFalse (h : ¬ p) : Decidable p
</syntaxhighlight>

* <code>isTrue</code>表示命题<code>p</code>为真。
* <code>isFalse</code>表示命题<code>p</code>为假。

=== 可判定性的作用 ===
在Lean中，某些构造（如<code>if-then-else</code>和<code>by decide</code>）要求命题是可判定的。例如：

<syntaxhighlight lang="lean">
def isEven (n : Nat) : Bool := n % 2 == 0

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

输出：
<pre>
Decidable.isTrue (isEven 4)
</pre>

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

== 可判定片段的分类 ==

=== 命题逻辑片段 ===
命题逻辑中的以下命题是可判定的：
* 原子命题（如<code>True</code>、<code>False</code>）
* 合取（<code>∧</code>）、析取（<code>∨</code>）、否定（<code>¬</code>）的组合

示例：
<syntaxhighlight lang="lean">
example : Decidable (True ∨ False) := by decide
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
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])
</syntaxhighlight>

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

<syntaxhighlight lang="lean">
example (x y : Int) : Decidable (x + y = y + x) := by decide
</syntaxhighlight>

== 不可判定的问题 ==
并非所有命题都可判定。例如：
* 高阶逻辑中的一般量化（如<code>∀ f : Nat → Nat, ...</code>）
* 非线性算术（如<code>x * y = 0</code>）

== 实际案例 ==

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

<syntaxhighlight lang="lean">
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)
</syntaxhighlight>

=== 案例2：自动证明线性不等式 ===
使用<code>omega</code>策略自动化证明线性不等式：

<syntaxhighlight lang="lean">
example (x y : Int) : Decidable (2 * x + 3 * y ≤ 5 * x - y) := by omega
</syntaxhighlight>

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

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

== 总结 ==
{| class="wikitable"
|-
! 片段类型 !! 是否可判定 !! 示例
|-
| 命题逻辑组合 || 是 || <code>p ∧ q</code>
|-
| 有限域量化 || 是 || <code>∀ x ∈ [1,2,3], p x</code>
|-
| 线性算术 || 是 || <code>x + y = y + x</code>
|-
| 高阶逻辑 || 否 || <code>∀ f : Nat → Nat, ...</code>
|}

== 进一步阅读 ==
* Lean标准库中的<code>Decidable</code>类型类
* 线性算术的<code>omega</code>策略
* 有限自动机与可判定性理论

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean高级证明技术]]