如何用Lean基础策略证明Nat.succ n - 1 = n

算力阿峰

2026-7-11

证明 Nat.succ n - 1 = n（无simp，仅用Prelude基础策略）

这里提供两种仅依赖Prelude中基础策略和引理的证明方法，完全不使用simp：

方法一：利用加法与减法的等价性

theorem succ_sub_one (n : Nat) : Nat.succ n - 1 = n := by
  -- 用引理将减法等式转化为加法等式：若a = b + c，则a - c = b
  apply Nat.sub_eq_of_eq_add
  -- 反转等式方向，匹配已知的succ定义引理
  symm
  -- 直接引用Prelude中succ与加法的基本等价性
  exact Nat.succ_eq_add_one n

步骤解释：

apply Nat.sub_eq_of_eq_add：将目标Nat.succ n - 1 = n转化为证明Nat.succ n = n + 1，这是Prelude中定义的减法核心等价关系。
symm：把目标等式反转成n + 1 = Nat.succ n，对齐Prelude中Nat.succ_eq_add_one的形式。
exact Nat.succ_eq_add_one n：直接调用Prelude内置的基本引理，完成证明。

方法二：自然数归纳法

theorem succ_sub_one (n : Nat) : Nat.succ n - 1 = n := by
  induction n with
  | zero =>
    -- 基例：n=0时，succ 0 = 1，1-1=0
    rw [Nat.succ_zero]
    exact Nat.one_sub_one_eq_zero
  | succ n ih =>
    -- 归纳步骤：假设succ n -1 = n，证succ (succ n) -1 = succ n
    rw [Nat.succ_succ]
    -- 利用succ a - 1 = succ (a -1)（当a ≥1时成立）
    rw [Nat.sub_succ]
    -- 代入归纳假设，完成证明
    rw [ih]

步骤解释：

基例（n=0）：展开Nat.succ_zero得到1 - 1，直接用Prelude中的Nat.one_sub_one_eq_zero得到结果0，匹配目标。
归纳步骤：
1. rw [Nat.succ_succ]：将succ (succ n)展开为标准形式。
2. rw [Nat.sub_succ]：利用Prelude中减法的性质，当被减数是succ形式且大于减数时，可将succ提到减法外。
3. rw [ih]：代入归纳假设succ n -1 = n，直接得到目标结果succ n。