我如何证明 `add_le_cases` (`forall n m p q, n + m <= p + q -> n <= p \/ m <= q`)

Question

我正在尝试完成 Logical Foundations' chapter on inductive propositions 中的 le_exercises 系列练习。

本级数主要基于归纳关系le，定义如下：

Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat)                : le n n
  | le_S (n m : nat) (H : le n m) : le n (S m).

Notation "n <= m" := (le n m).

我坚持的特定定理如下：

Theorem add_le_cases : forall n m p q,
  n + m <= p + q -> n <= p \/ m <= q.

到目前为止，我设法证明的这些系列中的先前定理是：

Lemma le_trans : ∀ m n o, m ≤ n → n ≤ o → m ≤ o.

Theorem O_le_n : ∀ n, 0 ≤ n.

Theorem n_le_m__Sn_le_Sm : ∀ n m, n ≤ m → S n ≤ S m.

Theorem Sn_le_Sm__n_le_m : ∀ n m, S n ≤ S m → n ≤ m.

Theorem lt_ge_cases : ∀ n m, n < m ∨ n ≥ m.

Theorem le_plus_l : ∀ a b, a ≤ a + b.

Theorem plus_le : ∀ n1 n2 m, n1 + n2 ≤ m → n1 ≤ m ∧ n2 ≤ m.

这本书给出了一个提示，指出定理 add_le_cases 可能“更容易通过对 n 的归纳法来证明”，我尝试了各种方法，但似乎无处可去。

Theorem add_le_cases : forall n m p q,
  n + m <= p + q -> n <= p \/ m <= q.
Proof.
  intros n. induction n.
  - intros. left. apply O_le_n.
  - intros. inversion H.
    + destruct m.
      * right. apply O_le_n.
      *  (* stuck *)

我考虑过使用 plus_le 定理，但似乎无法从中得到任何有用的信息。我觉得我的理解中肯定缺少一些关键的东西，但你不能知道你不知道什么。

Answer 1

好吧，我不会做 inversion H 和 destruct m。我会 destruct p 并在解决 O 案例后，然后稍微按摩 H 以便能够应用归纳假设。

我如何证明 `add_le_cases` (`forall n m p q, n + m <= p + q -> n <= p \/ m <= q`)

How can I prove `add_le_cases` (`forall n m p q, n + m <= p + q -> n <= p \/ m <= q`)

coq

logical-foundations