Commit 21734291 authored by jonathan julou's avatar jonathan julou

removed a long proof

parent a96e1bf6
Pipeline #18856 failed with stages
in 3 minutes and 41 seconds
......@@ -153,6 +153,28 @@ Section Prefixverif.
(* --- IV --- LEMMAS --- IV --- *)
(*========================================================================*)
Local Lemma utilitaire: forall j j' t t',
completes_at sched j t -> completes_at sched j' t' -> completed_by sched j (maxn t t').
Proof.
intros j j' t t' Q R.
assert (U: maxn t t' >= t). destruct (t <= t') eqn:E.
assert (V: maxn t t' = t'). apply/maxn_idPr. exact E.
rewrite V. exact E. assert (U': t >= t'). ssromega.
assert (V: maxn t t' = t). apply/maxn_idPl. exact U'.
rewrite V. apply leqnn.
unfold completed_by. unfold service.
unfold completes_at in Q. unfold service in Q.
assert (J: service_during sched j 0 t <= service_during sched j 0 (maxn t t')).
unfold service_during.
unfold service_during in Q.
apply sum.extend_sum. apply leqnn. exact U.
apply leq_trans with (service_during sched j 0 t). ssromega.
exact J.
Qed.
Lemma periodic_jitter_infinite: forall (tsk:Task),
( forall t, respects_periodic_jitter_task_model_up_to_t tsk t )
->
......@@ -168,6 +190,7 @@ Section Prefixverif.
assert (P1: correction_t tsk j (t))
by (apply P).
apply P1. unfold completes_at in Q. unfold completed_by. ssromega.
- intros j j'.
assert (Q: exists t, completes_at sched j t). apply all_jobs_complete.
destruct Q as [t Q].
......@@ -176,37 +199,9 @@ Section Prefixverif.
assert (P2: injection_t tsk j j' (maxn t t'))
by (apply P).
apply P2.
+ assert (U: maxn t t' >= t). destruct (t <= t') eqn:E.
assert (V: maxn t t' = t'). apply/maxn_idPr. exact E.
rewrite V. exact E. assert (U': t >= t'). ssromega.
assert (V: maxn t t' = t). apply/maxn_idPl. exact U'.
rewrite V. apply leqnn.
unfold completed_by. unfold service.
unfold completes_at in Q. unfold service in Q.
assert (J: service_during sched j 0 t <= service_during sched j 0 (maxn t t')).
unfold service_during.
unfold service_during in Q.
apply sum.extend_sum. apply leqnn. exact U.
apply leq_trans with (service_during sched j 0 t). ssromega.
exact J.
+ assert (U: maxn t t' >= t'). destruct (t <= t') eqn:E.
assert (V: maxn t t' = t'). apply/maxn_idPr. exact E.
rewrite V. apply leqnn. assert (U': t >= t'). ssromega.
assert (V: maxn t t' = t). apply/maxn_idPl. exact U'.
rewrite V. exact U'.
unfold completed_by. unfold service.
unfold completes_at in R. unfold service in R.
assert (J: service_during sched j' 0 t' <= service_during sched j' 0 (maxn t t')).
unfold service_during.
unfold service_during in R.
apply sum.extend_sum. apply leqnn. exact U.
apply leq_trans with (service_during sched j' 0 t'). ssromega.
exact J.
+ apply utilitaire with j'. exact Q. exact R.
+ rewrite maxnC. apply utilitaire with j. exact R. exact Q.
- intro n.
assert (P3: surjection_t tsk n (offset + n * period +jitter) )
by (apply P).
......
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