Require Export prosa.implementation.refinements.refinements.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-paramcoq.plugin is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file paramcoq.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.implementation.refinements.task.
Notations "[ eta _ ]" defined at level 0
and "[ TASK id: _ cost: _ deadline: _ arrival: _ priority: _ ]"
defined at level 6 have incompatible prefixes.
One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
Notations "[ eta _ ]" defined at level 0
and "[ PERIODIC-TASK id: _ cost: _ deadline: _ period: _ priority: _ ]"
defined at level 6 have incompatible prefixes.
One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
Notations "[ eta _ ]" defined at level 0
and "[ SPORADIC-TASK id: _ cost: _ deadline: _ separation: _ priority: _ ]"
defined at level 6 have incompatible prefixes.
One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
Notations "[ eta _ ]" defined at level 0
and "[ CURVE horizon: _ steps: _ ]" defined at level 6
have incompatible prefixes.
One of them will likely not work.
[notation-incompatible-prefix,parsing,default]
Require Export prosa.implementation.refinements.EDF.fast_search_space.
Require Export prosa.implementation.refinements.arrival_bound.

(** We begin by defining a generic version of the functions we seek to define. *)
Section Definitions.

  (** Consider a generic type T supporting basic arithmetic operations,
        neutral elements, and comparisons. *)
  Context {T : Type}.
  Context `{!zero_of T, !one_of T, !sub_of T, !add_of T, !mul_of T,
            !div_of T, !mod_of T, !eq_of T, !leq_of T, !lt_of T}.
  Context `{!eq_of (seq T)}.
  Context {eq_of2 : eq_of (@task_T T)}.

  (** We define a generic version of total request-bound function of
      higher-or-equal priority task, ... *)
  Definition total_rbf_T (ts : seq task_T) (Δ : T) : T :=
    let work_ts := map (fun tsk' => task_rbf_T tsk' Δ) ts in
    foldr +%C 0%C work_ts.

  (** ... of bound on total higher-or-equal priority workload, ...  *)
  Definition bound_on_total_hep_workload_T (ts : seq task_T) (tsk : task_T) (A Δ : T) : T :=
    let o_ts := filter (fun tsk_o => ~~ (eq_of2 tsk_o tsk)) ts in
    let o_work := map (fun tsk_o => task_rbf_T tsk_o (minn_T ((A + 1) + task_deadline_T tsk - task_deadline_T tsk_o) Δ))%C o_ts in
    foldr +%C 0%C o_work.

  (** Next, we define a generic version of [check_point_FP], ... *)
  Definition check_point_FP_T (ts : seq task_T) (tsk : task_T) (R : T) (P : T * T) : bool :=
    (task_rbf_T tsk (P.1 + 1) + bound_on_total_hep_workload_T ts tsk P.1 (P.1 + P.2) <= P.1 + P.2)%C
    && (P.2 <= R)%C.

  (** ... a generic version of [blocking_bound_NP], ... *)
  Definition blocking_bound_NP_T (ts : seq task_T) (tsk : task_T) A :=
    let blocking_relevant tsk_o := (0 < ConcreteMaxArrivals_T tsk_o 1)%C  && (0 < task_cost_T tsk_o)%C in
    let ts_lp := filter (fun tsk_o => (blocking_relevant tsk_o)
                                    && (@task_deadline_T T tsk + A < @task_deadline_T T tsk_o))%C ts in
    let ts_block := map (fun tsk_o => task_cost_T tsk_o - 1)%C ts_lp in
    foldr maxn_T 0%C ts_block.

  (** ... of [check_point_NP], ... *)
  Definition check_point_NP_T (ts : seq task_T) (tsk : task_T) (R : T) (P : T * T) : bool :=
    (blocking_bound_NP_T ts tsk P.1
     + (task_rbf_T tsk (P.1 + 1) - (task_cost_T tsk - 1))
     + bound_on_total_hep_workload_T ts tsk P.1 (P.1 + P.2) <= P.1 + P.2)%C
    && (P.2 + (task_cost_T tsk - 1) <= R)%C.

  (** ... of [valid_arrivals]. *)
  Definition valid_arrivals_T (tsk : task_T) : bool :=
    match @task_arrival_T T tsk with
    | Periodic_T p => (1 <= p)%C
    | Sporadic_T m => (1 <= m)%C
    | ArrivalPrefix_T emax_vec => valid_extrapolated_arrival_curve_T emax_vec
    end.

End Definitions.

(** In this section, we introduce some functions operating on binary numbers. *)
Section DefinitionsN.

  (** We provide a definition of [iota], ... *)
  Definition iota_N (a Δ : N) := iota_T a Δ.

  (** ... of [task_search_space_emax_EDF_h], ... *)
  Definition task_search_space_emax_EDF_h_N (tsk tsko : task_T) (l r : N) : seq N :=
    let h := get_horizon_of_task_T tsko in
    let offsets := map (N.mul h) (iota_N l r) in
    let emax_offsets := repeat_steps_with_offset_T tsko offsets in
    let emax_edf_offsets :=
        shift_points_neg_T
          (shift_points_pos_T emax_offsets (task_deadline_T tsko))
          (task_deadline_T tsk) in
    map predn_T emax_edf_offsets.

  (** ... of [task_search_space_emax_EDF], ... *)
  Definition task_search_space_emax_EDF_N (tsk tsko : task_T)  (L : N) :=
    let h := get_horizon_of_task_T tsko in
    task_search_space_emax_EDF_h_N
      tsk tsko 0
      (((L + (task_deadline_T tsk - task_deadline_T tsko)) %/ h) + 1)%C.

  (** ... and of [search_space_emax_EDF_N]. *)
  Definition search_space_emax_EDF_N (ts : seq task_T) (tsk : task_T) (L : N) :=
    let points := map (fun tsko => task_search_space_emax_EDF_N tsk tsko L) ts in
    flatten points.

End DefinitionsN.


(** ** Refinements *)

(** We now establish the desired refinements. *)

(** First, we prove a refinement for the [task_search_space_emax_EDF_h] function. *)
Local Instance refine_task_search_space_emax_EDF_h :
  refines (Rtask ==> Rtask ==> Rnat ==> Rnat ==> list_R Rnat)%rel
          task_search_space_emax_EDF_h
          task_search_space_emax_EDF_h_N.
refines
  (Rtask ==> Rtask ==> Rnat ==> Rnat ==> list_R Rnat)
  task_search_space_emax_EDF_h
  task_search_space_emax_EDF_h_N
Proof.
refines
  (Rtask ==> Rtask ==> Rnat ==> Rnat ==> list_R Rnat)
  task_search_space_emax_EDF_h
  task_search_space_emax_EDF_h_N
  rewrite refinesE => tsk tsk' Rtsk tsko tsko' Rtsko l l' Rl r r' Rr.
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
tsko: task.Task
tsko': task_T
Rtsko: Rtask tsko tsko'
l: nat
l': N
Rl: Rnat l l'
r: nat
r': N
Rr: Rnat r r'
list_R Rnat
  (task_search_space_emax_EDF_h tsk tsko l r)
  (task_search_space_emax_EDF_h_N tsk' tsko' l' r')
  apply refinesP; unfold task_search_space_emax_EDF_h, task_search_space_emax_EDF_h_N.
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
tsko: task.Task
tsko': task_T
Rtsko: Rtask tsko tsko'
l: nat
l': N
Rl: Rnat l l'
r: nat
r': N
Rr: Rnat r r'
refines (list_R Rnat)
  [seq i.-1
     | i <- shift_points_neg
              (shift_points_pos
                 (repeat_steps_with_offset tsko
                    [seq 
                     get_horizon_of_task tsko * i
                       | i <- 
                     iota l r]) 
                 (task_deadline tsko))
              (task_deadline tsk)]
  [seq predn_T i
     | i <- shift_points_neg_T
              (shift_points_pos_T
                 (repeat_steps_with_offset_T tsko'
                    [seq 
                     (get_horizon_of_task_T tsko' * i)%num
                       | i <- 
                     iota_N l' r'])
                 (task_deadline_T tsko'))
              (task_deadline_T tsk')]
  by refines_apply; refines_abstr.
Qed.

(** Next, we prove a refinement for the [task_search_space_emax_EDF] function. *)
Global Instance refine_task_search_space_emax_EDF :
  forall tsk tsko,
    refines (Rnat ==> list_R Rnat)%rel
            (task_search_space_emax_EDF (taskT_to_task tsk) (taskT_to_task tsko))
            (task_search_space_emax_EDF_N tsk tsko).
forall tsk tsko : task_T,
refines (Rnat ==> list_R Rnat)
  (task_search_space_emax_EDF (taskT_to_task tsk)
     (taskT_to_task tsko))
  (task_search_space_emax_EDF_N tsk tsko)
Proof.
forall tsk tsko : task_T,
refines (Rnat ==> list_R Rnat)
  (task_search_space_emax_EDF (taskT_to_task tsk)
     (taskT_to_task tsko))
  (task_search_space_emax_EDF_N tsk tsko)
  intros.
tsk, tsko: task_T
refines (Rnat ==> list_R Rnat)
  (task_search_space_emax_EDF (taskT_to_task tsk)
     (taskT_to_task tsko))
  (task_search_space_emax_EDF_N tsk tsko)
  rewrite refinesE => δ δ' Rδ.
tsk, tsko: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
list_R Rnat
  (task_search_space_emax_EDF 
     (taskT_to_task tsk) 
     (taskT_to_task tsko) δ)
  (task_search_space_emax_EDF_N tsk tsko δ')
  unfold task_search_space_emax_EDF, task_search_space_emax_EDF_N.
tsk, tsko: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
list_R Rnat
  (task_search_space_emax_EDF_h 
     (taskT_to_task tsk) 
     (taskT_to_task tsko) 0
     ((δ +
       (task_deadline (taskT_to_task tsk) -
        task_deadline (taskT_to_task tsko)))
      %/ get_horizon_of_task (taskT_to_task tsko)).+1)
  (task_search_space_emax_EDF_h_N tsk tsko 0
     ((δ' +
       (task_deadline_T tsk - task_deadline_T tsko))
      %/ get_horizon_of_task_T tsko + 1)%C)
  apply refinesP; rewrite -addn1.
tsk, tsko: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
refines (list_R Rnat)
  (task_search_space_emax_EDF_h 
     (taskT_to_task tsk) 
     (taskT_to_task tsko) 0
     ((δ +
       (task_deadline (taskT_to_task tsk) -
        task_deadline (taskT_to_task tsko)))
      %/ get_horizon_of_task (taskT_to_task tsko) + 1))
  (task_search_space_emax_EDF_h_N tsk tsko 0
     ((δ' +
       (task_deadline_T tsk - task_deadline_T tsko))
      %/ get_horizon_of_task_T tsko + 1)%C)
  refines_apply.
tsk, tsko: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
refines Rtask (taskT_to_task tsk) tsk
tsk, tsko: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
refines Rtask (taskT_to_task tsko) tsko
tsk, tsko: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
refines Rtask (taskT_to_task tsk) tsk
tsk, tsko: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
refines Rtask (taskT_to_task tsko) tsko
tsk, tsko: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
refines Rtask (taskT_to_task tsko) tsko
  all: by rewrite refinesE; unfold Rtask, fun_hrel.
Qed.

(** Next, we prove a refinement for the [search_space_emax_EDF] function. *)
Global Instance refine_search_space_emax_EDF :
  forall ts tsk,
    refines (Rnat ==> list_R Rnat)%rel
            (search_space_emax_EDF (map taskT_to_task ts) (taskT_to_task tsk))
            (search_space_emax_EDF_N ts tsk).
forall (ts : seq task_T) (tsk : task_T),
refines (Rnat ==> list_R Rnat)
  (search_space_emax_EDF
     [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk))
  (search_space_emax_EDF_N ts tsk)
Proof.
forall (ts : seq task_T) (tsk : task_T),
refines (Rnat ==> list_R Rnat)
  (search_space_emax_EDF
     [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk))
  (search_space_emax_EDF_N ts tsk)
  move=> ts tsk.
ts: seq task_T
tsk: task_T
refines (Rnat ==> list_R Rnat)
  (search_space_emax_EDF
     [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk))
  (search_space_emax_EDF_N ts tsk)
  unfold search_space_emax_EDF, search_space_emax_EDF_N.
ts: seq task_T
tsk: task_T
refines (Rnat ==> list_R Rnat)
  (fun L : nat =>
   \cat_(tsko<-[seq taskT_to_task i | i <- ts])
    task_search_space_emax_EDF (taskT_to_task tsk)
      tsko L)
  (fun L : N =>
   flatten
     [seq task_search_space_emax_EDF_N tsk tsko L
        | tsko <- ts])
  rewrite refinesE => L L' RL; apply refinesP.
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines (list_R Rnat)
  (\cat_(tsko<-[seq taskT_to_task i | i <- ts])
    task_search_space_emax_EDF (taskT_to_task tsk)
      tsko L)
  (flatten
     [seq task_search_space_emax_EDF_N tsk tsko L'
        | tsko <- ts])
  have F: forall xs f, \cat_(x <- xs) f x = flatten (map f xs).
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
forall (T T0 : Type) (xs : seq T) (f : T -> seq T0),
\cat_(x<-xs)f x = flatten [seq f i | i <- xs]
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
F: forall (T T0 : Type) (xs : seq T)
  (f : T -> seq T0),
\cat_(x<-xs)f x = flatten [seq f i | i <- xs]
refines (list_R Rnat)
  (\cat_(tsko<-[seq taskT_to_task i | i <- ts])
    task_search_space_emax_EDF (taskT_to_task tsk)
      tsko L)
  (flatten
     [seq task_search_space_emax_EDF_N tsk tsko L'
        | tsko <- ts])
  {
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
forall (T T0 : Type) (xs : seq T) (f : T -> seq T0),
\cat_(x<-xs)f x = flatten [seq f i | i <- xs] clear=> T T0; elim=> [|x xs IHxs] f.
T, T0: Type
f: T -> seq T0
\cat_(x<-[::])f x = flatten [seq f i | i <- [::]]
T, T0: Type
x: T
xs: seq T
IHxs: forall f : T -> seq T0,
\cat_(x<-xs)f x = flatten [seq f i | i <- xs]
f: T -> seq T0
\cat_(x<-(x :: xs))f x =
flatten [seq f i | i <- x :: xs]
    -
T, T0: Type
f: T -> seq T0
\cat_(x<-[::])f x = flatten [seq f i | i <- [::]] by rewrite big_nil.
    -
T, T0: Type
x: T
xs: seq T
IHxs: forall f : T -> seq T0,
\cat_(x<-xs)f x = flatten [seq f i | i <- xs]
f: T -> seq T0
\cat_(x<-(x :: xs))f x =
flatten [seq f i | i <- x :: xs] by rewrite big_cons //= IHxs. }
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
F: forall (T T0 : Type) (xs : seq T)
  (f : T -> seq T0),
\cat_(x<-xs)f x = flatten [seq f i | i <- xs]
refines (list_R Rnat)
  (\cat_(tsko<-[seq taskT_to_task i | i <- ts])
    task_search_space_emax_EDF 
      (taskT_to_task tsk) tsko L)
  (flatten
     [seq task_search_space_emax_EDF_N tsk tsko L'
        | tsko <- ts])
  rewrite F; clear F.
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines (list_R Rnat)
  (flatten
     [seq task_search_space_emax_EDF
            (taskT_to_task tsk) x L
        | x <- [seq taskT_to_task i | i <- ts]])
  (flatten
     [seq task_search_space_emax_EDF_N tsk tsko L'
        | tsko <- ts])
  refines_apply.
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines (?R0 ==> ?R ==> list_R (list_R Rnat)) map map
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines ?R0
  ((task_search_space_emax_EDF (taskT_to_task tsk))^~ L)
  ((task_search_space_emax_EDF_N tsk)^~ L')
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines ?R [seq taskT_to_task i | i <- ts] ts
  Unshelve.
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines (?R0 ==> ?R ==> list_R (list_R Rnat)) map map
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines ?R0
  ((task_search_space_emax_EDF (taskT_to_task tsk))^~ L)
  ((task_search_space_emax_EDF_N tsk)^~ L')
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines ?R [seq taskT_to_task i | i <- ts] ts
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
seq Task -> seq task_T -> Type
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
(Task -> seq nat) -> (task_T -> seq N) -> Type
  5: exact (Rtask ==> list_R Rnat)%rel.
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines
  ((Rtask ==> list_R Rnat) ==>
   ?R ==> list_R (list_R Rnat)) map map
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines (Rtask ==> list_R Rnat)
  ((task_search_space_emax_EDF (taskT_to_task tsk))^~ L)
  ((task_search_space_emax_EDF_N tsk)^~ L')
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines ?R [seq taskT_to_task i | i <- ts] ts
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
seq Task -> seq task_T -> Type
  4: exact (list_R Rtask).
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines
  ((Rtask ==> list_R Rnat) ==>
   list_R Rtask ==> list_R (list_R Rnat)) map map
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines (Rtask ==> list_R Rnat)
  ((task_search_space_emax_EDF (taskT_to_task tsk))^~ L)
  ((task_search_space_emax_EDF_N tsk)^~ L')
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines (list_R Rtask) [seq taskT_to_task i | i <- ts]
  ts
  -
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines
  ((Rtask ==> list_R Rnat) ==>
   list_R Rtask ==> list_R (list_R Rnat)) map map rewrite refinesE => f f' Rf xs xs' Rxs; apply refinesP.
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
f: Task -> seq nat
f': task_T -> seq N
Rf: (Rtask ==> list_R Rnat)%rel f f'
xs: seq Task
xs': seq task_T
Rxs: list_R Rtask xs xs'
refines (list_R (list_R Rnat)) [
  seq f i | i <- xs] [seq f' i | i <- xs']
    by eapply refine_map; [rewrite refinesE; exact Rxs | rewrite refinesE ].
  -
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines (Rtask ==> list_R Rnat)
  ((task_search_space_emax_EDF (taskT_to_task tsk))^~ L)
  ((task_search_space_emax_EDF_N tsk)^~ L') move: refine_task_search_space_emax_EDF=> R; rewrite refinesE in R.
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
R: forall tsk tsko : task_T,
(Rnat ==> list_R Rnat)%rel
  (task_search_space_emax_EDF 
     (taskT_to_task tsk) 
     (taskT_to_task tsko))
  (task_search_space_emax_EDF_N tsk tsko)
refines (Rtask ==> list_R Rnat)
  ((task_search_space_emax_EDF (taskT_to_task tsk))^~ L)
  ((task_search_space_emax_EDF_N tsk)^~ L')
    by rewrite refinesE => tsko tsko' Rtsko; rewrite -Rtsko; apply R.
  -
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
refines (list_R Rtask) [seq taskT_to_task i | i <- ts]
  ts move: refine_task_set' => RTS.
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
RTS: refines (unify (A:=seq task_T) ==> list_R Rtask)
  (map taskT_to_task) id
refines (list_R Rtask) [seq taskT_to_task i | i <- ts]
  ts
    rewrite refinesE; rewrite refinesE in RTS.
ts: seq task_T
tsk: task_T
L: nat
L': N
RL: Rnat L L'
RTS: (unify (A:=seq task_T) ==> list_R Rtask)%rel
  (map taskT_to_task) id
list_R Rtask [seq taskT_to_task i | i <- ts] ts
    by apply RTS; apply unifyxx.
Qed.

(** Next, we prove a refinement for the [total_request_bound_function] function. *)
Local Instance refine_total_rbf :
  refines (list_R Rtask ==> Rnat ==> Rnat)%rel total_request_bound_function total_rbf_T.
refines (list_R Rtask ==> Rnat ==> Rnat)
  total_request_bound_function total_rbf_T
Proof.
refines (list_R Rtask ==> Rnat ==> Rnat)
  total_request_bound_function total_rbf_T
  apply refines_abstr2;
    rewrite /total_request_bound_function /total_rbf_T /total_request_bound_function
            /concept.task_cost /TaskCost /max_arrivals /MaxArrivals => t t' Rt y y' Ry.
t: seq task.Task
t': seq task_T
Rt: refines (list_R Rtask) t t'
y: nat
y': N
Ry: refines Rnat y y'
refines Rnat
  (\sum_(tsk <- t) task_request_bound_function tsk y)
  (foldr +%C 0%C [seq task_rbf_T tsk' y' | tsk' <- t'])
  eapply refine_uncond_foldr; first exact Rt.
t: seq task.Task
t': seq task_T
Rt: refines (list_R Rtask) t t'
y: nat
y': N
Ry: refines Rnat y y'
refines (Rtask ==> Rnat)
  (task_request_bound_function^~ y) (task_rbf_T^~ y')
  by rewrite refinesE => tsko tsko' Rtsko; apply refinesP; refines_apply.
Qed.

(** Next, we prove a special-case refinement for the [total_request_bound_function] function
    when applied to a refined task set and a refined task. This special case
    is required to guide the typeclass engine. *)
Global Instance refine_total_rbf' :
  forall ts,
    refines (Rnat ==> Rnat)%rel
            (total_request_bound_function (map taskT_to_task ts))
            (total_rbf_T ts) | 0.
forall ts : seq task_T,
refines (Rnat ==> Rnat)
  (total_request_bound_function
     [seq taskT_to_task i | i <- ts]) (total_rbf_T ts)
Proof.
forall ts : seq task_T,
refines (Rnat ==> Rnat)
  (total_request_bound_function
     [seq taskT_to_task i | i <- ts]) (total_rbf_T ts)
  move=> ts; rewrite refinesE => δ δ' Rδ.
ts: seq task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
Rnat
  (total_request_bound_function
     [seq taskT_to_task i | i <- ts] δ)
  (total_rbf_T ts δ')
  move: refine_task_set' => RTS.
ts: seq task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: refines (unify (A:=seq task_T) ==> list_R Rtask) (map taskT_to_task) id
Rnat
  (total_request_bound_function
     [seq taskT_to_task i | i <- ts] δ)
  (total_rbf_T ts δ')
  rewrite refinesE in RTS.
ts: seq task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: (unify (A:=seq task_T) ==> list_R Rtask)%rel (map taskT_to_task) id
Rnat
  (total_request_bound_function
     [seq taskT_to_task i | i <- ts] δ)
  (total_rbf_T ts δ')
  specialize (RTS ts ts (unifyxx _)); simpl in RTS.
ts: seq task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
Rnat
  (total_request_bound_function
     [seq taskT_to_task i | i <- ts] δ)
  (total_rbf_T ts δ')
  apply refinesP.
ts: seq task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
refines Rnat
  (total_request_bound_function
     [seq taskT_to_task i | i <- ts] δ)
  (total_rbf_T ts δ')
  move: (refine_total_rbf) => EQ.
ts: seq task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
EQ: refines (list_R Rtask ==> Rnat ==> Rnat)
  total_request_bound_function total_rbf_T
refines Rnat
  (total_request_bound_function
     [seq taskT_to_task i | i <- ts] δ)
  (total_rbf_T ts δ')
  rewrite refinesE in EQ.
ts: seq task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
EQ: (list_R Rtask ==> Rnat ==> Rnat)%rel
  total_request_bound_function total_rbf_T
refines Rnat
  (total_request_bound_function
     [seq taskT_to_task i | i <- ts] δ)
  (total_rbf_T ts δ')
  erewrite <-EQ; [ | eassumption | eassumption].
ts: seq task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
EQ: (list_R Rtask ==> Rnat ==> Rnat)%rel
  total_request_bound_function total_rbf_T
refines Rnat (total_rbf_T ts δ') (total_rbf_T ts δ')
  set (x := total_rbf_T _ _).
ts: seq task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
EQ: (list_R Rtask ==> Rnat ==> Rnat)%rel
  total_request_bound_function total_rbf_T
x:= total_rbf_T ts δ': N
refines Rnat x x
  by rewrite refinesE.
Qed.

(** Next, we provide equality comparisons between different pairs of objects
    manipulated in Poet's certificates. *)
Global Instance eq_listN : eq_of (seq N) := fun x y => x == y.
Global Instance eq_NlistNN : eq_of (prod N (seq (prod N N))) := fun x y => x == y.
Global Instance eq_taskab : eq_of (@task_arrivals_bound_T N) := taskab_eqdef_T.
Global Instance eq_task : eq_of (@task_T N) := task_eqdef_T.

(** Next, we prove a refinement for the [task_eqdef] function. *)
Local Instance refine_task_eqdef :
  refines (Rtask ==> Rtask ==> bool_R)%rel task_eqdef task_eqdef_T.
refines (Rtask ==> Rtask ==> bool_R) task_eqdef
  task_eqdef_T
Proof.
refines (Rtask ==> Rtask ==> bool_R) task_eqdef
  task_eqdef_T
  apply refines_abstr2.
forall (a : task.Task) (b : task_T),
refines Rtask a b ->
forall (a' : task.Task) (b' : task_T),
refines Rtask a' b' ->
refines bool_R (task_eqdef a a') (task_eqdef_T b b')
  intros a a' Ra b b' Rb.
a: task.Task
a': task_T
Ra: refines Rtask a a'
b: task.Task
b': task_T
Rb: refines Rtask b b'
refines bool_R (task_eqdef a b) (task_eqdef_T a' b')
  unfold task_eqdef, task_eqdef_T.
a: task.Task
a': task_T
Ra: refines Rtask a a'
b: task.Task
b': task_T
Rb: refines Rtask b b'
refines bool_R
  ((task_id a == task_id b) &&
   (task_cost a == task_cost b) &&
   (task_arrival a == task_arrival b) &&
   (task_deadline a == task_deadline b) &&
   (task_priority a == task_priority b))
  ((task_id_T a' == task_id_T b')%C &&
   (task_cost_T a' == task_cost_T b')%C &&
   (task_arrival_T a' == task_arrival_T b')%C &&
   (task_deadline_T a' == task_deadline_T b')%C &&
   (task_priority_T a' == task_priority_T b')%C)
  by rewrite refinesE; repeat apply andb_R; apply refinesP; refines_apply.
Qed.

(** Next, we prove a refinement for the [bound_on_total_hep_workload] function. *)
Global Instance refine_bound_on_total_hep_workload :
  refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat ==> Rnat)%rel
          bound_on_total_hep_workload bound_on_total_hep_workload_T.
refines
  (list_R Rtask ==> Rtask ==> Rnat ==> Rnat ==> Rnat)
  bound_on_total_hep_workload
  bound_on_total_hep_workload_T
Proof.
refines
  (list_R Rtask ==> Rtask ==> Rnat ==> Rnat ==> Rnat)
  bound_on_total_hep_workload
  bound_on_total_hep_workload_T
  rewrite refinesE => ts ts' Rts tsk tsk' Rtsk a a' Ra δ δ' Rδ.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
a: nat
a': N
Ra: Rnat a a'
δ: nat
δ': N
Rδ: Rnat δ δ'
Rnat (bound_on_total_hep_workload ts tsk a δ)
  (bound_on_total_hep_workload_T ts' tsk' a' δ')
  unfold bound_on_total_hep_workload, bound_on_total_hep_workload_T.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
a: nat
a': N
Ra: Rnat a a'
δ: nat
δ': N
Rδ: Rnat δ δ'
Rnat
  (\sum_(tsk_o <- ts | tsk_o != tsk)
      task_rbf tsk_o
        (minn
           (a + 1 + task_deadline tsk -
            task_deadline tsk_o) δ))
  (foldr +%C 0%C
     [seq task_rbf_T tsk_o
            (minn_T
               (a' + 1 + task_deadline_T tsk' -
                task_deadline_T tsk_o)%C δ')
        | tsk_o <- ts'
        & ~~ eq_task tsk_o tsk'])
  apply refinesP.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
a: nat
a': N
Ra: Rnat a a'
δ: nat
δ': N
Rδ: Rnat δ δ'
refines Rnat
  (\sum_(tsk_o <- ts | tsk_o != tsk)
      task_rbf tsk_o
        (minn
           (a + 1 + task_deadline tsk -
            task_deadline tsk_o) δ))
  (foldr +%C 0%C
     [seq task_rbf_T tsk_o
            (minn_T
               (a' + 1 + task_deadline_T tsk' -
                task_deadline_T tsk_o)%C δ')
        | tsk_o <- ts'
        & ~~ eq_task tsk_o tsk'])
  eapply refine_foldr; rewrite refinesE; first by apply Rts.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
a: nat
a': N
Ra: Rnat a a'
δ: nat
δ': N
Rδ: Rnat δ δ'
(Rtask ==> Rnat)%rel
  (fun x : task.Task =>
   task_rbf x
     (minn
        (a + 1 + task_deadline tsk - task_deadline x)
        δ))
  (fun x' : task_T =>
   task_rbf_T x'
     (minn_T
        (a' + 1 + task_deadline_T tsk' -
         task_deadline_T x')%C δ'))
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
a: nat
a': N
Ra: Rnat a a'
δ: nat
δ': N
Rδ: Rnat δ δ'
(Rtask ==> bool_R)%rel (fun x : task.Task => x != tsk)
  (fun x' : task_T => ~~ eq_task x' tsk')
  all: by move=> tsko tsko' Rtsko; apply refinesP; refines_apply.
Qed.

(** Next, we prove a refinement for the [check_point_FP] function. *)
Global Instance refine_check_point_FP :
  refines (list_R Rtask ==> Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
          check_point_FP check_point_FP_T.
refines
  (list_R Rtask ==>
   Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)
  check_point_FP check_point_FP_T
Proof.
refines
  (list_R Rtask ==>
   Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)
  check_point_FP check_point_FP_T
  rewrite refinesE => ts ts' Rts tsk tsk' Rtsk l l' Rl p p' Rp.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
bool_R (check_point_FP ts tsk l p)
  (check_point_FP_T ts' tsk' l' p')
  unfold check_point_FP, check_point_FP_T.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
bool_R
  ((task_rbf tsk (p.1 + 1) +
    bound_on_total_hep_workload ts tsk p.1 (p.1 + p.2) <=
    p.1 + p.2) && (p.2 <= l))
  ((task_rbf_T tsk' (p'.1 + 1) +
    bound_on_total_hep_workload_T ts' tsk' p'.1
      (p'.1 + p'.2) <= p'.1 + p'.2)%C &&
   (p'.2 <= l')%C)
  by apply andb_R; apply refinesP; tc.
Qed.

(** Next, we prove a special-case refinement for the [check_point_FP] function
    when applied to a refined task set and a refined task. This special case
    is required to guide the typeclass engine. *)
Global Instance refine_check_point_FP' :
  forall ts tsk,
    refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
            (check_point_FP (map taskT_to_task ts) (taskT_to_task tsk))
            (check_point_FP_T ts tsk) | 0.
forall (ts : seq task_T) (tsk : task_T),
refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)
  (check_point_FP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (check_point_FP_T ts tsk)
Proof.
forall (ts : seq task_T) (tsk : task_T),
refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)
  (check_point_FP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (check_point_FP_T ts tsk)
  intros ts tsk; rewrite refinesE => l l' Rl p p' Rp.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
bool_R
  (check_point_FP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) l p)
  (check_point_FP_T ts tsk l' p')
  unfold check_point_NP, check_point_NP_T; apply andb_R; apply refinesP; tc.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
refines bool_R
  (task_rbf (taskT_to_task tsk) (p.1 + 1) +
   bound_on_total_hep_workload
     [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) p.1 (p.1 + p.2) <= p.1 + p.2)
  (task_rbf_T tsk (p'.1 + 1) +
   bound_on_total_hep_workload_T ts tsk p'.1
     (p'.1 + p'.2) <= p'.1 + p'.2)%C
  move: refine_task' => RT.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
RT: refines (unify (A:=task_T) ==> Rtask)
  taskT_to_task id
refines bool_R
  (task_rbf (taskT_to_task tsk) (p.1 + 1) +
   bound_on_total_hep_workload
     [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) p.1 (p.1 + p.2) <= p.1 + p.2)
  (task_rbf_T tsk (p'.1 + 1) +
   bound_on_total_hep_workload_T ts tsk p'.1
     (p'.1 + p'.2) <= p'.1 + p'.2)%C
  move: refine_task_set' => RTS.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
RT: refines (unify (A:=task_T) ==> Rtask)
  taskT_to_task id
RTS: refines (unify (A:=seq task_T) ==> list_R Rtask) (map taskT_to_task) id
refines bool_R
  (task_rbf (taskT_to_task tsk) (p.1 + 1) +
   bound_on_total_hep_workload
     [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) p.1 (p.1 + p.2) <= p.1 + p.2)
  (task_rbf_T tsk (p'.1 + 1) +
   bound_on_total_hep_workload_T ts tsk p'.1
     (p'.1 + p'.2) <= p'.1 + p'.2)%C
  rewrite refinesE in RT; rewrite refinesE in RTS.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
RT: (unify (A:=task_T) ==> Rtask)%rel taskT_to_task
  id
RTS: (unify (A:=seq task_T) ==> list_R Rtask)%rel (map taskT_to_task) id
refines bool_R
  (task_rbf (taskT_to_task tsk) (p.1 + 1) +
   bound_on_total_hep_workload
     [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) p.1 (p.1 + p.2) <= p.1 + p.2)
  (task_rbf_T tsk (p'.1 + 1) +
   bound_on_total_hep_workload_T ts tsk p'.1
     (p'.1 + p'.2) <= p'.1 + p'.2)%C
  by refines_apply; rewrite refinesE; [apply RT | apply RTS | apply RT].
Qed.

(** Next, we prove a refinement for the [blocking_bound_NP] function. *)
Global Instance refine_blocking_bound :
  refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)%rel blocking_bound_NP blocking_bound_NP_T.
refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  blocking_bound_NP blocking_bound_NP_T
Proof.
refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  blocking_bound_NP blocking_bound_NP_T
  rewrite refinesE => ts ts' Rts tsk tsk' Rtsk.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
(Rnat ==> Rnat)%rel (blocking_bound_NP ts tsk)
  (blocking_bound_NP_T ts' tsk')
  unfold blocking_bound_NP, blocking_bound_NP_T, blocking_relevant.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
(Rnat ==> Rnat)%rel
  (fun A : nat =>
   \max_(tsk_o <- [seq i | i <- ts] | 
   (0 < max_arrivals tsk_o 1) &&
   (0 < concept.task_cost tsk_o) &&
   (task_deadline tsk + A < task_deadline tsk_o))
      (task_cost tsk_o - 1))
  (fun A : N =>
   foldr maxn_T 0%C
     [seq (task_cost_T tsk_o - 1)%C
        | tsk_o <- ts'
        & (0 < ConcreteMaxArrivals_T tsk_o 1)%C &&
          (0 < task_cost_T tsk_o)%C &&
          (task_deadline_T tsk' + A <
           task_deadline_T tsk_o)%C])
  intros A A' RA; apply refinesP; eapply refine_foldr_max.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
refines (list_R ?rT) [seq i | i <- ts] ts'
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
refines (?rT ==> Rnat)
  (fun x : task.Task => task_cost x - 1)
  (fun x' : task_T => (task_cost_T x' - 1)%C)
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
refines (?rT ==> bool_R)
  (fun x : task.Task =>
   (0 < max_arrivals x 1) && (0 < concept.task_cost x) &&
   (task_deadline tsk + A < task_deadline x))
  (fun x' : task_T =>
   (0 < ConcreteMaxArrivals_T x' 1)%C &&
   (0 < task_cost_T x')%C &&
   (task_deadline_T tsk' + A' < task_deadline_T x')%C)
  -
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
refines (list_R ?rT) [seq i | i <- ts] ts' by rewrite refinesE map_id; apply Rts.
  -
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
refines (Rtask ==> Rnat)
  (fun x : task.Task => task_cost x - 1)
  (fun x' : task_T => (task_cost_T x' - 1)%C) by apply refines_abstr; move => tsk1 tsk1' Rtsk1; tc.
  -
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
refines (Rtask ==> bool_R)
  (fun x : task.Task =>
   (0 < max_arrivals x 1) && (0 < concept.task_cost x) &&
   (task_deadline tsk + A < task_deadline x))
  (fun x' : task_T =>
   (0 < ConcreteMaxArrivals_T x' 1)%C &&
   (0 < task_cost_T x')%C &&
   (task_deadline_T tsk' + A' < task_deadline_T x')%C) rewrite refinesE => tsk1 tsk1' Rtsk1.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
bool_R
  ((0 < max_arrivals tsk1 1) &&
   (0 < concept.task_cost tsk1) &&
   (task_deadline tsk + A < task_deadline tsk1))
  ((0 < ConcreteMaxArrivals_T tsk1' 1)%C &&
   (0 < task_cost_T tsk1')%C &&
   (task_deadline_T tsk' + A' < task_deadline_T tsk1')%C)
    apply andb_R; first apply andb_R.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
bool_R (0 < max_arrivals tsk1 1)
  (0 < ConcreteMaxArrivals_T tsk1' 1)%C
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
bool_R (0 < concept.task_cost tsk1)
  (0 < task_cost_T tsk1')%C
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
bool_R (task_deadline tsk + A < task_deadline tsk1)
  (task_deadline_T tsk' + A' < task_deadline_T tsk1')%C
    +
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
bool_R (0 < max_arrivals tsk1 1)
  (0 < ConcreteMaxArrivals_T tsk1' 1)%C apply refine_ltn; first by done.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
Rnat (max_arrivals tsk1 1)
  (ConcreteMaxArrivals_T tsk1' 1%C)
      by apply refinesP; rewrite /max_arrivals; refines_apply; apply refine_ConcreteMaxArrivals.
    +
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
bool_R (0 < concept.task_cost tsk1)
  (0 < task_cost_T tsk1')%C by apply refine_ltn; [done | apply refinesP; refines_apply].
    +
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
bool_R (task_deadline tsk + A < task_deadline tsk1)
  (task_deadline_T tsk' + A' < task_deadline_T tsk1')%C move: refine_task_deadline => Ra.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
Ra: refines (Rtask ==> Rnat) task_deadline
  task_deadline_T
bool_R (task_deadline tsk + A < task_deadline tsk1)
  (task_deadline_T tsk' + A' < task_deadline_T tsk1')%C
      rewrite refinesE in Ra; specialize (Ra _ _ Rtsk1).
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
Ra: Rnat (task_deadline tsk1) (task_deadline_T tsk1')
bool_R (task_deadline tsk + A < task_deadline tsk1)
  (task_deadline_T tsk' + A' < task_deadline_T tsk1')%C
      move: refine_task_deadline => Rb.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
Ra: Rnat (task_deadline tsk1) (task_deadline_T tsk1')
Rb: refines (Rtask ==> Rnat) task_deadline
  task_deadline_T
bool_R (task_deadline tsk + A < task_deadline tsk1)
  (task_deadline_T tsk' + A' < task_deadline_T tsk1')%C
      rewrite refinesE in Rb; specialize (Rb _ _ Rtsk).
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
Ra: Rnat (task_deadline tsk1) (task_deadline_T tsk1')
Rb: Rnat (task_deadline tsk) (task_deadline_T tsk')
bool_R (task_deadline tsk + A < task_deadline tsk1)
  (task_deadline_T tsk' + A' < task_deadline_T tsk1')%C
      inversion Ra; inversion Rb.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
Ra: Rnat (task_deadline tsk1) (task_deadline_T tsk1')
Rb: Rnat (task_deadline tsk) (task_deadline_T tsk')
H0: task_deadline_T tsk1' = task_deadline tsk1
H1: task_deadline_T tsk' = task_deadline tsk
bool_R
  (task_deadline_T tsk' + A < task_deadline_T tsk1')
  (task_deadline_T tsk' + A' < task_deadline_T tsk1')%C
      set (a := @task_deadline_T N tsk') in *.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
Ra: Rnat (task_deadline tsk1) (task_deadline_T tsk1')
a:= task_deadline_T tsk': N
Rb: Rnat (task_deadline tsk) a
H0: task_deadline_T tsk1' = task_deadline tsk1
H1: a = task_deadline tsk
bool_R (a + A < task_deadline_T tsk1')
  (a + A' < task_deadline_T tsk1')%C
      set (b := @task_deadline_T N tsk1') in *.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
A: nat
A': N
RA: Rnat A A'
tsk1: task.Task
tsk1': task_T
Rtsk1: Rtask tsk1 tsk1'
b:= task_deadline_T tsk1': N
Ra: Rnat (task_deadline tsk1) b
a:= task_deadline_T tsk': N
Rb: Rnat (task_deadline tsk) a
H0: b = task_deadline tsk1
H1: a = task_deadline tsk
bool_R (a + A < b) (a + A' < b)%C
      by apply refine_ltn; [apply refinesP; refines_apply | done].    
Qed.

(** Next, we prove a refinement for the [check_point_NP] function. *)
Global Instance refine_check_point_NP :
  refines (list_R Rtask ==> Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
          check_point_NP check_point_NP_T.
refines
  (list_R Rtask ==>
   Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)
  check_point_NP check_point_NP_T
Proof.
refines
  (list_R Rtask ==>
   Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)
  check_point_NP check_point_NP_T
  rewrite refinesE => ts ts' Rts tsk tsk' Rtsk l l' Rl p p' Rp.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
bool_R (check_point_NP ts tsk l p)
  (check_point_NP_T ts' tsk' l' p')
  unfold check_point_NP, check_point_NP_T.
ts: seq task.Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: task.Task
tsk': task_T
Rtsk: Rtask tsk tsk'
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
bool_R
  ((blocking_bound_NP ts tsk p.1 +
    (task_rbf tsk (p.1 + 1) - (task_cost tsk - 1)) +
    bound_on_total_hep_workload ts tsk p.1 (p.1 + p.2) <=
    p.1 + p.2) && (p.2 + (task_cost tsk - 1) <= l))
  ((blocking_bound_NP_T ts' tsk' p'.1 +
    (task_rbf_T tsk' (p'.1 + 1) -
     (task_cost_T tsk' - 1)) +
    bound_on_total_hep_workload_T ts' tsk' p'.1
      (p'.1 + p'.2) <= p'.1 + p'.2)%C &&
   (p'.2 + (task_cost_T tsk' - 1) <= l')%C)
  by apply andb_R; apply refinesP; tc.
Qed.

(** Finally, we prove a special-case refinement for the [check_point_NP] function
    when applied to a refined task set and a refined task. This special case
    is required to guide the typeclass engine. *)
Global Instance refine_check_point_NP' :
  forall ts tsk,
    refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
            (check_point_NP (map taskT_to_task ts) (taskT_to_task tsk))
            (check_point_NP_T ts tsk) | 0.
forall (ts : seq task_T) (tsk : task_T),
refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)
  (check_point_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (check_point_NP_T ts tsk)
Proof.
forall (ts : seq task_T) (tsk : task_T),
refines (Rnat ==> prod_R Rnat Rnat ==> bool_R)
  (check_point_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (check_point_NP_T ts tsk)
  intros ts tsk; rewrite refinesE => l l' Rl p p' Rp.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
bool_R
  (check_point_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) l p)
  (check_point_NP_T ts tsk l' p')
  move: refine_task' => RT.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
RT: refines (unify (A:=task_T) ==> Rtask)
  taskT_to_task id
bool_R
  (check_point_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) l p)
  (check_point_NP_T ts tsk l' p')
  move: refine_task_set' => RTS.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
RT: refines (unify (A:=task_T) ==> Rtask)
  taskT_to_task id
RTS: refines (unify (A:=seq task_T) ==> list_R Rtask) (map taskT_to_task) id
bool_R
  (check_point_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) l p)
  (check_point_NP_T ts tsk l' p')
  rewrite refinesE in RT; rewrite refinesE in RTS.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
RT: (unify (A:=task_T) ==> Rtask)%rel taskT_to_task
  id
RTS: (unify (A:=seq task_T) ==> list_R Rtask)%rel (map taskT_to_task) id
bool_R
  (check_point_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) l p)
  (check_point_NP_T ts tsk l' p')
  unfold check_point_NP, check_point_NP_T.
ts: seq task_T
tsk: task_T
l: nat
l': N
Rl: Rnat l l'
p: (nat * nat)%type
p': (N * N)%type
Rp: prod_R Rnat Rnat p p'
RT: (unify (A:=task_T) ==> Rtask)%rel taskT_to_task
  id
RTS: (unify (A:=seq task_T) ==> list_R Rtask)%rel (map taskT_to_task) id
bool_R
  ((blocking_bound_NP [seq taskT_to_task i | i <- ts]
      (taskT_to_task tsk) p.1 +
    (task_rbf (taskT_to_task tsk) (p.1 + 1) -
     (task_cost (taskT_to_task tsk) - 1)) +
    bound_on_total_hep_workload
      [seq taskT_to_task i | i <- ts]
      (taskT_to_task tsk) p.1 (p.1 + p.2) <= p.1 + p.2) &&
   (p.2 + (task_cost (taskT_to_task tsk) - 1) <= l))
  ((blocking_bound_NP_T ts tsk p'.1 +
    (task_rbf_T tsk (p'.1 + 1) - (task_cost_T tsk - 1)) +
    bound_on_total_hep_workload_T ts tsk p'.1
      (p'.1 + p'.2) <= p'.1 + p'.2)%C &&
   (p'.2 + (task_cost_T tsk - 1) <= l')%C)
  by apply andb_R; apply refinesP;refines_apply;rewrite refinesE;(apply RT || apply RTS).
Qed.