Coq证明add_succ定理时rewrite策略未按预期生效问题求助

问题核心原因 #

你rewrite失败有两层直接原因：

1. 模式匹配不上：你当前的归纳假设IHb左侧是add a (succ b')，而你目标左侧是add a (succ (succ b'))，二者第二个参数差了一层succ构造子，完全不是同一个模式，Coq自然找不到可重写的位置。
2. 你的add实现和归纳方式不匹配：你自定义的add递归逻辑是每次把第一个参数套succ、第二个参数剥succ：

   add a (succ b') = add (succ a) b'
   

   你在开始归纳b之前就固定了a的取值，导致归纳假设里的a无法适配递归后变成succ a的第一个参数，就算你匹配上了也没法完成后续证明。

修复方案 #

你需要先证明一个适配你add实现的辅助引理，再用它证明目标定理：

第一步：证明辅助引理 #

先证add (succ a) b = succ (add a b)，这个引理可以直接对b归纳完成：

Lemma add_succ_first : forall a b : nat, add (succ a) b = succ (add a b).
Proof.
  induction b as [ | b' IHb ].
  - simpl. reflexivity.
  - simpl. rewrite IHb. reflexivity.
Qed.

第二步：证明原目标定理 #

因为你的add实现里add a (succ b)会直接化简为add (succ a) b，直接调用上面的引理就能完成证明，完全不需要对b做归纳：

Theorem add_succ : forall a b : nat,
    add a (succ b) = succ (add a b).
Proof.
  intros a b.
  simpl. (* 目标自动化简为 add (succ a) b = succ (add a b) *)
  apply add_succ_first.
Qed.

内容的提问来源于stack exchange，提问作者azani