coq - coq中的计算理论
问题描述
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.
解决方案
确实，在纸面上您会简单地得出结论，因为x + 0 = x. 好吧，在 Coq 中你必须证明它，因为加法是左偏的（它通过查找它的第一个参数来计算）。
我建议先证明
forall n, n + 0 = n
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.
标签： coqcomputation-theory
确实，在纸面上您会简单地得出结论，因为x + 0 = x. 好吧，在 Coq 中你必须证明它，因为加法是左偏的（它通过查找它的第一个参数来计算）。
我建议先证明
forall n, n + 0 = n