Coq初学者证明加法不等式引理时自动证明工具失效的解决方法咨询

你调用Lia、Omega等自动证明工具无法完成目标，根本原因是这个待证明的引理本身是错误的，不存在合法的构造性证明，和工具的证明能力无关。

原引理将加法保序性质的条件错写为析取关系，很容易构造满足前提但不满足结论的反例：

• 取参数值：n=1, m=5, p=1, q=2
• 前提校验：n <= p \/ m <= q 中，1 <=1 成立，因此整个析取前提为真
• 结论校验：n+m =6，p+q=3，6 <=3 显然为假
  只要两个不等式仅需满足任意一个，剩下的变量取足够大的值，就会打破和的大小关系，命题本身不具备永真性。

1. 修正命题逻辑：自然数加法的保序性要求两个不等式同时成立，也就是把析取连接符\/替换为合取连接符/\
2. 修正后的命题可以直接通过自动工具完成证明，可运行的示例代码如下：

From Coq Require Export Lia.

Lemma test_correct:  forall n m p q : nat,
    n <= p /\ m <= q -> n + m <= p + q.
Proof.
    intros [H1 H2]. lia.
Qed.

如果确实需要在带析取前提的约束下证明和的大小关系，需要补充额外的全局约束条件，否则当前写法的命题无法完成证成。

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