如何证明定理plus_lt : forall n1 n2 m，n1 + n2 <m -> n1 <m /\ n2 <m

Question

在这里，我对如何在coq中证明定理有了另一个疑问。这就是我所得到的：

Theorem plus_lt : forall n1 n2 m,
  n1 + n2 < m ->
  n1 < m /\ n2 < m.
Proof.
  intros n1.
  induction n2 as [| n2' IHn2'].
  - intros m H. inversion H.
    + split.
      * unfold lt. rewrite add_0_r. 
        apply n_le_m__Sn_le_Sm. apply le_n.
      * unfold lt. rewrite add_0_r.
        apply n_le_m__Sn_le_Sm. apply O_le_n.
    + split.
      * rewrite add_0_r in H. rewrite H1. apply H.
      * unfold lt. apply n_le_m__Sn_le_Sm. apply O_le_n.
  - intros m H. 
    + induction m as [| m' IHm'].
      * unfold lt. apply n_le_m__Sn_le_Sm in H. apply Sn_le_Sm__n_le_m in H.
        rewrite add_comm in H. rewrite plus_n_Sm in H.
        inversion H.
      * inversion H.
        ++ rewrite H1. unfold lt in H. apply Sn_le_Sm__n_le_m in H.
           apply plus_le in H. unfold lt. destruct H. split.
           ** apply n_le_m__Sn_le_Sm. apply H.
           ** apply n_le_m__Sn_le_Sm. apply H0.
        ++ unfold lt in H. rewrite add_comm in H. rewrite plus_n_Sm in H.
           apply plus_le in H. destruct H. split.
           ** unfold lt. apply H2.
           ** unfold lt. 

但我盯着它看的时间越长，我就越意识到必须有更简单的方法来证明这一点。我试过的每一条路都以路障告终，有些事我无法证明。以下是我目前的目标：

  n1, n2' : nat
  IHn2' : forall m : nat, n1 + n2' < m -> n1 < m /\ n2' < m
  m' : nat
  H : S n2' <= S m'
  H2 : S n1 <= S m'
  IHm' : n1 + S n2' < m' -> n1 < m' /\ S n2' < m'
  m : nat
  H1 : S (n1 + S n2') <= m'
  H0 : m = m'
  ============================
  S (S n2') <= S m'

我的意思是，这个证据的大小已经告诉我，我一定是在什么地方搞错了。事实太清楚了，不能采取这么多步骤。我已经在这件小事上花了8个多小时了

希望有一天我能掌握它的诀窍:-)

谢谢

Answer 1

您可能还想拆分目标，然后在n_1和n_1 + n_2中使用不等式的传递性。n_2的Idem。

Answer 2

我不确定你是出于教育目的还是因为你在其他地方需要它。在后一种情况下，解决方案是使用lia (线性整数算术)策略：

Require Import Lia.

Theorem plus_lt : forall n1 n2 m,
  n1 + n2 < m ->
  n1 < m /\ n2 < m.
Proof.
  lia.
Qed.

如果你这样做是为了教育目的，问题是你已经有了什么引理。我不会尝试直接证明这一点，而是使用更简单的引理。