Commit 728aedee authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Almost done with EDF convergence

parent 0540f45a
......@@ -387,10 +387,10 @@ Module ResponseTimeIterationEDF.
{
intros x1 x2 LEinit LE.
assert (LEinit': all_le (initial_state ts) x2).
(*assert (LEinit': all_le (initial_state ts) x2).
{
by unfold transitive in TRANS; apply TRANS with (y := x1).
}
}*)
move: LE => /andP [/eqP ZIP LE]; unfold all_le.
assert (UNZIP': unzip1 (edf_rta_iteration x1) = unzip1 (edf_rta_iteration x2)).
......@@ -466,11 +466,33 @@ Module ResponseTimeIterationEDF.
rewrite -EQinit; unfold valid_sporadic_taskset.
move => tsk /mapP IN. destruct IN as [p INinit EQ]; subst.
by move: INinit => /mapP INinit; destruct INinit as [tsk INtsk]; subst; apply VALID.
} clear LEinit.
}
assert (GE_COST: all (fun p => task_cost (fst p) <= snd p) ((tsk0, R0) :: x1')).
{
admit.
clear LE; move: LEinit => /andP [/eqP UNZIP' LE].
move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
specialize (LE (tsk0, R0)).
apply/(all_nthP (tsk0,R0)).
intros j LTj; generalize UNZIP'; simpl; intro SIZE'.
have F := @f_equal _ _ size (unzip1 (initial_state ts)).
apply F in SIZE'; clear F; rewrite /= 3!size_map in SIZE'.
exploit LE; [by rewrite size_map /= | |].
{
rewrite size_zip size_map /= SIZE' minnn.
by simpl in LTj; apply LTj.
}
clear LE; intro LE.
unfold initial_state in LE.
have MAP := @nth_map _ tsk0 _ (tsk0,R0).
rewrite MAP /= in LE;
[clear MAP | by rewrite SIZE'; simpl in LTj].
apply leq_trans with (n := task_cost (nth tsk0 ts j));
[apply eq_leq; f_equal | by done].
have MAP := @nth_map _ (tsk0, R0) _ tsk0 (fun x => fst x).
rewrite -MAP; [clear MAP | by done].
unfold unzip1 in UNZIP'; rewrite -UNZIP'; f_equal.
clear -ts; induction ts; [by done | by simpl; f_equal].
}
move: GE_COST => /allP GE_COST.
......
......@@ -315,7 +315,8 @@ Module ResponseTimeIterationFP.
apply leq_trans with (n := W task_cost task_period i R x1);
first by apply geq_minl.
specialize (VALID i IN); des.
by apply W_monotonic; try (by ins); apply GE_COST.
by apply W_monotonic; try (by ins);
[by apply GE_COST | by apply leqnn].
}
{
apply leq_trans with (n := x1 - task_cost tsk + 1);
......
......@@ -698,67 +698,6 @@ Proof.
}
Qed.
(*Lemma mem_unzip {T: eqType} (X Y: seq T) x y :
uniq X -> uniq Y ->
x \in X -> y \in Y ->
(x, y) \in (zip X Y).
Proof.
intros UNIQx UNIQy INx INy.
generalize dependent x.
generalize dependent y.
generalize dependent Y.
induction X; first by ins.
induction Y; first by ins.
ins. apply IHY.
destruct Y; first by ins.
{
rewrite in_cons in INy.
move: INy => /orP [/eqP HEADy | TAILy]; subst;
move: INx => /orP [/eqP HEADx | TAILx]; subst.
{
by rewrite in_cons eq_refl orTb.
}
{
admit.
}
{
admit.
}
{
simpl in *.
destruct (x == a) eqn:EQx, (y == a0) eqn:EQy.
{
move: EQx => /eqP EQx; subst.
move: EQy => /eqP EQy; subst.
by rewrite in_cons; apply/orP; left.
}
{
simpl in *.
rewrite in_cons in INy.
simpl.
Qed.
Lemma index_zip1 {T: eqType} (X Y: seq T) x y :
uniq X ->
uniq Y ->
(x, y) \in (zip X Y) ->
index (x, y) (zip X Y) = index x X.
Proof.
admit.
Qed.
Lemma index_zip2 {T:eqType} (X Y: seq T) x y:
uniq X ->
uniq Y ->
(x, y) \in (zip X Y) ->
index (x, y) (zip X Y) = index y Y.
Proof.
admit.
Qed.*)
Definition no_intersection {T: eqType} (l1 l2: seq T) :=
~~ has (mem l1) l2.
......
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