Add notion of nonpreemptive schedule

model/schedule/uni/nonpreemptive/platform.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority rt.model.arrival.basic.task_arrival.
+Require Import rt.model.schedule.uni.schedule
+               rt.model.schedule.uni.basic.platform.
+Require Import rt.model.schedule.uni.nonpreemptive.schedule.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+ 
+Module NonpreemptivePlatform.
+
+  Import Job SporadicTaskset UniprocessorSchedule Priority.
+
+  (* In this section, we define properties of the processor platform. *)
+  Section Properties.
+    
+    Context {sporadic_task: eqType}.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> sporadic_task.
+
+    (* Consider any job arrival sequence ...*)
+    Variable arr_seq: arrival_sequence Job.
+    
+    (* ...and any uniprocessor schedule of these jobs. *)
+    Variable sched: schedule Job.
+
+    (* For simplicity, let's define some local names. *)
+    Let job_completed_by := completed_by job_cost sched.
+    Let job_scheduled_at := scheduled_at sched.
+
+    (* First, we define the notion of a preemption point. *)
+    Section PreemptionPoint.
+
+      (* We say that t is a preemption point iff (a) t is equal to 0 
+         or (b) there is no scheduling job at time t or 
+         (c) a job that was scheduled at time (t - 1) and 
+         has completed by t exists. *)
+      Definition is_preemption_point' (t: time) :=
+        t = 0
+        \/ sched (t-1) = None
+        \/ exists j, scheduled_at sched j (t - 1) /\ job_completed_by j t.
+
+      (* Moreover, we provide a shorter definition, more convenient for the proofs. *)
+      Definition is_preemption_point (t: time) :=
+        t = 0 \/ forall j, job_scheduled_at j (t - 1) -> job_completed_by j t.
+
+      (* Let's prove that the definitions above are equal. *)
+      Lemma defitions_of_preemption_point_are_equal:
+        forall t, is_preemption_point t <-> is_preemption_point' t.
+      Proof.
+        unfold is_preemption_point, is_preemption_point'.
+        intros; split; intros.
+        {
+          destruct H as [H | H]; [by left | right].
+          destruct (sched (t-1)) eqn:SCHED; [right; exists s | by left].
+          move: SCHED => /eqP SCHED.
+          by split; last by apply H in SCHED.
+        }
+        {
+          destruct H as [H | [H | H]]; [by left| | ]; right; intros.
+          unfold job_scheduled_at, scheduled_at in H0. rewrite H in H0. inversion H0.
+          inversion H as [j' [H1 H2]]. unfold job_scheduled_at in H0.
+          have EQ: j = j'. by apply (only_one_job_scheduled sched) with (t := t-1).
+            by subst j'.
+        }           
+        Qed.
+
+    End PreemptionPoint.
+    
+    (* Next, we define properties related to execution. *)
+    Section Execution.
+
+      (* We say that a scheduler is work-conserving iff whenever a job j
+         is backlogged, the processor is always busy with another job. *)
+      (* Imported from the preemptive schedule. *)
+      Definition work_conserving := Platform.work_conserving job_cost.
+
+    End Execution.
+
+    (* Next, we define properties related to FP scheduling. *)
+    Section FP.
+
+      (* We say that an FP policy...*)
+      Variable higher_eq_priority: FP_policy sporadic_task.
+      
+      (* ...is respected by the schedule iff a scheduled task has
+         higher (or same) priority than (as) any backlogged task at 
+         every preemption point. *)
+      Definition respects_FP_policy_at_preemption_point :=
+        forall j j_hp t,
+          arrives_in arr_seq j ->
+          backlogged job_arrival job_cost sched j t ->
+          scheduled_at sched j_hp t ->
+          is_preemption_point t ->
+          higher_eq_priority (job_task j_hp) (job_task j).
+      
+    End FP.
+    
+    (* Next, we define properties related to JLFP policies. *)
+    Section JLFP.
+
+      (* We say that a JLFP policy ...*)
+      Variable higher_eq_priority: JLFP_policy Job.
+
+      (* ... is respected by the scheduler iff a scheduled job has
+         higher (or same) priority than (as) any backlogged job at
+         every preemption point. *)      
+      Definition respects_JLFP_policy_at_preemption_point :=
+        forall j j_hp t,
+          arrives_in arr_seq j ->
+          backlogged job_arrival job_cost sched j t ->
+          scheduled_at sched j_hp t ->
+          is_preemption_point t ->
+          higher_eq_priority j_hp j.
+      
+    End JLFP.
+
+  End Properties.
+  
+End NonpreemptivePlatform.
\ No newline at end of file

model/schedule/uni/nonpreemptive/schedule.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job.
+Require Import rt.model.schedule.uni.schedule.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module NonpreemptiveSchedule.
+
+  Export UniprocessorSchedule.
+
+  Section Definitions.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    
+    (* Consider any uniprocessor schedule. *)
+    Variable sched: schedule Job.
+
+    (* For simplicity, let's define some local names. *)
+    Let job_completed_by := completed_by job_cost sched.
+    Let job_remaining_cost j t := remaining_cost job_cost sched j t.
+    
+    (* We define schedule to be nonpreemptive iff every job remains scheduled until completion. *)
+    Definition is_nonpreemptive_schedule := 
+      forall j t t',
+        t <= t' -> 
+        scheduled_at sched j t ->
+        ~~ job_completed_by j t' -> 
+        scheduled_at sched j t'. 
+
+    (* In this section, we prove some basic lemmas about nonpreemptive schedules. *)
+    Section Lemmas.
+
+      (* Assume that we have a nonpreemptive schedule. *)
+      Hypothesis H_nonpreemptive: is_nonpreemptive_schedule.
+
+      Section BasicLemmas.
+
+        (* Consider any job j. *)
+        Variable j: Job.
+        
+        (* Assume that completed jobs do not execute. *)
+        Hypothesis H_completed_jobs_dont_execute:
+          completed_jobs_dont_execute job_cost sched.
+        
+        (* First, we show that if j is scheduled at any two time instants, 
+           then it is also scheduled at any time between them. *)
+        Lemma continuity_of_nonpreemptive_scheduling:
+          forall t t1 t2,
+            t1 <= t <= t2 ->
+            scheduled_at sched j t1 ->
+            scheduled_at sched j t2 ->
+            scheduled_at sched j t.
+        Proof.
+          move => t t1 t2 /andP [GT LE] SCHEDt1 SCHEDt2.          
+          unfold is_nonpreemptive_schedule, job_completed_by in *.
+          apply H_nonpreemptive with (t := t1); [by done| by done| ].
+          apply /negP; intros COMP.
+          apply (scheduled_implies_not_completed job_cost) in SCHEDt2; last by done.
+          apply completion_monotonic with (t' := t2) in COMP; [ |by done| by done].
+            by move: SCHEDt2 => /negP SCHEDt2; apply: SCHEDt2.
+        Qed.
+
+        (* Next, we show that in any nonpreemptive schedule, once a job is scheduled, 
+           it cannot be preempted until completion. *)
+        Lemma in_nonpreemption_schedule_preemption_implies_completeness:
+          forall t t' ,
+            t <= t' ->
+            scheduled_at sched j t ->
+            ~~ scheduled_at sched j t' ->
+            job_completed_by j t'.
+        Proof.
+          intros t t' LE SCHED; apply contraNT.
+            by apply H_nonpreemptive with (t := t). 
+        Qed.
+         
+      End BasicLemmas.
+      
+      (* In this section, we prove properties related to job completion. *)
+      Section CompletionUnderNonpreemptive.
+        
+        (* Assume that completed jobs do not execute. *)
+        Hypothesis H_completed_jobs_dont_execute:
+          completed_jobs_dont_execute job_cost sched.
+
+        (* If job j is scheduled at time t, then it must complete by (t + remaining_cost j t). *)
+        Lemma job_completes_after_remaining_cost:
+          forall j t,
+            scheduled_at sched j t ->
+            job_completed_by j (t + job_remaining_cost j t).
+        Proof.
+          intros j t SCHED.
+          rewrite /job_completed_by /completed_by eqn_leq.
+          apply /andP; split;
+          first by apply cumulative_service_le_job_cost.
+          rewrite /service /service_during.
+          rewrite (@big_cat_nat _ _ _ t) //= ?leq_addr //.
+          apply leq_trans with (n := service sched j t + job_remaining_cost j t);
+            first by rewrite /remaining_cost subnKC //.
+          rewrite leq_add2l.
+          set t2 := t + _.
+          apply leq_trans with (n := \sum_(t <= i < t2) 1);
+            first by simpl_sum_const; rewrite /t2 addKn.
+          apply leq_sum_nat. 
+          move => i /andP [GE LT _].
+          rewrite lt0n eqb0 negbK.
+          apply (H_nonpreemptive j t i); try (by done).
+          unfold t2 in *; clear t2.
+          have NOTCOMP: ~~ job_completed_by j t.
+          {
+            apply contraT. rewrite negbK. intros COMP.
+            apply completed_implies_not_scheduled in COMP; last by done.
+              by rewrite SCHED in COMP.
+          }
+          apply job_doesnt_complete_before_remaining_cost in NOTCOMP; last by done.
+          apply contraT; rewrite negbK; intros COMP.
+          exfalso; move: NOTCOMP => /negP NOTCOMP; apply: NOTCOMP.
+          apply completion_monotonic with (t0 := i); try ( by done).
+          apply subh3; first by rewrite addn1.
+            by apply leq_ltn_trans with (n := i).
+        Qed.
+        
+      End CompletionUnderNonpreemptive.
+      
+      (* In this section, we determine bounds on the length of the execution interval. *)
+      Section ExecutionInterval.
+        
+        (* Assume that jobs do not execute after completion. *)
+        Hypothesis H_completed_jobs_dont_execute:
+          completed_jobs_dont_execute job_cost sched.
+
+        (* Let j be any job scheduled at time t. *)
+        Variable j: Job.
+        Variable t: time.
+        Hypothesis H_j_is_scheduled_at_t: scheduled_at sched j t.
+
+        (* Is this section we show that there is a bound for how early job j can start. *)
+        Section LeftBound.
+          
+          (* We prove that job j is scheduled at time (t - service sched j t)... *)
+          Lemma  j_is_scheduled_at_t_minus_service:
+            scheduled_at sched j (t - service sched j t).
+          Proof.
+            unfold is_nonpreemptive_schedule in *.
+            apply contraT; intros CONTRA; exfalso.
+            rename H_j_is_scheduled_at_t into SCHED.
+            
+            have COSTPOS: job_cost j > 0.
+            {
+              apply (scheduled_implies_not_completed job_cost) in SCHED.
+              unfold job_completed_by, completed_by in SCHED.
+              apply contraT; rewrite -eqn0Ngt.
+              move => /eqP EQ0.
+              rewrite EQ0 in SCHED.
+              move: SCHED => /eqP GT0.
+              exfalso; apply: GT0; apply /eqP.
+              rewrite eqn_leq.
+              apply /andP; split; last by done.
+              rewrite -EQ0.
+              apply H_completed_jobs_dont_execute.
+                by done.
+            } 
+            
+            have H := job_completes_after_remaining_cost
+                        H_completed_jobs_dont_execute
+                        j t SCHED.  
+            
+            unfold job_completed_by, completed_by in H.
+            move: H => /eqP H.
+
+            unfold service, service_during in H.
+
+            rewrite
+              (@big_cat_nat _ _ _ (t - service sched j t)) //= in H;
+              last by rewrite leq_subLR addnC -addnA leq_addr.
+            have R: forall a b c, a + b = c -> b < c -> a > 0.
+            {
+                by intros a b c EQ LT; induction a;
+                first by rewrite add0n in EQ; subst b;
+                rewrite ltnn in LT.        
+            }
+            
+            apply R in H; last first.
+            {
+              have CUMLED := cumulative_service_le_delta sched j 0 t.
+              have CUMLEJC := cumulative_service_le_job_cost _ _ H_completed_jobs_dont_execute j 0 t.
+              rewrite (@big_cat_nat _ _ _ ((t - service sched j t).+1)) //=.
+              {
+                rewrite big_nat_recl; last by done.
+                rewrite big_geq; last by done.
+                rewrite -eqb0 in CONTRA; move: CONTRA => /eqP CONTRA.
+                rewrite /service_at CONTRA add0n add0n.
+                apply leq_ltn_trans with
+                    (t + job_remaining_cost j t - ((t - service sched j t).+1)).
+                 set (t - service sched j t).+1 as T.
+                 apply leq_trans with (\sum_(T <= i < t + job_remaining_cost j t) 1).
+                 rewrite leq_sum //; intros; by destruct (scheduled_at sched j i).
+                 simpl_sum_const. by done.
+                 unfold job_remaining_cost, remaining_cost.
+                 rewrite -addn1 -addn1  subh1; first by
+                     by rewrite leq_subLR addnBA;
+                 first by  rewrite -addnA [1+job_cost j]addnC addnA -subh1.
+                 { 
+                  rewrite subh1; last by done.
+                  rewrite leq_subLR addnA.
+                  rewrite addnBA; last by done.
+                  rewrite [_+t]addnC [_+job_cost j]addnC addnA.
+                  rewrite -addnBA; last by done.
+                    by rewrite subnn addn0 addnC leq_add2r.
+                }
+              }
+              {
+                unfold remaining_cost.
+                rewrite addnBA; last by done.
+                rewrite -addn1 subh1; last by done.
+                rewrite leq_subLR -addnBA; last by done.
+                rewrite addnA [_+t]addnC -addnA leq_add2l addnBA; last by done.
+                  by rewrite addnC -addnBA; first by rewrite subnn addn0.
+              }
+            }
+            {
+              rewrite lt0n in H; move: H => /neqP H; apply: H.
+              rewrite big_nat_cond big1 //; move => i /andP [/andP [_ LT] _].
+              apply /eqP; rewrite eqb0; apply /negP; intros CONT.
+
+              have Y := continuity_of_nonpreemptive_scheduling j _ (t - service sched j t) i t.
+              feed_n 4 Y; try(done).
+                by apply/andP; split; [rewrite ltnW | rewrite leq_subr].
+                  by move: CONTRA => /negP CONTRA; apply CONTRA.
+            }
+          Qed. 
+          
+          (* ... and it is not scheduled at time (t - service sched j t - 1). *)
+          Lemma j_is_not_scheduled_at_t_minus_service_minus_one:
+            t - service sched j t > 0 ->
+            ~~ scheduled_at sched j (t - service sched j t - 1).
+          Proof.
+            rename H_j_is_scheduled_at_t into SCHED.
+            intros GT; apply/negP; intros CONTRA.
+
+            have L1 := job_doesnt_complete_before_remaining_cost
+                         job_cost sched H_completed_jobs_dont_execute
+                         j t.
+            feed L1; first by rewrite scheduled_implies_not_completed.
+
+            have L2 := job_completes_after_remaining_cost
+                         H_completed_jobs_dont_execute
+                         j (t-service sched j t - 1).
+            feed L2; first by done. 
+
+            have EQ:
+              t + job_remaining_cost j t - 1 =
+              t - service sched j t - 1 + job_remaining_cost j (t - service sched j t - 1).
+            {
+              have T1: service sched j (t - service sched j t - 1) = 0.
+              {
+
+                rewrite [service _ _ _]/service /service_during.
+                rewrite big_nat_cond big1 //; move => t' /andP [/andP [_ LT] _]. 
+                apply /eqP; rewrite eqb0; apply /negP; intros CONTR.
+
+                have COMPL: completed_by job_cost sched j (t + job_remaining_cost j t - 1).
+                {
+                  apply completion_monotonic with (t0 := t' + job_remaining_cost j t');
+                  [by done | | by apply job_completes_after_remaining_cost].
+              
+                  unfold remaining_cost.
+
+                  have LLF: t' < t - service sched j t.
+                  {
+                      by apply ltn_trans with (t - service sched j t - 1);
+                    last by rewrite -addn1 subh1 // -addnBA // subnn addn0.
+                  } clear LT.
+                  
+                  rewrite !addnBA;
+                    try(rewrite H_completed_jobs_dont_execute //).
+                  rewrite [t' + _]addnC [t + _]addnC.
+                  rewrite -addnBA; last by rewrite cumulative_service_le_delta.
+                  rewrite -addnBA; last by rewrite cumulative_service_le_delta.
+                  rewrite -addnBA ?leq_add2l; last by done.
+                  by apply leq_trans with (t' + 1 - 1);
+                    rewrite addn1 subn1 -pred_Sn;
+                  [rewrite leq_subr | rewrite subh3 // addn1].
+                }
+            
+                have L3 := job_doesnt_complete_before_remaining_cost job_cost sched
+                             H_completed_jobs_dont_execute j t;
+                    feed L3; first by rewrite scheduled_implies_not_completed.
+                unfold job_completed_by in *.
+                  by move: L3 => /negP L3; apply L3.
+              }
+              rewrite /job_remaining_cost /remaining_cost T1 subn0 addnBA; last by done.
+              rewrite -subh1.
+                by rewrite -[(t-service sched j t) + _ - _]subh1.
+                  by rewrite cumulative_service_le_delta.
+            }
+            move: L1 => /neqP L1; apply: L1.
+            rewrite -EQ in L2.
+              by unfold job_completed_by, completed_by in L2; move: L2 => /eqP L2.
+          Qed.
+
+          (* Using the previous lemma, we show that job j cannot be scheduled 
+             before (t - service sched j t). *)
+          Lemma j_is_not_scheduled_earlier_t_minus_service:
+            forall t',
+              t' < t - service sched j t ->
+              ~~ scheduled_at sched j t'.
+          Proof.
+            intros t' GT.
+            have NOTSCHED := j_is_not_scheduled_at_t_minus_service_minus_one;
+                feed NOTSCHED; first by apply leq_ltn_trans with t'.
+            apply/negP;  intros CONTRA.
+            move: NOTSCHED => /negP NOTSCHED; apply: NOTSCHED.
+            apply continuity_of_nonpreemptive_scheduling with (t1 := t') (t2 := t);
+              [ by done | | by done | by done ].
+            apply/andP; split; last by apply leq_trans with (t - service sched j t); rewrite leq_subr.
+            rewrite [t']pred_Sn -subn1 leq_sub2r //.
+          Qed.
+          
+        End LeftBound.
+
+        (* Is this section we prove that job j cannot be scheduled after (t + remaining_cost j t - 1). *)
+        Section RightBound.
+
+          (* We show that if job j is scheduled at time t, 
+             then it is also scheduled at time (t + remaining_cost j t - 1)... *)
+          Lemma j_is_scheduled_at_t_plus_remaining_cost_minus_one:
+            scheduled_at sched j (t + job_remaining_cost j t - 1).
+          Proof.
+            move: (H_j_is_scheduled_at_t) => COMP.
+            apply (scheduled_implies_not_completed job_cost) in COMP; last by done.
+            apply  job_doesnt_complete_before_remaining_cost in COMP; last by done.
+            move: COMP; apply contraR; intros CONTR.
+            apply in_nonpreemption_schedule_preemption_implies_completeness
+            with (t:=t); [|by done| by done].
+            rewrite subh3 // ?leq_add2l;
+              first by rewrite scheduled_implies_positive_remaining_cost //.
+            rewrite addn_gt0; apply/orP; right;
+            rewrite scheduled_implies_positive_remaining_cost //.
+          Qed.
+
+          (* ... and it is not scheduled after (t + remaining cost j t - 1). *)       
+          Lemma j_is_not_scheduled_after_t_plus_remaining_cost_minus_one:
+            forall t',
+              t + job_remaining_cost j t <= t' ->
+              ~~ scheduled_at sched j t'.
+          Proof.
+            intros t' GE.
+            unfold job_completed_by in *.
+            rename H_j_is_scheduled_at_t into SCHED.
+            apply job_completes_after_remaining_cost in SCHED; last by done.
+            by apply (completion_monotonic job_cost) with (t' := t') in SCHED; first
+              by apply (completed_implies_not_scheduled job_cost).
+          Qed.
+          
+        End RightBound.
+        
+        (* To conclude, we identify the interval where job j is scheduled. *) 
+        Lemma nonpreemptive_executing_interval:
+          forall t',
+            t - service sched j t <= t' < t + job_remaining_cost j t ->
+            scheduled_at sched j t'.
+        Proof.
+          move => t' /andP [GE LE].
+          move: (H_j_is_scheduled_at_t) => SCHED1; move: (H_j_is_scheduled_at_t) => SCHED2.
+          rewrite -addn1 in LE; apply subh3 with (m := t') (p := 1) in LE;
+          last by rewrite addn_gt0; apply/orP; right;
+          rewrite scheduled_implies_positive_remaining_cost //.
+          apply continuity_of_nonpreemptive_scheduling with
+          (t1 := t - service sched j t)
+            (t2 := t + job_remaining_cost j t - 1); first by done.
+          - by apply/andP;split.
+          - by apply j_is_scheduled_at_t_minus_service.
+          - by apply j_is_scheduled_at_t_plus_remaining_cost_minus_one.
+        Qed.
+        
+      End ExecutionInterval.
+      
+    End Lemmas.
+
+  End Definitions.
+
+End NonpreemptiveSchedule.
\ No newline at end of file

model/schedule/uni/schedule.v

@@ -8,7 +8,7 @@ Module UniprocessorSchedule.
   Export Time ArrivalSequence.
 
   Section Schedule.
-
+ 
     (* We begin by defining a uniprocessor schedule. *)
     Section ScheduleDef.
 
@@ -60,9 +60,14 @@ Module UniprocessorSchedule.
         (* Job j is pending at time t iff it has arrived but has not yet completed. *)
         Definition pending (t: time) := has_arrived job_arrival j t && ~~ completed_by t.
 
+        (* Job j is pending earlier and at time t iff it has arrived before time t 
+           and has not been completed yet. *)
+        Definition pending_earlier_and_at (t: time) :=
+          arrived_before job_arrival j t && ~~ completed_by t.
+
         (* Job j is backlogged at time t iff it is pending and not scheduled. *)
         Definition backlogged (t: time) := pending t && ~~ scheduled_at t.
-
+        
       End JobProperties.
 
       (* In this section, we define some properties of the processor. *)
@@ -80,6 +85,25 @@ Module UniprocessorSchedule.
         Definition total_service (t2: time) := total_service_during 0 t2.
 
       End ProcessorProperties.
+
+      Section PropertyOfSequentiality.
+
+        Context {Task: eqType}.    
+        Variable job_task: Job -> Task.
+
+        (* We say that two jobs j1 and j2 are from the same task, if job_task j1 is equal to job_task j2. *)
+        Let same_task j1 j2 := job_task j1 == job_task j2.
+
+        (* We say that the jobs are sequential if they are executed
+           in the order they arrived. *) 
+        Definition sequential_jobs :=
+          forall j1 j2 t,
+            same_task j1 j2 ->
+            job_arrival j1 < job_arrival j2 ->
+            scheduled_at j2 t ->
+            completed_by j1 t.
+        
+      End PropertyOfSequentiality.
       
     End ScheduleProperties.
 
@@ -117,6 +141,11 @@ Module UniprocessorSchedule.
       (* Consider any uniprocessor schedule. *)
       Variable sched: schedule Job.
 
+      (* Let's define the remaining cost of job j as the amount of service 
+         that has to be received for its completion. *)
+      Definition remaining_cost j t :=
+        job_cost j - service sched j t.      
+
       (* Let's begin with lemmas about service. *)
       Section Service.
 
@@ -142,6 +171,24 @@ Module UniprocessorSchedule.
           by apply leq_sum; intros t0 _; apply leq_b1.
         Qed.
 
+        (* Assume that completed jobs do not execute. *)
+        Hypothesis H_completed_jobs:
+          completed_jobs_dont_execute job_cost sched.
+        
+        (* Note that if a job scheduled at some time t then remaining 
+             cost at this point is positive *)
+        Lemma scheduled_implies_positive_remaining_cost:
+          forall t,
+            scheduled_at sched j t ->
+            remaining_cost j t > 0.
+        Proof. 
+          intros.
+          rewrite subn_gt0 /service /service_during.
+          apply leq_trans with (\sum_(0 <= t0 < t.+1) service_at sched j t0);
+            last by rewrite H_completed_jobs.
+          by rewrite big_nat_recr //= -addn1 leq_add2l lt0b.
+        Qed.
+          
       End Service.
 
       (* Next, we prove properties related to job completion. *)
@@ -160,7 +207,7 @@ Module UniprocessorSchedule.
             t <= t' ->
             completed_by job_cost sched j t ->
             completed_by job_cost sched j t'.
-        Proof.
+        Proof. 
           unfold completed_by; move => t t' LE /eqP COMPt.
           rewrite eqn_leq; apply/andP; split; first by apply H_completed_jobs.
           rewrite- COMPt; by apply extend_sum.
@@ -182,6 +229,29 @@ Module UniprocessorSchedule.
           apply leq_add; first by move: COMPLETED => /eqP <-.
           by rewrite /service_at SCHED.
         Qed.
+
+        (* ... and that a scheduled job cannot be completed. *)
+        Lemma scheduled_implies_not_completed:
+          forall t,
+            scheduled_at sched j t ->
+            ~~ completed_by job_cost sched j t.
+        Proof.
+          rename H_completed_jobs into COMP.
+          unfold completed_jobs_dont_execute in COMP.
+          move => t SCHED.
+          rewrite /completed_by neq_ltn.
+          apply /orP; left.
+          apply leq_trans with (service sched j t.+1); last by done.
+          rewrite /service /service_during.            
+          rewrite [in X in _ < X] (@big_cat_nat _ _ _ t) //=.
+          rewrite -[\sum_(0 <= t0 < t) service_at sched j t0]addn0;
+          rewrite -addnA ltn_add2l addnC addn0 big_nat1.
+          rewrite lt0n; apply/neqP; intros CONT;
+          move: CONT => /eqP CONT; rewrite eqb0 in CONT;
+          move: CONT => /neqP CONT; apply CONT;
+          unfold scheduled_at in SCHED; move: SCHED => /eqP SCHED;
+          by rewrite SCHED.
+        Qed.
         
         (* Next, we show that the service received by job j in any interval
            is no larger than its cost. *)
@@ -198,7 +268,113 @@ Module UniprocessorSchedule.
             rewrite -> big_cat_nat with (m := 0) (n := t);
               [by apply leq_addl | by ins | by rewrite leqNgt negbT //].
         Qed.
-      
+
+        (* If a job isn't complete at time t, 
+           it can't be completed at time (t + remaining_cost j t - 1). *)
+        Lemma job_doesnt_complete_before_remaining_cost:
+          forall t,
+            ~~ completed_by job_cost sched j t -> 
+            ~~ completed_by job_cost sched j (t + remaining_cost j t - 1).
+        Proof.
+          intros t GT0.
+          unfold remaining_cost, completed_by in *.
+          have COSTGT0: job_cost j > 0.
+          {
+            apply contraT; rewrite -eqn0Ngt.
+            move => /eqP EQ0.
+            rewrite EQ0 in GT0.
+            move: GT0 => /eqP GT0.
+            exfalso; apply: GT0; apply /eqP.
+            rewrite eqn_leq.
+            apply /andP; split; last by done.
+            by rewrite -EQ0.
+          }
+          rewrite neq_ltn; apply /orP; left.
+          rewrite /service /service_during.
+          set delta := (X in (t + X - 1)).
+          have NONZERO: delta > 0.
+          {
+            rewrite neq_ltn in GT0.
+            move: GT0 => /orP [LTcost | GTcost]; first by rewrite ltn_subRL addn0.
+            exfalso.
+            rewrite ltnNge in GTcost; move: GTcost => /negP GTcost.
+              by apply GTcost.
+          }
+          rewrite (@big_cat_nat _ _ _ t) //= ?leq_addr //;
+            last by rewrite -addnBA; [rewrite leq_addr | done].
+          apply leq_ltn_trans with (n := service sched j t + \sum_(t <= i < t + delta - 1) 1);
+            first by rewrite leq_add2l; apply leq_sum; intros; apply leq_b1.
+          simpl_sum_const.
+          rewrite -addnBA // addKn.
+          rewrite addnBA // /delta.
+          rewrite subnKC; last by done.
+          rewrite subn1 -(ltn_add2r 1) addn1. 
+            by rewrite prednK // addn1 ltnSn.
+        Qed.
+        
+        (* In this section, we prove that the job with a positive 
+           cost must be scheduled to be completed. *)
+        Section JobMustBeScheduled.
+          
+          (* We assume that job j has positive cost, from which we can
+             infer that there always is a time in which j is pending. *)
+          Hypothesis H_positive_cost: job_cost j > 0.
+
+          (* Assume that jobs must arrive to execute. *)
+          Hypothesis H_jobs_must_arrive:
+            jobs_must_arrive_to_execute job_arrival sched.
+        
+          (* Then, we prove that the job with a positive cost 
+             must be scheduled to be completed. *)
+          Lemma completed_implies_scheduled_before:
+            forall t,
+              completed_by job_cost sched j t ->
+              exists t',
+                job_arrival j <= t' < t
+                /\ scheduled_at sched j t'.
+          Proof.
+            intros t COMPL.
+            induction t.
+            {
+              exfalso.
+              unfold completed_by, service, service_during in COMPL.
+              move: COMPL; rewrite big_geq //; move => /eqP H0.
+                by destruct (job_cost j).
+            }
+
+            destruct (completed_by job_cost sched j t) eqn:COMPLatt.
+            {
+              feed IHt; first by done.
+              move: IHt => [t' [JA SCHED]].
+              exists t'. split; first apply/andP; first split.
+              - by apply H_jobs_must_arrive in SCHED.
+              - move: JA => /andP [_ LT]. by apply leq_trans with t.
+              - by done.
+            }
+            {
+              clear IHt.
+              apply negbT in COMPLatt. unfold completed_by in *.
+              rewrite neq_ltn in COMPLatt; move: COMPLatt => /orP [LT | F]. 
+              {
+                unfold service, service_during in COMPL.
+                rewrite big_nat_recr //= in COMPL.
+                move: COMPL => /eqP COMPL. rewrite -COMPL -addn1 leq_add2l in LT.
+                rewrite lt0b in LT.
+                
+                exists t; split.
+                - by apply/andP; by split; first by apply H_jobs_must_arrive in LT.
+                - by done.
+              }
+              {
+                exfalso.
+                rewrite ltnNge in F. move: F => /negP F. apply F.
+                apply H_completed_jobs.
+              }
+            }
+          Qed.
+
+        End JobMustBeScheduled.
+        
       End Completion.
 
       (* In this section we prove properties related to job arrivals. *)
@@ -476,5 +652,5 @@ Module UniprocessorSchedule.
     End Lemmas.
   
   End Schedule.
-
+ 
 End UniprocessorSchedule.
\ No newline at end of file