如何证明 `plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.`

Question

SFv1 的另一个问题让我卡住了。

定理如下：

Theorem plus_le_compat_l : forall n m p,
  n <= m ->
  p + n <= p + m.

到目前为止，我已经尝试了几种途径，最让我受益的是介绍 n 并开始对其进行归纳。基本情况相当微不足道 (intros m p H. rewrite add_0_r. apply le_plus_l.)。

至于归纳步骤，我试过destruct p，这给了我两个子情况。对于第一个 p = O，通过应用 H 可以非常容易地证明。当 p = S n 我卡住了。到目前为止，这是完整的证明：

Theorem plus_le_compat_l : forall n m p,
  n <= m ->
  p + n <= p + m.
Proof.
  intros n.
  induction n as [| n' IHn'].
  - intros m p H. rewrite add_0_r. apply le_plus_l.
  - destruct p eqn:E.
    + intros H. simpl. apply H.
    + intros H. simpl. apply n_le_m__Sn_le_Sm.

我目前的目标：

  n' : nat
  IHn' : forall m p : nat, n' <= m -> p + n' <= p + m
  m, p, n : nat
  E : p = S n
  H : S n' <= m
  ============================
  n + S n' <= n + m

我尝试了一个简单的操作来将不等式的 LHS 变成 n' + S n，这让我 rewrite 将 S n 作为 p，但这也不行带我去任何地方。

非常感谢这里的任何提示:-)

谢谢

PS：我尝试应用一个先前证明的定理但没有成功：

Theorem add_le_cases : forall n m p q,
  n + m <= p + q -> n <= p \/ m <= q.

Answer 1

我认为在这种情况下，在 p 上使用归纳法是可行的方法，并且两个目标都应该可以很好地证明——通过使用 le_n_S.[=12 的归纳法=]

如何证明 `plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.`

How to prove `plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m.`

coq

coq-tactic