coq中的计算理论
coq中的计算理论
提问于 2021-09-27 19:11:42
2子目标x，y: nat H:x+0=y+0
but after that I don't know how to to get rid of 0 in H.回答 2
Stack Overflow用户
发布于 2021-09-27 20:35:31
这是真的，在纸上，你会简单地得出结论，因为x + 0 = x。在Coq中，你必须证明这一点，因为加法是左偏的(它通过查找第一个参数进行计算)。
我建议先证明
forall n, n + 0 = nStack Overflow用户
发布于 2021-09-28 14:03:57
我会选择这样的方式：
Theorem ex9: forall x y n, x + n = y + n -> x = y.
Proof.
intros.
induction n as [| n' IH].
- rewrite add_0_r in H. (* replace x + 0 with x *)
rewrite add_0_r in H. (* replace y + 0 with y *)
assumption.
- apply IH. (* replace x=y with x+n' = y+n' *)
rewrite <- plus_n_Sm in H. (* replace x + S n' with S (x + n') *)
rewrite <- plus_n_Sm in H. (* replace y + S n' with S (y + n') *)
apply S_injective in H. (* drop both S constructors *)
assumption.
Qed.页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/69352099
复制相关文章
相似问题
腾讯云开发者
