# Library prosa.analysis.facts.completes_at

Require Export prosa.analysis.definitions.busy_interval.classical.
Require Export prosa.analysis.facts.model.preemption.
In this file, we prove a few useful lemmas about the completes_at predicate.
Section CompletesAtLemmas.
Consider any type of jobs with a priority relation.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JLFP_policy Job}.
Consider any kind of uniprocessor state model.
Context {PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Consider any arrival sequence with consistent non-duplicate arrivals
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Next, consider any schedule of this arrival sequence ...
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
... where jobs do not execute before their arrival or after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
If a job j completes at time t > 0, then it must have been scheduled at time t - 1.
Lemma scheduled_at_precedes_completes_at :
∀ (j : Job) (t : instant),
t > 0 →
completes_at sched j t →
scheduled_at sched j t.-1.
Proof.
move⇒ j t POS COMP.
move: COMP; rewrite /completes_at /completed_by -ltnNge.
destruct t as [|t]; first by lia.
rewrite -pred_Sn -service_last_plus_before.
have ->: t.+1 == 0 = false by lia.
rewrite orbF ⇒ /andP [A B]; move: (leq_trans A B).
rewrite -addn1 leq_add2l ⇒ SP.
by apply service_at_implies_scheduled_at.
Qed.
Next, we show that any job j can be completed at most once.
Lemma job_completes_at_most_once :
∀ (j : Job) (t1 t2 : instant),
\sum_(t1 ≤ t < t2) completes_at sched j t ≤ 1.
Proof.
move⇒ j t1 t2; move_neq_up TWO.
apply sum_ge_2_nat in TWO; last by intros; destruct completes_at.
destruct TWO as [to1 [to2 [LE1 [LE2 [LE3 [EQ1 EQ2]]]]]].
move: EQ1 EQ2; rewrite !eqb1 ⇒ /andP [_ C1] /andP [NC2 _].
have EQ: (to2 == 0) = false; [by lia | rewrite EQ orbF in NC2; clear EQ].
move: NC2 ⇒ /negP NC2; apply:NC2.
by apply: completion_monotonic; try exact C1; lia.
Qed.
At any time t > 0, at most one job satisfying predicate P and arriving before time B can complete.
Lemma only_one_job_completes_at_a_time :
∀ (P : pred Job) (t B : instant),
t > 0 →
\sum_(j <- arrivals_before arr_seq B | P j) completes_at sched j t ≤ 1.
Proof.
move⇒ P t B POS; rewrite big_seq_cond big_mkcond //=.
move_neq_up TWO; apply sum_ge_2_seq in TWO; first last.
{ by intros; destruct (_ \in _), P, completes_at. }
{ by apply arrivals_uniq. }
destruct TWO as [j1 [j2 [NEQ [IN1 [IN2 [CA1 CA2]]]]]].
rewrite IN1 andTb in CA1; rewrite IN2 andTb in CA2.
destruct (P j1), (P j2) ⇒ //.
move: CA1 CA2; rewrite !eqb1 ⇒ CA1 CA2; apply scheduled_at_precedes_completes_at in CA1, CA2 ⇒ //.
move: NEQ ⇒ /negP NEQ; apply: NEQ; apply/eqP.
by apply: H_uniprocessor_proc_model.
Qed.
Consider a valid preemption model.
Context `{JobPreemptable Job}.
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
We prove that any completion time is a preemption time.
Lemma completetion_time_is_preemption_time :
∀ (j : Job) (t : instant),
completes_at sched j t →
preemption_time arr_seq sched t.
Proof.
move⇒ s t CA; move: (CA) ⇒ /andP [NCOMP COMP].
have [Z|POS] := posnP t.
{ subst. apply zero_is_pt ⇒ //. }
{ eapply scheduled_at_precedes_completes_at in CA ⇒ //.
apply completed_implies_not_scheduled in COMP ⇒ //.
apply/negPn/negP ⇒ NPI.
eapply neg_pt_scheduled_before in NPI ⇒ //.
by rewrite NPI in COMP.
}
Qed.
No higher-or-equal priority job that arrived before the start of a busy-interval prefix can complete during the prefix.
Lemma no_early_hep_job_completes_during_busy_prefix :
∀ (j : Job) (t t1 t2 : instant),
busy_interval_prefix arr_seq sched j t1 t2 →
t1 < t ≤ t2 →
∀ jhp : Job,
(jhp \in arrivals_before arr_seq t1) →
hep_job jhp j →
~~ completes_at sched jhp t.
Proof.
move⇒ j t t1 t2 BUSY NEQ jhp ARR HEP.
rewrite /completes_at.
have ->: t == 0 = false by lia.
rewrite orbF negb_and; apply/orP; left.
apply/negPn; apply completion_monotonic with t1; first by lia.
apply BUSY ⇒ //.
{ by apply: in_arrivals_implies_arrived. }
{ by apply in_arrivals_implies_arrived_between in ARR ⇒ //. }
Qed.
End CompletesAtLemmas.