如何证明Logical Foundations练习中的add_le_cases定理

证明思路 #

你已经走在正确的归纳方向上了，缺的是归纳步里对p的情况拆分，以及归纳假设的正确应用：

1. 对n归纳的基例没问题，0 <= p恒成立直接左项得证。
2. 归纳步（对应S n的情况）时，先对p做分情况讨论：
   • 若p = 0：此时S n <= 0不可能成立，我们转而证明右项m <= q：由le_plus_l得m <= S n + m，结合前提S n + m <= 0 + q = q，用le_trans直接得m <= q。
   • 若p = S p'：先对前提S n + m <= S p' + q做化简，等价于S (n + m) <= S (p' + q)，调用前置定理Sn_le_Sm__n_le_m可得n + m <= p' + q，这时就可以套用归纳假设得到n <= p' \/ m <= q：
     • 若m <= q，直接右项得证
     • 若n <= p'，调用前置定理n_le_m__Sn_le_Sm可得S n <= S p' = p，左项得证

完整证明代码 #

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 m p q H.
    destruct p as [| p'].
    + (* p = 0 的情况 *)
      right. eapply le_trans. apply le_plus_l. simpl in H. apply H.
    + (* p = S p' 的情况 *)
      simpl in H. apply Sn_le_Sm__n_le_m in H.
      specialize (IHn m p' q H). destruct IHn as [Hn | Hm].
      * left. apply n_le_m__Sn_le_Sm. apply Hn.
      * right. apply Hm.
Qed.

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