use*_*206 5 coq logical-foundations
我正在努力完成逻辑基础归纳命题章节中le_exercises
的一系列练习。
该系列主要基于归纳关系le
,定义如下:
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我所坚持的特定定理如下:
\nTheorem 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到目前为止我成功证明的本系列中的先前定理是:
\nLemma 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
”,我尝试了各种方法,但似乎无济于事。
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
定理,但似乎无法从中得到任何有用的东西。我觉得我的理解中肯定缺少一些重要的东西,但你无法知道你不知道的东西。