编辑“︁Lean良基归纳”︁（章节）

== 语法与实现 ==

Lean中使用`wellFounded_induction`进行良基归纳。基本模式如下：

<syntaxhighlight lang="lean">
theorem example (x : α) : P x :=
  wellFounded_induction wf (λ y IH, ...)
where
  `wf`是良基关系证明
  `IH`是归纳假设（对所有`y < x`有`P y`）
</syntaxhighlight>

=== 基础示例：整数递减 ===

定义一个基于整数绝对值的良基递归函数：

<syntaxhighlight lang="lean">
def factorial : ℤ → ℕ
| n :=
  if h : n ≤ 0 then 1
  else n * factorial (n - 1)
termination_by _ => n  -- 指定度量标准
decreasing_by simp [h] -- 证明递归参数减小
</syntaxhighlight>

'''输入/输出示例'''：
<pre>
#eval factorial 5  -- 输出: 120
#eval factorial (-3) -- 输出: 1（根据基线条件）
</pre>