Clean-up code

Makefile

@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile BertognaResponseTimeDefsEDF.v BertognaResponseTimeDefsJitter.v BertognaResponseTimeDefs.v BertognaResponseTimeEDFComp.v BertognaResponseTimeFPJitter.v BertognaResponseTimeFP.v divround.v extralib.v ExtraRelations.v GuanDefs.v GuanFP.v helper.v InterferenceDefs.v JobDefs.v PlatformDefs.v PriorityDefs.v ResponseTimeDefs.v SchedulabilityDefs.v ScheduleDefs.v ssromega.v TaskArrivalDefs.v TaskDefs.v Vbase.v WorkloadDefsJitter.v WorkloadDefs.v 
+# coq_makefile bertogna_edf_comp.v bertogna_edf_theory.v bertogna_fp_comp.v bertogna_fp_jitter_comp.v bertogna_fp_jitter_theory.v bertogna_fp_theory.v extralib.v ExtraRelations.v guan_fp_comp.v guan_fp_theory.v interference.v job.v platform.v priority.v response_time.v schedulability.v schedule.v ssromega.v task_arrival.v task.v util_divround.v util_lemmas.v Vbase.v workload_jitter.v workload.v 
 #
 
 .DEFAULT_GOAL := all
@@ -80,31 +80,31 @@ endif
 #                    #
 ######################
 
-VFILES:=BertognaResponseTimeDefsEDF.v\
-  BertognaResponseTimeDefsJitter.v\
-  BertognaResponseTimeDefs.v\
-  BertognaResponseTimeEDFComp.v\
-  BertognaResponseTimeFPJitter.v\
-  BertognaResponseTimeFP.v\
-  divround.v\
+VFILES:=bertogna_edf_comp.v\
+  bertogna_edf_theory.v\
+  bertogna_fp_comp.v\
+  bertogna_fp_jitter_comp.v\
+  bertogna_fp_jitter_theory.v\
+  bertogna_fp_theory.v\
   extralib.v\
   ExtraRelations.v\
-  GuanDefs.v\
-  GuanFP.v\
-  helper.v\
-  InterferenceDefs.v\
-  JobDefs.v\
-  PlatformDefs.v\
-  PriorityDefs.v\
-  ResponseTimeDefs.v\
-  SchedulabilityDefs.v\
-  ScheduleDefs.v\
+  guan_fp_comp.v\
+  guan_fp_theory.v\
+  interference.v\
+  job.v\
+  platform.v\
+  priority.v\
+  response_time.v\
+  schedulability.v\
+  schedule.v\
   ssromega.v\
-  TaskArrivalDefs.v\
-  TaskDefs.v\
+  task_arrival.v\
+  task.v\
+  util_divround.v\
+  util_lemmas.v\
   Vbase.v\
-  WorkloadDefsJitter.v\
-  WorkloadDefs.v
+  workload_jitter.v\
+  workload.v
 
 -include $(addsuffix .d,$(VFILES))
 .SECONDARY: $(addsuffix .d,$(VFILES))

BertognaResponseTimeEDFComp.v → bertogna_edf_comp.v

-Require Import Vbase ScheduleDefs BertognaResponseTimeDefsEDF divround helper
-               ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
+Require Import Vbase schedule bertogna_edf_theory util_divround util_lemmas
+               ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationEDF.
 

BertognaResponseTimeDefsEDF.v → bertogna_edf_theory.v

-Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
-        PlatformDefs WorkloadDefs SchedulabilityDefs PriorityDefs
-        ResponseTimeDefs BertognaResponseTimeDefs divround helper
-        ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
+Require Import Vbase task job task_arrival schedule platform
+        workload schedulability priority response_time
+        bertogna_fp_theory util_divround util_lemmas
+        ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeAnalysisEDF.
 

BertognaResponseTimeFP.v → bertogna_fp_comp.v

-Require Import Vbase ScheduleDefs BertognaResponseTimeDefs divround helper
-               ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
+Require Import Vbase schedule bertogna_fp_theory util_divround util_lemmas
+               ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
 
 Module ResponseTimeIterationFP.
 

BertognaResponseTimeFPJitter.v → bertogna_fp_jitter_comp.v

-Require Import Vbase JobDefs TaskDefs ScheduleDefs TaskArrivalDefs PriorityDefs WorkloadDefsJitter BertognaResponseTimeDefsJitter InterferenceDefs divround helper
+Require Import Vbase job task schedule task_arrival priority workload_jitter
+               bertogna_fp_jitter_theory interference platform
+               schedulability response_time util_divround util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
 
 Module ResponseTimeIterationFPWithJitter.
 
-  Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority WorkloadWithJitter ResponseTimeAnalysisJitter Interference.
+  Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority WorkloadWithJitter ResponseTimeAnalysisJitter Interference Platform Schedulability ResponseTime.
 
   Section Analysis.
     

BertognaResponseTimeDefsJitter.v → bertogna_fp_jitter_theory.v

-Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
-               PlatformDefs WorkloadDefsJitter BertognaResponseTimeDefs SchedulabilityDefs PriorityDefs
-               ResponseTimeDefs divround helper
+Require Import Vbase task job task_arrival schedule platform workload_jitter
+               response_time schedulability priority interference workload
+               util_divround util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
 
 Module ResponseTimeAnalysisJitter.
 
-  Import Job SporadicTaskset ScheduleOfTaskWithJitter Schedulability ResponseTime Priority SporadicTaskArrival.
-  Export WorkloadWithJitter ResponseTimeAnalysis.
+  Import Job SporadicTaskset ScheduleOfTaskWithJitter Schedulability ResponseTime Priority SporadicTaskArrival Platform Interference Workload.
+  Export WorkloadWithJitter.
   
   Section InterferenceBoundJitter.
 
@@ -570,7 +570,7 @@ Module ResponseTimeAnalysisJitter.
         rewrite big_seq_cond [\sum_(i <- _ | true) _]big_seq_cond.
         apply leq_sum; move => tsk_k /andP [HPk _]; destruct tsk_k as [tsk_k R_k].
         specialize (ALL (tsk_k, R_k) HPk).
-        unfold interference_bound, workload_bound, x in *.
+        unfold interference_bound_jitter, workload_bound, x in *.
         fold (interferes_with_tsk); destruct (interferes_with_tsk tsk_k) eqn:INTERFk;
           [rewrite andbT in ALL; rewrite andbT | by rewrite andbF min0n].
         destruct (tsk_k \in ts) eqn:INk; last by rewrite min0n.

BertognaResponseTimeDefs.v → bertogna_fp_theory.v

-Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
-               PlatformDefs WorkloadDefs SchedulabilityDefs PriorityDefs
-               ResponseTimeDefs InterferenceDefs divround helper
+Require Import Vbase task job task_arrival schedule platform workload
+               schedulability priority response_time interference
+               util_divround util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
 
 Module ResponseTimeAnalysis.

GuanFP.v → guan_fp_comp.v

-Require Import Vbase JobDefs TaskDefs ScheduleDefs TaskArrivalDefs PriorityDefs WorkloadDefsJitter GuanDefs divround helper
+Require Import Vbase job task schedule task_arrival priority workload_jitter
+               guan_fp_theory util_divround util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
 
 Module ResponseTimeIterationFPGuan.

GuanDefs.v → guan_fp_theory.v

-Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
-               PlatformDefs WorkloadDefs BertognaResponseTimeDefs SchedulabilityDefs PriorityDefs InterferenceDefs PlatformDefs
-               ResponseTimeDefs divround helper
+Require Import Vbase task job task_arrival schedule platform workload
+               bertogna_fp_theory schedulability priority interference
+               platform response_time util_divround util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
 
 Module ResponseTimeAnalysisGuan.

InterferenceDefs.v → interference.v

-Require Import Vbase TaskDefs JobDefs ScheduleDefs PriorityDefs WorkloadDefs divround
-              helper ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Import Vbase task job schedule priority workload util_divround
+               util_lemmas ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Interference.
 

JobDefs.v → job.v

-Require Import TaskDefs helper ssrnat ssrbool eqtype.  
+Require Import task util_lemmas ssrnat ssrbool eqtype.  
 
 Module Job.
 

PlatformDefs.v → platform.v

-Require Import Vbase TaskDefs ScheduleDefs JobDefs PriorityDefs
-               InterferenceDefs helper
+Require Import Vbase task schedule job priority interference util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module Platform.

PriorityDefs.v → priority.v

-Require Import Vbase ExtraRelations TaskDefs JobDefs ScheduleDefs (*TaskArrivalDefs*)
+Require Import Vbase task job schedule
                ssreflect ssrbool eqtype ssrnat seq.
 Set Implicit Arguments.
 

ResponseTimeDefs.v → response_time.v

-Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
-               helper ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Import Vbase task job task_arrival schedule util_lemmas
+               ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module ResponseTime.
 

SchedulabilityDefs.v → schedulability.v

-Require Import Vbase TaskDefs ScheduleDefs
+Require Import Vbase task schedule
                ssreflect eqtype ssrbool ssrnat seq.
 
 Module Schedulability.

ScheduleDefs.v → schedule.v

-Require Import Vbase JobDefs TaskDefs helper
+Require Import Vbase job task util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Definition time := nat.

TaskDefs.v → task.v

-Require Import Vbase helper ssrnat ssrbool eqtype fintype seq.
+Require Import Vbase util_lemmas ssrnat ssrbool eqtype fintype seq.
 
 Module SporadicTask.
 

TaskArrivalDefs.v → task_arrival.v

-Require Import Vbase TaskDefs JobDefs ScheduleDefs helper
+Require Import Vbase task job schedule util_lemmas
                ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 Module SporadicTaskArrival.

helper.v → util_lemmas.v

@@ -359,24 +359,6 @@ Proof.
 Qed.
 
 Lemma fun_mon_iter_mon :
-  forall (f: nat -> nat) x0 x1 x2 (LE: x1 <= x2) (MIN: f 0 >= x0)
-         (MON: forall x1 x2, x1 <= x2 -> f x1 <= f x2),
-    iter x1 f x0 <= iter x2 f x0.
-Proof.
-  ins; revert LE; revert x2; rewrite leq_as_delta; intros delta.
-  induction x1; try rewrite add0n.
-  {
-    destruct delta; first by apply leqnn.
-    apply leq_trans with (n := f 0); first by apply MIN.
-    by rewrite iterS MON.
-  }
-  {
-    rewrite iterS -addn1 -addnA [1 + delta]addnC addnA addn1 iterS.
-    by apply MON, IHx1.
-  }
-Qed.
-
-Lemma fun_mon_iter_mon' :
   forall (f: nat -> nat) x0 x1 x2 (LE: x1 <= x2)
          (MIN: f x0 >= x0)
          (MON: forall x1 x2, x1 <= x2 -> f x1 <= f x2),
@@ -806,46 +788,4 @@ Proof.
     last by apply leq_trans with (n := t2).
   rewrite -> big_cat_nat with (p := t2') (n := t2); try (by done); simpl.
   by rewrite addnC -addnA; apply leq_addr.
-Qed.
-
-
-    (*Program Definition fun_ord_to_nat2 {n} {T} (x0: T) (f: 'I_n -> T)
-        (x : nat) : T :=
-  match (x < n) with
-      true => (f _)
-    | false => x0
-  end.
-Next Obligation.
-  eby eapply Ordinal, Logic.eq_sym.
-Defined.
-
-Lemma eq_fun_ord_to_nat2 :
-  forall n {T: Type} x0 (f: 'I_n -> T) (x: 'I_n),
-    (fun_ord_to_nat2 x0 f) x = f x.
-Proof.
-  ins. unfold fun_ord_to_nat2.
-  des_eqrefl.
-    by f_equal; apply ord_inj.
-    by destruct x; ins; rewrite i in EQ.
-Qed.
-
-(* For all x: 'I_n (i.e., x < n), the conversion preserves equality. *)
-Program Definition eq_fun_ord_to_nat :
-  forall n {T: Type} x0 (f: 'I_n -> T) (x: 'I_n),
-    (fun_ord_to_nat x0 f) x = f x :=
-  fun n T x0 f x =>
-    match ltn_ord x in eq _ b return
-          ( 
-            (if b as b' return b = b' -> T then
-               fun (H : b = true) => f (@Ordinal n x ( H))
-             else fun _ => x0) Logic.eq_refl = f x
-          )
-          -> fun_ord_to_nat x0 f x = f x
-    with
-      | Logic.eq_refl => _
-    end (Logic.eq_refl (f x)).
-Next Obligation.
-  destruct x; simpl.
-  f_equal; f_equal.
-  exact: bool_irrelevance.
-Qed.*)
\ No newline at end of file
+Qed.
\ No newline at end of file