add definitions of super- and sub-additivity

...and some supporting theory. This will be needed to handle arrival curves extrapolated from a finite prefix.

analysis/facts/hyperperiod.v

@@ -210,7 +210,7 @@ Section PeriodicLemmas.
       now apply leq_trunc_div.
     + specialize (div_floor_add_g (job_arrival j1 - O_max) HP) => AB.
       feed_n 1 AB; first by apply valid_periods_imply_pos_hp => //.
-      apply ltn_subLR in AB.
+      rewrite ltn_subLR // in AB.
       now rewrite -/(HP); ssrlia.
   Qed.
 

scripts/wordlist.pws

@@ -56,4 +56,8 @@ pointwise
 notational
 multiset
 superset
-RTCT
+RTCT
\ No newline at end of file
+superadditivity
+superadditive
+subadditivity
+subadditive
\ No newline at end of file

util/div_mod.v

-Require Export prosa.util.nat.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
-
+Require Export prosa.util.nat prosa.util.subadditivity.
+From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
 
 Definition div_floor (x y: nat) : nat := x %/ y.
 Definition div_ceil (x y: nat) := if y %| x then x %/ y else (x %/ y).+1.
@@ -30,4 +29,27 @@ Proof.
   rewrite [in X in X < _]DIV.
   rewrite ltn_add2l.
   now apply ltn_pmod.
-Qed.    
+Qed.
+
+(** We show that the division with ceiling by a constant [T] is a subadditive function. *)
+Lemma div_ceil_subadditive:
+  forall T,
+    subadditive (div_ceil^~T).
+Proof.
+  move=> T ab a b SUM.
+  rewrite -SUM.
+  destruct (T %| a) eqn:DIVa, (T %| b) eqn:DIVb.
+  - have DIVab: T %| a + b by apply dvdn_add.
+    by rewrite /div_ceil DIVa DIVb DIVab divnDl.
+  - have DIVab: T %| a+b = false by rewrite -DIVb; apply dvdn_addr.
+    by rewrite /div_ceil DIVa DIVb DIVab divnDl //=; ssrlia.
+  - have DIVab: T %| a+b = false by rewrite -DIVa; apply dvdn_addl.
+    by rewrite /div_ceil DIVa DIVb DIVab divnDr //=; ssrlia.
+  - destruct (T %| a + b) eqn:DIVab.
+    + rewrite /div_ceil DIVa DIVb DIVab.
+      apply leq_trans with (a %/ T + b %/T + 1); last by ssrlia.
+      by apply leq_divDl.
+    + rewrite /div_ceil DIVa DIVb DIVab.
+      apply leq_ltn_trans with (a %/ T + b %/T + 1); last by ssrlia.
+      by apply leq_divDl.
+Qed.

util/subadditivity.v

+From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.
+
+(** In this section, we define and prove facts about subadditivity and 
+    subadditive functions. The definition of subadditivity presented here 
+    slightly differs from the standard one ([f (a + b) <= f a + f b] for any 
+    [a] and [b]), but it is proven to be equivalent to it. *)
+Section Subadditivity.
+
+  (** 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 subadditive_at f h :=
+    forall a b,
+      a + b = h ->
+      f h <= f a + f b.
+
+  (** Second, we define the concept of partial subadditivity until a certain 
+      horizon [h]. This definition is useful when dealing with finite sequences. *)
+  Definition subadditive_until f h :=
+    forall x,
+      x < h ->
+      subadditive_at f x.
+
+  (** Finally, give a definition of subadditive function: [f] is subadditive 
+      when it is subadditive at any point [h].*)
+  Definition subadditive f :=
+    forall h,
+      subadditive_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 subadditive_standard f :=
+      forall a b,
+         f (a + b) <= f a + f b.
+
+    (** Then, we prove that the two definitions are implied by each other. *)
+    Lemma subadditive_standard_equivalence :
+      forall f,
+        subadditive f <-> subadditive_standard f.
+    Proof.
+      split.
+      - move=> SUB a b.
+        by apply SUB.
+      - move=> SUB h a b AB.
+        rewrite -AB.
+        by apply SUB.
+    Qed.
+
+  End EquivalenceWithStandardDefinition.
+
+  (** In the following section, we prove some useful facts about subadditivity. *)
+  Section Facts.
+
+    (** Consider a function [f]. *)
+    Variable f : nat -> nat.
+
+    (** In this section, we show some of the properties of subadditive functions. *)
+    Section SubadditiveFunctions.
+
+      (** Assume that [f] is subadditive. *)
+      Hypothesis h_subadditive : subadditive f.
+
+      (** Then, we prove that moving any non-zero factor [m] outside of the arguments
+          of [f] leads to a bigger or equal number. *)
+      Lemma subadditive_leq_mul:
+        forall n m,
+          0 < m ->
+          f (m * n) <= m * f n.
+      Proof.
+        move=> n [// | m] _.
+        elim: m => [ | m IHm]; first by rewrite !mul1n.
+        rewrite mulSnr [X in _ <= X]mulSnr.
+        move: IHm; rewrite -(leq_add2r (f n)).
+        exact /leq_trans/h_subadditive.
+      Qed.
+
+    End SubadditiveFunctions.
+    
+  End Facts.
+  
+End Subadditivity.
+

util/superadditivity.v

+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 :=
+    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.
+    Proof.
+      split.
+      - move=> SUPER a b.
+        by apply SUPER.
+      - move=> SUPER h a b AB.
+        rewrite -AB.
+        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.
+    Proof.
+      move => SUPER.
+      destruct (f 0) eqn:Fx; first by done.
+      specialize (SUPER 0 0 (addn0 0)).
+      contradict SUPER.
+      apply /negP; rewrite -ltnNge.
+      by ssrlia.
+    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.
+      Proof.
+        move=> x y LEQ.
+        apply leq_trans with (f x + f (y - x)).
+        - by ssrlia.
+        - apply h_superadditive.
+          by ssrlia.
+      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).
+      Proof.
+        move=> n m.
+        elim: m=> [| m IHm]; first by ssrlia.
+        rewrite !mulSnr.
+        apply leq_trans with (f (m * n) + f n).
+        - by rewrite leq_add2r.
+        - 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'.
+        Proof. 
+          move=> t.
+          move: h_non_zero => [n LT_n].
+          exists (t * n).
+          apply leq_trans with (t * f n).
+          - by apply leq_pmulr.
+          - 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.
+      Proof.
+        move => a b SUM.
+        rewrite !h_f'_min_extension.
+        rewrite -SUM.
+        destruct a as [|a'] eqn:EQa; destruct b as [|b'] eqn:EQb => //=.
+        { rewrite add0n eq_refl superadditive_first_zero; first by rewrite add0n.
+          by apply h_superadditive_until; ssrlia. }
+        { rewrite addn0 eq_refl superadditive_first_zero; first by rewrite addn0.
+          by apply h_superadditive_until; ssrlia. }
+        { rewrite -!EQa -!EQb eq_refl //=.
+          rewrite -{1}(addn0 a) eqn_add2l {1}EQb //=.
+          rewrite -{1}(add0n b) eqn_add2r {2}EQa //=.
+          rewrite /minimal_superadditive_extension.
+          apply in_max0_le.
+          apply /mapP; exists a.
+          - by rewrite mem_iota; ssrlia.
+          - by have -> : a + b - a = b by ssrlia. }
+      Qed. 
+
+      (** And finally, we prove that [f'] is superadditive until [h.+1]. *)
+      Lemma minimal_extension_superadditive_until :
+        superadditive_until f' h.+1.
+      Proof.
+        move=> t LEQh a b SUM.
+        destruct (ltngtP t h) as [LT | GT | EQ].
+        - rewrite !h_f'_min_extension.
+          rewrite !ltn_eqF; try ssrlia.
+          by apply h_superadditive_until.
+        - by ssrlia.
+        - rewrite EQ in SUM; rewrite EQ.
+          by apply minimal_extension_superadditive_at_horizon.
+      Qed.
+      
+    End Facts.
+    
+  End MinimalExtensionOfSuperadditiveFunctions.
+
+End Superadditivity.