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

Question (re3el)

I am unable to prove the simple logic max a b <= a + b using coq's tactics. How should I go about solving it? Below is the code that I worked on till now. s_le_n is proved but not mentioned here for the sake of simplicity.

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

Theorem max_sum: forall (a b: nat), max a b <= a + b.
forall a b : nat, Nat.max a b <= a + b
Proof.
forall a b : nat, Nat.max a b <= a + b
  intros.
a, b: nat
Nat.max a b <= a + b induction a.
b: nat
Nat.max 0 b <= 0 + b
a, b: nat
IHa: Nat.max a b <= a + b
Nat.max (S a) b <= S a + b
  -
b: nat
Nat.max 0 b <= 0 + b simpl.
b: nat
b <= b apply le_n.
  -
a, b: nat
IHa: Nat.max a b <= a + b
Nat.max (S a) b <= S a + b rewrite plus_Sn_m.
a, b: nat
IHa: Nat.max a b <= a + b
Nat.max (S a) b <= S (a + b) induction b.
a: nat
IHa: Nat.max a 0 <= a + 0
Nat.max (S a) 0 <= S (a + 0)
a, b: nat
IHa: Nat.max a (S b) <= a + S b
IHb: Nat.max a b <= a + b -> Nat.max (S a) b <= S (a + b)
Nat.max (S a) (S b) <= S (a + S b)
    +
a: nat
IHa: Nat.max a 0 <= a + 0
Nat.max (S a) 0 <= S (a + 0) simpl.
a: nat
IHa: Nat.max a 0 <= a + 0
S a <= S (a + 0) rewrite <- plus_n_O.
a: nat
IHa: Nat.max a 0 <= a + 0
S a <= S a apply le_n.
    +
a, b: nat
IHa: Nat.max a (S b) <= a + S b
IHb: Nat.max a b <= a + b -> Nat.max (S a) b <= S (a + b)
Nat.max (S a) (S b) <= S (a + S b) rewrite <- plus_Sn_m.
a, b: nat
IHa: Nat.max a (S b) <= a + S b
IHb: Nat.max a b <= a + b -> Nat.max (S a) b <= S (a + b)
Nat.max (S a) (S b) <= S a + S b simpl.
a, b: nat
IHa: Nat.max a (S b) <= a + S b
IHb: Nat.max a b <= a + b -> Nat.max (S a) b <= S (a + b)
S (Nat.max a b) <= S (a + S b) apply s_le_n.
a, b: nat
IHa: Nat.max a (S b) <= a + S b
IHb: Nat.max a b <= a + b -> Nat.max (S a) b <= S (a + b)
Nat.max a b <= a + S b rewrite IHa.
Found no subterm matching "Nat.max a (S b)" in the current goal.
a, b: nat
IHa: Nat.max a (S b) <= a + S b
IHb: Nat.max a b <= a + b -> Nat.max (S a) b <= S (a + b)
Nat.max a b <= a + S b

Q (ejgallego): The proof is less than 40 characters using the library, I could post it; however, let me ask you something, how would you prove this lemma using pen and paper?

A (re3el): @ejgallego if (a > b) then max a b = a, a < a + b; else max a b = b, b < a + b. I am unable to use this logic in coq.

Answer (ejgallego)

Taking into account @re3el comment, we start from their "pen and paper proof":

if (a > b) then max a b = a, a < a + b; else max a b = b, b < a + b

Let's now translate that into Coq! In fact, the first thing we need to do is case on the decidability of <, this is done using the le_lt_dec a b lemma. The rest is routine:

Require Import Arith.

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

However, we can improve this proof quite a bit. There are various candidates, a good one using the stdlib is:

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

Using my library of choice [math-comp], you can chain the rewrites to get a more compact proof:

From mathcomp Require Import all_ssreflect.
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ ^ _" was already used in scope nat_scope.
[notation-overridden,parsing]

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

In fact, on the light of short proof, maybe the original lemma was not even needed in the first place.

edit: @Jason Gross mentions another style of proof a more seasoned used would use:

Proof.
a, b: nat
Nat.max a b <= a + b apply Max.max_case_strong; lia. Qed.

However, this proof involves the use of a heavyweight automation tactic, lia; I strongly advise all beginners to avoid such tactics for a while, and learn how to do proofs more "manually". In fact, using any of the SMT-enabled tactics, the original goal can be simply solved with a call to a SMT.

A (Jason Gross): There's also a short proof without ssr: Require Import Lia. apply Max.max_case_strong; lia. It might be nice to mention this in the answer.

A (ejgallego): Thanks Jason; I tend to prefer not to teach lia and other automated tactics to beginners, IMHO it is very important that they learn how to do proofs without automation first.