Coq 证明加法不等式答案

【问题标题】：Coq proving addition inequalityCoq 证明加法不等式
【发布时间】：2021-04-20 10:25:54
【问题描述】：

我是一个初学者并试图证明这个引理：

Lemma test:  forall n m p q : nat,
    n <= p \/ m <= q -> n + m <= p + q.

我试过了

From Coq Require Export Lia.

Lemma test:  forall n m p q : nat,
        n <= p \/ m <= q -> n + m <= p + q
Proof.
    intros; omega.

和Lia，但它不起作用。我该如何继续？

【问题讨论】：

【解决方案1】：

你可能是说

Lemma test:  forall n m p q : nat,
    n <= p /\ m <= q -> n + m <= p + q.

使用/\（逻辑与）而不是\/（逻辑或），因为您的定理不成立。作为反例，选择 n = p = q = 0 和 m = 1。

以这种方式修复后，lia 会自动找到证明。

另外，请注意，在 Coq 中，currify 类型更为惯用，即用箭头替换箭头左侧的连词。这会读

Lemma test:  forall n m p q : nat,
    n <= p -> m <= q -> n + m <= p + q.

这是等价的。

【讨论】：

【解决方案2】：

感谢您的回答。然而，

Proof.
  intros. lia.

给予：

Error: Tactic failure:  Cannot find witness.

有办法继续吗？

【讨论】：