Coq中使用rewrite策略改写函数参数遇阻，改写S n + S n失败求解

问题根源 #

Coq提示找不到S n + S n子项，是因为加法的默认化简规则（比如结合律、后继的展开）已经把目标里的S n + S n转换成了等价但字面不同的形式（例如S (S (n + n))），导致字面匹配的rewrite策略失效。而乘法优先级更高，S n * S n * S n未被自动化简，所以能被匹配到。

可行解决方案 #

以下是几种直接有效的处理方法：

• 全量展开后继再处理
  先把所有S n展开为n + 1，再用代数策略处理，避免字面匹配问题：

  unfold S in *.  (* 同时展开目标和归纳假设中的S *)
  rewrite IHn. ring.
  

  也可以分步验证改写规则：

  unfold S in |-.
  assert (Rw1 : (n+1)+(n+1) = 2 + n + n). ring. rewrite Rw1.
  

• 定向替换S n为n+1
  先建立S n与n+1的等式，再全局替换，绕过字面匹配限制：

  assert (Sn_def : S n = n + 1). reflexivity.
  rewrite Sn_def in *.
  rewrite IHn. ring.
  

• 直接用代数化简策略一步到位
  无需单独改写子项，ring策略能自动处理所有代数运算的等价转换，结合归纳假设直接完成证明：

  rewrite IHn. ring.
  

内容的提问来源于stack exchange，提问作者Attila Károly