superadditivity.v

From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.util.nat prosa.util.rel prosa.util.list.[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]

(** 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 :=
    forall 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 :=
    forall 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 :=
    forall 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 :=
      forall 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 :
      forall f,
        superadditive f <-> superadditive_standard f.forall f : nat -> nat,
superadditive f <-> superadditive_standard f
    Proof.forall f : nat -> nat,
superadditive f <-> superadditive_standard f
      split.f: nat -> nat
superadditive f -> superadditive_standard f
f: nat -> nat
superadditive_standard f -> superadditive f
      -f: nat -> nat
superadditive f -> superadditive_standard f move=> SUPER a b.f: nat -> nat
SUPER: superadditive f
a, b: nat
f a + f b <= f (a + b)
        by apply SUPER.
      -f: nat -> nat
superadditive_standard f -> superadditive f move=> SUPER h a b AB.f: nat -> nat
SUPER: superadditive_standard f
h, a, b: nat
AB: a + b = h
f a + f b <= f h
        rewrite -AB.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.
    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.f: nat -> nat
superadditive_at f 0 -> f 0 = 0
    Proof.f: nat -> nat
superadditive_at f 0 -> f 0 = 0
      move => SUPER.f: nat -> nat
SUPER: superadditive_at f 0
f 0 = 0
      destruct (f 0) eqn:Fx; first by done.f: nat -> nat
SUPER: superadditive_at f 0
n: nat
Fx: f 0 = n.+1
n.+1 = 0
      specialize (SUPER 0 0 (addn0 0)).f: nat -> nat
SUPER: f 0 + f 0 <= f 0
n: nat
Fx: f 0 = n.+1
n.+1 = 0
      contradict SUPER.f: nat -> nat
n: nat
Fx: f 0 = n.+1
~ f 0 + f 0 <= f 0
      apply /negP; rewrite -ltnNge.f: nat -> nat
n: nat
Fx: f 0 = n.+1
f 0 < f 0 + f 0
      by lia.
    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 leq f.f: nat -> nat
h_superadditive: superadditive f
monotone leq f
      Proof.f: nat -> nat
h_superadditive: superadditive f
monotone leq f
        move=> x y LEQ.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)).f: nat -> nat
h_superadditive: superadditive f
x, y: nat
LEQ: x <= y
f x <= f x + f (y - x)
f: nat -> nat
h_superadditive: superadditive f
x, y: nat
LEQ: x <= y
f x + f (y - x) <= f y
        -f: nat -> nat
h_superadditive: superadditive f
x, y: nat
LEQ: x <= y
f x <= f x + f (y - x) by lia.
        -f: nat -> nat
h_superadditive: superadditive f
x, y: nat
LEQ: x <= y
f x + f (y - x) <= f y apply h_superadditive.f: nat -> nat
h_superadditive: superadditive f
x, y: nat
LEQ: x <= y
x + (y - x) = y
          by lia.
      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:
        forall n m,
          m * f n <= f (m * n).f: nat -> nat
h_superadditive: superadditive f
forall n m : nat, m * f n <= f (m * n)
      Proof.f: nat -> nat
h_superadditive: superadditive f
forall n m : nat, m * f n <= f (m * n)
        move=> n m.f: nat -> nat
h_superadditive: superadditive f
n, m: nat
m * f n <= f (m * n)
        elim: m=> [| m IHm]; first by lia.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.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).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
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)
        -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 by rewrite leq_add2r.
        -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.
      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: exists n, f n > 0.

        (** ... then, [f] will eventually grow larger than any number. *)
        Lemma superadditive_unbounded:
          forall t, exists n', t <= f n'.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.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' 
          move=> t.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].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'
          exists (t * n).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).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
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)
          -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 by apply leq_pmulr.
          -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.
        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 : forall 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.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.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
        move => a b SUM.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.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.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 => //=.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))
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))
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))
        {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.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; lia. }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))
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))
        {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.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; lia. }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))
        {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 //=.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 //=.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 //=.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.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.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; exists a.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)
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)
          -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) by rewrite mem_iota; lia.
          -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 lia. }
      Qed. 

      (** And finally, we prove that [f'] is superadditive until [h.+1]. *)
      Lemma minimal_extension_superadditive_until :
        superadditive_until f' h.+1.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.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
        move=> t LEQh a b SUM.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].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
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
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
        -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 rewrite !h_f'_min_extension.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)
          rewrite !ltn_eqF; try lia.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
          by apply h_superadditive_until.
        -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 by lia.
        -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.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.
      Qed.
      
    End Facts.
    
  End MinimalExtensionOfSuperadditiveFunctions.

End Superadditivity.