Coq: Как доказать max a b <= a+b?

Question

Я не могу доказать простую логику max a b <= a+b используя тактику Coq. Как мне решить эту проблему? Ниже приведен код, над которым я работал до сих пор. 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.

На самом деле, в свете краткого доказательства, возможно, первоначальная лемма вообще не была нужна.

edit: @Jason Gross упоминает другой стиль доказательства, который использовался бы более опытным:

Proof. apply Max.max_case_strong; omega. Qed.

Тем не менее, это доказательство предполагает использование тяжелой тактики автоматизации, omega; Я настоятельно советую всем начинающим избегать такой тактики на некоторое время и научиться делать доказательства более "вручную". Фактически, используя любую из тактик с поддержкой SMT, первоначальная цель может быть просто решена с помощью вызова SMT.