Library rt.restructuring.analysis.basic_facts.service


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.10.1 (October 2019)

----------------------------------------------------------------------------- *)

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.

In this file, we establish basic facts about the service received by jobs.

Section Composition.
To begin with, we provide some simple but handy rewriting rules for [service] and [service_during].
Consider any job type and any processor state.
  Context {Job: JobType}.
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

For any given schedule...
  Variable sched: schedule PState.

...and any given job...
  Variable j: Job.

...we establish a number of useful rewriting rules that decompose the service received during an interval into smaller intervals.
As a trivial base case, no job receives any service during an empty interval.
  Lemma service_during_geq:
    ∀ t1 t2,
      t1 ≥ t2 → service_during sched j t1 t2 = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 39)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t1 t2 : nat, t2 <= t1 -> service_during sched j t1 t2 = 0

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ t1 t2 t1t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 42)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : nat
  t1t2 : t2 <= t1
  ============================
  service_during sched j t1 t2 = 0

----------------------------------------------------------------------------- *)

    rewrite /service_during big_geq //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Equally trivially, no job has received service prior to time zero.
  Corollary service0:
    service sched j 0 = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  service sched j 0 = 0

----------------------------------------------------------------------------- *)

  Proof.
    rewrite /service service_during_geq //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Trivially, an interval consiting of one time unit is equivalent to service_at.
  Lemma service_during_instant:
    ∀ t,
      service_during sched j t t.+1 = service_at sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 55)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t : instant, service_during sched j t t.+1 = service_at sched j t

----------------------------------------------------------------------------- *)

  Proof.
    move ⇒ t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 56)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  ============================
  service_during sched j t t.+1 = service_at sched j t

----------------------------------------------------------------------------- *)

     by rewrite /service_during big_nat_recr ?big_geq //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Next, we observe that we can look at the service received during an interval [t1, t3) as the sum of the service during [t1, t2) and [t2, t3) for any t2 \in [t1, t3]. (The "_cat" suffix denotes the concatenation of the two intervals.)
  Lemma service_during_cat:
    ∀ t1 t2 t3,
      t1 ≤ t2 ≤ t3 →
      (service_during sched j t1 t2) + (service_during sched j t2 t3)
      = service_during sched j t1 t3.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 70)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t1 t2 t3 : nat,
  t1 <= t2 <= t3 ->
  service_during sched j t1 t2 + service_during sched j t2 t3 =
  service_during sched j t1 t3

----------------------------------------------------------------------------- *)

  Proof.
    move ⇒ t1 t2 t3 /andP [t1t2 t2t3].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 137)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2, t3 : nat
  t1t2 : t1 <= t2
  t2t3 : t2 <= t3
  ============================
  service_during sched j t1 t2 + service_during sched j t2 t3 =
  service_during sched j t1 t3

----------------------------------------------------------------------------- *)

      by rewrite /service_during -big_cat_nat /=.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Since [service] is just a special case of [service_during], the same holds for [service].
  Lemma service_cat:
    ∀ t1 t2,
      t1 ≤ t2 →
      (service sched j t1) + (service_during sched j t1 t2)
      = service sched j t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 84)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t1 t2 : nat,
  t1 <= t2 ->
  service sched j t1 + service_during sched j t1 t2 = service sched j t2

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ t1 t2 t1t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 87)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : nat
  t1t2 : t1 <= t2
  ============================
  service sched j t1 + service_during sched j t1 t2 = service sched j t2

----------------------------------------------------------------------------- *)

    rewrite /service service_during_cat //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

As a special case, we observe that the service during an interval can be decomposed into the first instant and the rest of the interval.
  Lemma service_during_first_plus_later:
    ∀ t1 t2,
      t1 < t2 →
      (service_at sched j t1) + (service_during sched j t1.+1 t2)
      = service_during sched j t1 t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 98)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t1 t2 : nat,
  t1 < t2 ->
  service_at sched j t1 + service_during sched j t1.+1 t2 =
  service_during sched j t1 t2

----------------------------------------------------------------------------- *)

  Proof.
    move ⇒ t1 t2 t1t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 101)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : nat
  t1t2 : t1 < t2
  ============================
  service_at sched j t1 + service_during sched j t1.+1 t2 =
  service_during sched j t1 t2

----------------------------------------------------------------------------- *)

    have TIMES: t1 ≤ t1.+1 ≤ t2 by rewrite /(_ && _) ifT //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 121)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : nat
  t1t2 : t1 < t2
  TIMES : t1 <= t1.+1 <= t2
  ============================
  service_at sched j t1 + service_during sched j t1.+1 t2 =
  service_during sched j t1 t2

----------------------------------------------------------------------------- *)

    have SPLIT := service_during_cat t1 t1.+1 t2 TIMES.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 126)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : nat
  t1t2 : t1 < t2
  TIMES : t1 <= t1.+1 <= t2
  SPLIT : service_during sched j t1 t1.+1 + service_during sched j t1.+1 t2 =
          service_during sched j t1 t2
  ============================
  service_at sched j t1 + service_during sched j t1.+1 t2 =
  service_during sched j t1 t2

----------------------------------------------------------------------------- *)

      by rewrite -service_during_instant //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Symmetrically, we have the same for the end of the interval.
  Lemma service_during_last_plus_before:
    ∀ t1 t2,
      t1 ≤ t2 →
      (service_during sched j t1 t2) + (service_at sched j t2)
      = service_during sched j t1 t2.+1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 112)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t1 t2 : nat,
  t1 <= t2 ->
  service_during sched j t1 t2 + service_at sched j t2 =
  service_during sched j t1 t2.+1

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ t1 t2 t1t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 115)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : nat
  t1t2 : t1 <= t2
  ============================
  service_during sched j t1 t2 + service_at sched j t2 =
  service_during sched j t1 t2.+1

----------------------------------------------------------------------------- *)

    rewrite -(service_during_cat t1 t2 t2.+1); last by rewrite /(_ && _) ifT //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 118)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : nat
  t1t2 : t1 <= t2
  ============================
  service_during sched j t1 t2 + service_at sched j t2 =
  service_during sched j t1 t2 + service_during sched j t2 t2.+1

----------------------------------------------------------------------------- *)

    rewrite service_during_instant //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

And hence also for [service].
  Corollary service_last_plus_before:
    ∀ t,
      (service sched j t) + (service_at sched j t)
      = service sched j t.+1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 125)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t : instant,
  service sched j t + service_at sched j t = service sched j t.+1

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 126)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  ============================
  service sched j t + service_at sched j t = service sched j t.+1

----------------------------------------------------------------------------- *)

    rewrite /service.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 133)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  ============================
  service_during sched j 0 t + service_at sched j t =
  service_during sched j 0 t.+1

----------------------------------------------------------------------------- *)

rewrite -service_during_last_plus_before //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Finally, we deconstruct the service received during an interval [t1, t3) into the service at a midpoint t2 and the service in the intervals before and after.
  Lemma service_split_at_point:
    ∀ t1 t2 t3,
      t1 ≤ t2 < t3 →
      (service_during sched j t1 t2) + (service_at sched j t2) + (service_during sched j t2.+1 t3)
      = service_during sched j t1 t3.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 143)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t1 t2 t3 : nat,
  t1 <= t2 < t3 ->
  service_during sched j t1 t2 + service_at sched j t2 +
  service_during sched j t2.+1 t3 = service_during sched j t1 t3

----------------------------------------------------------------------------- *)

  Proof.
    move ⇒ t1 t2 t3 /andP [t1t2 t2t3].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 210)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2, t3 : nat
  t1t2 : t1 <= t2
  t2t3 : t2 < t3
  ============================
  service_during sched j t1 t2 + service_at sched j t2 +
  service_during sched j t2.+1 t3 = service_during sched j t1 t3

----------------------------------------------------------------------------- *)

    rewrite -addnA service_during_first_plus_later// service_during_cat// /(_ && _) ifT//.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 290)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2, t3 : nat
  t1t2 : t1 <= t2
  t2t3 : t2 < t3
  ============================
  t2 <= t3

----------------------------------------------------------------------------- *)

      by exact: ltnW.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End Composition.

Section UnitService.
As a common special case, we establish facts about schedules in which a job receives either 1 or 0 service units at all times.
Consider any job type and any processor state.
  Context {Job: JobType}.
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

Let's consider a unit-service model...
  Hypothesis H_unit_service: unit_service_proc_model PState.

...and a given schedule.
  Variable sched: schedule PState.

Let j be any job that is to be scheduled.
  Variable j: Job.

First, we prove that the instantaneous service cannot be greater than 1, ...
  Lemma service_at_most_one:
    ∀ t, service_at sched j t ≤ 1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 38)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  ============================
  forall t : instant, service_at sched j t <= 1

----------------------------------------------------------------------------- *)

  Proof.
      by move⇒ t; rewrite /service_at.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

...which implies that the cumulative service received by job j in any interval of length delta is at most delta.
  Lemma cumulative_service_le_delta:
    ∀ t delta,
      service_during sched j t (t + delta) ≤ delta.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 44)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  ============================
  forall (t : instant) (delta : nat),
  service_during sched j t (t + delta) <= delta

----------------------------------------------------------------------------- *)

  Proof.
    unfold service_during; intros t delta.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  t : instant
  delta : nat
  ============================
  \sum_(t <= t0 < t + delta) service_at sched j t0 <= delta

----------------------------------------------------------------------------- *)

    apply leq_trans with (n := \sum_(t ≤ t0 < t + delta) 1);
      last by rewrite sum_of_ones.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 53)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  t : instant
  delta : nat
  ============================
  \sum_(t <= t0 < t + delta) service_at sched j t0 <=
  \sum_(t <= t0 < t + delta) 1

----------------------------------------------------------------------------- *)

    by apply: leq_sum ⇒ t' _; apply: service_at_most_one.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Section ServiceIsAStepFunction.

We show that the service received by any job j is a step function.
    Lemma service_is_a_step_function:
      is_step_function (service sched j).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  ============================
  is_step_function (service sched j)

----------------------------------------------------------------------------- *)

    Proof.
      rewrite /is_step_function ⇒ t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 50)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  t : nat
  ============================
  service sched j (t + 1) <= service sched j t + 1

----------------------------------------------------------------------------- *)

      rewrite addn1 -service_last_plus_before leq_add2l.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 69)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  t : nat
  ============================
  service_at sched j t <= 1

----------------------------------------------------------------------------- *)

      apply service_at_most_one.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

Next, consider any time t...
    Variable t: instant.

...and let s0 be any value less than the service received by job j by time t.
    Variable s0: duration.
    Hypothesis H_less_than_s: s0 < service sched j t.

Then, we show that there exists an earlier time t0 where job j had s0 units of service.
    Corollary exists_intermediate_service:
      ∃ t0,
        t0 < t ∧
        service sched j t0 = s0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 59)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  t : instant
  s0 : duration
  H_less_than_s : s0 < service sched j t
  ============================
  exists t0 : nat, t0 < t /\ service sched j t0 = s0

----------------------------------------------------------------------------- *)

    Proof.
      feed (exists_intermediate_point (service sched j));
        [by apply service_is_a_step_function | intros EX].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 69)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  t : instant
  s0 : duration
  H_less_than_s : s0 < service sched j t
  EX : forall x1 x2 : nat,
       x1 <= x2 ->
       forall y : nat,
       service sched j x1 <= y < service sched j x2 ->
       exists x_mid : nat, x1 <= x_mid < x2 /\ service sched j x_mid = y
  ============================
  exists t0 : nat, t0 < t /\ service sched j t0 = s0

----------------------------------------------------------------------------- *)

      feed (EX 0 t); first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 75)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  t : instant
  s0 : duration
  H_less_than_s : s0 < service sched j t
  EX : forall y : nat,
       service sched j 0 <= y < service sched j t ->
       exists x_mid : nat, 0 <= x_mid < t /\ service sched j x_mid = y
  ============================
  exists t0 : nat, t0 < t /\ service sched j t0 = s0

----------------------------------------------------------------------------- *)

      feed (EX s0);
        first by rewrite /service /service_during big_geq //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 81)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  H_unit_service : unit_service_proc_model PState
  sched : schedule PState
  j : Job
  t : instant
  s0 : duration
  H_less_than_s : s0 < service sched j t
  EX : exists x_mid : nat, 0 <= x_mid < t /\ service sched j x_mid = s0
  ============================
  exists t0 : nat, t0 < t /\ service sched j t0 = s0

----------------------------------------------------------------------------- *)

        by move: EX ⇒ /= [x_mid EX]; ∃ x_mid.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.
  End ServiceIsAStepFunction.

End UnitService.

Section Monotonicity.
We establish a basic fact about the monotonicity of service.
Consider any job type and any processor model.
  Context {Job: JobType}.
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

Consider any given schedule...
  Variable sched: schedule PState.

...and a given job that is to be scheduled.
  Variable j: Job.

We observe that the amount of service received is monotonic by definition.
  Lemma service_monotonic:
    ∀ t1 t2,
      t1 ≤ t2 →
      service sched j t1 ≤ service sched j t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 40)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t1 t2 : nat, t1 <= t2 -> service sched j t1 <= service sched j t2

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ t1 t2 let1t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 43)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : nat
  let1t2 : t1 <= t2
  ============================
  service sched j t1 <= service sched j t2

----------------------------------------------------------------------------- *)

      by rewrite -(service_cat sched j t1 t2 let1t2); apply: leq_addr.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End Monotonicity.

Section RelationToScheduled.
Consider any job type and any processor model.
  Context {Job: JobType}.
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

Consider any given schedule...
  Variable sched: schedule PState.

...and a given job that is to be scheduled.
  Variable j: Job.

We observe that a job that isn't scheduled cannot possibly receive service.
  Lemma not_scheduled_implies_no_service:
    ∀ t,
      ~~ scheduled_at sched j t → service_at sched j t = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 41)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t : instant, ~~ scheduled_at sched j t -> service_at sched j t = 0

----------------------------------------------------------------------------- *)

  Proof.
    rewrite /service_at /scheduled_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 55)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t : instant,
  ~~ scheduled_in j (sched t) -> service_in j (sched t) = 0

----------------------------------------------------------------------------- *)

    move⇒ t NOT_SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  NOT_SCHED : ~~ scheduled_in j (sched t)
  ============================
  service_in j (sched t) = 0

----------------------------------------------------------------------------- *)

    rewrite service_implies_scheduled //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Conversely, if a job receives service, then it must be scheduled.
  Lemma service_at_implies_scheduled_at:
    ∀ t,
      service_at sched j t > 0 → scheduled_at sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 49)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t : instant, 0 < service_at sched j t -> scheduled_at sched j t

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 50)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  ============================
  0 < service_at sched j t -> scheduled_at sched j t

----------------------------------------------------------------------------- *)

    destruct (scheduled_at sched j t) eqn:SCHEDULED; first trivial.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 66)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  SCHEDULED : scheduled_at sched j t = false
  ============================
  0 < service_at sched j t -> false

----------------------------------------------------------------------------- *)

    rewrite not_scheduled_implies_no_service // negbT //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Thus, if the cumulative amount of service changes, then it must be scheduled, too.
  Lemma service_delta_implies_scheduled:
    ∀ t,
      service sched j t < service sched j t.+1 → scheduled_at sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 60)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t : instant,
  service sched j t < service sched j t.+1 -> scheduled_at sched j t

----------------------------------------------------------------------------- *)

  Proof.
    move ⇒ t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 61)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  ============================
  service sched j t < service sched j t.+1 -> scheduled_at sched j t

----------------------------------------------------------------------------- *)

    rewrite -service_last_plus_before -{1}(addn0 (service sched j t)) ltn_add2l.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 85)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  ============================
  0 < service_at sched j t -> scheduled_at sched j t

----------------------------------------------------------------------------- *)

    apply: service_at_implies_scheduled_at.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We observe that a job receives cumulative service during some interval iff it receives services at some specific time in the interval.
  Lemma service_during_service_at:
    ∀ t1 t2,
      service_during sched j t1 t2 > 0
      ↔
      ∃ t,
        t1 ≤ t < t2 ∧
        service_at sched j t > 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 71)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t1 t2 : instant,
  0 < service_during sched j t1 t2 <->
  (exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t)

----------------------------------------------------------------------------- *)

  Proof.
    split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 75)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  ============================
  0 < service_during sched j t1 t2 ->
  exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

subgoal 2 (ID 76) is:
 (exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t) ->
 0 < service_during sched j t1 t2

----------------------------------------------------------------------------- *)

    {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 75)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  ============================
  0 < service_during sched j t1 t2 ->
  exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

----------------------------------------------------------------------------- *)

      move⇒ NONZERO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 77)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  NONZERO : 0 < service_during sched j t1 t2
  ============================
  exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

----------------------------------------------------------------------------- *)

      case (boolP([∃ t: 'I_t2,
                      (t ≥ t1) && (service_at sched j t > 0)])) ⇒ [EX | ALL].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 90)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  NONZERO : 0 < service_during sched j t1 t2
  EX : [exists t, (t1 <= t) && (0 < service_at sched j t)]
  ============================
  exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

subgoal 2 (ID 91) is:
 exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

----------------------------------------------------------------------------- *)

      - move: EX ⇒ /existsP [x /andP [GE SERV]].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 219)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  NONZERO : 0 < service_during sched j t1 t2
  x : ordinal_finType t2
  GE : t1 <= x
  SERV : 0 < service_at sched j x
  ============================
  exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

subgoal 2 (ID 91) is:
 exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

----------------------------------------------------------------------------- *)

        ∃ x; split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 223)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  NONZERO : 0 < service_during sched j t1 t2
  x : ordinal_finType t2
  GE : t1 <= x
  SERV : 0 < service_at sched j x
  ============================
  t1 <= x < t2

subgoal 2 (ID 91) is:
 exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

----------------------------------------------------------------------------- *)

        apply /andP; by split.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 91)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  NONZERO : 0 < service_during sched j t1 t2
  ALL : ~~ [exists t, (t1 <= t) && (0 < service_at sched j t)]
  ============================
  exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

----------------------------------------------------------------------------- *)

      - rewrite negb_exists in ALL; move: ALL ⇒ /forallP ALL.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 373)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  NONZERO : 0 < service_during sched j t1 t2
  ALL : forall x : ordinal_finType t2,
        ~~ ((t1 <= x) && (0 < service_at sched j x))
  ============================
  exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

----------------------------------------------------------------------------- *)

        rewrite /service_during big_nat_cond in NONZERO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 405)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  ALL : forall x : ordinal_finType t2,
        ~~ ((t1 <= x) && (0 < service_at sched j x))
  NONZERO : 0 <
            \sum_(t1 <= i < t2 | (t1 <= i < t2) && true) service_at sched j i
  ============================
  exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

----------------------------------------------------------------------------- *)

        rewrite big1 ?ltn0 // in NONZERO ⇒ i.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 492)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  ALL : forall x : ordinal_finType t2,
        ~~ ((t1 <= x) && (0 < service_at sched j x))
  i : nat
  ============================
  (t1 <= i < t2) && true -> service_at sched j i = 0

----------------------------------------------------------------------------- *)

        rewrite andbT; move ⇒ /andP [GT LT].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 561)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  ALL : forall x : ordinal_finType t2,
        ~~ ((t1 <= x) && (0 < service_at sched j x))
  i : nat
  GT : t1 <= i
  LT : i < t2
  ============================
  service_at sched j i = 0

----------------------------------------------------------------------------- *)

        specialize (ALL (Ordinal LT)); simpl in ALL.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 566)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  i : nat
  LT : i < t2
  ALL : ~~ ((t1 <= i) && (0 < service_at sched j i))
  GT : t1 <= i
  ============================
  service_at sched j i = 0

----------------------------------------------------------------------------- *)

        rewrite GT andTb -eqn0Ngt in ALL.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 594)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  i : nat
  LT : i < t2
  GT : t1 <= i
  ALL : service_at sched j i == 0
  ============================
  service_at sched j i = 0

----------------------------------------------------------------------------- *)

        apply /eqP ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 76)

subgoal 1 (ID 76) is:
 (exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t) ->
 0 < service_during sched j t1 t2

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 76)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  ============================
  (exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t) ->
  0 < service_during sched j t1 t2

----------------------------------------------------------------------------- *)

    {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 76)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  ============================
  (exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t) ->
  0 < service_during sched j t1 t2

----------------------------------------------------------------------------- *)

      move⇒ [t [TT SERVICE]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 698)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t : nat
  TT : t1 <= t < t2
  SERVICE : 0 < service_at sched j t
  ============================
  0 < service_during sched j t1 t2

----------------------------------------------------------------------------- *)

      case (boolP (0 < service_during sched j t1 t2)) ⇒ // NZ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 732)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t : nat
  TT : t1 <= t < t2
  SERVICE : 0 < service_at sched j t
  NZ : ~~ (0 < service_during sched j t1 t2)
  ============================
  0 < service_during sched j t1 t2

----------------------------------------------------------------------------- *)

      exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 733)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t : nat
  TT : t1 <= t < t2
  SERVICE : 0 < service_at sched j t
  NZ : ~~ (0 < service_during sched j t1 t2)
  ============================
  False

----------------------------------------------------------------------------- *)

      rewrite -eqn0Ngt in NZ.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 754)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t : nat
  TT : t1 <= t < t2
  SERVICE : 0 < service_at sched j t
  NZ : service_during sched j t1 t2 == 0
  ============================
  False

----------------------------------------------------------------------------- *)

move/eqP: NZ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 811)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t : nat
  TT : t1 <= t < t2
  SERVICE : 0 < service_at sched j t
  ============================
  service_during sched j t1 t2 = 0 -> False

----------------------------------------------------------------------------- *)

      rewrite big_nat_eq0 ⇒ IS_ZERO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 837)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t : nat
  TT : t1 <= t < t2
  SERVICE : 0 < service_at sched j t
  IS_ZERO : forall i : nat, t1 <= i < t2 -> service_at sched j i = 0
  ============================
  False

----------------------------------------------------------------------------- *)

      have NO_SERVICE := IS_ZERO t TT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 842)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t : nat
  TT : t1 <= t < t2
  SERVICE : 0 < service_at sched j t
  IS_ZERO : forall i : nat, t1 <= i < t2 -> service_at sched j i = 0
  NO_SERVICE : service_at sched j t = 0
  ============================
  False

----------------------------------------------------------------------------- *)

      apply lt0n_neq0 in SERVICE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 843)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t : nat
  TT : t1 <= t < t2
  SERVICE : service_at sched j t != 0
  IS_ZERO : forall i : nat, t1 <= i < t2 -> service_at sched j i = 0
  NO_SERVICE : service_at sched j t = 0
  ============================
  False

----------------------------------------------------------------------------- *)

        by move/neqP in SERVICE; contradiction.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Thus, any job that receives some service during an interval must be scheduled at some point during the interval...
  Corollary cumulative_service_implies_scheduled:
    ∀ t1 t2,
      service_during sched j t1 t2 > 0 →
      ∃ t,
        t1 ≤ t < t2 ∧
        scheduled_at sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 82)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t1 t2 : instant,
  0 < service_during sched j t1 t2 ->
  exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ t1 t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 84)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  ============================
  0 < service_during sched j t1 t2 ->
  exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t

----------------------------------------------------------------------------- *)

    rewrite service_during_service_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 109)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  ============================
  (exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t) ->
  exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t

----------------------------------------------------------------------------- *)

    move⇒ [t' [TIMES SERVICED]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 130)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t' : nat
  TIMES : t1 <= t' < t2
  SERVICED : 0 < service_at sched j t'
  ============================
  exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t

----------------------------------------------------------------------------- *)

    ∃ t'; split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 135)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  t' : nat
  TIMES : t1 <= t' < t2
  SERVICED : 0 < service_at sched j t'
  ============================
  scheduled_at sched j t'

----------------------------------------------------------------------------- *)

    by apply: service_at_implies_scheduled_at.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

 Qed.

...which implies that any job with positive cumulative service must have been scheduled at some point.
  Corollary positive_service_implies_scheduled_before:
    ∀ t,
      service sched j t > 0 → ∃ t', (t' < t ∧ scheduled_at sched j t').

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 92)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  ============================
  forall t : instant,
  0 < service sched j t -> exists t' : nat, t' < t /\ scheduled_at sched j t'

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 93)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t2 : instant
  ============================
  0 < service sched j t2 ->
  exists t' : nat, t' < t2 /\ scheduled_at sched j t'

----------------------------------------------------------------------------- *)

    rewrite /service ⇒ NONZERO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 101)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t2 : instant
  NONZERO : 0 < service_during sched j 0 t2
  ============================
  exists t' : nat, t' < t2 /\ scheduled_at sched j t'

----------------------------------------------------------------------------- *)

    have EX_SCHED := cumulative_service_implies_scheduled 0 t2 NONZERO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 106)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t2 : instant
  NONZERO : 0 < service_during sched j 0 t2
  EX_SCHED : exists t : nat, 0 <= t < t2 /\ scheduled_at sched j t
  ============================
  exists t' : nat, t' < t2 /\ scheduled_at sched j t'

----------------------------------------------------------------------------- *)

    by move: EX_SCHED ⇒ [t [TIMES SCHED_AT]]; ∃ t; split.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Section GuaranteedService.
If we can assume that a scheduled job always receives service, we can further prove the converse.
Assume j always receives some positive service.
    Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.

In other words, not being scheduled is equivalent to receiving zero service.
    Lemma no_service_not_scheduled:
      ∀ t,
        ~~ scheduled_at sched j t ↔ service_at sched j t = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 104)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  ============================
  forall t : instant, ~~ scheduled_at sched j t <-> service_at sched j t = 0

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 105)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t : instant
  ============================
  ~~ scheduled_at sched j t <-> service_at sched j t = 0

----------------------------------------------------------------------------- *)

rewrite /scheduled_at /service_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 119)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t : instant
  ============================
  ~~ scheduled_in j (sched t) <-> service_in j (sched t) = 0

----------------------------------------------------------------------------- *)

      split ⇒ [NOT_SCHED | NO_SERVICE].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 123)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t : instant
  NOT_SCHED : ~~ scheduled_in j (sched t)
  ============================
  service_in j (sched t) = 0

subgoal 2 (ID 124) is:
 ~~ scheduled_in j (sched t)

----------------------------------------------------------------------------- *)

      - by rewrite service_implies_scheduled //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 124)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t : instant
  NO_SERVICE : service_in j (sched t) = 0
  ============================
  ~~ scheduled_in j (sched t)

----------------------------------------------------------------------------- *)

      - apply (contra (H_scheduled_implies_serviced j (sched t))).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 139)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t : instant
  NO_SERVICE : service_in j (sched t) = 0
  ============================
  ~~ (0 < service_in j (sched t))

----------------------------------------------------------------------------- *)

        by rewrite -eqn0Ngt; apply /eqP ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

Then, if a job does not receive any service during an interval, it is not scheduled.
    Lemma no_service_during_implies_not_scheduled:
      ∀ t1 t2,
        service_during sched j t1 t2 = 0 →
        ∀ t,
          t1 ≤ t < t2 → ~~ scheduled_at sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 116)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  ============================
  forall t1 t2 : instant,
  service_during sched j t1 t2 = 0 ->
  forall t : nat, t1 <= t < t2 -> ~~ scheduled_at sched j t

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t1 t2 ZERO_SUM t /andP [GT_t1 LT_t2].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 184)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t1, t2 : instant
  ZERO_SUM : service_during sched j t1 t2 = 0
  t : nat
  GT_t1 : t1 <= t
  LT_t2 : t < t2
  ============================
  ~~ scheduled_at sched j t

----------------------------------------------------------------------------- *)

      rewrite no_service_not_scheduled.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 194)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t1, t2 : instant
  ZERO_SUM : service_during sched j t1 t2 = 0
  t : nat
  GT_t1 : t1 <= t
  LT_t2 : t < t2
  ============================
  service_at sched j t = 0

----------------------------------------------------------------------------- *)

      move: ZERO_SUM.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 196)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t1, t2 : instant
  t : nat
  GT_t1 : t1 <= t
  LT_t2 : t < t2
  ============================
  service_during sched j t1 t2 = 0 -> service_at sched j t = 0

----------------------------------------------------------------------------- *)

      rewrite /service_during big_nat_eq0 ⇒ IS_ZERO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 231)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t1, t2 : instant
  t : nat
  GT_t1 : t1 <= t
  LT_t2 : t < t2
  IS_ZERO : forall i : nat, t1 <= i < t2 -> service_at sched j i = 0
  ============================
  service_at sched j t = 0

----------------------------------------------------------------------------- *)

      by apply (IS_ZERO t); apply /andP; split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

If a job is scheduled at some point in an interval, it receivees positive cumulative service during the interval...
    Lemma scheduled_implies_cumulative_service:
      ∀ t1 t2,
        (∃ t,
            t1 ≤ t < t2 ∧
            scheduled_at sched j t) →
        service_during sched j t1 t2 > 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 127)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  ============================
  forall t1 t2 : nat,
  (exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t) ->
  0 < service_during sched j t1 t2

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t1 t2 [t' [TIMES SCHED]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 150)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t1, t2, t' : nat
  TIMES : t1 <= t' < t2
  SCHED : scheduled_at sched j t'
  ============================
  0 < service_during sched j t1 t2

----------------------------------------------------------------------------- *)

      rewrite service_during_service_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 161)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t1, t2, t' : nat
  TIMES : t1 <= t' < t2
  SCHED : scheduled_at sched j t'
  ============================
  exists t : nat, t1 <= t < t2 /\ 0 < service_at sched j t

----------------------------------------------------------------------------- *)

      ∃ t'; split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 166)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t1, t2, t' : nat
  TIMES : t1 <= t' < t2
  SCHED : scheduled_at sched j t'
  ============================
  0 < service_at sched j t'

----------------------------------------------------------------------------- *)

      move: SCHED.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 190)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t1, t2, t' : nat
  TIMES : t1 <= t' < t2
  ============================
  scheduled_at sched j t' -> 0 < service_at sched j t'

----------------------------------------------------------------------------- *)

rewrite /scheduled_at /service_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 204)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t1, t2, t' : nat
  TIMES : t1 <= t' < t2
  ============================
  scheduled_in j (sched t') -> 0 < service_in j (sched t')

----------------------------------------------------------------------------- *)

        by apply (H_scheduled_implies_serviced j (sched t')).

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

...which again applies to total service, too.
    Corollary scheduled_implies_nonzero_service:
      ∀ t,
        (∃ t',
            t' < t ∧
            scheduled_at sched j t') →
        service sched j t > 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 137)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  ============================
  forall t : nat,
  (exists t' : nat, t' < t /\ scheduled_at sched j t') ->
  0 < service sched j t

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t [t' [TT SCHED]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 159)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t, t' : nat
  TT : t' < t
  SCHED : scheduled_at sched j t'
  ============================
  0 < service sched j t

----------------------------------------------------------------------------- *)

      rewrite /service.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 166)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t, t' : nat
  TT : t' < t
  SCHED : scheduled_at sched j t'
  ============================
  0 < service_during sched j 0 t

----------------------------------------------------------------------------- *)

apply scheduled_implies_cumulative_service.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 167)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  t, t' : nat
  TT : t' < t
  SCHED : scheduled_at sched j t'
  ============================
  exists t0 : nat, 0 <= t0 < t /\ scheduled_at sched j t0

----------------------------------------------------------------------------- *)

      ∃ t'; split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

  End GuaranteedService.

  Section AfterArrival.
Futhermore, if we know that jobs are not released early, then we can narrow the interval during which they must have been scheduled.

    Context `{JobArrival Job}.

Assume that jobs must arrive to execute.
    Hypothesis H_jobs_must_arrive:
      jobs_must_arrive_to_execute sched.

We prove that any job with positive cumulative service at time [t] must have been scheduled some time since its arrival and before time [t].
    Lemma positive_service_implies_scheduled_since_arrival:
      ∀ t,
        service sched j t > 0 →
        ∃ t', (job_arrival j ≤ t' < t ∧ scheduled_at sched j t').

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  ============================
  forall t : instant,
  0 < service sched j t ->
  exists t' : nat, job_arrival j <= t' < t /\ scheduled_at sched j t'

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t SERVICE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 110)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : instant
  SERVICE : 0 < service sched j t
  ============================
  exists t' : nat, job_arrival j <= t' < t /\ scheduled_at sched j t'

----------------------------------------------------------------------------- *)

      have EX_SCHED := positive_service_implies_scheduled_before t SERVICE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 115)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : instant
  SERVICE : 0 < service sched j t
  EX_SCHED : exists t' : nat, t' < t /\ scheduled_at sched j t'
  ============================
  exists t' : nat, job_arrival j <= t' < t /\ scheduled_at sched j t'

----------------------------------------------------------------------------- *)

      inversion EX_SCHED as [t'' [TIMES SCHED_AT]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 128)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : instant
  SERVICE : 0 < service sched j t
  EX_SCHED : exists t' : nat, t' < t /\ scheduled_at sched j t'
  t'' : nat
  TIMES : t'' < t
  SCHED_AT : scheduled_at sched j t''
  ============================
  exists t' : nat, job_arrival j <= t' < t /\ scheduled_at sched j t'

----------------------------------------------------------------------------- *)

      ∃ t''; split; last by assumption.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 132)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : instant
  SERVICE : 0 < service sched j t
  EX_SCHED : exists t' : nat, t' < t /\ scheduled_at sched j t'
  t'' : nat
  TIMES : t'' < t
  SCHED_AT : scheduled_at sched j t''
  ============================
  job_arrival j <= t'' < t

----------------------------------------------------------------------------- *)

      rewrite /(_ && _) ifT //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 150)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : instant
  SERVICE : 0 < service sched j t
  EX_SCHED : exists t' : nat, t' < t /\ scheduled_at sched j t'
  t'' : nat
  TIMES : t'' < t
  SCHED_AT : scheduled_at sched j t''
  ============================
  job_arrival j <= t''

----------------------------------------------------------------------------- *)

      move: H_jobs_must_arrive.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 173)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : instant
  SERVICE : 0 < service sched j t
  EX_SCHED : exists t' : nat, t' < t /\ scheduled_at sched j t'
  t'' : nat
  TIMES : t'' < t
  SCHED_AT : scheduled_at sched j t''
  ============================
  jobs_must_arrive_to_execute sched -> job_arrival j <= t''

----------------------------------------------------------------------------- *)

rewrite /jobs_must_arrive_to_execute /has_arrived ⇒ ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 186)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : instant
  SERVICE : 0 < service sched j t
  EX_SCHED : exists t' : nat, t' < t /\ scheduled_at sched j t'
  t'' : nat
  TIMES : t'' < t
  SCHED_AT : scheduled_at sched j t''
  ARR : forall (j : Job) (t : instant),
        scheduled_at sched j t -> job_arrival j <= t
  ============================
  job_arrival j <= t''

----------------------------------------------------------------------------- *)

        by apply: ARR; exact.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

    Lemma not_scheduled_before_arrival:
      ∀ t, t < job_arrival j → ~~ scheduled_at sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 115)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  ============================
  forall t : nat, t < job_arrival j -> ~~ scheduled_at sched j t

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t EARLY.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 117)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : nat
  EARLY : t < job_arrival j
  ============================
  ~~ scheduled_at sched j t

----------------------------------------------------------------------------- *)

      apply: (contra (H_jobs_must_arrive j t)).

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 128)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : nat
  EARLY : t < job_arrival j
  ============================
  ~~ has_arrived j t

----------------------------------------------------------------------------- *)

      rewrite /has_arrived -ltnNge //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

   Qed.

We show that job j does not receive service at any time t prior to its arrival.
    Lemma service_before_job_arrival_zero:
      ∀ t,
        t < job_arrival j →
        service_at sched j t = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 124)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  ============================
  forall t : nat, t < job_arrival j -> service_at sched j t = 0

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t NOT_ARR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 126)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : nat
  NOT_ARR : t < job_arrival j
  ============================
  service_at sched j t = 0

----------------------------------------------------------------------------- *)

      rewrite not_scheduled_implies_no_service // not_scheduled_before_arrival //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

Note that the same property applies to the cumulative service.
    Lemma cumulative_service_before_job_arrival_zero :
      ∀ t1 t2 : instant,
        t2 ≤ job_arrival j →
        service_during sched j t1 t2 = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 132)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  ============================
  forall t1 t2 : instant,
  t2 <= job_arrival j -> service_during sched j t1 t2 = 0

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t1 t2 EARLY.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 135)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : instant
  EARLY : t2 <= job_arrival j
  ============================
  service_during sched j t1 t2 = 0

----------------------------------------------------------------------------- *)

      rewrite /service_during.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 142)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : instant
  EARLY : t2 <= job_arrival j
  ============================
  \sum_(t1 <= t < t2) service_at sched j t = 0

----------------------------------------------------------------------------- *)

      have ZERO_SUM: \sum_(t1 ≤ t < t2) service_at sched j t = \sum_(t1 ≤ t < t2) 0;
        last by rewrite ZERO_SUM sum0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 156)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : instant
  EARLY : t2 <= job_arrival j
  ============================
  \sum_(t1 <= t < t2) service_at sched j t = \sum_(t1 <= t < t2) 0

----------------------------------------------------------------------------- *)

      rewrite big_nat_cond [in RHS]big_nat_cond.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 190)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : instant
  EARLY : t2 <= job_arrival j
  ============================
  \sum_(t1 <= i < t2 | (t1 <= i < t2) && true) service_at sched j i =
  \sum_(t1 <= i < t2 | (t1 <= i < t2) && true) 0

----------------------------------------------------------------------------- *)

      apply: eq_bigr ⇒ i /andP [TIMES _].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 307)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : instant
  EARLY : t2 <= job_arrival j
  i : nat
  TIMES : t1 <= i < t2
  ============================
  service_at sched j i = 0

----------------------------------------------------------------------------- *)

move: TIMES ⇒ /andP [le_t1_i lt_i_t2].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 373)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : instant
  EARLY : t2 <= job_arrival j
  i : nat
  le_t1_i : t1 <= i
  lt_i_t2 : i < t2
  ============================
  service_at sched j i = 0

----------------------------------------------------------------------------- *)

      apply (service_before_job_arrival_zero i).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 374)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : instant
  EARLY : t2 <= job_arrival j
  i : nat
  le_t1_i : t1 <= i
  lt_i_t2 : i < t2
  ============================
  i < job_arrival j

----------------------------------------------------------------------------- *)

        by apply leq_trans with (n := t2); auto.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

Hence, one can ignore the service received by a job before its arrival time...
    Lemma ignore_service_before_arrival:
      ∀ t1 t2,
        t1 ≤ job_arrival j →
        t2 ≥ job_arrival j →
        service_during sched j t1 t2 = service_during sched j (job_arrival j) t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 149)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  ============================
  forall t1 t2 : nat,
  t1 <= job_arrival j ->
  job_arrival j <= t2 ->
  service_during sched j t1 t2 = service_during sched j (job_arrival j) t2

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t1 t2 le_t1 le_t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 153)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : nat
  le_t1 : t1 <= job_arrival j
  le_t2 : job_arrival j <= t2
  ============================
  service_during sched j t1 t2 = service_during sched j (job_arrival j) t2

----------------------------------------------------------------------------- *)

      rewrite -(service_during_cat sched j t1 (job_arrival j) t2).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 166)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : nat
  le_t1 : t1 <= job_arrival j
  le_t2 : job_arrival j <= t2
  ============================
  service_during sched j t1 (job_arrival j) +
  service_during sched j (job_arrival j) t2 =
  service_during sched j (job_arrival j) t2

subgoal 2 (ID 167) is:
 t1 <= job_arrival j <= t2

----------------------------------------------------------------------------- *)

      rewrite cumulative_service_before_job_arrival_zero //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 167)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t1, t2 : nat
  le_t1 : t1 <= job_arrival j
  le_t2 : job_arrival j <= t2
  ============================
  t1 <= job_arrival j <= t2

----------------------------------------------------------------------------- *)

        by apply/andP; split; exact.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

... which we can also state in terms of cumulative service.
    Corollary no_service_before_arrival:
      ∀ t,
        t ≤ job_arrival j → service sched j t = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 158)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  ============================
  forall t : nat, t <= job_arrival j -> service sched j t = 0

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t EARLY.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 160)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  H0 : JobArrival Job
  H_jobs_must_arrive : jobs_must_arrive_to_execute sched
  t : nat
  EARLY : t <= job_arrival j
  ============================
  service sched j t = 0

----------------------------------------------------------------------------- *)

      rewrite /service cumulative_service_before_job_arrival_zero //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

  End AfterArrival.

  Section TimesWithSameService.
In this section, we prove some lemmas about time instants with same service.
Consider any time instants t1 and t2...
    Variable t1 t2: instant.

...where t1 is no later than t2...
    Hypothesis H_t1_le_t2: t1 ≤ t2.

...and where job j has received the same amount of service.
    Hypothesis H_same_service: service sched j t1 = service sched j t2.

First, we observe that this means that the job receives no service during [t1, t2)...
    Lemma constant_service_implies_no_service_during:
      service_during sched j t1 t2 = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 106)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  ============================
  service_during sched j t1 t2 = 0

----------------------------------------------------------------------------- *)

    Proof.
      move: H_same_service.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 107)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  ============================
  service sched j t1 = service sched j t2 -> service_during sched j t1 t2 = 0

----------------------------------------------------------------------------- *)

      rewrite -(service_cat sched j t1 t2) // -[service sched j t1 in LHS]addn0 ⇒ /eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 242)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  ============================
  service sched j t1 + 0 == service sched j t1 + service_during sched j t1 t2 ->
  service_during sched j t1 t2 = 0

----------------------------------------------------------------------------- *)

      by rewrite eqn_add2l ⇒ /eqP //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

...which of course implies that it does not receive service at any point, either.
    Lemma constant_service_implies_not_scheduled:
      ∀ t,
        t1 ≤ t < t2 → service_at sched j t = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 113)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  ============================
  forall t : nat, t1 <= t < t2 -> service_at sched j t = 0

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ t /andP [GE_t1 LT_t2].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 178)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : nat
  GE_t1 : t1 <= t
  LT_t2 : t < t2
  ============================
  service_at sched j t = 0

----------------------------------------------------------------------------- *)

      move: constant_service_implies_no_service_during.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 179)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : nat
  GE_t1 : t1 <= t
  LT_t2 : t < t2
  ============================
  service_during sched j t1 t2 = 0 -> service_at sched j t = 0

----------------------------------------------------------------------------- *)

      rewrite /service_during big_nat_eq0 ⇒ IS_ZERO.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 214)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : nat
  GE_t1 : t1 <= t
  LT_t2 : t < t2
  IS_ZERO : forall i : nat, t1 <= i < t2 -> service_at sched j i = 0
  ============================
  service_at sched j t = 0

----------------------------------------------------------------------------- *)

      apply IS_ZERO.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 215)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : nat
  GE_t1 : t1 <= t
  LT_t2 : t < t2
  IS_ZERO : forall i : nat, t1 <= i < t2 -> service_at sched j i = 0
  ============================
  t1 <= t < t2

----------------------------------------------------------------------------- *)

apply /andP; split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

We show that job j receives service at some point t < t1 iff j receives service at some point t' < t2.
    Lemma same_service_implies_serviced_at_earlier_times:
      [∃ t: 'I_t1, service_at sched j t > 0] =
      [∃ t': 'I_t2, service_at sched j t' > 0].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 130)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  ============================
  [exists t, 0 < service_at sched j t] =
  [exists t', 0 < service_at sched j t']

----------------------------------------------------------------------------- *)

    Proof.
      apply /idP/idP ⇒ /existsP [t SERVICED].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 309)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t1
  SERVICED : 0 < service_at sched j t
  ============================
  [exists t', 0 < service_at sched j t']

subgoal 2 (ID 310) is:
 [exists t0, 0 < service_at sched j t0]

----------------------------------------------------------------------------- *)

      {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 309)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t1
  SERVICED : 0 < service_at sched j t
  ============================
  [exists t', 0 < service_at sched j t']

----------------------------------------------------------------------------- *)

        have LE: t < t2
          by apply: (leq_trans _ H_t1_le_t2) ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 324)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t1
  SERVICED : 0 < service_at sched j t
  LE : t < t2
  ============================
  [exists t', 0 < service_at sched j t']

----------------------------------------------------------------------------- *)

        by apply /existsP; ∃ (Ordinal LE).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 310)

subgoal 1 (ID 310) is:
 [exists t0, 0 < service_at sched j t0]

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 310)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t2
  SERVICED : 0 < service_at sched j t
  ============================
  [exists t0, 0 < service_at sched j t0]

----------------------------------------------------------------------------- *)

      {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 310)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t2
  SERVICED : 0 < service_at sched j t
  ============================
  [exists t0, 0 < service_at sched j t0]

----------------------------------------------------------------------------- *)

        case (boolP (t < t1)) ⇒ LE.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 382)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t2
  SERVICED : 0 < service_at sched j t
  LE : t < t1
  ============================
  [exists t0, 0 < service_at sched j t0]

subgoal 2 (ID 383) is:
 [exists t0, 0 < service_at sched j t0]

----------------------------------------------------------------------------- *)

        - by apply /existsP; ∃ (Ordinal LE).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 383)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t2
  SERVICED : 0 < service_at sched j t
  LE : ~~ (t < t1)
  ============================
  [exists t0, 0 < service_at sched j t0]

----------------------------------------------------------------------------- *)

        - exfalso.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 436)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t2
  SERVICED : 0 < service_at sched j t
  LE : ~~ (t < t1)
  ============================
  False

----------------------------------------------------------------------------- *)

          have TIMES: t1 ≤ t < t2
            by apply /andP; split ⇒ //; rewrite leqNgt //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 516)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t2
  SERVICED : 0 < service_at sched j t
  LE : ~~ (t < t1)
  TIMES : t1 <= t < t2
  ============================
  False

----------------------------------------------------------------------------- *)

          have NO_SERVICE := constant_service_implies_not_scheduled t TIMES.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 521)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  t : ordinal_finType t2
  SERVICED : 0 < service_at sched j t
  LE : ~~ (t < t1)
  TIMES : t1 <= t < t2
  NO_SERVICE : service_at sched j t = 0
  ============================
  False

----------------------------------------------------------------------------- *)

          by rewrite NO_SERVICE in SERVICED.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

Then, under the assumption that scheduled jobs receives service, we can translate this into a claim about scheduled_at.
Assume j always receives some positive service.
    Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.

We show that job j is scheduled at some point t < t1 iff j is scheduled at some point t' < t2.
    Lemma same_service_implies_scheduled_at_earlier_times:
      [∃ t: 'I_t1, scheduled_at sched j t] =
      [∃ t': 'I_t2, scheduled_at sched j t'].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 149)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  ============================
  [exists t, scheduled_at sched j t] = [exists t', scheduled_at sched j t']

----------------------------------------------------------------------------- *)

    Proof.
      have CONV: ∀ B, [∃ b: 'I_B, scheduled_at sched j b]
                           = [∃ b: 'I_B, service_at sched j b > 0].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 167)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  ============================
  forall B : nat,
  [exists b, scheduled_at sched j b] = [exists b, 0 < service_at sched j b]

subgoal 2 (ID 169) is:
 [exists t, scheduled_at sched j t] = [exists t', scheduled_at sched j t']

----------------------------------------------------------------------------- *)

      {

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 167)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  ============================
  forall B : nat,
  [exists b, scheduled_at sched j b] = [exists b, 0 < service_at sched j b]

----------------------------------------------------------------------------- *)

        move⇒ B.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 170)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  B : nat
  ============================
  [exists b, scheduled_at sched j b] = [exists b, 0 < service_at sched j b]

----------------------------------------------------------------------------- *)

apply/idP/idP ⇒ /existsP [b P]; apply /existsP; ∃ b.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 448)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  B : nat
  b : ordinal_finType B
  P : scheduled_at sched j b
  ============================
  0 < service_at sched j b

subgoal 2 (ID 450) is:
 scheduled_at sched j b

----------------------------------------------------------------------------- *)

        - by move: P; rewrite /scheduled_at /service_at;
            apply (H_scheduled_implies_serviced j (sched b)).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 450)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  B : nat
  b : ordinal_finType B
  P : 0 < service_at sched j b
  ============================
  scheduled_at sched j b

----------------------------------------------------------------------------- *)

        - by apply service_at_implies_scheduled_at.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 169)

subgoal 1 (ID 169) is:
 [exists t, scheduled_at sched j t] = [exists t', scheduled_at sched j t']

----------------------------------------------------------------------------- *)

      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 169)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  CONV : forall B : nat,
         [exists b, scheduled_at sched j b] =
         [exists b, 0 < service_at sched j b]
  ============================
  [exists t, scheduled_at sched j t] = [exists t', scheduled_at sched j t']

----------------------------------------------------------------------------- *)

      rewrite !CONV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 473)
  
  Job : JobType
  PState : Type
  H : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t1, t2 : instant
  H_t1_le_t2 : t1 <= t2
  H_same_service : service sched j t1 = service sched j t2
  H_scheduled_implies_serviced : ideal_progress_proc_model PState
  CONV : forall B : nat,
         [exists b, scheduled_at sched j b] =
         [exists b, 0 < service_at sched j b]
  ============================
  [exists b, 0 < service_at sched j b] = [exists b, 0 < service_at sched j b]

----------------------------------------------------------------------------- *)

      apply same_service_implies_serviced_at_earlier_times.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.
  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:
    ∀ j t1 t2,
      0 < service_during sched j t1 t2 →
      ∃ t : nat, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 50)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  ============================
  forall (j : Job) (t1 t2 : instant),
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 54)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 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

----------------------------------------------------------------------------- *)

    have LE: t1 ≤ t2.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 55)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  ============================
  t1 <= t2

subgoal 2 (ID 57) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 55)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  ============================
  t1 <= t2

----------------------------------------------------------------------------- *)

rewrite leqNgt; apply/negP; intros CONTR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 103)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  CONTR : t2 < t1
  ============================
  False

----------------------------------------------------------------------------- *)

        by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)

subgoal 1 (ID 57) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    destruct (scheduled_at sched j t1) eqn:SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 167)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

subgoal 2 (ID 168) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 167)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

∃ t1; repeat split; try done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 172)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  t1 <= t1 < t2

subgoal 2 (ID 177) is:
 service_during sched j t1 t1 = 0

----------------------------------------------------------------------------- *)

      - apply/andP; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 274)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  t1 < t2

subgoal 2 (ID 177) is:
 service_during sched j t1 t1 = 0

----------------------------------------------------------------------------- *)

        rewrite ltnNge; apply/negP; intros CONTR.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 320)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  CONTR : t2 <= t1
  ============================
  False

subgoal 2 (ID 177) is:
 service_during sched j t1 t1 = 0

----------------------------------------------------------------------------- *)

          by move: SERV; rewrite/service_during big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 177)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  service_during sched j t1 t1 = 0

----------------------------------------------------------------------------- *)

      - by rewrite /service_during big_geq.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)

subgoal 1 (ID 168) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)


    }
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = false
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

 
    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 168)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = false
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

apply negbT in SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 388)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

      move: SERV; rewrite /service /service_during; move ⇒ /sum_seq_gt0P [t [IN SCHEDt]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 484)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  IN : t \in index_iota t1 t2
  SCHEDt : 0 < service_at sched j t
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      rewrite lt0b in SCHEDt.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 507)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  IN : t \in index_iota t1 t2
  SCHEDt : sched t == Some j
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      rewrite mem_iota subnKC in IN; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 538)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN : t1 <= t < t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      move: IN ⇒ /andP [IN1 IN2].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 619)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      move: (exists_first_intermediate_point
               ((fun t ⇒ scheduled_at sched j t)) t1 t IN1 SCHED) ⇒ A.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 625)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  A : scheduled_at sched j t ->
      exists t0 : nat,
        t1 < t0 <= t /\
        (forall x : nat, t1 <= x < t0 -> ~~ scheduled_at sched j x) /\
        scheduled_at sched j t0
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      feed A; first by rewrite scheduled_at_def/=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 631)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  A : exists t0 : nat,
        t1 < t0 <= t /\
        (forall x : nat, t1 <= x < t0 -> ~~ scheduled_at sched j x) /\
        scheduled_at sched j t0
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      move: A ⇒ [x [/andP [T1 T4] [T2 T3]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 735)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      ∃ x; repeat split; try done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 739)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  t1 <= x < t2

subgoal 2 (ID 744) is:
 \sum_(t1 <= t0 < x) service_at sched j t0 = 0

----------------------------------------------------------------------------- *)

      - apply/andP; split; first by apply ltnW.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 841)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  x < t2

subgoal 2 (ID 744) is:
 \sum_(t1 <= t0 < x) service_at sched j t0 = 0

----------------------------------------------------------------------------- *)

          by apply leq_ltn_trans with t.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 744)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  \sum_(t1 <= t0 < x) service_at sched j t0 = 0

----------------------------------------------------------------------------- *)

      - apply/eqP; rewrite big_nat_cond big1 //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 947)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  forall i : nat, (t1 <= i < x) && true -> service_at sched j i = 0

----------------------------------------------------------------------------- *)

        move ⇒ y /andP [T5 _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1038)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  y : nat
  T5 : t1 <= y < x
  ============================
  service_at sched j y = 0

----------------------------------------------------------------------------- *)

          by apply/eqP; rewrite eqb0; specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  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:
    ∀ j t1 t2 k,
      service_during sched j t1 t2 > k →
      ∃ t, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = k.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 71)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  ============================
  forall (j : Job) (t1 t2 : instant) (k : nat),
  k < service_during sched j t1 t2 ->
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

----------------------------------------------------------------------------- *)

  Proof.
    intros j t1 t2 k SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 76)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

----------------------------------------------------------------------------- *)

    have LE: t1 ≤ t2.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 77)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  ============================
  t1 <= t2

subgoal 2 (ID 79) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 77)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  ============================
  t1 <= t2

----------------------------------------------------------------------------- *)

rewrite leqNgt; apply/negP; intros CONTR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 125)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  CONTR : t2 < t1
  ============================
  False

----------------------------------------------------------------------------- *)

        by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 79)

subgoal 1 (ID 79) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 79)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  LE : t1 <= t2
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

----------------------------------------------------------------------------- *)

    induction k; first by apply positive_service_during in SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 191)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k.+1 < service_during sched j t1 t2
  LE : t1 <= t2
  IHk : k < service_during sched j t1 t2 ->
        exists t : nat,
          t1 <= t < t2 /\
          scheduled_at sched j t /\ service_during sched j t1 t = k
  ============================
  exists t : nat,
    t1 <= t < t2 /\
    scheduled_at sched j t /\ service_during sched j t1 t = k.+1

----------------------------------------------------------------------------- *)

    feed IHk; first by apply ltn_trans with k.+1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 199)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k.+1 < service_during sched j t1 t2
  LE : t1 <= t2
  IHk : exists t : nat,
          t1 <= t < t2 /\
          scheduled_at sched j t /\ service_during sched j t1 t = k
  ============================
  exists t : nat,
    t1 <= t < t2 /\
    scheduled_at sched j t /\ service_during sched j t1 t = k.+1

----------------------------------------------------------------------------- *)

    move: IHk ⇒ [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 297)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k.+1 < service_during sched j t1 t2
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

    have SERVk1: service_during sched j t1 t.+1 = k.+1.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 303)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k.+1 < service_during sched j t1 t2
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  service_during sched j t1 t.+1 = k.+1

subgoal 2 (ID 305) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 303)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k.+1 < service_during sched j t1 t2
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  service_during sched j t1 t.+1 = k.+1

----------------------------------------------------------------------------- *)

rewrite -(service_during_cat _ _ _ t); last by apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 327)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k.+1 < service_during sched j t1 t2
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  service_during sched j t1 t + service_during sched j t t.+1 = k.+1

----------------------------------------------------------------------------- *)

      rewrite SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 480)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k.+1 < service_during sched j t1 t2
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  service_during sched j t t.+1 == 1

----------------------------------------------------------------------------- *)

        by rewrite /service_during big_nat1 /service_at eqb1 -scheduled_at_def/=.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 305)

subgoal 1 (ID 305) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)


    }
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 305)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k.+1 < service_during sched j t1 t2
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)


    move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 537)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  ============================
  t1 <= t.+1 <= t2

subgoal 2 (ID 536) is:
 k.+1 < service_during sched j t1 t.+1 + service_during sched j t.+1 t2 ->
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 537)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  ============================
  t1 <= t.+1 <= t2

----------------------------------------------------------------------------- *)

by apply/andP; split; first apply leq_trans with t.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 536)

subgoal 1 (ID 536) is:
 k.+1 < service_during sched j t1 t.+1 + service_during sched j t.+1 t2 ->
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 536)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  ============================
  k.+1 < service_during sched j t1 t.+1 + service_during sched j t.+1 t2 ->
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

    rewrite SERVk1 -addn1 leq_add2l; move ⇒ SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 601)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SERV : 0 < service_during sched j t.+1 t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

    destruct (scheduled_at sched j t.+1) eqn:SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 614)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SERV : 0 < service_during sched j t.+1 t2
  SCHED : scheduled_at sched j t.+1 = true
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

subgoal 2 (ID 615) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

    - ∃ t.+1; repeat split; try done.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 619)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SERV : 0 < service_during sched j t.+1 t2
  SCHED : scheduled_at sched j t.+1 = true
  ============================
  t1 <= t.+1 < t2

subgoal 2 (ID 615) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 698)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SERV : 0 < service_during sched j t.+1 t2
  SCHED : scheduled_at sched j t.+1 = true
  ============================
  t1 <= t.+1

subgoal 2 (ID 699) is:
 t.+1 < t2
subgoal 3 (ID 615) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

      + apply leq_trans with t; by done.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 699)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SERV : 0 < service_during sched j t.+1 t2
  SCHED : scheduled_at sched j t.+1 = true
  ============================
  t.+1 < t2

subgoal 2 (ID 615) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

      + rewrite ltnNge; apply/negP; intros CONTR.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 747)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SERV : 0 < service_during sched j t.+1 t2
  SCHED : scheduled_at sched j t.+1 = true
  CONTR : t2 <= t.+1
  ============================
  False

subgoal 2 (ID 615) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

          by move: SERV; rewrite /service_during big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 615)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SERV : 0 < service_during sched j t.+1 t2
  SCHED : scheduled_at sched j t.+1 = false
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

    - apply negbT in SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 797)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SERV : 0 < service_during sched j t.+1 t2
  SCHED : ~~ scheduled_at sched j t.+1
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = k.+1

----------------------------------------------------------------------------- *)

       move: SERV; rewrite /service /service_during; move ⇒ /sum_seq_gt0P [x [INx SCHEDx]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 893)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  INx : x \in index_iota t.+1 t2
  SCHEDx : 0 < service_at sched j x
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = k.+1

----------------------------------------------------------------------------- *)

       rewrite lt0b in SCHEDx.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 923)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  INx : x \in index_iota t.+1 t2
  SCHEDx : sched x == Some j
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = k.+1

----------------------------------------------------------------------------- *)

       rewrite mem_iota subnKC in INx; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 961)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx : t < x < t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = k.+1

----------------------------------------------------------------------------- *)

       move: INx ⇒ /andP [INx1 INx2].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1049)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = k.+1

----------------------------------------------------------------------------- *)

       move: (exists_first_intermediate_point _ _ _ INx1 SCHED) ⇒ A.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1057)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  A : scheduled_at sched j x ->
      exists t0 : nat,
        t.+1 < t0 <= x /\
        (forall x : nat, t < x < t0 -> ~~ scheduled_at sched j x) /\
        scheduled_at sched j t0
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = k.+1

----------------------------------------------------------------------------- *)

       feed A; first by rewrite scheduled_at_def/=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1063)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  A : exists t0 : nat,
        t.+1 < t0 <= x /\
        (forall x : nat, t < x < t0 -> ~~ scheduled_at sched j x) /\
        scheduled_at sched j t0
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = k.+1

----------------------------------------------------------------------------- *)

       move: A ⇒ [y [/andP [T1 T4] [T2 T3]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1167)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = k.+1

----------------------------------------------------------------------------- *)

       ∃ y; repeat split; try done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1171)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  t1 <= y < t2

subgoal 2 (ID 1176) is:
 \sum_(t1 <= t0 < y) service_at sched j t0 = k.+1

----------------------------------------------------------------------------- *)

       + apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 1272)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  t1 <= y

subgoal 2 (ID 1273) is:
 y < t2
subgoal 3 (ID 1176) is:
 \sum_(t1 <= t0 < y) service_at sched j t0 = k.+1

----------------------------------------------------------------------------- *)

         apply leq_trans with t; first by done.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 1275)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  t <= y

subgoal 2 (ID 1273) is:
 y < t2
subgoal 3 (ID 1176) is:
 \sum_(t1 <= t0 < y) service_at sched j t0 = k.+1

----------------------------------------------------------------------------- *)

         apply ltnW, ltn_trans with t.+1; by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1273)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  y < t2

subgoal 2 (ID 1176) is:
 \sum_(t1 <= t0 < y) service_at sched j t0 = k.+1

----------------------------------------------------------------------------- *)

           by apply leq_ltn_trans with x.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1176)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  \sum_(t1 <= t0 < y) service_at sched j t0 = k.+1

----------------------------------------------------------------------------- *)

       + rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1303)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 t.+1 = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  \sum_(t1 <= i < t.+1) (sched i == Some j) +
  \sum_(t.+1 <= i < y) (sched i == Some j) = k.+1

----------------------------------------------------------------------------- *)

         unfold service_during in SERVk1; rewrite SERVk1; apply/eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 1461)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : \sum_(t1 <= t < t.+1) service_at sched j t = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  k.+1 + \sum_(t.+1 <= i < y) (sched i == Some j) == k.+1

----------------------------------------------------------------------------- *)

         rewrite -{2}[k.+1]addn0 eqn_add2l.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1471)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : \sum_(t1 <= t < t.+1) service_at sched j t = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  \sum_(t.+1 <= i < y) (sched i == Some j) == 0

----------------------------------------------------------------------------- *)

         rewrite big_nat_cond big1 //; move ⇒ z /andP [H5 _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1582)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 <= t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : \sum_(t1 <= t < t.+1) service_at sched j t = k.+1
  SCHED : ~~ scheduled_at sched j t.+1
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : t.+1 < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  z : nat
  H5 : t < z < y
  ============================
  (sched z == Some j) = 0

----------------------------------------------------------------------------- *)

           by apply/eqP; rewrite eqb0; specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End IncrementalService.