如何证明定理 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 个多小时了:-p

希望有一天我能掌握窍门:-)

谢谢

Answer 1

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

Require Import Lia.

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

如果您出于教育目的这样做，问题是您已经拥有哪些引理。我不会尝试直接证明它，而是使用更简单的引理。

Answer 2

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

同上

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

How to prove Theorem plus_lt : forall n1 n2 m, n1 + n2 < m -> n1 < m /\ n2 < m

coq

coq-tactic