编辑“︁Lean谓词逻辑”︁（章节）

== 实际应用案例 ==

=== 数学定理形式化 ===
形式化数学陈述“任意两个连续自然数中至少有一个是偶数”：
<syntaxhighlight lang="lean">
theorem consecutive_evens : ∀ (n : ℕ), Even n ∨ Even (n + 1) :=
fun n => Or.elim (Nat.even_or_odd n)
  (fun h => Or.inl h)
  (fun h => Or.inr (h ▸ Even (n + 1)))
</syntaxhighlight>
'''步骤'''：
1. 使用`Nat.even_or_odd`将`n`分为偶数或奇数情况。
2. 若`n`为偶数，直接得证（`Or.inl`）。
3. 若`n`为奇数，则`n + 1`为偶数（通过`h ▸`替换）。

=== 程序验证 ===
验证列表操作的正确性：
<syntaxhighlight lang="lean">
def NonEmpty (α : Type) (lst : List α) : Prop := ∃ (x : α), x ∈ lst

example : NonEmpty ℕ [1, 2, 3] :=
Exists.intro 1 (by simp)
</syntaxhighlight>
'''解释'''：
* `NonEmpty`谓词断言列表非空。
* 提供见证`1`并通过`simp`策略证明`1 ∈ [1, 2, 3]`。