如何证明plus的单射性？

Question

这就是我想要证明的：

Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.

我尝试过 Coq 的内置策略，但不起作用。有没有简单的方法可以证明这一点？ 这是我所做的：

Theorem plus_injective : forall n m, n + n = m + m -> n = m.
Proof. intros n m H.
       induction n.
       - simpl in H. induction m.
         + reflexivity.
         + rewrite H. discriminate.
       - simpl in H. induction m.
         + simpl in H. rewrite <- H. discriminate.
         + rewrite <- H in IHn. rewrite IHn in IHm.
            
Qed.

并且它被一个子目标困住了

Answer 1

你如何在纸上证明这一点？我想说可能不是通过归纳法。也许你已经有了

+n

的逆矩阵？

请注意，还有解决线性整数算术问题的

lia

策略。您只需使用以下命令导入它即可。

From Coq Require Import Lia.