Library prosa.implementation.refinements.EDF.refinements
Require Export prosa.implementation.refinements.refinements.
Require Export prosa.implementation.refinements.task.
Require Export prosa.implementation.refinements.EDF.fast_search_space.
Require Export prosa.implementation.refinements.arrival_bound.
Require Export prosa.implementation.refinements.task.
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.
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_of (@task_T T)}.
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_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.
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.
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.
(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.
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.
(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.
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.
We provide a definition of iota, ...
... 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.
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.
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.
let points := map (fun tsko ⇒ task_search_space_emax_EDF_N tsk tsko L) ts in
flatten points.
End DefinitionsN.
Refinements
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.
Proof.
rewrite refinesE ⇒ tsk tsk' Rtsk tsko tsko' Rtsko l l' Rl r r' Rr.
apply refinesP; unfold task_search_space_emax_EDF_h, task_search_space_emax_EDF_h_N.
by refines_apply; refines_abstr.
Qed.
refines (Rtask ==> Rtask ==> Rnat ==> Rnat ==> list_R Rnat)%rel
task_search_space_emax_EDF_h
task_search_space_emax_EDF_h_N.
Proof.
rewrite refinesE ⇒ tsk tsk' Rtsk tsko tsko' Rtsko l l' Rl r r' Rr.
apply refinesP; unfold task_search_space_emax_EDF_h, task_search_space_emax_EDF_h_N.
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 :
∀ 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).
Proof.
intros.
rewrite refinesE ⇒ δ δ' Rδ.
unfold task_search_space_emax_EDF, task_search_space_emax_EDF_N.
apply refinesP; rewrite -addn1.
refines_apply.
all: by rewrite refinesE; unfold Rtask, fun_hrel.
Qed.
∀ 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).
Proof.
intros.
rewrite refinesE ⇒ δ δ' Rδ.
unfold task_search_space_emax_EDF, task_search_space_emax_EDF_N.
apply refinesP; rewrite -addn1.
refines_apply.
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 :
∀ 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).
Proof.
intros ? ?.
unfold search_space_emax_EDF, search_space_emax_EDF_N.
rewrite refinesE ⇒ L L' RL; apply refinesP.
have F: ∀ xs f, \cat_(x <- xs) f x = flatten (map f xs).
{ clear; induction xs as [ | x xs]; intros.
- by rewrite big_nil.
- by rewrite big_cons //= IHxs. }
rewrite F; clear F.
refines_apply.
Unshelve.
5: exact (Rtask ==> list_R Rnat)%rel.
4: exact (list_R Rtask).
- rewrite refinesE ⇒ f f' Rf xs xs' Rxs; apply refinesP.
by eapply refine_map; [rewrite refinesE; exact Rxs | rewrite refinesE ].
- move: refine_task_search_space_emax_EDF⇒ R; rewrite refinesE in R.
by rewrite refinesE ⇒ tsko tsko' Rtsko; rewrite -Rtsko; apply R.
- move: refine_task_set' ⇒ RTS.
rewrite refinesE; rewrite refinesE in RTS.
by apply RTS; apply unifyxx.
Qed.
∀ 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).
Proof.
intros ? ?.
unfold search_space_emax_EDF, search_space_emax_EDF_N.
rewrite refinesE ⇒ L L' RL; apply refinesP.
have F: ∀ xs f, \cat_(x <- xs) f x = flatten (map f xs).
{ clear; induction xs as [ | x xs]; intros.
- by rewrite big_nil.
- by rewrite big_cons //= IHxs. }
rewrite F; clear F.
refines_apply.
Unshelve.
5: exact (Rtask ==> list_R Rnat)%rel.
4: exact (list_R Rtask).
- rewrite refinesE ⇒ f f' Rf xs xs' Rxs; apply refinesP.
by eapply refine_map; [rewrite refinesE; exact Rxs | rewrite refinesE ].
- move: refine_task_search_space_emax_EDF⇒ R; rewrite refinesE in R.
by rewrite refinesE ⇒ tsko tsko' Rtsko; rewrite -Rtsko; apply R.
- move: refine_task_set' ⇒ RTS.
rewrite refinesE; rewrite refinesE in RTS.
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.
Proof.
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.
eapply refine_uncond_foldr; first exact Rt.
by rewrite refinesE ⇒ tsko tsko' Rtsko; apply refinesP; refines_apply.
Qed.
refines (list_R Rtask ==> Rnat ==> Rnat)%rel total_request_bound_function total_rbf_T.
Proof.
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.
eapply refine_uncond_foldr; first exact Rt.
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' :
∀ ts,
refines (Rnat ==> Rnat)%rel
(total_request_bound_function (map taskT_to_task ts))
(total_rbf_T ts) | 0.
Proof.
intros; rewrite refinesE; intros δ δ' Rδ.
move: refine_task_set' ⇒ RTS.
rewrite refinesE in RTS.
specialize (RTS ts ts (unifyxx _)); simpl in RTS.
apply refinesP.
move: (refine_total_rbf) ⇒ EQ.
rewrite refinesE in EQ.
erewrite <-EQ; [ | eassumption | eassumption].
set (x := total_rbf_T _ _).
by rewrite refinesE.
Qed.
∀ ts,
refines (Rnat ==> Rnat)%rel
(total_request_bound_function (map taskT_to_task ts))
(total_rbf_T ts) | 0.
Proof.
intros; rewrite refinesE; intros δ δ' Rδ.
move: refine_task_set' ⇒ RTS.
rewrite refinesE in RTS.
specialize (RTS ts ts (unifyxx _)); simpl in RTS.
apply refinesP.
move: (refine_total_rbf) ⇒ EQ.
rewrite refinesE in EQ.
erewrite <-EQ; [ | eassumption | eassumption].
set (x := total_rbf_T _ _).
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.
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.
Proof.
apply refines_abstr2.
intros a a' Ra b b' Rb.
unfold task_eqdef, task_eqdef_T.
by rewrite refinesE; repeat apply andb_R; apply refinesP; refines_apply.
Qed.
refines (Rtask ==> Rtask ==> bool_R)%rel task_eqdef task_eqdef_T.
Proof.
apply refines_abstr2.
intros a a' Ra b b' Rb.
unfold task_eqdef, task_eqdef_T.
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.
Proof.
rewrite refinesE ⇒ ts ts' Rts tsk tsk' Rtsk a a' Ra δ δ' Rδ.
unfold bound_on_total_hep_workload, bound_on_total_hep_workload_T.
apply refinesP.
eapply refine_foldr; rewrite refinesE; first by apply Rts.
all: by move⇒ tsko tsko' Rtsko; apply refinesP; refines_apply.
Qed.
refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat ==> Rnat)%rel
bound_on_total_hep_workload bound_on_total_hep_workload_T.
Proof.
rewrite refinesE ⇒ ts ts' Rts tsk tsk' Rtsk a a' Ra δ δ' Rδ.
unfold bound_on_total_hep_workload, bound_on_total_hep_workload_T.
apply refinesP.
eapply refine_foldr; rewrite refinesE; first by apply Rts.
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.
Proof.
rewrite refinesE ⇒ ts ts' Rts tsk tsk' Rtsk l l' Rl p p' Rp.
unfold check_point_FP, check_point_FP_T.
by apply andb_R; apply refinesP; tc.
Qed.
refines (list_R Rtask ==> Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
check_point_FP check_point_FP_T.
Proof.
rewrite refinesE ⇒ ts ts' Rts tsk tsk' Rtsk l l' Rl p p' Rp.
unfold check_point_FP, check_point_FP_T.
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' :
∀ 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.
Proof.
intros ts tsk; rewrite refinesE ⇒ l l' Rl p p' Rp.
unfold check_point_NP, check_point_NP_T; apply andb_R; apply refinesP; tc.
move: refine_task' ⇒ RT.
move: refine_task_set' ⇒ RTS.
rewrite refinesE in RT; rewrite refinesE in RTS.
by refines_apply; rewrite refinesE; [apply RT | apply RTS | apply RT].
Qed.
∀ 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.
Proof.
intros ts tsk; rewrite refinesE ⇒ l l' Rl p p' Rp.
unfold check_point_NP, check_point_NP_T; apply andb_R; apply refinesP; tc.
move: refine_task' ⇒ RT.
move: refine_task_set' ⇒ RTS.
rewrite refinesE in RT; rewrite refinesE in RTS.
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.
Proof.
rewrite refinesE ⇒ ts ts' Rts tsk tsk' Rtsk.
unfold blocking_bound_NP, blocking_bound_NP_T, blocking_relevant.
intros A A' RA; apply refinesP; eapply refine_foldr_max.
- by rewrite refinesE map_id; apply Rts.
- by apply refines_abstr; move ⇒ tsk1 tsk1' Rtsk1; unfold ε; tc.
- rewrite refinesE ⇒ tsk1 tsk1' Rtsk1.
apply andb_R; first apply andb_R.
+ unfold ε.
apply refine_ltn; first by done.
by apply refinesP; rewrite /max_arrivals; refines_apply; apply refine_ConcreteMaxArrivals.
+ by apply refine_ltn; [done | apply refinesP; refines_apply].
+ move: refine_task_deadline ⇒ Ra.
rewrite refinesE in Ra; specialize (Ra _ _ Rtsk1).
move: refine_task_deadline ⇒ Rb.
rewrite refinesE in Rb; specialize (Rb _ _ Rtsk).
inversion Ra; inversion Rb.
set (a := @task_deadline_T N tsk') in ×.
set (b := @task_deadline_T N tsk1') in ×.
by apply refine_ltn; [apply refinesP; refines_apply | done].
Qed.
refines (list_R Rtask ==> Rtask ==> Rnat ==> Rnat)%rel blocking_bound_NP blocking_bound_NP_T.
Proof.
rewrite refinesE ⇒ ts ts' Rts tsk tsk' Rtsk.
unfold blocking_bound_NP, blocking_bound_NP_T, blocking_relevant.
intros A A' RA; apply refinesP; eapply refine_foldr_max.
- by rewrite refinesE map_id; apply Rts.
- by apply refines_abstr; move ⇒ tsk1 tsk1' Rtsk1; unfold ε; tc.
- rewrite refinesE ⇒ tsk1 tsk1' Rtsk1.
apply andb_R; first apply andb_R.
+ unfold ε.
apply refine_ltn; first by done.
by apply refinesP; rewrite /max_arrivals; refines_apply; apply refine_ConcreteMaxArrivals.
+ by apply refine_ltn; [done | apply refinesP; refines_apply].
+ move: refine_task_deadline ⇒ Ra.
rewrite refinesE in Ra; specialize (Ra _ _ Rtsk1).
move: refine_task_deadline ⇒ Rb.
rewrite refinesE in Rb; specialize (Rb _ _ Rtsk).
inversion Ra; inversion Rb.
set (a := @task_deadline_T N tsk') in ×.
set (b := @task_deadline_T N tsk1') in ×.
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.
Proof.
rewrite refinesE ⇒ ts ts' Rts tsk tsk' Rtsk l l' Rl p p' Rp.
unfold check_point_NP, check_point_NP_T.
by apply andb_R; apply refinesP; tc.
Qed.
refines (list_R Rtask ==> Rtask ==> Rnat ==> prod_R Rnat Rnat ==> bool_R)%rel
check_point_NP check_point_NP_T.
Proof.
rewrite refinesE ⇒ ts ts' Rts tsk tsk' Rtsk l l' Rl p p' Rp.
unfold check_point_NP, check_point_NP_T.
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' :
∀ 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.
Proof.
intros ts tsk; rewrite refinesE ⇒ l l' Rl p p' Rp.
move: refine_task' ⇒ RT.
move: refine_task_set' ⇒ RTS.
rewrite refinesE in RT; rewrite refinesE in RTS.
unfold check_point_NP, check_point_NP_T.
by apply andb_R; apply refinesP;refines_apply;rewrite refinesE;(apply RT || apply RTS).
Qed.
∀ 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.
Proof.
intros ts tsk; rewrite refinesE ⇒ l l' Rl p p' Rp.
move: refine_task' ⇒ RT.
move: refine_task_set' ⇒ RTS.
rewrite refinesE in RT; rewrite refinesE in RTS.
unfold check_point_NP, check_point_NP_T.
by apply andb_R; apply refinesP;refines_apply;rewrite refinesE;(apply RT || apply RTS).
Qed.