Coq计算理论证明：如何消去假设H:x + 0 = y + 0中的0

nat 类型的加法满足右加零恒等性质，Coq 标准库已经内置了对应引理add_0_r : forall n:nat, n + 0 = n，你可以直接用这个引理处理假设H：

常用操作方法 #

• 直接重写假设H
  执行命令：

  rewrite add_0_r in H.
  

  执行后H的内容会自动更新为x = y，后续你可以直接用这个等式处理剩下的2个子目标：

  • 如果子目标需要证明x和y相等，直接用exact H.或者assumption.即可完成证明
  • 如果子目标中出现x或者y，可以用rewrite H.做变量替换简化目标

• 显式指定重写对象（适合复杂场景避免歧义）
  如果你怕重写范围出错，可以显式指定x和y分别重写：

  rewrite (add_0_r x) in H.
  rewrite (add_0_r y) in H.
  

  最终效果和第一种操作完全一致。

注意事项 #

如果执行时提示找不到add_0_r引理，在你的证明脚本开头引入Peano自然数库即可：

Require Import PeanoNat.

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