diff --git a/analysis/facts/hyperperiod.v b/analysis/facts/hyperperiod.v
index 6ba6b68d5bcb03271b0248532bae3e3b994ccb17..fdcd392df8f506bd85e302c9d4577ee613a40f54 100644
--- a/analysis/facts/hyperperiod.v
+++ b/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.
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index a1eba2fda3cb9b0962357b67cc6dd9e6b549f172..3df9e5318c4eff68edc4a31cb98e17e613f9b830 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -56,4 +56,8 @@ pointwise
notational
multiset
superset
-RTCT
\ No newline at end of file
+RTCT
+superadditivity
+superadditive
+subadditivity
+subadditive
\ No newline at end of file
diff --git a/util/div_mod.v b/util/div_mod.v
index 60347602daaafacc99e791a2c0d911ba4bbfd4c4..100a2b28fd77e371b50908b33ff5d08012066447 100644
--- a/util/div_mod.v
+++ b/util/div_mod.v
@@ -1,6 +1,5 @@
-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.
diff --git a/util/subadditivity.v b/util/subadditivity.v
new file mode 100644
index 0000000000000000000000000000000000000000..576c93e0c55d35639c43210da6aaf7e9652dcfd9
--- /dev/null
+++ b/util/subadditivity.v
@@ -0,0 +1,85 @@
+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.
+
diff --git a/util/superadditivity.v b/util/superadditivity.v
new file mode 100644
index 0000000000000000000000000000000000000000..592be15970a4b3e00fae6d4b5df2f21d34dee701
--- /dev/null
+++ b/util/superadditivity.v
@@ -0,0 +1,223 @@
+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.