Coq: Wie beweisen Sie max a b <= a + b?

Question

Ich kann die einfache Logik max a b <= a+b mit Coq Taktiken nicht beweisen. Wie soll ich es lösen? Unten ist der Code, an dem ich bis jetzt gearbeitet habe. s_le_n ist bewiesen, aber hier der Einfachheit halber nicht erwähnt.

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

Unter Berücksichtigung @ re3el Kommentar, beginnen wir von ihrem "Stift und Papier Beweis":

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

Lassen Sie uns jetzt, dass in Coq übersetzen! In der Tat, das erste, was wir tun müssen, ist Fall auf die Entscheidbarkeit von <, dies geschieht mit der le_lt_dec a b Lemma. Der Rest ist Routine:

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. 

Allerdings können wir diesen Beweis ein wenig verbessern. Es gibt verschiedene Kandidaten, ein gutes den stdlib verwendet, ist:

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. 

Mit meiner Bibliothek der Wahl [Math-comp] können Sie die Neufassungen Kette ein kompakteres Beweis zu erhalten:

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. 

Tatsächlich wurde das ursprüngliche Lemma angesichts des Kurzbeweises vielleicht gar nicht gebraucht.

edit: @ Jason Gross erwähnt eine andere Art von Beweis eine reifere gebrauchte verwenden würde:

Proof. apply Max.max_case_strong; omega. Qed. 

Doch dieser Beweis beinhaltet die Verwendung einer Schwergewichts-Automatisierungs Taktik, omega; Ich rate allen Anfängern dringend, solche Taktiken für eine Weile zu vermeiden und zu lernen, Beweise "mehr" manuell zu machen. Mit einer der SMT-fähigen Taktiken kann das ursprüngliche Ziel einfach mit einem Aufruf an eine SMT gelöst werden.