Commit be861aca authored by Vedant Chavda's avatar Vedant Chavda

some proofs

parent 93aad096
Pipeline #31989 failed with stages
in 13 minutes and 45 seconds
......@@ -238,22 +238,87 @@ Section todo_name.
intros *.
rewrite /task_arrivals_up_to /task_arrivals_between.
pose proof task_arrivals_at_size as SIZE_AT.
rewrite /task_arrivals_at in SIZE_AT.
rewrite /task_arrivals_at in SIZE_AT.
(* This proof looks a bit tough. *)
Admitted.
Lemma uniq_task_arrivals_tsk :
forall tsk t,
uniq (task_arrivals_up_to arr_seq tsk t).
Proof.
intros *.
apply filter_uniq.
now apply arrivals_uniq.
Qed.
Lemma todo_name4 :
forall tsk j' n,
valid_offset arr_seq tsk ->
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
job_task j' = tsk ->
job_arrival j' = task_offset tsk + n * task_period tsk ->
job_index arr_seq j' = n.
Proof.
Admitted.
Lemma todo_name5 :
forall tsk n j' t,
arrives_in arr_seq j' ->
job_task j' = tsk ->
job_index arr_seq j' = n ->
t >= job_arrival j' ->
nth j (task_arrivals_up_to arr_seq tsk t) n = j'.
Proof.
intros * ARR TSK IND T_G.
rewrite /job_index in IND.
rewrite -IND.
Admitted.
Lemma exists_job_in_task_arrivals_at :
forall tsk t,
valid_offset arr_seq tsk ->
valid_period tsk ->
respects_periodic_task_model arr_seq tsk ->
(exists n, t = task_offset tsk + n * task_period tsk) ->
exists j',
job_task j' = tsk /\
task_arrivals_at arr_seq tsk t = [::j'].
Proof.
intros * T.
intros * OFFSET PERIOD PERIODIC T.
destruct T as [n T].
exists (nth j (task_arrivals_up_to arr_seq tsk t) n).
split.
pose proof only_j as J_AT.
exists (nth j (task_arrivals_up_to arr_seq tsk t) n).
have SM_TSK : job_task (nth j (task_arrivals_up_to arr_seq tsk t) n) = tsk.
{ have IN : nth j (task_arrivals_up_to arr_seq tsk t) n \in task_arrivals_up_to arr_seq tsk t.
{ rewrite -index_mem index_uniq; try by rewrite T task_arrivals_up_to_size; ssromega.
now apply uniq_task_arrivals_tsk. }
rewrite mem_filter in IN.
now move : IN => /andP [/eqP TSK IN_ARR].
}
split => //.
specialize (jobs_exists_later n tsk) => LATER_JB.
feed_n 3 LATER_JB => //.
move : LATER_JB => [j' [ARR' [TSK' J'ARR]]].
move : (J'ARR) => IND.
apply todo_name4 in IND => //.
set nj := nth j (task_arrivals_up_to arr_seq tsk t) n.
have IND_JB : job_index arr_seq nj = n.
rewrite /job_index /nj.
have EQ_SEQ : (task_arrivals_up_to_job_arrival arr_seq (nth j (task_arrivals_up_to arr_seq tsk t) n)) = task_arrivals_up_to arr_seq tsk t.
rewrite /task_arrivals_up_to_job_arrival SM_TSK.
rewrite -> todo_name5 with (j' := j') => //; try by ssromega.
now rewrite J'ARR -T.
rewrite EQ_SEQ.
apply index_uniq.
rewrite T task_arrivals_up_to_size; ssromega.
now apply uniq_task_arrivals_tsk.
rewrite -IND in IND_JB.
apply equal_index_implies_equal_jobs in IND_JB => //.
rewrite IND_JB.
apply only_j => //.
now rewrite T.
admit.
admit. (* both admits provable. *)
Admitted.
Lemma all_t_cases :
......
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