Library rt.restructuring.analysis.arrival.rbf


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

Welcome to Coq 8.10.1 (October 2019)

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

From rt.util Require Import all.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.aggregate Require Import task_arrivals.
From rt.restructuring.model.arrival Require Import arrival_curves.
From rt.restructuring.analysis Require Import arrival.workload_bound.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Request Bound Functions (RBF)

In this section, we prove some properties of Request Bound Functions (RBF).
Section RequestBoundFunctions.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent:
    consistent_arrival_times arr_seq.

Let tsk be any task.
  Variable tsk : Task.

Let max_arrivals be a family of valid arrival curves, i.e., for any task tsk in ts [max_arrival tsk] is (1) an arrival bound of tsk, and (2) it is a monotonic function that equals 0 for the empty interval delta = 0.
  Context `{MaxArrivals Task}.
  Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
  Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).

Let's define some local names for clarity.
  Let task_rbf := task_request_bound_function tsk.

We prove that [task_rbf 0] is equal to 0.
  Lemma task_rbf_0_zero:
    task_rbf 0 = 0.

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

1 subgoal (ID 183)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  ============================
  task_rbf 0 = 0

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

  Proof.
    rewrite /task_rbf /task_request_bound_function.

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

1 subgoal (ID 191)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  ============================
  task_cost tsk * max_arrivals tsk 0 = 0

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

    apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.

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

1 focused subgoal
(shelved: 1) (ID 304)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  ============================
  max_arrivals tsk 0 = 0

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

      by move: H_valid_arrival_curve ⇒ [T1 T2].

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

No more subgoals.

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

  Qed.

We prove that task_rbf is monotone.
  Lemma task_rbf_monotone:
    monotone task_rbf leq.

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

1 subgoal (ID 185)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  ============================
  monotone task_rbf leq

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

  Proof.
    rewrite /monotone; intros ? ? LE.

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

1 subgoal (ID 191)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  x, y : duration
  LE : x <= y
  ============================
  task_rbf x <= task_rbf y

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

    rewrite /task_rbf /task_request_bound_function leq_mul2l.

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

1 subgoal (ID 204)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  x, y : duration
  LE : x <= y
  ============================
  (task_cost tsk == 0) || (max_arrivals tsk x <= max_arrivals tsk y)

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

    apply/orP; right.

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

1 subgoal (ID 230)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  x, y : duration
  LE : x <= y
  ============================
  max_arrivals tsk x <= max_arrivals tsk y

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

      by move: H_valid_arrival_curve ⇒ [_ T]; apply T.

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

No more subgoals.

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

  Qed.

Consider any job j of tsk. This guarantees that there exists at least one job of task tsk.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_of_tsk : job_task j = tsk.

Then we prove that task_rbf 1 is greater than or equal to task cost.
  Lemma task_rbf_1_ge_task_cost:
    task_rbf 1 ≥ task_cost tsk.

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

1 subgoal (ID 194)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  ============================
  task_cost tsk <= task_rbf 1

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

  Proof.
    have ALT: ∀ n, n = 0 ∨ n > 0.

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

2 subgoals (ID 199)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  ============================
  forall n : nat, n = 0 \/ 0 < n

subgoal 2 (ID 201) is:
 task_cost tsk <= task_rbf 1

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

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

1 subgoal (ID 199)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  ============================
  forall n : nat, n = 0 \/ 0 < n

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

by clear; intros n; destruct n; [left | right].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 201)

subgoal 1 (ID 201) is:
 task_cost tsk <= task_rbf 1

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

}

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

1 subgoal (ID 201)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  ALT : forall n : nat, n = 0 \/ 0 < n
  ============================
  task_cost tsk <= task_rbf 1

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

    specialize (ALT (task_cost tsk)); destruct ALT as [Z | POS]; first by rewrite Z.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 224)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  ============================
  task_cost tsk <= task_rbf 1

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

    rewrite leqNgt; apply/negP; intros CONTR.

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

1 subgoal (ID 252)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ============================
  False

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

    move: H_is_arrival_curve ⇒ ARRB.

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

1 subgoal (ID 254)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ARRB : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  ============================
  False

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

    specialize (ARRB (job_arrival j) (job_arrival j + 1)).

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

1 subgoal (ID 260)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ARRB : job_arrival j <= job_arrival j + 1 ->
         number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <=
         max_arrivals tsk (job_arrival j + 1 - job_arrival j)
  ============================
  False

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

    feed ARRB; first by rewrite leq_addr.

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

1 subgoal (ID 266)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <=
         max_arrivals tsk (job_arrival j + 1 - job_arrival j)
  ============================
  False

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

    rewrite addKn in ARRB.

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

1 subgoal (ID 302)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : task_rbf 1 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <= max_arrivals tsk 1
  ============================
  False

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

    move: CONTR; rewrite /task_rbf /task_request_bound_function; move ⇒ CONTR.

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

1 subgoal (ID 313)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <= max_arrivals tsk 1
  CONTR : task_cost tsk * max_arrivals tsk 1 < task_cost tsk
  ============================
  False

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

    move: CONTR; rewrite -{2}[task_cost tsk]muln1 ltn_mul2l; move ⇒ /andP [_ CONTR].

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

1 subgoal (ID 367)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <= max_arrivals tsk 1
  CONTR : max_arrivals tsk 1 < 1
  ============================
  False

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

    move: CONTR; rewrite -addn1 -{3}[1]add0n leq_add2r leqn0; move ⇒ /eqP CONTR.

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

1 subgoal (ID 419)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  ARRB : number_of_task_arrivals arr_seq tsk (job_arrival j)
           (job_arrival j + 1) <= max_arrivals tsk 1
  CONTR : max_arrivals tsk 1 = 0
  ============================
  False

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

    move: ARRB; rewrite CONTR leqn0 eqn0Ngt; move ⇒ /negP T; apply: T.

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

1 subgoal (ID 461)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  0 < number_of_task_arrivals arr_seq tsk (job_arrival j) (job_arrival j + 1)

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

    rewrite /number_of_task_arrivals -has_predT.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 472)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  has (pred_of_simpl (T:=Job) predT)
    (task_arrivals_between arr_seq tsk (job_arrival j) (job_arrival j + 1))

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

    rewrite /task_arrivals_between.

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

1 subgoal (ID 479)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  has (pred_of_simpl (T:=Job) predT)
    [seq j0 <- arrivals_between arr_seq (job_arrival j) (job_arrival j + 1)
       | job_task j0 == tsk]

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

    apply/hasP; ∃ j; last by done.

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

1 subgoal (ID 509)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  j
    \in [seq j0 <- arrivals_between arr_seq (job_arrival j)
                     (job_arrival j + 1)
           | job_task j0 == tsk]

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

    rewrite /arrivals_between addn1 big_nat_recl; last by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 525)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  j
    \in [seq j0 <- arrivals_at arr_seq (job_arrival j) ++
                   \big[cat/[::]]_(job_arrival j <= i < 
                   job_arrival j) arrivals_at arr_seq (succn i)
           | job_task j0 == tsk]

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

    rewrite big_geq ?cats0; last by done.

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

1 subgoal (ID 541)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  j \in [seq j0 <- arrivals_at arr_seq (job_arrival j) | job_task j0 == tsk]

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

    rewrite mem_filter.

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

1 subgoal (ID 551)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  (job_task j == tsk) && (j \in arrivals_at arr_seq (job_arrival j))

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

    apply/andP; split.

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

2 subgoals (ID 577)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  job_task j == tsk

subgoal 2 (ID 578) is:
 j \in arrivals_at arr_seq (job_arrival j)

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

    - by apply/eqP.

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

1 subgoal (ID 578)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

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

    - move: H_j_arrives ⇒ [t ARR].

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

1 subgoal (ID 618)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  t : instant
  ARR : j \in arrivals_at arr_seq t
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

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

      move: (ARR) ⇒ CONS.

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

1 subgoal (ID 620)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  t : instant
  ARR, CONS : j \in arrivals_at arr_seq t
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

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

      apply H_arrival_times_are_consistent in CONS.

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

1 subgoal (ID 621)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  tsk : Task
  H2 : MaxArrivals Task
  H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk)
  H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk)
  task_rbf := task_request_bound_function tsk : duration -> nat
  j : Job
  H_j_arrives : arrives_in arr_seq j
  H_job_of_tsk : job_task j = tsk
  POS : 0 < task_cost tsk
  CONTR : max_arrivals tsk 1 = 0
  t : instant
  ARR : j \in arrivals_at arr_seq t
  CONS : job_arrival j = t
  ============================
  j \in arrivals_at arr_seq (job_arrival j)

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

        by rewrite CONS.

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

No more subgoals.

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

  Qed.

End RequestBoundFunctions.