Add lemmas about incremental service

classic/util/step_function.v

@@ -2,52 +2,3 @@ From rt.util Require Export step_function.
 
 Require Import rt.classic.util.tactics rt.classic.util.notation rt.classic.util.induction.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
-
-Section StepFunction.
-
-  (* In this section, we prove an analogue of the intermediate
-     value theorem, but for predicates of natural numbers. *) 
-  Section ExistsIntermediateValuePredicates. 
-
-    (* Let P be any predicate on natural numbers. *)
-    Variable P: nat -> bool.
-
-    (* Consider a time interval [t1,t2] such that ... *)
-    Variables t1 t2: nat.
-    Hypothesis H_t1_le_t2: t1 <= t2.
-
-    (* ... P doesn't hold for t1 ... *)
-    Hypothesis H_not_P_at_t1: ~~ P t1.
-
-    (* ... but holds for t2. *)
-    Hypothesis H_P_at_t2: P t2.
-    
-    (* Then we prove that within time interval [t1,t2] there exists time 
-       instant t such that t is the first time instant when P holds. *)
-    Lemma exists_first_intermediate_point:
-      exists t, (t1 < t <= t2) /\ (forall x, t1 <= x < t -> ~~ P x) /\ P t.
-    Proof.
-      have EX: exists x, P x && (t1 < x <= t2).
-      { exists t2.
-        apply/andP; split; first by done.
-        apply/andP; split; last by done.
-        move: H_t1_le_t2; rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
-          by exfalso; subst t2; move: H_not_P_at_t1 => /negP NPt1. 
-      }
-      have MIN := ex_minnP EX.
-      move: MIN => [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.
-      exists x; repeat split; [ apply/andP; split | | ]; try done.
-      move => y /andP [NEQ1 NEQ2]; apply/negPn; intros Py.
-      feed (MIN y). 
-      { apply/andP; split; first by done.
-        apply/andP; split.
-        - move: NEQ1. rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
-            by exfalso; subst y; move: H_not_P_at_t1 => /negP NPt1. 
-        - by apply ltnW, leq_trans with x.
-      }
-        by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
-    Qed.
-    
-  End ExistsIntermediateValuePredicates.  
-
-End StepFunction.
\ No newline at end of file

restructuring/analysis/basic_facts/service.v

 From mathcomp Require Import ssrnat ssrbool fintype.
 
 From rt.restructuring.behavior Require Export all.
+From rt.restructuring Require Export analysis.basic_facts.ideal_schedule.
 From rt.restructuring.model.processor Require Export platform_properties.
 From rt.util Require Import tactics step_function sum.
 
@@ -576,3 +577,112 @@ Section RelationToScheduled.
   End TimesWithSameService.
 
 End RelationToScheduled.
+
+From rt.restructuring.model Require Import processor.ideal.
+
+(** * Incremental Service in Ideal Schedule *)
+(** In the following section we prove a few facts about service in ideal schedeule. *)
+(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
+Section IncrementalService.
+
+  (** Consider any job type, ... *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** ... any arrival sequence, ... *)
+  Variable arr_seq : arrival_sequence Job.
+
+  (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
+  Variable sched : schedule (ideal.processor_state Job).  
+
+  (** As a base case, we prove that if a job j receives service in
+      some time interval [t1,t2), then there exists a time instant t
+      ∈ [t1,t2) such that j is scheduled at time t and t is the first
+      instant where j receives service. *)
+  Lemma positive_service_during:
+    forall j t1 t2,
+      0 < service_during sched j t1 t2 -> 
+      exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0.
+  Proof.
+    intros j t1 t2 SERV.
+    have LE: t1 <= t2.
+    { rewrite leqNgt; apply/negP; intros CONTR.
+        by apply ltnW in CONTR;  move: SERV; rewrite /service_during big_geq.
+    }
+    destruct (scheduled_at sched j t1) eqn:SCHED.
+    { exists t1; repeat split; try done.
+      - apply/andP; split; first by done.
+        rewrite ltnNge; apply/negP; intros CONTR.
+          by move: SERV; rewrite/service_during big_geq.
+      - by rewrite /service_during big_geq.                
+    }  
+    { apply negbT in SCHED.
+      move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [t [IN SCHEDt]].
+      rewrite lt0b in SCHEDt.
+      rewrite mem_iota subnKC in IN; last by done.
+      move: IN => /andP [IN1 IN2].
+      move: (exists_first_intermediate_point
+               ((fun t => scheduled_at sched j t)) t1 t IN1 SCHED) => A.
+      feed A; first by rewrite scheduled_at_def/=.
+      move: A => [x [/andP [T1 T4] [T2 T3]]].
+      exists x; repeat split; try done.
+      - apply/andP; split; first by apply ltnW.
+          by apply leq_ltn_trans with t. 
+      - apply/eqP; rewrite big_nat_cond big1 //.
+        move => y /andP [T5 _].
+          by apply/eqP; rewrite eqb0; specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.
+    }
+  Qed.
+
+  (** Next, we prove that if in some time interval [t1,t2) a job j
+     receives k units of service, then there exists a time instant t ∈
+     [t1,t2) such that j is scheduled at time t and service of job j
+     within interval [t1,t) is equal to k. *)
+  Lemma incremental_service_during:
+    forall j t1 t2 k,
+      service_during sched j t1 t2 > k ->
+      exists t, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k.
+  Proof.
+    intros j t1 t2 k SERV.
+    have LE: t1 <= t2.
+    { rewrite leqNgt; apply/negP; intros CONTR.
+        by apply ltnW in CONTR;  move: SERV; rewrite /service_during big_geq.
+    }
+    induction k; first by apply positive_service_during in SERV.
+    feed IHk; first by apply ltn_trans with k.+1.
+    move: IHk => [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].
+    have SERVk1: service_during sched j t1 t.+1 = k.+1.
+    { rewrite -(service_during_cat _ _ _ t); last by apply/andP; split.
+      rewrite  SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l.
+        by rewrite /service_during big_nat1 /service_at eqb1 -scheduled_at_def/=.  
+    } 
+    move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first.
+    { by apply/andP; split; first apply leq_trans with t. }
+    rewrite SERVk1 -addn1 leq_add2l; move => SERV.
+    destruct (scheduled_at sched j t.+1) eqn:SCHED.
+    - exists t.+1; repeat split; try done. apply/andP; split.
+      + apply leq_trans with t; by done. 
+      + rewrite ltnNge; apply/negP; intros CONTR.
+          by move: SERV; rewrite /service_during big_geq.
+    -  apply negbT in SCHED.
+       move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [x [INx SCHEDx]].
+       rewrite lt0b in SCHEDx.
+       rewrite mem_iota subnKC in INx; last by done.
+       move: INx => /andP [INx1 INx2].
+       move: (exists_first_intermediate_point _ _ _ INx1 SCHED) => A.
+       feed A; first by rewrite scheduled_at_def/=.
+       move: A => [y [/andP [T1 T4] [T2 T3]]].
+       exists y; repeat split; try done.
+       + apply/andP; split.
+         apply leq_trans with t; first by done. 
+         apply ltnW, ltn_trans with t.+1; by done.
+           by apply leq_ltn_trans with x. 
+       + rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1].
+         unfold service_during in SERVk1; rewrite SERVk1; apply/eqP.
+         rewrite -{2}[k.+1]addn0 eqn_add2l.
+         rewrite big_nat_cond big1 //; move => z /andP [H5 _].
+           by apply/eqP; rewrite eqb0; specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.
+  Qed.
+
+End IncrementalService.
\ No newline at end of file

util/step_function.v

@@ -79,4 +79,49 @@ Section StepFunction.
 
   End Lemmas.
 
+  (* In this section, we prove an analogue of the intermediate
+     value theorem, but for predicates of natural numbers. *) 
+  Section ExistsIntermediateValuePredicates. 
+
+    (* Let P be any predicate on natural numbers. *)
+    Variable P : nat -> bool.
+
+    (* Consider a time interval [t1,t2] such that ... *)
+    Variables t1 t2 : nat.
+    Hypothesis H_t1_le_t2 : t1 <= t2.
+
+    (* ... P doesn't hold for t1 ... *)
+    Hypothesis H_not_P_at_t1 : ~~ P t1.
+
+    (* ... but holds for t2. *)
+    Hypothesis H_P_at_t2 : P t2.
+    
+    (* Then we prove that within time interval [t1,t2] there exists time 
+       instant t such that t is the first time instant when P holds. *)
+    Lemma exists_first_intermediate_point:
+      exists t, (t1 < t <= t2) /\ (forall x, t1 <= x < t -> ~~ P x) /\ P t.
+    Proof.
+      have EX: exists x, P x && (t1 < x <= t2).
+      { exists t2.
+        apply/andP; split; first by done.
+        apply/andP; split; last by done.
+        move: H_t1_le_t2; rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
+          by exfalso; subst t2; move: H_not_P_at_t1 => /negP NPt1. 
+      }
+      have MIN := ex_minnP EX.
+      move: MIN => [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.
+      exists x; repeat split; [ apply/andP; split | | ]; try done.
+      move => y /andP [NEQ1 NEQ2]; apply/negPn; intros Py.
+      feed (MIN y). 
+      { apply/andP; split; first by done.
+        apply/andP; split.
+        - move: NEQ1. rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
+            by exfalso; subst y; move: H_not_P_at_t1 => /negP NPt1. 
+        - by apply ltnW, leq_trans with x.
+      }
+        by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
+    Qed.
+    
+  End ExistsIntermediateValuePredicates.  
+
 End StepFunction.
\ No newline at end of file