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 的评论，我们从他们的“纸笔证明”开始：

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；我强烈建议所有初学者暂时避免这种策略，并学习如何更“手动”地进行证明。事实上，使用任何支持 SMT 的策略，最初的目标都可以通过调用 SMT 来解决。