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

use*_*206 5 coq logical-foundations

我正在努力完成逻辑基础归纳命题章节中le_exercises的一系列练习。

\n

该系列主要基于归纳关系le,定义如下:

\n
Inductive le : nat -> nat -> Prop :=\n  | le_n (n : nat)                : le n n\n  | le_S (n m : nat) (H : le n m) : le n (S m).\n\nNotation "n <= m" := (le n m).\n
Run Code Online (Sandbox Code Playgroud)\n

我所坚持的特定定理如下:

\n
Theorem add_le_cases : forall n m p q,\n  n + m <= p + q -> n <= p \\/ m <= q.\n
Run Code Online (Sandbox Code Playgroud)\n

到目前为止我成功证明的本系列中的先前定理是:

\n
Lemma le_trans : \xe2\x88\x80 m n o, m \xe2\x89\xa4 n \xe2\x86\x92 n \xe2\x89\xa4 o \xe2\x86\x92 m \xe2\x89\xa4 o.\n\nTheorem O_le_n : \xe2\x88\x80 n, 0 \xe2\x89\xa4 n.\n\nTheorem n_le_m__Sn_le_Sm : \xe2\x88\x80 n m, n \xe2\x89\xa4 m \xe2\x86\x92 S n \xe2\x89\xa4 S m.\n\nTheorem Sn_le_Sm__n_le_m : \xe2\x88\x80 n m, S n \xe2\x89\xa4 S m \xe2\x86\x92 n \xe2\x89\xa4 m.\n\nTheorem lt_ge_cases : \xe2\x88\x80 n m, n < m \xe2\x88\xa8 n \xe2\x89\xa5 m.\n\nTheorem le_plus_l : \xe2\x88\x80 a b, a \xe2\x89\xa4 a + b.\n\nTheorem plus_le : \xe2\x88\x80 n1 n2 m, n1 + n2 \xe2\x89\xa4 m \xe2\x86\x92 n1 \xe2\x89\xa4 m \xe2\x88\xa7 n2 \xe2\x89\xa4 m.\n
Run Code Online (Sandbox Code Playgroud)\n

书中给出了一个提示,指出该定理add_le_cases可能“通过归纳法更容易证明n”,我尝试了各种方法,但似乎无济于事。

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

我考虑过使用该plus_le定理,但似乎无法从中得到任何有用的东西。我觉得我的理解中肯定缺少一些重要的东西,但你无法知道你不知道的东西。

\n

And*_*rey 5

好吧,我不会做inversion Hdestruct m。我会destruct p在解决这个O问题后,稍微按摩一下H,以便能够应用归纳假设。