需要来自 Software Foundations 的练习帮助。这是定理:
Theorem plus_n_n_injective : ∀n m,
n + n = m + m →
n = m.
Proof.
我最终以 n = 0 作为目标，以 n + n = 0 作为假设。如何继续前进？
最佳答案
n + n 无法进一步简化，因为 n 是变量，而不是类型构造函数。
正如 Ptival 所说，您可以通过 destruct 来公开 n 的所有构造案例。然而，在这种情况下使用inversion在我看来有点极端，而不是这个Sf练习的目的。
当被 O 构造函数替换时，O + O 将减少(例如使用 simpl)到 O 和 reflexivity 应该可以解决问题。
当被 S 构造函数替换时，S foo + bar 将始终缩减为 S some 形状，且不能相等到 O(最简单的断言方法是使用 discriminate)，因为它们是同一类型的两个构造函数。
最好， 五、
关于coq - 定理 plus_n_n_内射，练习，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/23119202/