Coq：如何证明 max a b <= a+b？

Question

我无法使用 coq 的策略证明简单的逻辑 max a b <= a+b。我应该如何解决它？以下是我迄今为止使用的代码。 s_le_n已证明，为简单起见，此处不再赘述。

Theorem s_le_n: forall (a b: nat),  a <= b -> S a <= S b.
Proof. Admitted.

Theorem max_sum: forall (a b: nat), max a b <= a + b.
Proof. 
intros.
induction a.
- simpl. reflexivity.
- rewrite plus_Sn_m. induction b.
  + simpl. rewrite <- plus_n_O. reflexivity.
  + rewrite <- plus_Sn_m. simpl. apply s_le_n. rewrite IHa.

Answer 1

考虑到@re3el 的评论，我们从他们的 "pen and paper proof":

开始

if a>b max a b = a, a < a+b; else max a b = b, b < a+b

现在让我们把它翻译成 Coq！事实上，我们需要做的第一件事是 < 的可判定性，这是使用 le_lt_dec a b 引理完成的。剩下的就是例行公事了：

Require Import Arith.

Theorem max_sum (a b: nat) : max a b <= a + b.
Proof.
case (le_lt_dec a b).
+ now rewrite <- Nat.max_r_iff; intros ->; apply le_plus_r.
+ intros ha; apply Nat.lt_le_incl, Nat.max_l_iff in ha.
  now rewrite ha; apply le_plus_l.
Qed.

但是，我们可以大大改进这个证明。有各种各样的候选者，使用 stdlib 的一个很好的是：

Theorem max_sum_1 (a b: nat) : max a b <= a + b.
Proof.
now rewrite Nat.max_lub_iff; split; [apply le_plus_l | apply le_plus_r].
Qed.

使用我选择的库 [math-comp]，您可以链接重写以获得更紧凑的证明：

From mathcomp Require Import all_ssreflect.

Theorem max_sum_2 (a b: nat) : maxn a b <= a + b.
Proof. by rewrite geq_max leq_addl leq_addr. Qed.

事实上，根据简短的证明，也许根本就不需要原始引理。

编辑：@Jason Gross 提到了另一种更老练的人会使用的证明方式：

Proof. apply Max.max_case_strong; omega. Qed.

然而，这个证明涉及使用重量级的自动化策略，omega；我强烈建议所有初学者暂时避免这种策略，并多学习如何做证明"manually"。事实上，使用任何启用 SMT 的策略，最初的目标都可以通过调用 SMT 来简单地解决。

Coq：如何证明 max a b <= a+b？

Coq: How to prove max a b <= a+b?

coq

coq-tactic