refinements.v

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.FP.fast_search_space.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.arrival_bound.


(** Throughout this file, we work with Prosa's fixed-priority policy implementation. *)
#[local] Existing Instance NumericFPAscending.

(** 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 higher-or-equal priority task, ... *)
  Definition hep_task_T tsk_o tsk := (task_priority_T tsk <= @task_priority_T T tsk_o)%C.

  (** ... of total request-bound function of higher-or-equal priority task, ...  *)
  Definition total_hep_rbf_T (ts : seq task_T) (tsk : task_T) (Δ : T) : T :=
    let hep_ts := filter (fun tsk' => hep_task_T tsk' tsk) ts in
    let work_ts := map (fun tsk' => task_rbf_T tsk' Δ) hep_ts in
    foldr +%C 0%C work_ts.

  (** ... an analogous version of [hep_task] in without symmetry, ... *)
  Definition ohep_task_T tsk_o tsk :=
    (hep_task_T tsk_o tsk) && (~~ (eq_of2 tsk_o tsk)%C).

  (** ... with a respective cumulative version. *)
  Definition total_ohep_rbf_T (ts : seq task_T) (tsk : task_T) (Δ : T) : T :=
    let hep_ts := filter (fun tsk' => ohep_task_T tsk' tsk) ts in
    let work_ts := map (fun tsk' => task_rbf_T tsk' Δ) hep_ts in
    foldr +%C 0%C work_ts.

  (** 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) +
     total_ohep_rbf_T ts tsk (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) :=
    let lp_ts := filter (fun tsk_o => ~~ hep_task_T tsk_o tsk) ts in
    let block_ts := map (fun tsk_o => task_cost_T tsk_o - 1)%C lp_ts in
    foldr maxn_T 0%C block_ts.

  (** ... and 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
     + (task_rbf_T tsk (P.1 + 1) - (task_cost_T tsk - 1))
     + total_ohep_rbf_T ts tsk (P.1 + P.2) <= P.1 + P.2)%C
    && (P.2 + (task_cost_T tsk - 1) <= R)%C.

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 [search_space_emax_FP_h], ... *)
  Definition search_space_emax_FP_h_N (tsk : task_T) (l r : N) : seq N :=
    let h := get_horizon_of_task_T tsk in
    let offsets := map (N.mul h) (iota_N l r) in
    let emax_offsets := repeat_steps_with_offset_T tsk offsets in
    map predn_T emax_offsets.

  (** ... and of [search_space_emax_FP]. *)
  Definition search_space_emax_FP_N (tsk : task_T) (L : N) :=
    let h := get_horizon_of_task_T tsk in
    search_space_emax_FP_h_N tsk 0 (((L %/ h)+1))%C.

End DefinitionsN.

(** ** Refinements *)

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

(** First, we prove a refinement for the [search_space_emax_h] function. *)
Local Instance refine_search_space_emax_h :
  refines (Rtask ==> Rnat ==> Rnat ==> list_R Rnat)%rel
          search_space_emax_FP_h
          search_space_emax_FP_h_N.refines (Rtask ==> Rnat ==> Rnat ==> list_R Rnat)
  search_space_emax_FP_h search_space_emax_FP_h_N
Proof.refines (Rtask ==> Rnat ==> Rnat ==> list_R Rnat)
  search_space_emax_FP_h search_space_emax_FP_h_N
  rewrite refinesE => tsk tsk' Rtsk l l' Rl r r' Rr.tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
l: nat
l': N
Rl: Rnat l l'
r: nat
r': N
Rr: Rnat r r'
list_R Rnat (search_space_emax_FP_h tsk l r)
  (search_space_emax_FP_h_N tsk' l' r')
  apply refinesP; unfold search_space_emax_FP_h, search_space_emax_FP_h_N.tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
l: nat
l': N
Rl: Rnat l l'
r: nat
r': N
Rr: Rnat r r'
refines (list_R Rnat)
  [seq i.-1
     | i <- repeat_steps_with_offset tsk
              [seq get_horizon_of_task tsk * i
                 | i <- iota l r]]
  [seq predn_T i
     | i <- repeat_steps_with_offset_T tsk'
              [seq (get_horizon_of_task_T tsk' * i)%num
                 | i <- iota_N l' r']]
  by refines_apply; refines_abstr.
Qed.

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

(** Next, we prove a refinement for the [hep_task] function. *)
Global Instance refine_hep_task :
  refines ( Rtask ==> Rtask ==> bool_R )%rel hep_task hep_task_T.refines (Rtask ==> Rtask ==> bool_R) hep_task
  hep_task_T
Proof.refines (Rtask ==> Rtask ==> bool_R) hep_task
  hep_task_T
  apply refines_abstr2.forall (a : Task) (b : task_T),
refines Rtask a b ->
forall (a' : Task) (b' : task_T),
refines Rtask a' b' ->
refines bool_R (hep_task a a') (hep_task_T b b')
  rewrite /hep_task /hep_task_T /NumericFPAscending
          /numeric_fixed_priority.task_priority /TaskPriority.forall (a : Task) (b : task_T),
refines Rtask a b ->
forall (a' : Task) (b' : task_T),
refines Rtask a' b' ->
refines bool_R (task_priority a' <= task_priority a)
  (task_priority_T b' <= task_priority_T b)%C
  move=> tsk1 tsk1' Rtsk1 tsk2 tsk2' Rtsk2.tsk1: Task
tsk1': task_T
Rtsk1: refines Rtask tsk1 tsk1'
tsk2: Task
tsk2': task_T
Rtsk2: refines Rtask tsk2 tsk2'
refines bool_R
  (task_priority tsk2 <= task_priority tsk1)
  (task_priority_T tsk2' <= task_priority_T tsk1')%C
  by refines_apply.
Qed.

(** Next, we prove a refinement for the [total_hep_rbf] function. *)
Global Instance refine_total_hep_rbf :
  refines ( list_R Rtask ==> Rtask ==> Rnat ==> Rnat )%rel total_hep_rbf total_hep_rbf_T.refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  total_hep_rbf total_hep_rbf_T
Proof.refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  total_hep_rbf total_hep_rbf_T
  apply refines_abstr; move => ts ts' Rts.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
refines (Rtask ==> Rnat ==> Rnat) (total_hep_rbf ts)
  (total_hep_rbf_T ts')
  apply refines_abstr; move => tsk tsk' Rtsk.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
refines (Rnat ==> Rnat) (total_hep_rbf ts tsk)
  (total_hep_rbf_T ts' tsk')
  apply refines_abstr; move => Δ Δ' RΔ.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines Rnat (total_hep_rbf ts tsk Δ)
  (total_hep_rbf_T ts' tsk' Δ')
  rewrite /total_hep_rbf /total_hep_request_bound_function_FP /total_hep_rbf_T.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines Rnat
  (\sum_(tsk_other <- ts | 
   hep_task tsk_other tsk)
      task_request_bound_function tsk_other Δ)
  (foldr +%C 0%C
     [seq task_rbf_T tsk' Δ'
        | tsk' <- [seq tsk'0 <- ts'
                     | hep_task_T tsk'0 tsk']])
  eapply refine_foldr.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (list_R ?rT) ts ts'
ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (?rT ==> Rnat)
  (task_request_bound_function^~ Δ) 
  (task_rbf_T^~ Δ')
ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (?rT ==> bool_R) 
  (hep_task^~ tsk) (hep_task_T^~ tsk')
  -ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (list_R ?rT) ts ts' by apply Rts.
  -ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (Rtask ==> Rnat)
  (task_request_bound_function^~ Δ) 
  (task_rbf_T^~ Δ') by apply refines_abstr; move => tsk1 tsk1' Rtsk1; tc.
  -ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (Rtask ==> bool_R) 
  (hep_task^~ tsk) (hep_task_T^~ tsk') by apply refines_abstr; move => tsk1 tsk1' Rtsk1; tc.
Qed.

(** Next, we prove a special-case refinement for the [total_hep_rbf] 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_hep_rbf' :
  forall ts tsk,
    refines (Rnat ==> Rnat)%rel
            (total_hep_rbf (map taskT_to_task ts) (taskT_to_task tsk))
            (total_hep_rbf_T ts tsk) | 0.forall (ts : seq task_T) (tsk : task_T),
refines (Rnat ==> Rnat)
  (total_hep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (total_hep_rbf_T ts tsk)
Proof.forall (ts : seq task_T) (tsk : task_T),
refines (Rnat ==> Rnat)
  (total_hep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (total_hep_rbf_T ts tsk)
  move=> ts tsk; rewrite refinesE => δ δ' Rδ.ts: seq task_T
tsk: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
Rnat
  (total_hep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) δ)
  (total_hep_rbf_T ts tsk δ')
  move: refine_task_set' => RTS.ts: seq task_T
tsk: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: refines (unify (A:=seq task_T) ==> list_R Rtask) (map taskT_to_task) id
Rnat
  (total_hep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) δ)
  (total_hep_rbf_T ts tsk δ')
  rewrite refinesE in RTS.ts: seq task_T
tsk: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: (unify (A:=seq task_T) ==> list_R Rtask)%rel (map taskT_to_task) id
Rnat
  (total_hep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) δ)
  (total_hep_rbf_T ts tsk δ')
  specialize (RTS ts ts (unifyxx _)); simpl in RTS.ts: seq task_T
tsk: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
Rnat
  (total_hep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) δ)
  (total_hep_rbf_T ts tsk δ')
  apply refinesP.ts: seq task_T
tsk: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
refines Rnat
  (total_hep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) δ)
  (total_hep_rbf_T ts tsk δ')
  move: refine_total_hep_rbf => EQ.ts: seq task_T
tsk: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
EQ: refines
  (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  total_hep_rbf total_hep_rbf_T
refines Rnat
  (total_hep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) δ)
  (total_hep_rbf_T ts tsk δ')
  refines_apply.ts: seq task_T
tsk: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
EQ: refines
  (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  total_hep_rbf total_hep_rbf_T
refines Rtask (taskT_to_task tsk) tsk
  move: refine_task' => Rtsk.ts: seq task_T
tsk: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
EQ: refines
  (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  total_hep_rbf total_hep_rbf_T
Rtsk: refines (unify (A:=task_T) ==> Rtask)
  taskT_to_task id
refines Rtask (taskT_to_task tsk) tsk
  rewrite refinesE; rewrite refinesE in Rtsk.ts: seq task_T
tsk: task_T
δ: nat
δ': N
Rδ: Rnat δ δ'
RTS: list_R Rtask [seq taskT_to_task i | i <- ts] ts
EQ: refines
  (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  total_hep_rbf total_hep_rbf_T
Rtsk: (unify (A:=task_T) ==> Rtask)%rel taskT_to_task
  id
Rtask (taskT_to_task tsk) tsk
  by apply Rtsk.
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_listNN : eq_of (seq (prod N 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. *)
Global 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) (b : task_T),
refines Rtask a b ->
forall (a' : 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
a': task_T
Ra: refines Rtask a a'
b: 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
a': task_T
Ra: refines Rtask a a'
b: 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 [ohep_task] function. *)
Global Instance refine_ohep_task :
  refines ( Rtask ==> Rtask ==> bool_R )%rel ohep_task ohep_task_T.refines (Rtask ==> Rtask ==> bool_R) ohep_task
  ohep_task_T
Proof.refines (Rtask ==> Rtask ==> bool_R) ohep_task
  ohep_task_T
  apply refines_abstr2.forall (a : Task) (b : task_T),
refines Rtask a b ->
forall (a' : Task) (b' : task_T),
refines Rtask a' b' ->
refines bool_R (ohep_task a a') (ohep_task_T b b')
  rewrite /ohep_task /ohep_task_T /NumericFPAscending
          /numeric_fixed_priority.task_priority /TaskPriority.forall (a : Task) (b : task_T),
refines Rtask a b ->
forall (a' : Task) (b' : task_T),
refines Rtask a' b' ->
refines bool_R (hep_task a a' && (a != a'))
  (hep_task_T b b' && ~~ eq_task b b')
  move=> tsk1 tsk1' Rtsk1 tsk2 tsk2' Rtsk2.tsk1: Task
tsk1': task_T
Rtsk1: refines Rtask tsk1 tsk1'
tsk2: Task
tsk2': task_T
Rtsk2: refines Rtask tsk2 tsk2'
refines bool_R (hep_task tsk1 tsk2 && (tsk1 != tsk2))
  (hep_task_T tsk1' tsk2' && ~~ eq_task tsk1' tsk2')
  by refines_apply.
Qed.

(** Next, we prove a refinement for the [total_ohep_rbf] function. *)
Global Instance refine_total_ohep_rbf :
  refines ( list_R Rtask ==> Rtask ==> Rnat ==> Rnat )%rel total_ohep_rbf total_ohep_rbf_T.refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  total_ohep_rbf total_ohep_rbf_T
Proof.refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)
  total_ohep_rbf total_ohep_rbf_T
  apply refines_abstr; move => ts ts' Rts.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
refines (Rtask ==> Rnat ==> Rnat) (total_ohep_rbf ts)
  (total_ohep_rbf_T ts')
  apply refines_abstr; move => tsk tsk' Rtsk.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
refines (Rnat ==> Rnat) (total_ohep_rbf ts tsk)
  (total_ohep_rbf_T ts' tsk')
  apply refines_abstr; move => Δ Δ' RΔ.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines Rnat (total_ohep_rbf ts tsk Δ)
  (total_ohep_rbf_T ts' tsk' Δ')
  rewrite /total_hep_rbf /total_hep_request_bound_function_FP.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines Rnat (total_ohep_rbf ts tsk Δ)
  (total_ohep_rbf_T ts' tsk' Δ')
  eapply refine_foldr.ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (list_R ?rT) ts ts'
ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (?rT ==> Rnat)
  (task_request_bound_function^~ Δ) 
  (task_rbf_T^~ Δ')
ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (?rT ==> bool_R)
  (fun tsk_other : Task =>
   hep_task tsk_other tsk && (tsk_other != tsk))
  (ohep_task_T^~ tsk')
  -ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (list_R ?rT) ts ts' by apply Rts.
  -ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (Rtask ==> Rnat)
  (task_request_bound_function^~ Δ) 
  (task_rbf_T^~ Δ') by apply refines_abstr; move => tsk1 tsk1' Rtsk1; tc.
  -ts: seq Task
ts': seq task_T
Rts: refines (list_R Rtask) ts ts'
tsk: Task
tsk': task_T
Rtsk: refines Rtask tsk tsk'
Δ: nat
Δ': N
RΔ: refines Rnat Δ Δ'
refines (Rtask ==> bool_R)
  (fun tsk_other : Task =>
   hep_task tsk_other tsk && (tsk_other != tsk))
  (ohep_task_T^~ tsk') by unfold ohep_task_T; apply refines_abstr; move => tsk1 tsk1' Rtsk1; tc.
Qed.

(** Next, we prove a refinement for the [check_point_FP] function. *)
Global Instance refine_check_point :
  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
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: 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')
  by unfold check_point_FP, check_point_FP_T; 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' :
  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_FP, check_point_FP_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) +
   total_ohep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) (p.1 + p.2) <= p.1 + p.2)
  (task_rbf_T tsk (p'.1 + 1) +
   total_ohep_rbf_T ts tsk (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) +
   total_ohep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) (p.1 + p.2) <= p.1 + p.2)
  (task_rbf_T tsk (p'.1 + 1) +
   total_ohep_rbf_T ts tsk (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) +
   total_ohep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) (p.1 + p.2) <= p.1 + p.2)
  (task_rbf_T tsk (p'.1 + 1) +
   total_ohep_rbf_T ts tsk (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) +
   total_ohep_rbf [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk) (p.1 + p.2) <= p.1 + p.2)
  (task_rbf_T tsk (p'.1 + 1) +
   total_ohep_rbf_T ts tsk (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 )%rel blocking_bound_NP blocking_bound_NP_T.refines (list_R Rtask ==> Rtask ==> Rnat)
  blocking_bound_NP blocking_bound_NP_T
Proof.refines (list_R Rtask ==> Rtask ==> Rnat)
  blocking_bound_NP blocking_bound_NP_T
  rewrite refinesE => ts ts' Rts tsk tsk' Rtsk.ts: seq Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
Rnat (blocking_bound_NP ts tsk)
  (blocking_bound_NP_T ts' tsk')
  unfold blocking_bound, blocking_bound_NP_T.ts: seq Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
Rnat (blocking_bound_NP ts tsk)
  (foldr maxn_T 0%C
     [seq (task_cost_T tsk_o - 1)%C
        | tsk_o <- ts'
        & ~~ hep_task_T tsk_o tsk'])
  apply refinesP; eapply refine_foldr_max.ts: seq Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
refines (list_R ?rT) ts ts'
ts: seq Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
refines (?rT ==> Rnat)
  (fun x : Task => concept.task_cost x - 1)
  (fun x' : task_T => (task_cost_T x' - 1)%C)
ts: seq Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
refines (?rT ==> bool_R)
  (fun x : Task => ~~ hep_task x tsk)
  (fun x' : task_T => ~~ hep_task_T x' tsk')
  -ts: seq Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
refines (list_R ?rT) ts ts' by rewrite refinesE; apply Rts.
  -ts: seq Task
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
refines (Rtask ==> Rnat)
  (fun x : Task => concept.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
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: Task
tsk': task_T
Rtsk: Rtask tsk tsk'
refines (Rtask ==> bool_R)
  (fun x : Task => ~~ hep_task x tsk)
  (fun x' : task_T => ~~ hep_task_T x' tsk') by apply refines_abstr; move => tsk1 tsk1' Rtsk1; tc.
Qed.

(** Next, we prove a special-case refinement for the [blocking_bound_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_blocking_bound' :
  forall ts tsk,
    refines ( Rnat )%rel
            (blocking_bound_NP (map taskT_to_task ts) (taskT_to_task tsk))
            (blocking_bound_NP_T ts tsk) | 0.forall (ts : seq task_T) (tsk : task_T),
refines Rnat
  (blocking_bound_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (blocking_bound_NP_T ts tsk)
Proof.forall (ts : seq task_T) (tsk : task_T),
refines Rnat
  (blocking_bound_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (blocking_bound_NP_T ts tsk)
  intros ts tsk; rewrite refinesE.ts: seq task_T
tsk: task_T
Rnat
  (blocking_bound_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (blocking_bound_NP_T ts tsk)
  move: refine_task' => RT.ts: seq task_T
tsk: task_T
RT: refines (unify (A:=task_T) ==> Rtask)
  taskT_to_task id
Rnat
  (blocking_bound_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (blocking_bound_NP_T ts tsk)
  move: refine_task_set' => RTS.ts: seq task_T
tsk: task_T
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
Rnat
  (blocking_bound_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (blocking_bound_NP_T ts tsk)
  rewrite refinesE in RT; rewrite refinesE in RTS.ts: seq task_T
tsk: task_T
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
Rnat
  (blocking_bound_NP [seq taskT_to_task i | i <- ts]
     (taskT_to_task tsk)) (blocking_bound_NP_T ts tsk)
  by apply refinesP; refines_apply; (rewrite refinesE; (apply RT || apply RTS)).
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
ts': seq task_T
Rts: list_R Rtask ts ts'
tsk: 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')
  by unfold check_point_NP, check_point_NP_T; 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; apply andb_R; apply refinesP; refines_apply.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 Rtask (taskT_to_task tsk) tsk
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 Rtask (taskT_to_task tsk) tsk
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 (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'
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 Rtask (taskT_to_task tsk) tsk
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 Rtask (taskT_to_task tsk) tsk
  all: try by (rewrite refinesE; (apply RT || apply RTS)).
Qed.