.gitlab-ci.yml

@@ -11,7 +11,7 @@ stages:
     - opam install -y -v -j ${NJOBS} coq-prosa
 
 .preferred-stable-version:
-    image: mathcomp/mathcomp:1.10.0-coq-8.11
+    image: mathcomp/mathcomp:1.12.0-coq-8.13
 
 .build:
   image: mathcomp/mathcomp:${CI_JOB_NAME}
@@ -23,14 +23,14 @@ stages:
 
 .build-for-process:
   stage: build
-  image: mathcomp/mathcomp:1.10.0-coq-8.11
+  image: mathcomp/mathcomp:1.12.0-coq-8.13
   script:
     - ./create_makefile.sh --without-classic
     - make -j ${NJOBS}
 
 .build-for-process-classic:
   stage: build
-  image: mathcomp/mathcomp:1.10.0-coq-8.11
+  image: mathcomp/mathcomp:1.12.0-coq-8.13
   script:
     - ./create_makefile.sh --only-classic
     - make -j ${NJOBS}
@@ -72,6 +72,9 @@ stages:
 1.11.0-coq-8.12:
   extends: .build
 
+1.12.0-coq-8.13:
+  extends: .build
+
 build-for-process:
   extends:
     - .build-for-process
@@ -94,7 +97,7 @@ spell-check:
   script:
     - scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './classic/*'`
 
-coq-8.12:
+coq-8.13:
   extends:
     - .build-dev
   # it's ok to fail with an unreleased version of ssreflect

analysis/definitions/completion_sequence.v

+From mathcomp Require Export ssreflect seq ssrnat ssrbool eqtype.
+Require Import prosa.behavior.service.
+
+(** This module contains basic definitions and properties of job
+    completion sequences. *)
+
+(** * Notion of a Completion Sequence *)
+
+(** We begin by defining a job completion sequence. *)
+Section CompletionSequence.
+
+  (** Consider any kind of jobs with a cost
+     and any kind of processor state. *)
+  Context {Job : JobType} `{JobCost Job} {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** Consider any job arrival sequence. *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (** Consider any schedule. *)
+  Variable sched : schedule PState.
+
+  (** For each instant [t], the completion sequence returns all
+     arrived jobs that have completed at [t]. *)
+  Definition completion_sequence : arrival_sequence Job :=
+    fun t => [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
+
+End CompletionSequence.

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.
 

coq-prosa.opam

@@ -13,8 +13,8 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {((>= "8.11" & < "8.13~") | = "dev")}
-  "coq-mathcomp-ssreflect" {((>= "1.10" & < "1.12~") | = "dev")}
+  "coq" {((>= "8.11" & < "8.14~") | = "dev")}
+  "coq-mathcomp-ssreflect" {((>= "1.10" & < "1.13~") | = "dev")}
 ]
 
 tags: [

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

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.