Library prosa.util.superadditivity


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)

From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.
Require Export prosa.util.nat prosa.util.rel prosa.util.list.

In this section, we define and prove facts about superadditivity and superadditive functions. The definition of superadditivity presented here slightly differs from the standard one ([f a + f b <= f (a + b)] for any [a] and [b]), but it is proven to be equivalent to it.
Section Superadditivity.

First, we define subadditivity as a point-wise property; i.e., [f] is subadditive at [h] if standard subadditivity holds for any pair [(a,b)] that sums to [h].
  Definition superadditive_at f h :=
    ∀ a b,
      a + b = h →
      f a + f b ≤ f h.

Second, we define the concept of partial subadditivity until a certain horizon [h]. This definition is useful when dealing with finite sequences.
  Definition superadditive_until f h :=
    ∀ x,
      x < h →
      superadditive_at f x.

Finally, give a definition of subadditive function: [f] is subadditive when it is subadditive at any point [h].
  Definition superadditive f :=
    ∀ h,
      superadditive_at f h.

In this section, we show that the proposed definition of subadditivity is equivalent to the standard one.
  Section EquivalenceWithStandardDefinition.

First, we give a standard definition of subadditivity.
    Definition superadditive_standard f :=
      ∀ a b,
        f a + f b ≤ f (a + b).

Then, we prove that the two definitions are implied by each other.
    Lemma superadditive_standard_equivalence :
      ∀ f,
        superadditive f ↔ superadditive_standard f.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 36)
  
  ============================
  forall f : nat -> nat, superadditive f <-> superadditive_standard f

----------------------------------------------------------------------------- *)

    Proof.
      split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 39)
  
  f : nat -> nat
  ============================
  superadditive f -> superadditive_standard f

subgoal 2 (ID 40) is:
 superadditive_standard f -> superadditive f

----------------------------------------------------------------------------- *)

      - move⇒ SUPER a b.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 44)
  
  f : nat -> nat
  SUPER : superadditive f
  a, b : nat
  ============================
  f a + f b <= f (a + b)

subgoal 2 (ID 40) is:
 superadditive_standard f -> superadditive f

----------------------------------------------------------------------------- *)

        by apply SUPER.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 40)
  
  f : nat -> nat
  ============================
  superadditive_standard f -> superadditive f

----------------------------------------------------------------------------- *)

      - move⇒ SUPER h a b AB.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 52)
  
  f : nat -> nat
  SUPER : superadditive_standard f
  h, a, b : nat
  AB : a + b = h
  ============================
  f a + f b <= f h

----------------------------------------------------------------------------- *)

        rewrite -AB.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 54)
  
  f : nat -> nat
  SUPER : superadditive_standard f
  h, a, b : nat
  AB : a + b = h
  ============================
  f a + f b <= f (a + b)

----------------------------------------------------------------------------- *)

        by apply SUPER.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

  End EquivalenceWithStandardDefinition.

In the following section, we prove some useful facts about superadditivity.
  Section Facts.

Consider a function [f].
    Variable f : nat → nat.

First, we show that if [f] is superadditive in zero, then its value in zero must also be zero.
    Lemma superadditive_first_zero:
      superadditive_at f 0 →
      f 0 = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 29)
  
  f : nat -> nat
  ============================
  superadditive_at f 0 -> f 0 = 0

----------------------------------------------------------------------------- *)

    Proof.
      move ⇒ SUPER.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 30)
  
  f : nat -> nat
  SUPER : superadditive_at f 0
  ============================
  f 0 = 0

----------------------------------------------------------------------------- *)

      destruct (f 0) eqn:Fx; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 44)
  
  f : nat -> nat
  SUPER : superadditive_at f 0
  n : nat
  Fx : f 0 = n.+1
  ============================
  n.+1 = 0

----------------------------------------------------------------------------- *)

      specialize (SUPER 0 0 (addn0 0)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 46)
  
  f : nat -> nat
  SUPER : f 0 + f 0 <= f 0
  n : nat
  Fx : f 0 = n.+1
  ============================
  n.+1 = 0

----------------------------------------------------------------------------- *)

      contradict SUPER.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 51)
  
  f : nat -> nat
  n : nat
  Fx : f 0 = n.+1
  ============================
  ~ f 0 + f 0 <= f 0

----------------------------------------------------------------------------- *)

      apply /negP; rewrite -ltnNge.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 97)
  
  f : nat -> nat
  n : nat
  Fx : f 0 = n.+1
  ============================
  f 0 < f 0 + f 0

----------------------------------------------------------------------------- *)

      by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

In this section, we show some of the properties of superadditive functions.
    Section SuperadditiveFunctions.

Assume that [f] is superadditive.
      Hypothesis h_superadditive : superadditive f.

First, we show that [f] must also be monotone.
      Lemma superadditive_monotone:
        monotone f leq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 31)
  
  f : nat -> nat
  h_superadditive : superadditive f
  ============================
  monotone f leq

----------------------------------------------------------------------------- *)

      Proof.
        move⇒ x y LEQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 35)
  
  f : nat -> nat
  h_superadditive : superadditive f
  x, y : nat
  LEQ : x <= y
  ============================
  f x <= f y

----------------------------------------------------------------------------- *)

        apply leq_trans with (f x + f (y - x)).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 36)
  
  f : nat -> nat
  h_superadditive : superadditive f
  x, y : nat
  LEQ : x <= y
  ============================
  f x <= f x + f (y - x)

subgoal 2 (ID 37) is:
 f x + f (y - x) <= f y

----------------------------------------------------------------------------- *)

        - by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 37)
  
  f : nat -> nat
  h_superadditive : superadditive f
  x, y : nat
  LEQ : x <= y
  ============================
  f x + f (y - x) <= f y

----------------------------------------------------------------------------- *)

        - apply h_superadditive.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 156)
  
  f : nat -> nat
  h_superadditive : superadditive f
  x, y : nat
  LEQ : x <= y
  ============================
  x + (y - x) = y

----------------------------------------------------------------------------- *)

          by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      Qed.

Next, we prove that moving any factor [m] outside of the arguments of [f] leads to a smaller or equal number.
      Lemma superadditive_leq_mul:
        ∀ n m,
          m × f n ≤ f (m × n).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 34)
  
  f : nat -> nat
  h_superadditive : superadditive f
  ============================
  forall n m : nat, m * f n <= f (m * n)

----------------------------------------------------------------------------- *)

      Proof.
        move⇒ n m.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 36)
  
  f : nat -> nat
  h_superadditive : superadditive f
  n, m : nat
  ============================
  m * f n <= f (m * n)

----------------------------------------------------------------------------- *)

        elim: m⇒ [| m IHm]; first by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 47)
  
  f : nat -> nat
  h_superadditive : superadditive f
  n, m : nat
  IHm : m * f n <= f (m * n)
  ============================
  m.+1 * f n <= f (m.+1 * n)

----------------------------------------------------------------------------- *)

        rewrite !mulSnr.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 132)
  
  f : nat -> nat
  h_superadditive : superadditive f
  n, m : nat
  IHm : m * f n <= f (m * n)
  ============================
  m * f n + f n <= f (m * n + n)

----------------------------------------------------------------------------- *)

        apply leq_trans with (f (m × n) + f n).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 135)
  
  f : nat -> nat
  h_superadditive : superadditive f
  n, m : nat
  IHm : m * f n <= f (m * n)
  ============================
  m * f n + f n <= f (m * n) + f n

subgoal 2 (ID 136) is:
 f (m * n) + f n <= f (m * n + n)

----------------------------------------------------------------------------- *)

        - by rewrite leq_add2r.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 136)
  
  f : nat -> nat
  h_superadditive : superadditive f
  n, m : nat
  IHm : m * f n <= f (m * n)
  ============================
  f (m * n) + f n <= f (m * n + n)

----------------------------------------------------------------------------- *)

        - by apply h_superadditive.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      Qed.

In the next section, we show that any superadditive function that is not the zero constant function (i.e., [f x = 0] for any [x]) is forced to grow beyond any finite limit.
      Section NonZeroSuperadditiveFunctions.

Assume that [f] is not the zero constant function ...
        Hypothesis h_non_zero: ∃ n, f n > 0.

... then, [f] will eventually grow larger than any number.
        Lemma superadditive_unbounded:
          ∀ t, ∃ n', t ≤ f n'.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 40)
  
  f : nat -> nat
  h_superadditive : superadditive f
  h_non_zero : exists n : nat, 0 < f n
  ============================
  forall t : nat, exists n' : nat, t <= f n'

----------------------------------------------------------------------------- *)

        Proof.
          move⇒ t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 41)
  
  f : nat -> nat
  h_superadditive : superadditive f
  h_non_zero : exists n : nat, 0 < f n
  t : nat
  ============================
  exists n' : nat, t <= f n'

----------------------------------------------------------------------------- *)

          move: h_non_zero ⇒ [n LT_n].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 53)
  
  f : nat -> nat
  h_superadditive : superadditive f
  h_non_zero : exists n : nat, 0 < f n
  t, n : nat
  LT_n : 0 < f n
  ============================
  exists n' : nat, t <= f n'

----------------------------------------------------------------------------- *)

          ∃ (t × n).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 55)
  
  f : nat -> nat
  h_superadditive : superadditive f
  h_non_zero : exists n : nat, 0 < f n
  t, n : nat
  LT_n : 0 < f n
  ============================
  t <= f (t * n)

----------------------------------------------------------------------------- *)

          apply leq_trans with (t × f n).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 56)
  
  f : nat -> nat
  h_superadditive : superadditive f
  h_non_zero : exists n : nat, 0 < f n
  t, n : nat
  LT_n : 0 < f n
  ============================
  t <= t * f n

subgoal 2 (ID 57) is:
 t * f n <= f (t * n)

----------------------------------------------------------------------------- *)

          - by apply leq_pmulr.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  f : nat -> nat
  h_superadditive : superadditive f
  h_non_zero : exists n : nat, 0 < f n
  t, n : nat
  LT_n : 0 < f n
  ============================
  t * f n <= f (t * n)

----------------------------------------------------------------------------- *)

          - by apply superadditive_leq_mul.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

        Qed.

      End NonZeroSuperadditiveFunctions.

    End SuperadditiveFunctions.

  End Facts.

In this section, we present the define and prove facts about the minimal superadditive extension of superadditive functions. Given a prefix of a function, there are many ways to continue the function in order to maintain superadditivity. Among these possible extrapolations, there always exists a minimal one.
  Section MinimalExtensionOfSuperadditiveFunctions.

Consider a function [f].
    Variable f : nat → nat.

First, we define what it means to find the minimal extension once a horizon is specified.
    Section Definitions.

Consider a horizon [h]..
      Variable h : nat.

Then, the minimal superadditive extension will be the maximum sum over the pairs that sum to [h]. Note that, in this formula, there are two important edge cases: both [h=0] and [h=1], the sequence of valid sums will be empty, so their maximum will be [0]. In both cases, the extrapolation is nonetheless correct.
      Definition minimal_superadditive_extension :=
        max0 [seq f a + f (h-a) | a <- index_iota 1 h].

    End Definitions.

In the following section, we prove some facts about the minimal superadditive extension. Note that we currently do not prove that the implemented extension is minimal. However, we plan to add this fact in the future. The following discussion provides useful information on the subject, including its connection with Network Calculus: https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/127#note_64177
    Section Facts.

Consider a horizon [h] ...
      Variable h : nat.

... and assume that we know [f] to be superadditive until [h].
      Hypothesis h_superadditive_until : superadditive_until f h.

Moreover, consider a second function, [f'], which is equivalent to [f] in all of its points except for [h], in which its value is exactly the superadditive extension of [f] in [h].
      Variable f' : nat → nat.
      Hypothesis h_f'_min_extension : ∀ t,
          f' t =
          if t == h
          then minimal_superadditive_extension h
          else f t.

First, we prove that [f'] is superadditive also in [h].
      Theorem minimal_extension_superadditive_at_horizon :
        superadditive_at f' h.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 32)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  ============================
  superadditive_at f' h

----------------------------------------------------------------------------- *)

      Proof.
        move ⇒ a b SUM.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 36)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b : nat
  SUM : a + b = h
  ============================
  f' a + f' b <= f' h

----------------------------------------------------------------------------- *)

        rewrite !h_f'_min_extension.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b : nat
  SUM : a + b = h
  ============================
  (if a == h then minimal_superadditive_extension h else f a) +
  (if b == h then minimal_superadditive_extension h else f b) <=
  (if h == h then minimal_superadditive_extension h else f h)

----------------------------------------------------------------------------- *)

        rewrite -SUM.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b : nat
  SUM : a + b = h
  ============================
  (if a == a + b then minimal_superadditive_extension (a + b) else f a) +
  (if b == a + b then minimal_superadditive_extension (a + b) else f b) <=
  (if a + b == a + b
   then minimal_superadditive_extension (a + b)
   else f (a + b))

----------------------------------------------------------------------------- *)

        destruct a as [|a'] eqn:EQa; destruct b as [|b'] eqn:EQb ⇒ //=.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 100)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b : nat
  EQa : a = 0
  b' : nat
  EQb : b = b'.+1
  SUM : 0 + b'.+1 = h
  ============================
  f 0 +
  (if b'.+1 == 0 + b'.+1
   then minimal_superadditive_extension (0 + b'.+1)
   else f b'.+1) <=
  (if 0 + b'.+1 == 0 + b'.+1
   then minimal_superadditive_extension (0 + b'.+1)
   else f (0 + b'.+1))

subgoal 2 (ID 147) is:
 (if a'.+1 == a'.+1 + 0
  then minimal_superadditive_extension (a'.+1 + 0)
  else f a'.+1) + f 0 <=
 (if a'.+1 + 0 == a'.+1 + 0
  then minimal_superadditive_extension (a'.+1 + 0)
  else f (a'.+1 + 0))
subgoal 3 (ID 176) is:
 (if a'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f a'.+1) +
 (if b'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f b'.+1) <=
 (if a'.+1 + b'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f (a'.+1 + b'.+1))

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 100)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b : nat
  EQa : a = 0
  b' : nat
  EQb : b = b'.+1
  SUM : 0 + b'.+1 = h
  ============================
  f 0 +
  (if b'.+1 == 0 + b'.+1
   then minimal_superadditive_extension (0 + b'.+1)
   else f b'.+1) <=
  (if 0 + b'.+1 == 0 + b'.+1
   then minimal_superadditive_extension (0 + b'.+1)
   else f (0 + b'.+1))

----------------------------------------------------------------------------- *)

rewrite add0n eq_refl superadditive_first_zero; first by rewrite add0n.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 211)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b : nat
  EQa : a = 0
  b' : nat
  EQb : b = b'.+1
  SUM : 0 + b'.+1 = h
  ============================
  superadditive_at f 0

----------------------------------------------------------------------------- *)

          by apply h_superadditive_until; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals

subgoal 1 (ID 147) is:
 (if a'.+1 == a'.+1 + 0
  then minimal_superadditive_extension (a'.+1 + 0)
  else f a'.+1) + f 0 <=
 (if a'.+1 + 0 == a'.+1 + 0
  then minimal_superadditive_extension (a'.+1 + 0)
  else f (a'.+1 + 0))
subgoal 2 (ID 176) is:
 (if a'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f a'.+1) +
 (if b'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f b'.+1) <=
 (if a'.+1 + b'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f (a'.+1 + b'.+1))

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 147)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  EQb : b = 0
  SUM : a'.+1 + 0 = h
  ============================
  (if a'.+1 == a'.+1 + 0
   then minimal_superadditive_extension (a'.+1 + 0)
   else f a'.+1) + f 0 <=
  (if a'.+1 + 0 == a'.+1 + 0
   then minimal_superadditive_extension (a'.+1 + 0)
   else f (a'.+1 + 0))

subgoal 2 (ID 176) is:
 (if a'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f a'.+1) +
 (if b'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f b'.+1) <=
 (if a'.+1 + b'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f (a'.+1 + b'.+1))

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 147)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  EQb : b = 0
  SUM : a'.+1 + 0 = h
  ============================
  (if a'.+1 == a'.+1 + 0
   then minimal_superadditive_extension (a'.+1 + 0)
   else f a'.+1) + f 0 <=
  (if a'.+1 + 0 == a'.+1 + 0
   then minimal_superadditive_extension (a'.+1 + 0)
   else f (a'.+1 + 0))

----------------------------------------------------------------------------- *)

rewrite addn0 eq_refl superadditive_first_zero; first by rewrite addn0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 350)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  EQb : b = 0
  SUM : a'.+1 + 0 = h
  ============================
  superadditive_at f 0

----------------------------------------------------------------------------- *)

          by apply h_superadditive_until; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 176) is:
 (if a'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f a'.+1) +
 (if b'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f b'.+1) <=
 (if a'.+1 + b'.+1 == a'.+1 + b'.+1
  then minimal_superadditive_extension (a'.+1 + b'.+1)
  else f (a'.+1 + b'.+1))

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 176)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  b' : nat
  EQb : b = b'.+1
  SUM : a'.+1 + b'.+1 = h
  ============================
  (if a'.+1 == a'.+1 + b'.+1
   then minimal_superadditive_extension (a'.+1 + b'.+1)
   else f a'.+1) +
  (if b'.+1 == a'.+1 + b'.+1
   then minimal_superadditive_extension (a'.+1 + b'.+1)
   else f b'.+1) <=
  (if a'.+1 + b'.+1 == a'.+1 + b'.+1
   then minimal_superadditive_extension (a'.+1 + b'.+1)
   else f (a'.+1 + b'.+1))

----------------------------------------------------------------------------- *)

        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 176)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  b' : nat
  EQb : b = b'.+1
  SUM : a'.+1 + b'.+1 = h
  ============================
  (if a'.+1 == a'.+1 + b'.+1
   then minimal_superadditive_extension (a'.+1 + b'.+1)
   else f a'.+1) +
  (if b'.+1 == a'.+1 + b'.+1
   then minimal_superadditive_extension (a'.+1 + b'.+1)
   else f b'.+1) <=
  (if a'.+1 + b'.+1 == a'.+1 + b'.+1
   then minimal_superadditive_extension (a'.+1 + b'.+1)
   else f (a'.+1 + b'.+1))

----------------------------------------------------------------------------- *)

rewrite -!EQa -!EQb eq_refl //=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 484)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  b' : nat
  EQb : b = b'.+1
  SUM : a'.+1 + b'.+1 = h
  ============================
  (if a == a + b then minimal_superadditive_extension (a + b) else f a) +
  (if b == a + b then minimal_superadditive_extension (a + b) else f b) <=
  minimal_superadditive_extension (a + b)

----------------------------------------------------------------------------- *)

          rewrite -{1}(addn0 a) eqn_add2l {1}EQb //=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 516)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  b' : nat
  EQb : b = b'.+1
  SUM : a'.+1 + b'.+1 = h
  ============================
  f a + (if b == a + b then minimal_superadditive_extension (a + b) else f b) <=
  minimal_superadditive_extension (a + b)

----------------------------------------------------------------------------- *)

          rewrite -{1}(add0n b) eqn_add2r {2}EQa //=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 548)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  b' : nat
  EQb : b = b'.+1
  SUM : a'.+1 + b'.+1 = h
  ============================
  f a + f b <= minimal_superadditive_extension (a + b)

----------------------------------------------------------------------------- *)

          rewrite /minimal_superadditive_extension.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 570)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  b' : nat
  EQb : b = b'.+1
  SUM : a'.+1 + b'.+1 = h
  ============================
  f a + f b <= max0 [seq f a0 + f (a + b - a0) | a0 <- index_iota 1 (a + b)]

----------------------------------------------------------------------------- *)

          apply in_max0_le.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 571)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  b' : nat
  EQb : b = b'.+1
  SUM : a'.+1 + b'.+1 = h
  ============================
  f a + f b \in [seq f a0 + f (a + b - a0) | a0 <- index_iota 1 (a + b)]

----------------------------------------------------------------------------- *)

          apply /mapP; ∃ a.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 609)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  b' : nat
  EQb : b = b'.+1
  SUM : a'.+1 + b'.+1 = h
  ============================
  a \in index_iota 1 (a + b)

subgoal 2 (ID 610) is:
 f a + f b = f a + f (a + b - a)

----------------------------------------------------------------------------- *)

          - by rewrite mem_iota; ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 610)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  a, b, a' : nat
  EQa : a = a'.+1
  b' : nat
  EQb : b = b'.+1
  SUM : a'.+1 + b'.+1 = h
  ============================
  f a + f b = f a + f (a + b - a)

----------------------------------------------------------------------------- *)

          - by have → : a + b - a = b by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      Qed.

And finally, we prove that [f'] is superadditive until [h.+1].
      Lemma minimal_extension_superadditive_until :
        superadditive_until f' h.+1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 33)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  ============================
  superadditive_until f' h.+1

----------------------------------------------------------------------------- *)

      Proof.
        move⇒ t LEQh a b SUM.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 40)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  t : nat
  LEQh : t < h.+1
  a, b : nat
  SUM : a + b = t
  ============================
  f' a + f' b <= f' t

----------------------------------------------------------------------------- *)

        destruct (ltngtP t h) as [LT | GT | EQ].

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 149)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  t : nat
  LEQh : t < h.+1
  a, b : nat
  SUM : a + b = t
  LT : t < h
  ============================
  f' a + f' b <= f' t

subgoal 2 (ID 150) is:
 f' a + f' b <= f' t
subgoal 3 (ID 151) is:
 f' a + f' b <= f' t

----------------------------------------------------------------------------- *)

        - rewrite !h_f'_min_extension.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 160)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  t : nat
  LEQh : t < h.+1
  a, b : nat
  SUM : a + b = t
  LT : t < h
  ============================
  (if a == h then minimal_superadditive_extension h else f a) +
  (if b == h then minimal_superadditive_extension h else f b) <=
  (if t == h then minimal_superadditive_extension h else f t)

subgoal 2 (ID 150) is:
 f' a + f' b <= f' t
subgoal 3 (ID 151) is:
 f' a + f' b <= f' t

----------------------------------------------------------------------------- *)

          rewrite !ltn_eqF; try ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 178)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  t : nat
  LEQh : t < h.+1
  a, b : nat
  SUM : a + b = t
  LT : t < h
  ============================
  f a + f b <= f t

subgoal 2 (ID 150) is:
 f' a + f' b <= f' t
subgoal 3 (ID 151) is:
 f' a + f' b <= f' t

----------------------------------------------------------------------------- *)

          by apply h_superadditive_until.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 150)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  t : nat
  LEQh : t < h.+1
  a, b : nat
  SUM : a + b = t
  GT : h < t
  ============================
  f' a + f' b <= f' t

subgoal 2 (ID 151) is:
 f' a + f' b <= f' t

----------------------------------------------------------------------------- *)

        - by ssrlia.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 151)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  t : nat
  LEQh : t < h.+1
  a, b : nat
  SUM : a + b = t
  EQ : t = h
  ============================
  f' a + f' b <= f' t

----------------------------------------------------------------------------- *)

        - rewrite EQ in SUM; rewrite EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1082)
  
  f : nat -> nat
  h : nat
  h_superadditive_until : superadditive_until f h
  f' : nat -> nat
  h_f'_min_extension : forall t : nat,
                       f' t =
                       (if t == h
                        then minimal_superadditive_extension h
                        else f t)
  t : nat
  LEQh : t < h.+1
  a, b : nat
  EQ : t = h
  SUM : a + b = h
  ============================
  f' a + f' b <= f' h

----------------------------------------------------------------------------- *)

          by apply minimal_extension_superadditive_at_horizon.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      Qed.

    End Facts.

  End MinimalExtensionOfSuperadditiveFunctions.

End Superadditivity.