时间戳

首页 > 解决方案 > 如何证明`plus_le_compat_l : forall nmp, n <= m -> p + n <= p + m.`

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

问题描述

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，这给了我两个子案例。对于第一个 where 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我as ，但这也不会带我去任何地方。rewriteS np

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

谢谢

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

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

标签： coqcoq-tactic

解决方案

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

推荐阅读