Add lemmas about step functions

Makefile

@@ -14,7 +14,7 @@
 
 #
 # This Makefile was generated by the command line :
-# coq_makefile -f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/minmax.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/uni/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/arrival_sequence.v ./model/task.v ./model/task_arrival.v ./model/partitioned/schedulability.v ./model/partitioned/schedule.v ./model/priority.v ./model/global/workload.v ./model/global/schedulability.v ./model/global/jitter/interference_edf.v ./model/global/jitter/interference.v ./model/global/jitter/job.v ./model/global/jitter/constrained_deadlines.v ./model/global/jitter/schedule.v ./model/global/jitter/platform.v ./model/global/response_time.v ./model/global/basic/interference_edf.v ./model/global/basic/interference.v ./model/global/basic/constrained_deadlines.v ./model/global/basic/schedule.v ./model/global/basic/platform.v ./model/job.v ./model/time.v ./model/arrival_bounds.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/affinity.v ./model/apa/constrained_deadlines.v ./model/apa/platform.v ./model/uni/workload.v ./model/uni/transformation/construction.v ./model/uni/schedulability.v ./model/uni/schedule_of_task.v ./model/uni/response_time.v ./model/uni/schedule.v ./model/uni/basic/arrival_bounds.v ./model/uni/basic/busy_interval.v ./model/uni/basic/platform.v ./model/uni/service.v ./implementation/arrival_sequence.v ./implementation/task.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/job.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v ./implementation/uni/basic/fp_rta_example.v ./implementation/uni/basic/schedule.v -o Makefile 
+# coq_makefile -f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/step_function.v ./util/minmax.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/uni/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/arrival_sequence.v ./model/task.v ./model/task_arrival.v ./model/partitioned/schedulability.v ./model/partitioned/schedule.v ./model/priority.v ./model/global/workload.v ./model/global/schedulability.v ./model/global/jitter/interference_edf.v ./model/global/jitter/interference.v ./model/global/jitter/job.v ./model/global/jitter/constrained_deadlines.v ./model/global/jitter/schedule.v ./model/global/jitter/platform.v ./model/global/response_time.v ./model/global/basic/interference_edf.v ./model/global/basic/interference.v ./model/global/basic/constrained_deadlines.v ./model/global/basic/schedule.v ./model/global/basic/platform.v ./model/job.v ./model/time.v ./model/arrival_bounds.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/affinity.v ./model/apa/constrained_deadlines.v ./model/apa/platform.v ./model/uni/workload.v ./model/uni/transformation/construction.v ./model/uni/schedulability.v ./model/uni/schedule_of_task.v ./model/uni/response_time.v ./model/uni/schedule.v ./model/uni/basic/arrival_bounds.v ./model/uni/basic/busy_interval.v ./model/uni/basic/platform.v ./model/uni/service.v ./implementation/arrival_sequence.v ./implementation/task.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/job.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v ./implementation/uni/basic/fp_rta_example.v ./implementation/uni/basic/schedule.v -o Makefile 
 #
 
 .DEFAULT_GOAL := all
@@ -97,6 +97,7 @@ endif
 VFILES:=util/ssromega.v\
   util/seqset.v\
   util/sorting.v\
+  util/step_function.v\
   util/minmax.v\
   util/powerset.v\
   util/all.v\

util/all.v

@@ -15,3 +15,4 @@ Require Export rt.util.ssromega.
 Require Export rt.util.sum.
 Require Export rt.util.minmax.
 Require Export rt.util.seqset.
+Require Export rt.util.step_function.

util/step_function.v

+Require Import rt.util.tactics rt.util.notation rt.util.induction.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
+
+Section StepFunction.
+
+  Section Defs.
+
+    (* We say that a function f... *)
+    Variable f: nat -> nat.
+
+    (* ...is a step function iff the following holds. *)
+    Definition is_step_function :=
+      forall t, f (t + 1) <= f t + 1.
+
+  End Defs.
+
+  Section Lemmas.
+
+    (* Let f be any step function over natural numbers. *)
+    Variable f: nat -> nat.
+    Hypothesis H_step_function: is_step_function f.
+
+    (* In this section, we prove a result similar to the intermediate
+       value theorem for continuous functions. *)
+    Section ExistsIntermediateValue.
+
+      (* Consider any interval [x1, x2]. *)
+      Variable x1 x2: nat.
+      Hypothesis H_is_interval: x1 <= x2.
+
+      (* Let t be any value such that f x1 < y < f x2. *)
+      Variable y: nat.
+      Hypothesis H_between: f x1 <= y < f x2.
+
+      (* Then, we prove that there exists an intermediate point x_mid such that
+         f x_mid = y. *)
+      Lemma exists_intermediate_point:
+        exists x_mid, x1 <= x_mid < x2 /\ f x_mid = y.
+      Proof.
+        unfold is_step_function in *.
+        rename H_is_interval into INT,
+               H_step_function into STEP, H_between into BETWEEN.
+        move: x2 INT BETWEEN; clear x2.
+        suff DELTA:
+          forall delta,
+            f x1 <= y < f (x1 + delta) ->
+            exists x_mid, x1 <= x_mid < x1 + delta /\ f x_mid = y.                  {
+          move => x2 LE /andP [GEy LTy].
+          exploit (DELTA (x2 - x1));
+            first by apply/andP; split; last by rewrite addnBA // addKn.
+          by rewrite addnBA // addKn.
+        }
+        induction delta.
+        {
+          rewrite addn0; move => /andP [GE0 LT0].
+          by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
+        }
+        {
+          move => /andP [GT LT].
+          specialize (STEP (x1 + delta)); rewrite leq_eqVlt in STEP.
+          have LE: y <= f (x1 + delta).
+          {
+            move: STEP => /orP [/eqP EQ | STEP];
+              first by rewrite !addn1 in EQ; rewrite addnS EQ ltnS in LT.
+            rewrite [X in _ < X]addn1 ltnS in STEP.
+            apply: (leq_trans _ STEP).
+            by rewrite addn1 -addnS ltnW.
+          } clear STEP LT.
+          rewrite leq_eqVlt in LE.
+          move: LE => /orP [/eqP EQy | LT].
+          {
+            exists (x1 + delta); split; last by rewrite EQy.
+            by apply/andP; split; [by apply leq_addr | by rewrite addnS].
+          }
+          {
+            feed (IHdelta); first by apply/andP; split.
+            move: IHdelta => [x_mid [/andP [GE0 LT0] EQ0]].
+            exists x_mid; split; last by done.
+            apply/andP; split; first by done.
+            by apply: (leq_trans LT0); rewrite addnS.
+          }  
+        }
+      Qed.
+
+    End ExistsIntermediateValue.
+
+  End Lemmas.
+
+End StepFunction.
\ No newline at end of file