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 

現在，讓我們翻譯成勒柯克！事實上，我們需要做的第一件事情是<的可判定性，這是通過使用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. 

使用我所選擇的庫[數學-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總提到的證明另一種風格更豐富的使用將使用：

Proof. apply Max.max_case_strong; omega. Qed. 

然而，這個證明涉及使用一個重量級的自動化策略，omega的;我強烈建議所有初學者暫時避免這種策略，並學習如何更「手動」地進行校樣。實際上，使用任何SMT技術，最初的目標都可以通過調用SMT來解決。