Commit 100795b2 authored by Lucien RAKOTOMALALA's avatar Lucien RAKOTOMALALA

Refrac complete of beta in F

The min-plus service doesn't need anymore of a Fplus function.
parent a622a142
This diff is collapsed.
......@@ -269,13 +269,13 @@ Definition WC_backlog (A D : dflow) (S : server) (hAD : S A D) :=
(* Def 5 p 32 *)
(* Final Def 1.5 p10 *)
(** *** Horizontal and vertical deviations **)
Definition hDev (f g : nnR -> nnRbar) (t : nnR) :=
Definition hDev (f g : F) (t : nnR) :=
\inf{d | ((f t) <= (g (t + d)%nnR))%Rbar}%nnR.
Definition vDev (f g : nnR -> nnRbar) (t : nnR) :=
Definition vDev (f g : F) (t : nnR) :=
((f t) - (g t))%Rbar.
(** Worst Case hDev and vDev **)
Program Definition WC_hDev (f g : nnR -> nnRbar): nnRbar :=
Program Definition WC_hDev (f g : F): nnRbar :=
mk_nnRbar (\sup_t {hDev f g t}) _ .
Next Obligation.
rewrite /Rbar_lub.
......@@ -285,22 +285,22 @@ apply (Rbar_le_trans _ (hDev f g nnR0)); [apply nnRbar_pos | apply Hl].
by exists nnR0.
Qed.
Definition WC_vDev (f g : nnR -> nnRbar) :=
Definition WC_vDev (f g : F) :=
\sup_t {vDev f g t}.
(** Equality of hDev and vDev *)
Lemma hDev_eq (f g f' g' : nnR -> nnRbar) (t : nnR) :
Lemma hDev_eq (f g f' g' : F) (t : nnR) :
f =1 f' -> g =1 g' -> hDev f g t = hDev f' g' t.
Proof. by move => Hf Hg; apply Glb_nnRbar_eqset => d; rewrite Hf Hg. Qed.
Lemma WC_vDev_eq (f g f' g' : nnR -> nnRbar) :
Lemma WC_vDev_eq (f g f' g' : F) :
f =1 f' -> g =1 g' -> WC_vDev f g = WC_vDev f' g'.
Proof.
move=> Hf Hg; apply Rbar_lub_rw => y.
by split => [] [] t ->; exists t; rewrite /vDev Hf Hg.
Qed.
Lemma WC_hDev_eq (f g f' g' : nnR -> nnRbar) :
Lemma WC_hDev_eq (f g f' g' : F) :
f =1 f' -> g =1 g' -> WC_hDev f g = WC_hDev f' g'.
Proof.
move => Hf Hg.
......@@ -321,8 +321,8 @@ Qed.
(* Final Lem 5.1 p116 *)
Lemma sup_horizontal_deviations (f g : Fup) :
forall t,
hDev (Fup_val f) (Fup_val g) t =
\sup{d | ((Fup_val g) (t + d)%nnR < (Fup_val f) t)%Rbar}%nnR.
hDev (f) (Fup_val g) t =
\sup{d | ((Fup_val g) (t + d)%nnR < (f) t)%Rbar}%nnR.
Proof.
move => t.
have [f' Hf'] : exists f' : Fup, forall x, (Fup_val f') x = (Fup_val g) (t + x)%nnR.
......@@ -334,8 +334,8 @@ have [f' Hf'] : exists f' : Fup, forall x, (Fup_val f') x = (Fup_val g) (t + x)%
by rewrite Rplus_comm.
}
}
rewrite /hDev -(Glb_nnRbar_eqset (fun d => ((Fup_val f) t <= (Fup_val f') d)%Rbar)).
{ rewrite -(Lub_nnRbar_eqset (fun d => ((Fup_val f') d < (Fup_val f) t)%Rbar)).
rewrite /hDev -(Glb_nnRbar_eqset (fun d => ((f) t <= (Fup_val f') d)%Rbar)).
{ rewrite -(Lub_nnRbar_eqset (fun d => ((Fup_val f') d < (f) t)%Rbar)).
{ apply alt_def_pseudo_inv_inf_nnR. }
by move=> d; rewrite Hf'.
}
......@@ -344,7 +344,7 @@ Qed.
(* Proposition 41 p 136 *)
(* Final Proposition 5.12 p 115 *)
Proposition monotony_deviations (f f' g g' : nnR -> nnRbar) :
Proposition monotony_deviations (f f' g g' : Fplus) :
(forall t, f' t <= f t)%Rbar -> (forall t, g t <= g' t)%Rbar ->
(WC_vDev f' g' <= WC_vDev f g)%Rbar /\
(WC_hDev f' g' <= WC_hDev f g)%Rbar.
......@@ -352,7 +352,7 @@ Proof.
move=> Hyp_f Hyp_g.
split.
{ apply Rle_Rbar_lub => x.
rewrite /vDev.
rewrite /vDev /Fplus_val /=.
apply Rbar_minus_le_compat => //; left.
unfold not => Hfal.
move : (Rbar_eq_le Hfal).
......@@ -361,8 +361,8 @@ split.
}
apply Rle_Rbar_lub => t.
apply Glb_nnRbar_subset => d Hd.
apply (Rbar_le_trans _ (f t)) => //.
by apply (Rbar_le_trans _ _ _ Hd).
apply (Rbar_le_trans _ (f t)); [apply Hyp_f|].
by apply (Rbar_le_trans _ _ _ Hd); apply Hyp_g.
Qed.
Lemma F_min_conv_non_decr (f g : Fup) : non_decr (f * g)%F.
......@@ -408,8 +408,8 @@ Qed.
(* Th 10 p.135 *)
(* Final : Th 5.2 p.115 *)
(** *** Backlog and delay bounds**)
Theorem delay_backlog_bounds (S : server) (alpha : Fup)
(beta : Fup) : (* (H_beta' : beta nnR0 = 0 :> Rbar) : *)
Theorem delay_backlog_bounds (S : server)
(alpha beta : Fup) : (* (H_beta' : beta nnR0 = 0 :> Rbar) : *)
forall (A D : dflow), forall hAD : S A D,
is_maximal_arrival A alpha -> is_min_service S beta ->
(WC_delay hAD <= WC_hDev alpha beta)%Rbar
......@@ -417,13 +417,14 @@ Theorem delay_backlog_bounds (S : server) (alpha : Fup)
Proof.
move => A D hS Halpha Hbeta.
split.
{ have -> : WC_delay hS = WC_hDev (A : Fup) [eta D] :> Rbar.
{ have -> : WC_delay hS = WC_hDev (A : Fup) D :> Rbar.
{ rewrite /WC_delay /WC_hDev /=.
apply Rbar_lub_rw => y.
by split; move => [t Ht]; exists t.
}
apply (Rbar_le_trans _ (WC_hDev (A : Fup) ((A : Fup) * beta)%D)).
{ apply monotony_deviations .
apply (Rbar_le_trans _ (WC_hDev A ((A : Fup)* beta)%D)).
{
apply monotony_deviations.
{ move=> t; apply Rbar_le_refl. }
move=> t.
by move: (Hbeta A D hS) => /F_min_leP Hbeta'; move: (Hbeta' t).
......@@ -505,7 +506,7 @@ apply Hl1 => {Hl1} _ [t ->].
rewrite Rbar_plus_le_opp.
rewrite RbarDioid.Rbar_plus_comm.
rewrite -Rbar_plus_le_opp.
rewrite /vDev /GDioid.mul /= /F_min_conv /Rbar_glb.
rewrite /vDev /GDioid.mul /Fplus_val /= /F_min_conv /Rbar_glb /=.
case Rbar_ex_glb => l3 [_ Hl3] /=.
apply Hl3 => {Hl3} _ [u [v [Huv ->]]].
rewrite Rbar_plus_le_opp RbarDioid.Rbar_plus_comm.
......@@ -743,7 +744,7 @@ is_resiual_contr :
*)
Program Definition residual_server_constr (n : nat) (S : n.-server) i
(alpha : Fup^n) : server :=
(alpha : F^n) : server :=
@Build_server (fun Ai Di =>
exists A D, nserver_f S A D /\ A i =1 Ai /\ D i =1 Di
/\ forall j, is_maximal_arrival (A j) (alpha j)) _.
......@@ -755,9 +756,8 @@ apply S_leq, H1.
Qed.
Lemma residual_server_constrE n (S : n.-server) i (Ai Di : Fplus)
(alpha : Fup^n) :
(residual_server_constr S i) alpha Ai Di
(alpha : F^n) :
(residual_server_constr S i) alpha Ai Di
<-> exists A D, S A D /\ Ai =1 A i /\ Di =1 D i /\ forall j, is_maximal_arrival (A j) (alpha j).
Proof.
split.
......@@ -801,8 +801,8 @@ Qed.
Theorem FIFO_delay n (S : n.+1.-server) (S_FIFO : FIFO_service_policy S)
(alpha : Fup^n.+1) (beta : F0up) i :
is_min_service (aggregate_server S) beta ->
is_min_service (residual_server_constr S i alpha)
(delta (WC_hDev (fun t => \sum_j alpha j t)%nnRbar beta)).
is_min_service (residual_server_constr S i [ffun i => alpha i : F])
(delta (WC_hDev (fun t => \sum_j alpha j t)%Rbar beta)).
Proof.
move : (F0up_start0 beta) => Hbeta0.
move=> Hbeta Ai Di.
......@@ -851,29 +851,37 @@ rewrite -delta_prop_conv.
rewrite nnRbar_valE.
rewrite Hd' => {dfl}.
set sum_alpha := \big[Fup_plus/Fup0]_j alpha j.
(* set sum_alpha := \big[F_plus/(fun => nnRbar_val 0%nnRbar)]_j alpha j. *)
have Hfun_sum_alpha : (fun t : nnR => (\sum_j (alpha j) t)%nnRbar)
= sum_alpha.
(* have Hfun_sum_alpha : (fun t : nnR => (\sum_j (alpha j) t)%Rbar) *)
(* = sum_alpha. *)
{ apply functional_extensionality => t' /=.
rewrite /sum_alpha.
apply nnRbar_inj.
apply (big_ind2 (R1 := Fup)) => //=.
by move => x1 x2 y1 y2 -> ->.
}
rewrite Hfun_sum_alpha nnRbar_valE nnRbar_dflowE.
apply /Fup_leP.
apply (@Service_for_a_jitter (sum_dflow a) (aggregate_server S)) => //.
rewrite (@WC_hDev_eq (fun t : nnR => (\sum_j (alpha j) t)%Rbar) _ sum_alpha beta) => //.
{
rewrite -(proj2 (@Fplus_e _ _) Hfun_sum_alpha).
apply UIB_sum_dflow => j.
move : (Halpha j).
apply is_maximal_arrival_eq => //.
apply fsym => t'.
rewrite /Fplus_val /= nnRbar_valE.
by rewrite (Haa' j t').
rewrite nnRbar_valE nnRbar_dflowE.
apply /Fup_leP.
apply (@Service_for_a_jitter (sum_dflow a) (aggregate_server S)) => //.
{
rewrite -(proj2 (@Fplus_e _ _) Hfun_sum_alpha).
apply UIB_sum_dflow => j.
move : (Halpha j).
apply is_maximal_arrival_eq; [|by rewrite ffunE].
apply fsym => t'.
rewrite /Fplus_val /= nnRbar_valE.
by rewrite (Haa' j t').
}
exists (sum_dflow a), (sum_dflow d).
split; [by []| split; [by []| ]].
by exists a, d.
}
exists (sum_dflow a), (sum_dflow d).
split; [by []| split; [by []| ]].
by exists a, d.
rewrite /Fplus_val -(Hfun_sum_alpha) => t'.
by rewrite -sum_Rbar_nnRbar.
Qed.
(* TODO changer dflowen FPlus *)
......
......@@ -42,7 +42,7 @@ apply (Rbar_le_trans _ _ _ H).
by apply (proj2_sig (Rbar_ex_glb _)); exists t, d.
Qed.
Lemma is_maximal_arrival_eq (A A' : F) (alpha alpha' : Fup) :
Lemma is_maximal_arrival_eq (A A' : F) (alpha alpha' : F) :
A=1 A' -> (alpha =1 alpha') ->
is_maximal_arrival A alpha <-> is_maximal_arrival A' alpha'.
Proof.
......@@ -150,6 +150,32 @@ apply led_divl. (* A / A <= alpha *)
by rewrite -mul_div_equiv muldC.
Qed.
Corollary output_arrival_curve_mp_Fplus (S : server) (A D : dflow)
(alpha : Fup) (beta : Fplus) :
S A D ->
is_min_service S beta -> is_maximal_arrival A alpha ->
is_maximal_arrival D ((alpha : Fplus) / beta).
Proof.
(* some preprocessing *)
rewrite !UIB_alt_def.
move => SAD /(_ _ _ SAD).
rewrite -[_ <= _]/((A : Fplus) * beta <= (D : Fplus)).
move => Hbeta.
rewrite -[_ <= _]/(A <= (A : Fplus) * alpha).
move => Halpha.
rewrite -[_ <= _]/(D <= (D : Fplus) * ((alpha : Fplus) / beta)).
move: SAD => /server_leq /Fplus_leP HAD.
(* goal is now: D <= D * (alpha / beta)
under hypotheses: Halpha : A <= A * alpha, Hbeta : A * beta <= D, HAD : D <= A *)
rewrite muldC mul_div_equiv. (* goal: D / D <= alpha / beta *)
rewrite -[is_true _ ]/(is_true ((D : Fplus) / D <= (alpha : Fplus) / beta)).
refine (led_trans _ (led_div HAD Hbeta)). (* A / (A * beta) <= alpha / beta *)
rewrite muldC div_mul /=. (* A / A / beta <= alpha / beta *)
apply led_divl. (* A / A <= alpha *)
by rewrite -mul_div_equiv muldC.
Qed.
(* Lemma conv_preserves_arrival_curve f phi psi : *)
(* is_maximal_arrival f phi -> is_maximal_arrival f psi -> *)
(* is_maximal_arrival f (phi * psi)%D. *)
......
......@@ -458,7 +458,7 @@ Definition is_min_service_for (S : Fplus -> Fplus -> Prop) (beta : F) A:=
Definition is_min_service S beta := forall A, is_min_service_for S beta A.
Definition backlogged_period (A D : F) (u v : R) :=
forall x : nnR, u < x <= u + v -> (D x < A x)%Rbar.
forall x : nnR, u < x <= v -> (D x < A x)%Rbar.
(** Strict service *)
(* def p128 *)
......
......@@ -25,13 +25,56 @@ Local Open Scope dioid_scope.
Section static_priority.
(** A sum dflow equality *)
Lemma sum_dflow_equiv n A D (S : n.-server) :
S A D ->
(forall i, A i =1 D i) <-> \big[Fplus_plus/Fplus0]_i A i = \big[Fplus_plus/Fplus0]_i D i.
Proof.
move => HS.
split.
{
move => H; apply eq_big => // i _.
by apply Fplus_inj, (H i).
}
move=> H i t.
apply nnRbar_inj, Rbar_le_antisym; [|apply (nserver_leq HS)].
Admitted.
Lemma backlogged_period_eq n (S : n.-server) s t A D :
S A D ->
backlogged_period
(\big[Fplus_plus/Fplus0]_i A i) (\big[Fplus_plus/Fplus0]_i D i) s t
<-> exists i, backlogged_period (A i) (D i) s t.
Proof.
move => Hs.
split.
{
Admitted.
Lemma backlogged_period_server n (S : n.-server) s t (A D : dflow^n) :
nserver_f S A D ->
backlogged_period (sum_dflow A) (sum_dflow D) s t
<-> forall u : nnR, s < u <= t -> exists i, ((D i) u) < ((A i) u).
Proof.
move => Hs.
split.
{ move => H u Hu. admit. }
move => H u Hu.
Admitted.
Lemma backlogged_period_aggregate n (S : (n.+1).-server) A D u v :
S A D -> forall i, backlogged_period (A i) (D i) u v ->
aggregate_server S (A i) (D i) -> backlogged_period (A i) (D i) u v.
Proof.
Admitted.
Definition preemptive_SP n (S : (n.+1).-server) :=
forall i, forall t s : nnR, forall A D, S A D -> (s <= t)%Re
-> (forall u : nnR, (s <= u /\ u <= t)%Re
-> (\big[Fplus_plus/Fplus0]_j D j) u < (\big[Fplus_plus/Fplus0]_j A j) u)
-> (D i) t = (D i) s.
(* dans cette definition : on donnera comme priorité l'ordre naturel *)
(* dans cette definition : on donnera comme priorité l'ordre naturel *)
Theorem SP_residual_service_curve n (S : (n.+1).-server) A D alpha (beta : Fplus^n.+1) :
S A D -> preemptive_SP S ->
......
......@@ -62,7 +62,7 @@ Next Obligation.
apply /leFP => t /=.
apply Rplus_le_le_0_compat; [|apply nnR_pos].
rewrite -(Rmult_0_r 0).
apply Rmult_le_compat; [ | | apply nnR_pos | apply nnR_pos].
apply Rmult_le_compat; [ | | apply nnR_pos | apply nnR_pos].
apply Rle_refl. apply Rle_refl.
Qed.
Next Obligation.
......@@ -173,13 +173,13 @@ case Rbar_le_dec => Habt.
by apply Rmult_le_compat_l.
}
by rewrite Rbar_plus_0_r.
}
}
apply nnRbar_inj => /=.
apply Rbar_le_antisym.
{
set F := F_min_conv _ _.
by case F.
}
by case F.
}
rewrite /Fplus_min_conv /= /F_min_conv /= /Rbar_glb.
case Rbar_ex_glb => l [Hl Hl'] /=.
apply Hl' => y [u [v [Huv ->]]].
......@@ -353,7 +353,7 @@ apply nnRbar_inj, Rbar_le_antisym.
move: Pd => /Rbar_le_bool_Rbar_le Pd.
move=> /(_ (mk_nnR _ Pd + mk_nnR 1 Rle_0_1)%nnR).
rewrite -Hl''; apply.
rewrite Heqf => /=.
rewrite Heqf /Fplus_val /=.
case Rbar_le_dec => //=.
move=> H; exfalso; move: H.
move: (nnR_pos t).
......@@ -371,7 +371,7 @@ apply nnRbar_inj, Rbar_le_antisym.
rewrite /Glb_nnRbar.
case ex_glb_nnRbar => l' [Hl' Hl''].
apply Hl'.
rewrite Heqf => /=.
rewrite Heqf /Fplus_val /=.
case Rbar_le_dec => //=.
move=> H; exfalso; move: H.
move: (nnR_pos t).
......@@ -393,7 +393,7 @@ apply Rbar_le_antisym.
move => u Hu.
apply Rbar_not_lt_le => Hud.
move : Hu; apply Rbar_lt_not_le.
rewrite Heqf /del /=.
rewrite Heqf /del /Fplus_val /=.
case Rbar_le_dec.
{ by move => _; rewrite Rmult_0_r Rplus_0_l. }
move => /Rbar_not_le_lt; rewrite Rplus_0_l => Hfal.
......@@ -423,16 +423,23 @@ case_eq (andb (b == 0%Re :> R) (r == 0%Re :> R)); last first.
apply hDev_delta_aux.
}
move => /eqP /Rdichotomy [] => H.
{ exfalso; move : H; apply Rle_not_lt, nnR_pos. }
{ exfalso; move : H; apply Rle_not_lt, nnR_pos. }
admit.
}
Admitted.
Lemma sum_gamma_h r r' b b' :
(gamma_h r b + gamma_h r' b')%F = gamma_h (r + r') (b + b').
Proof.
apply functional_extensionality => t.
rewrite /Fplus_val /= /F_plus /Rbar_plus /= Rbar_finite_eq; lra.
Qed.
Lemma sum_gamma r r' b b' :
(gamma_h r b + gamma_h r' b')%Fp = gamma_h (r + r') (b + b').
Proof.
apply Fplus_inj => t; apply nnRbar_inj; rewrite /= Rbar_finite_eq; lra.
apply Fplus_inj => t.
apply nnRbar_inj; rewrite /Rbar_plus /= Rbar_finite_eq; lra.
Qed.
Fact Rmax_sym x : Rmax x x = x.
......@@ -538,6 +545,6 @@ Qed.
(* Admitted. *)
Definition linearF := (delta_min_conv, delta_prop_deconv, deconv_gamma_delta,
sum_gamma_h, hDev_delta).
sum_gamma, sum_gamma_h, hDev_delta, nnRbar_valE).
End usual_functions.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment