Coq中使用minus_n_n重写消去double n项被拒绝如何解决？

问题原因与解决方法 #

你遇到的重写失败问题来自容易忽略的Coq运算符结合性规则，不需要额外补充前提条件：

• Coq中自然数的+和-属于同优先级运算符，默认采用左结合规则。你目标里的m + p + double n - double n实际会被解析为((m + p) + double n) - double n，不存在独立的double n - double n子项，所以你直接调用rewrite minus_n_n (double n)时，Coq无法在目标中找到匹配的可重写结构，自然会报错。
• 你可以选择两种方案完成证明：
  1. 如果你坚持用minus_n_n完成重写：先执行rewrite <- Nat.add_assoc把目标右侧调整为m + p + (double n - double n)，此时再执行rewrite (minus_n_n (double n))即可完成重写，最后用reflexivity就可以结束证明。
  2. 更简便的写法：直接调用加法消去引理rewrite Nat.add_sub_cancel_r，一步就能把右侧重写为m + p，无需调整运算顺序。

小提示：如果Coq提示找不到Nat相关引理，先在文件开头执行Require Import Arith.导入标准库算术模块即可。

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