diff --git a/analysis/definitions/schedule_prefix.v b/analysis/definitions/schedule_prefix.v index 38cd8797f40684c856df3c21688baefb12c404f0..570b86668e6b51d68dc65fa6d358218a9eeaa855 100644 --- a/analysis/definitions/schedule_prefix.v +++ b/analysis/definitions/schedule_prefix.v @@ -20,7 +20,7 @@ Section PrefixDefinition. (** In other words, two schedules with a shared prefix are completely interchangeable w.r.t. whether a job is scheduled (in the prefix). *) - Fact identical_prefix_scheduled_at: + Fact identical_prefix_scheduled_at : forall sched sched' h, identical_prefix sched sched' h -> forall j t, @@ -33,16 +33,10 @@ Section PrefixDefinition. (** Trivially, any prefix of an identical prefix is also an identical prefix. *) - Fact identical_prefix_inclusion: - forall sched sched' h, - identical_prefix sched sched' h -> - forall h', - h' <= h -> - identical_prefix sched sched' h'. - Proof. - move=> sched sched' h IDENT h' INCL t LT_h'. - apply IDENT. - now apply (leq_trans LT_h'). - Qed. + Fact identical_prefix_inclusion : + forall sched sched' h h', + h' <= h -> + identical_prefix sched sched' h -> identical_prefix sched sched' h'. + Proof. by move=> sched sched' h h' h'_le_h + t t_lt_h'; apply; apply: leq_trans h'_le_h. Qed. End PrefixDefinition. diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v index 44639d4683907ba20235cd4116dde3463c1ce9bf..05335ff2b4c38665df66dd9eb23bff17dfc19bc5 100644 --- a/analysis/facts/behavior/arrivals.v +++ b/analysis/facts/behavior/arrivals.v @@ -16,10 +16,7 @@ Section ArrivalPredicates. forall j t1 t2, arrived_between j t1 t2 -> arrived_before j t2. - Proof. - move=> j t1 t2. - now rewrite /arrived_before /arrived_between => /andP [_ CLAIM]. - Qed. + Proof. by move=> ? ? ? /andP[]. Qed. (** A job that arrives before a time [t] certainly has arrived by time [t]. *) @@ -27,17 +24,13 @@ Section ArrivalPredicates. forall j t, arrived_before j t -> has_arrived j t. - Proof. - move=> j t. - rewrite /arrived_before /has_arrived. - now apply ltnW. - Qed. + Proof. move=> ? ?; exact: ltnW. Qed. End ArrivalPredicates. (** In this section, we relate job readiness to [has_arrived]. *) Section Arrived. - + (** Consider any kinds of jobs and any kind of processor state. *) Context {Job : JobType} {PState : ProcessorState Job}. @@ -55,65 +48,36 @@ Section Arrived. Lemma any_ready_job_is_pending: forall j t, job_ready sched j t -> pending sched j t. - Proof. - move: jr => [is_ready CONSISTENT]. - move=> j t READY. - apply CONSISTENT. - by exact READY. - Qed. + Proof. move: jr => [? +] /= ?; exact. Qed. (** Next, we observe that a given job must have arrived to be ready... *) - Lemma ready_implies_arrived: + Lemma ready_implies_arrived : forall j t, job_ready sched j t -> has_arrived j t. - Proof. - move=> j t READY. - move: (any_ready_job_is_pending j t READY). - by rewrite /pending => /andP [ARR _]. - Qed. + Proof. by move=> ? ? /any_ready_job_is_pending => /andP[]. Qed. (** ...and lift this observation also to the level of whole schedules. *) Lemma jobs_must_arrive_to_be_ready: - jobs_must_be_ready_to_execute sched -> - jobs_must_arrive_to_execute sched. - Proof. - rewrite /jobs_must_be_ready_to_execute /jobs_must_arrive_to_execute. - move=> READY_IF_SCHED j t SCHED. - move: (READY_IF_SCHED j t SCHED) => READY. - by apply ready_implies_arrived. - Qed. + jobs_must_be_ready_to_execute sched -> jobs_must_arrive_to_execute sched. + Proof. move=> READY ? ? ?; exact/ready_implies_arrived/READY. Qed. (** Furthermore, in a valid schedule, jobs must arrive to execute. *) - Corollary valid_schedule_implies_jobs_must_arrive_to_execute: - forall arr_seq, - valid_schedule sched arr_seq -> - jobs_must_arrive_to_execute sched. - Proof. - move=> arr_seq [??]. - by apply jobs_must_arrive_to_be_ready. - Qed. - + Corollary valid_schedule_implies_jobs_must_arrive_to_execute : + forall arr_seq, + valid_schedule sched arr_seq -> jobs_must_arrive_to_execute sched. + Proof. move=> ? [? ?]; exact: jobs_must_arrive_to_be_ready. Qed. + (** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *) Corollary backlogged_implies_arrived: forall j t, backlogged sched j t -> has_arrived j t. - Proof. - rewrite /backlogged. - move=> j t /andP [READY _]. - now apply ready_implies_arrived. - Qed. + Proof. move=> ? ? /andP[? ?]; exact: ready_implies_arrived. Qed. (** Similarly, since backlogged jobs are by definition pending, any backlogged job must be incomplete. *) Lemma backlogged_implies_incomplete: forall j t, backlogged sched j t -> ~~ completed_by sched j t. - Proof. - move=> j t BACK. - have suff: pending sched j t. - - by move /andP => [_ INCOMP]. - - apply; move: BACK => /andP [READY _]. - by apply any_ready_job_is_pending. - Qed. + Proof. by move=> ? ? /andP[/any_ready_job_is_pending /andP[]]. Qed. End Arrived. @@ -147,12 +111,9 @@ Section ArrivalSequencePrefix. t <= t2 -> arrivals_between arr_seq t1 t2 = arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2. - Proof. - unfold arrivals_between; intros t1 t t2 GE LE. - by rewrite (@big_cat_nat _ _ _ t). - Qed. + Proof. by move=> ? ? ? ? ?; rewrite -big_cat_nat. Qed. - (** We also prove a stronger version of the above lemma + (** We also prove a stronger version of the above lemma in the case of arrivals that satisfy a predicate [P]. *) Lemma arrivals_P_cat: forall P t t1 t2, @@ -160,11 +121,10 @@ Section ArrivalSequencePrefix. arrivals_between_P arr_seq P t1 t2 = arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2. Proof. - intros P t t1 t2 INEQ. - rewrite -filter_cat. - now rewrite -arrivals_between_cat => //; lia. + move=> P t t1 t2. + by move=> /andP[? ?]; rewrite -filter_cat -arrivals_between_cat// ltnW. Qed. - + (** The same observation applies to membership in the set of arrived jobs. *) Lemma arrivals_between_mem_cat: @@ -173,63 +133,77 @@ Section ArrivalSequencePrefix. t <= t2 -> j \in arrivals_between arr_seq t1 t2 = (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2). - Proof. - by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t). - Qed. + Proof. by move=> ? ? ? ? ? ?; rewrite -arrivals_between_cat. Qed. (** We observe that we can grow the considered interval without "losing" any arrived jobs, i.e., membership in the set of arrived jobs is monotonic. *) - Lemma arrivals_between_sub: + Lemma arrivals_between_sub : forall j t1 t1' t2 t2', t1' <= t1 -> t2 <= t2' -> j \in arrivals_between arr_seq t1 t2 -> j \in arrivals_between arr_seq t1' t2'. Proof. - intros j t1 t1' t2 t2' GE1 LE2 IN. - move: (leq_total t1 t2) => /orP [BEFORE | AFTER]; - last by rewrite /arrivals_between big_geq // in IN. - rewrite /arrivals_between. - rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)]. - rewrite mem_cat; apply/orP; right. - rewrite -> big_cat_nat with (n := t2); [simpl | by done | by done]. - by rewrite mem_cat; apply/orP; left. + move=> j t1 t1' t2 t2' t1'_le_t1 t2_le_t2' j_in. + have /orP[t2_le_t1|t1_le_t2] := leq_total t2 t1. + { by move: j_in; rewrite /arrivals_between big_geq. } + rewrite (arrivals_between_mem_cat _ _ t1)// ?mem_cat. + 2:{ exact: leq_trans t2_le_t2'. } + rewrite [X in _ || X](arrivals_between_mem_cat _ _ t2)// mem_cat. + by rewrite j_in orbT. Qed. End Composition. - + (** Next, we relate the arrival prefixes with job arrival times. *) Section ArrivalTimes. (** Assume that job arrival times are consistent. *) - Hypothesis H_consistent_arrival_times: - consistent_arrival_times arr_seq. - - (** First, we prove that if a job belongs to the prefix - (jobs_arrived_before t), then it arrives in the arrival sequence. *) + Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq. + + (** To simplify subsequent proofs, we restate the + [H_consistent_arrival_times] assumption as a trivial corollary. *) + Lemma job_arrival_at : + forall {j t}, + j \in arrivals_at arr_seq t -> job_arrival j = t. + Proof. exact: H_consistent_arrival_times. Qed. + + (** First, we observe that any job in the set of all arrivals + between time instants [t1] and [t2] must arrive in the + interval <<[t1,t2)>>. *) + Lemma job_arrival_between : + forall {j t1 t2}, + j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j < t2. + Proof. by move=> ? ? ? /mem_bigcat_nat_exists[i [/job_arrival_at <-]]. Qed. + + (** For convenience, we restate the left bound of the above lemma... *) + Corollary job_arrival_between_ge : + forall {j t1 t2}, + j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j. + Proof. by move=> ? ? ? /job_arrival_between/andP[]. Qed. + + (** ... as well as the right bound separately as corollaries. *) + Corollary job_arrival_between_lt : + forall {j t1 t2}, + j \in arrivals_between arr_seq t1 t2 -> job_arrival j < t2. + Proof. by move=> ? ? ? /job_arrival_between/andP[]. Qed. + + (** Second, we prove that if a job belongs to the prefix + (jobs_arrived_before t), then it arrives in the arrival + sequence. *) Lemma in_arrivals_implies_arrived: forall j t1 t2, j \in arrivals_between arr_seq t1 t2 -> arrives_in arr_seq j. - Proof. - rename H_consistent_arrival_times into CONS. - intros j t1 t2 IN. - apply mem_bigcat_nat_exists in IN. - move: IN => [arr [IN _]]. - by exists arr. - Qed. - + Proof. by move=> ? ? ? /mem_bigcat_nat_exists[arr [? _]]; exists arr. Qed. + (** We also prove a weaker version of the above lemma. *) Lemma in_arrseq_implies_arrives: forall t j, j \in arr_seq t -> arrives_in arr_seq j. - Proof. - move => t j J_ARR. - exists t. - now rewrite /arrivals_at. - Qed. + Proof. by move=> t ? ?; exists t. Qed. (** Next, we prove that if a job belongs to the prefix (jobs_arrived_between t1 t2), then it indeed arrives between t1 and @@ -238,13 +212,7 @@ Section ArrivalSequencePrefix. forall j t1 t2, j \in arrivals_between arr_seq t1 t2 -> arrived_between j t1 t2. - Proof. - rename H_consistent_arrival_times into CONS. - intros j t1 t2 IN. - apply mem_bigcat_nat_exists in IN. - move: IN => [t0 [IN /= LT]]. - by apply CONS in IN; rewrite /arrived_between IN. - Qed. + Proof. by move=> ? ? ? /mem_bigcat_nat_exists[t0 [/job_arrival_at <-]]. Qed. (** Similarly, if a job belongs to the prefix (jobs_arrived_before t), then it indeed arrives before time t. *) @@ -252,11 +220,7 @@ Section ArrivalSequencePrefix. forall j t, j \in arrivals_before arr_seq t -> arrived_before j t. - Proof. - intros j t IN. - have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between. - by rewrite /arrived_between /=. - Qed. + Proof. by move=> ? ? /in_arrivals_implies_arrived_between. Qed. (** Similarly, we prove that if a job from the arrival sequence arrives before t, then it belongs to the sequence (jobs_arrived_before t). *) @@ -266,27 +230,22 @@ Section ArrivalSequencePrefix. arrived_between j t1 t2 -> j \in arrivals_between arr_seq t1 t2. Proof. - rename H_consistent_arrival_times into CONS. - move => j t1 t2 [a_j ARRj] BEFORE. - have SAME := ARRj; apply CONS in SAME; subst a_j. - now apply mem_bigcat_nat with (j := (job_arrival j)). + move=> j t1 t2 [a_j arrj] before; apply: mem_bigcat_nat (arrj). + by rewrite -(job_arrival_at arrj). Qed. - + (** Any job in arrivals between time instants [t1] and [t2] must arrive in the interval <<[t1,t2)>>. *) - Lemma job_arrival_between: + Lemma job_arrival_between_P: forall j P t1 t2, j \in arrivals_between_P arr_seq P t1 t2 -> t1 <= job_arrival j < t2. Proof. - intros * ARR. - move: ARR; rewrite mem_filter => /andP [PJ JARR]. - apply mem_bigcat_nat_exists in JARR. - move : JARR => [i [ARR INEQ]]. - apply H_consistent_arrival_times in ARR. - now rewrite ARR. + move=> j P t1 t2. + rewrite mem_filter => /andP[Pj /mem_bigcat_nat_exists[i [+ iitv]]]. + by move=> /job_arrival_at ->. Qed. - + (** Any job [j] is in the sequence [arrivals_between t1 t2] given that [j] arrives in the interval <<[t1,t2)>>. *) Lemma job_in_arrivals_between: @@ -295,23 +254,18 @@ Section ArrivalSequencePrefix. t1 <= job_arrival j < t2 -> j \in arrivals_between arr_seq t1 t2. Proof. - intros * ARR INEQ. - apply mem_bigcat_nat with (j := job_arrival j) => //. - move : ARR => [t J_IN]. - now rewrite -> H_consistent_arrival_times with (t := t). + move=> j t1 t2 [t jarr] jitv; apply: mem_bigcat_nat (jarr). + by rewrite -(job_arrival_at jarr). Qed. - + (** Next, we prove that if the arrival sequence doesn't contain duplicate jobs, the same applies for any of its prefixes. *) Lemma arrivals_uniq: arrival_sequence_uniq arr_seq -> forall t1 t2, uniq (arrivals_between arr_seq t1 t2). Proof. - rename H_consistent_arrival_times into CONS. - unfold arrivals_up_to; intros SET t1 t2. - apply bigcat_nat_uniq; first by done. - intros x t t' IN1 IN2. - by apply CONS in IN1; apply CONS in IN2; subst. + move=> SET t1 t2; apply: bigcat_nat_uniq => // j t1' t2'. + by move=> /job_arrival_at <- /job_arrival_at <-. Qed. (** Also note that there can't by any arrivals in an empty time interval. *) @@ -319,27 +273,23 @@ Section ArrivalSequencePrefix. forall t1 t2, t1 >= t2 -> arrivals_between arr_seq t1 t2 = [::]. - Proof. - by intros ? ? GE; rewrite /arrivals_between big_geq. - Qed. - + Proof. by move=> ? ? ?; rewrite /arrivals_between big_geq. Qed. + (** Given jobs [j1] and [j2] in [arrivals_between_P arr_seq P t1 t2], the fact that [j2] arrives strictly before [j1] implies that [j2] also belongs in the sequence [arrivals_between_P arr_seq P t1 (job_arrival j1)]. *) - Lemma arrival_lt_implies_job_in_arrivals_between_P: + Lemma arrival_lt_implies_job_in_arrivals_between_P : forall (j1 j2 : Job) (P : Job -> bool) (t1 t2 : instant), - (j1 \in arrivals_between_P arr_seq P t1 t2) -> - (j2 \in arrivals_between_P arr_seq P t1 t2) -> + j1 \in arrivals_between_P arr_seq P t1 t2 -> + j2 \in arrivals_between_P arr_seq P t1 t2 -> job_arrival j2 < job_arrival j1 -> j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1). Proof. - intros * J1_IN J2_IN ARR_LT. - rewrite mem_filter in J2_IN; move : J2_IN => /andP [PJ2 J2ARR] => //. - rewrite mem_filter; apply /andP; split => //. - apply mem_bigcat_nat_exists in J2ARR; move : J2ARR => [i [J2_IN INEQ]]. - apply mem_bigcat_nat with (j := i) => //. - apply H_consistent_arrival_times in J2_IN; rewrite J2_IN in ARR_LT. - now lia. + move=> j1 j2 P t1 t2. + rewrite !mem_filter => /andP[_ j1arr] /andP[Pj2 j2arr] arr_lt. + rewrite Pj2/=; apply: job_in_arrivals_between. + - exact: in_arrivals_implies_arrived j2arr. + - by rewrite (job_arrival_between_ge j2arr). Qed. End ArrivalTimes. diff --git a/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v index f7ce9f59f7a5f299c4c95caade2467ae4633f22f..29ff9170af990be57e50a9c2c32eced060230b0f 100644 --- a/analysis/facts/behavior/completion.v +++ b/analysis/facts/behavior/completion.v @@ -28,11 +28,7 @@ Section CompletionFacts. t <= t' -> completed_by sched j t -> completed_by sched j t'. - Proof. - move => t t' LE. rewrite /completed_by /service => COMP. - apply leq_trans with (n := service_during sched j 0 t); auto. - by apply service_monotonic. - Qed. + Proof. move=> ? ? ? /leq_trans; apply; exact: service_monotonic. Qed. (** We prove that if [j] is not completed by [t'], then it's also not completed by any earlier instant. *) @@ -41,11 +37,7 @@ Section CompletionFacts. t <= t' -> ~~ completed_by sched j t' -> ~~ completed_by sched j t. - Proof. - move => t t' LE. - apply contra. - by apply completion_monotonic. - Qed. + Proof. move=> ? ? ?; exact/contra/completion_monotonic. Qed. (** We observe that being incomplete is the same as not having received sufficient service yet... *) @@ -53,9 +45,7 @@ Section CompletionFacts. forall t, service sched j t < job_cost j <-> ~~ completed_by sched j t. - Proof. - move=> t. by split; rewrite /completed_by; [rewrite -ltnNge // | rewrite ltnNge //]. - Qed. + Proof. by move=> ?; rewrite -ltnNge. Qed. (** ...which is also the same as having positive remaining cost. *) Lemma incomplete_is_positive_remaining_cost: @@ -63,7 +53,7 @@ Section CompletionFacts. ~~ completed_by sched j t <-> remaining_cost sched j t > 0. Proof. - move=> t. by split; rewrite /remaining_cost -less_service_than_cost_is_incomplete subn_gt0 //. + by move=> ?; rewrite -less_service_than_cost_is_incomplete subn_gt0. Qed. (** Trivially, it follows that an incomplete job has a positive cost. *) @@ -72,11 +62,8 @@ Section CompletionFacts. ~~ completed_by sched j t -> job_cost_positive j. Proof. - move=> t INCOMP. - apply: (leq_trans _); - last by apply leq_subr. - apply incomplete_is_positive_remaining_cost. - exact INCOMP. + move=> t INCOMP; apply: leq_trans (leq_subr (service sched j t) _). + by rewrite -incomplete_is_positive_remaining_cost. Qed. @@ -86,13 +73,20 @@ Section CompletionFacts. Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_completed_jobs : completed_jobs_dont_execute sched. + (** To simplify subsequent proofs, we restate the assumption + [H_completed_jobs] as a trivial corollary. *) + Corollary service_lt_cost : + forall t, + scheduled_at sched j t -> service sched j t < job_cost j. + Proof. exact: H_completed_jobs. Qed. + (** We observe that a job that is completed at the instant of its arrival has a cost of zero. *) Lemma completed_on_arrival_implies_zero_cost : completed_by sched j (job_arrival j) -> job_cost j = 0. Proof. - by rewrite /completed_by no_service_before_arrival // leqn0 => /eqP. + by rewrite /completed_by no_service_before_arrival// leqn0 => /eqP. Qed. (** Further, we note that if a job receives service at some time t, then its @@ -103,9 +97,9 @@ Section CompletionFacts. remaining_cost sched j t > 0. Proof. move=> t SERVICE. - rewrite -incomplete_is_positive_remaining_cost -less_service_than_cost_is_incomplete. - apply H_completed_jobs. - by apply service_at_implies_scheduled_at. + rewrite -incomplete_is_positive_remaining_cost. + rewrite -less_service_than_cost_is_incomplete. + exact/service_lt_cost/service_at_implies_scheduled_at. Qed. (** Consequently, if we have a have processor model where scheduled jobs @@ -115,47 +109,44 @@ Section CompletionFacts. (** Assume a scheduled job always receives some positive service. *) Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState. + (** To simplify subsequent proofs, we restate the assumption + [H_scheduled_implies_serviced] as a trivial corollary. *) + Corollary scheduled_implies_serviced : + forall s, + scheduled_in j s -> 0 < service_in j s. + Proof. exact: H_scheduled_implies_serviced. Qed. + (** Then a scheduled job has positive remaining cost. *) Corollary scheduled_implies_positive_remaining_cost: forall t, scheduled_at sched j t -> remaining_cost sched j t > 0. Proof. - rewrite /scheduled_at => t SCHEDULED. - by apply: serviced_implies_positive_remaining_cost; rewrite /service_at; apply: H_scheduled_implies_serviced. + move=> t sch. + exact/serviced_implies_positive_remaining_cost/scheduled_implies_serviced. Qed. - (** We also prove that a completed job cannot be scheduled... *) - Lemma completed_implies_not_scheduled: + (** We also prove that a scheduled job cannot be completed... *) + Lemma scheduled_implies_not_completed : forall t, - completed_by sched j t -> - ~~ scheduled_at sched j t. + scheduled_at sched j t -> ~~ completed_by sched j t. Proof. - move=> t COMP. - apply contra with (b := ~~ completed_by sched j t); - last by apply /negPn. - move=> SCHED. move: (H_completed_jobs j t SCHED). - by rewrite less_service_than_cost_is_incomplete. + move=> t sch. + by rewrite -less_service_than_cost_is_incomplete service_lt_cost. Qed. - (** ... and that a scheduled job cannot be completed. *) - Lemma scheduled_implies_not_completed: + (** ... and that a completed job cannot be scheduled. *) + Lemma completed_implies_not_scheduled : forall t, - scheduled_at sched j t -> - ~~ completed_by sched j t. - Proof. - move=> t SCHED. - have REMPOS := scheduled_implies_positive_remaining_cost t SCHED. - rewrite /remaining_cost subn_gt0 in REMPOS. - by rewrite -less_service_than_cost_is_incomplete. - Qed. + completed_by sched j t -> ~~ scheduled_at sched j t. + Proof. move=> ? /negPn; exact/contra/scheduled_implies_not_completed. Qed. End CompletionFacts. (** In this section, we establish some facts that are really about service, but are also related to completion and rely on some of the above lemmas. Hence they are in this file rather than in the service facts file. *) -Section ServiceAndCompletionFacts. +Section ServiceAndCompletionFacts. (** Consider any job type,...*) Context {Job: JobType}. @@ -177,6 +168,13 @@ Section ServiceAndCompletionFacts. (** Assume that a scheduled job receives exactly one time unit of service. *) Hypothesis H_unit_service: unit_service_proc_model PState. + (** To simplify subsequent proofs, we restate the assumption + [H_unit_service] as a trivial corollary. *) + Lemma unit_service : + forall s, + service_in j s <= 1. + Proof. exact: H_unit_service. Qed. + (** To begin with, we establish that the cumulative service never exceeds a job's total cost if service increases only by one at each step since completed jobs don't execute. *) @@ -184,18 +182,15 @@ Section ServiceAndCompletionFacts. forall t, service sched j t <= job_cost j. Proof. - move=> t. - elim: t => [|t]; first by rewrite service0. + elim=> [|t]; first by rewrite service0. rewrite -service_last_plus_before. - rewrite leq_eqVlt => /orP [/eqP EQ|LT]. - - rewrite not_scheduled_implies_no_service; - first by rewrite addn0 EQ. - apply completed_implies_not_scheduled => //. + rewrite leq_eqVlt => /orP[/eqP EQ|LT]. + - rewrite not_scheduled_implies_no_service ?EQ ?addn0//. + apply: completed_implies_not_scheduled => //. by rewrite /completed_by EQ. - - apply leq_trans with (n := service sched j t + 1); - last by rewrite addn1. - rewrite leq_add2l. - by apply H_unit_service. + - have: service_at sched j t <= 1 by exact: unit_service. + rewrite -(leq_add2l (service sched j t)) => /leq_trans; apply. + by rewrite addn1. Qed. (** This lets us conclude that [service] and [remaining_cost] are complements @@ -203,11 +198,7 @@ Section ServiceAndCompletionFacts. Lemma service_cost_invariant: forall t, (service sched j t) + (remaining_cost sched j t) = job_cost j. - Proof. - move=> t. - rewrite /remaining_cost subnKC //. - by apply service_at_most_cost. - Qed. + Proof. by move=> ?; rewrite subnKC// service_at_most_cost. Qed. (** We show that the service received by job [j] in any interval is no larger than its cost. *) @@ -216,9 +207,9 @@ Section ServiceAndCompletionFacts. service_during sched j t t' <= job_cost j. Proof. move=> t t'. - case/orP: (leq_total t t') => [tt'|tt']; last by rewrite service_during_geq //. - apply leq_trans with (n := service sched j t'); last by apply: service_at_most_cost. - rewrite /service. rewrite -(service_during_cat sched j 0 t t') // leq_addl //. + have [t'_le_t|t_lt_t'] := leqP t' t; first by rewrite service_during_geq. + apply: leq_trans (service_at_most_cost t'). + by rewrite -(service_cat _ _ _ _ (ltnW t_lt_t')) leq_addl. Qed. (** If a job isn't complete at time [t], it can't be completed at time [t + @@ -228,15 +219,14 @@ Section ServiceAndCompletionFacts. ~~ completed_by sched j t -> ~~ completed_by sched j (t + remaining_cost sched j t - 1). Proof. - move=> t. - rewrite incomplete_is_positive_remaining_cost => REMCOST. + move=> t; rewrite incomplete_is_positive_remaining_cost => rem_cost. rewrite -less_service_than_cost_is_incomplete -(service_cat sched j t); - last by rewrite -addnBA //; apply: leq_addr. - apply leq_ltn_trans with (n := service sched j t + remaining_cost sched j t - 1). - - by rewrite -!addnBA //; rewrite leq_add2l; apply cumulative_service_le_delta; exact. - - rewrite service_cost_invariant // -subn_gt0 subKn //. - move: REMCOST. rewrite /remaining_cost subn_gt0 => SERVICE. - by apply leq_ltn_trans with (n := service sched j t). + last by rewrite -addnBA//; exact: leq_addr. + have: service sched j t + remaining_cost sched j t - 1 < job_cost j. + { rewrite service_cost_invariant -subn_gt0 subKn//. + exact/(leq_trans rem_cost)/leq_subr. } + apply: leq_ltn_trans. + by rewrite -!addnBA// leq_add2l cumulative_service_le_delta. Qed. Section GuaranteedService. @@ -248,17 +238,21 @@ Section ServiceAndCompletionFacts. Context `{JobArrival Job}. Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched. + (** To simplify subsequent proofs, we restate the assumption + [H_jobs_must_arrive] as a trivial corollary. *) + Corollary has_arrived_scheduled : + forall t, + scheduled_at sched j t -> has_arrived j t. + Proof. exact: H_jobs_must_arrive. Qed. + (** We show that if job j is scheduled, then it must be pending. *) Lemma scheduled_implies_pending: forall t, scheduled_at sched j t -> pending sched j t. Proof. - move=> t SCHED. - rewrite /pending. - apply /andP; split; - first by apply: H_jobs_must_arrive => //. - by apply: scheduled_implies_not_completed => //. + move=> t sch; apply/andP; split; first exact: has_arrived_scheduled. + exact: scheduled_implies_not_completed. Qed. End GuaranteedService. @@ -300,27 +294,23 @@ Section PositiveCost. job_arrival j <= t' < t /\ scheduled_at sched j t'. Proof. - rewrite /completed_by. - move=> t COMPLETE. - have POSITIVE_SERVICE: 0 < service sched j t - by apply leq_trans with (n := job_cost j); auto. - by apply: positive_service_implies_scheduled_since_arrival; assumption. + move=> t comp. + have: 0 < service sched j t by exact: leq_trans comp. + exact: positive_service_implies_scheduled_since_arrival. Qed. (** We also prove that the job is pending at the moment of its arrival. *) Lemma job_pending_at_arrival: pending sched j (job_arrival j). Proof. - rewrite /pending. - apply/andP; split; - first by rewrite /has_arrived //. - rewrite /completed_by no_service_before_arrival // -ltnNge //. + apply/andP; split; first by rewrite /has_arrived. + by rewrite /completed_by no_service_before_arrival// -ltnNge. Qed. End PositiveCost. Section CompletedJobs. - + (** Consider any kinds of jobs and any kind of processor state. *) Context {Job : JobType} {PState : ProcessorState Job}. @@ -336,22 +326,15 @@ Section CompletedJobs. (** We observe that a given job is ready only if it is also incomplete... *) Lemma ready_implies_incomplete: forall j t, job_ready sched j t -> ~~ completed_by sched j t. - Proof. - move=> j t READY. - move: (any_ready_job_is_pending sched j t READY). - by rewrite /pending => /andP [_ INCOMPLETE]. - Qed. + Proof. by move=> ? ? /any_ready_job_is_pending /andP[]. Qed. (** ...and lift this observation also to the level of whole schedules. *) Lemma completed_jobs_are_not_ready: jobs_must_be_ready_to_execute sched -> completed_jobs_dont_execute sched. Proof. - rewrite /jobs_must_be_ready_to_execute /completed_jobs_dont_execute. - move=> READY_IF_SCHED j t SCHED. - move: (READY_IF_SCHED j t SCHED) => READY. - rewrite less_service_than_cost_is_incomplete. - by apply ready_implies_incomplete. + move=> + j t sch => /(_ j t sch) ready. + by rewrite less_service_than_cost_is_incomplete ready_implies_incomplete. Qed. (** Furthermore, in a valid schedule, completed jobs don't execute. *) @@ -359,10 +342,7 @@ Section CompletedJobs. forall arr_seq, valid_schedule sched arr_seq -> completed_jobs_dont_execute sched. - Proof. - move=> arr_seq [??]. - by apply completed_jobs_are_not_ready. - Qed. + Proof. move=> ? [? ?]; exact: completed_jobs_are_not_ready. Qed. (** We further observe that completed jobs don't execute if scheduled jobs always receive non-zero service and cumulative service never exceeds job @@ -373,11 +353,8 @@ Section CompletedJobs. completed_jobs_dont_execute sched. Proof. move=> IDEAL SERVICE_BOUND j t SCHED. - have UB := SERVICE_BOUND j t.+1. - have POS := IDEAL _ _ SCHED. - apply leq_trans with (n := service sched j t.+1) => //. - rewrite -service_last_plus_before /service_at. - by rewrite -{1}(addn0 (service sched j t)) ltn_add2l. + apply: leq_trans (SERVICE_BOUND j t.+1). + by rewrite -service_last_plus_before -addn1 leq_add2l IDEAL. Qed. End CompletedJobs. @@ -402,9 +379,8 @@ Section CompletionInTwoSchedules. completed_by sched1 j t = completed_by sched2 j t. Proof. move=> sched1 sched2 h PREFIX j t LE_h. - rewrite /completed_by. - rewrite (identical_prefix_service sched1 sched2) //. - now apply (identical_prefix_inclusion _ _ h). + rewrite /completed_by (identical_prefix_service sched1 sched2)//. + exact: identical_prefix_inclusion PREFIX. Qed. (** For convenience, we restate the previous lemma in terms of [pending]. *) @@ -415,9 +391,8 @@ Section CompletionInTwoSchedules. t <= h -> pending sched1 j t = pending sched2 j t. Proof. - move=> sched1 sched2 h PREFIX j t LE_h. - now rewrite /pending (identical_prefix_completed_by _ sched2 h). + move=> sched1 sched2 h PREFIX j t t_le_h. + by rewrite /pending (identical_prefix_completed_by _ sched2 h). Qed. - End CompletionInTwoSchedules. diff --git a/analysis/facts/behavior/deadlines.v b/analysis/facts/behavior/deadlines.v index eab3862b82de4aa3971db3b4481ab4d562b62633..23dc60e5e58567e4ee5d4272a4da17fcaba452e7 100644 --- a/analysis/facts/behavior/deadlines.v +++ b/analysis/facts/behavior/deadlines.v @@ -27,11 +27,9 @@ Section DeadlineFacts. ~~ completed_by sched j t -> t < job_deadline j. Proof. - move=> j t MET INCOMP. - apply contraT; rewrite -leqNgt => PAST_DL. - have DL_MISS: ~~ completed_by sched j (job_deadline j) - by apply incompletion_monotonic with (t' := t) => //. - by move: DL_MISS => /negP. + move=> j t MET INCOMP; apply: contraT; rewrite -leqNgt => PAST_DL. + have /negP// : ~~ completed_by sched j (job_deadline j). + exact: incompletion_monotonic INCOMP. Qed. (** Furthermore, a job that both meets its deadline and is incomplete at a @@ -46,11 +44,8 @@ Section DeadlineFacts. move=> j t MET INCOMP. apply: cumulative_service_implies_scheduled. rewrite -(ltn_add2l (service sched j t)) addn0. - rewrite service_cat; - last by (apply ltnW; apply incomplete_implies_later_deadline). - apply leq_trans with (n := job_cost j); - first by rewrite less_service_than_cost_is_incomplete. - by apply MET. + rewrite service_cat; last exact/ltnW/incomplete_implies_later_deadline. + by apply: leq_trans MET; rewrite less_service_than_cost_is_incomplete. Qed. End Incompletion. @@ -77,8 +72,8 @@ Section DeadlineFacts. t < job_deadline j. Proof. move=> j t MET SCHED_AT. - apply (incomplete_implies_later_deadline sched) => //. - by apply scheduled_implies_not_completed. + apply: (incomplete_implies_later_deadline sched) => //. + exact: scheduled_implies_not_completed. Qed. End IdealProgressSchedules. @@ -101,8 +96,7 @@ Section DeadlineFacts. (job_meets_deadline sched j <-> job_meets_deadline sched' j). Proof. move=> j SERVICE. - split; - by rewrite /job_meets_deadline /completed_by -SERVICE. + by split; rewrite /job_meets_deadline /completed_by -SERVICE. Qed. End EqualProgress. diff --git a/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v index 4558a0782652dc72817372893ed685241e04d928..d201540e4f66e235e0c157bec8b7ee167b8aa246 100644 --- a/analysis/facts/behavior/service.v +++ b/analysis/facts/behavior/service.v @@ -30,27 +30,19 @@ Section Composition. Lemma service_during_geq: forall t1 t2, t1 >= t2 -> service_during sched j t1 t2 = 0. - Proof. - move=> t1 t2 t1t2. - by rewrite /service_during big_geq //. - Qed. + Proof. by move=> ? ? ?; rewrite /service_during big_geq. Qed. (** Equally trivially, no job has received service prior to time zero. *) Corollary service0: service sched j 0 = 0. - Proof. - by rewrite /service service_during_geq //. - Qed. + Proof. by rewrite /service service_during_geq. Qed. (** Trivially, an interval consisting of one time unit is equivalent to [service_at]. *) Lemma service_during_instant: forall t, service_during sched j t t.+1 = service_at sched j t. - Proof. - move => t. - by rewrite /service_during big_nat_recr ?big_geq //. - Qed. + Proof. by move=> ?; rewrite /service_during big_nat_recr// big_geq. Qed. (** Next, we observe that we can look at the service received during an interval <<[t1, t3)>> as the sum of the service during [t1, t2) and [t2, t3) @@ -61,10 +53,7 @@ Section Composition. t1 <= t2 <= t3 -> (service_during sched j t1 t2) + (service_during sched j t2 t3) = service_during sched j t1 t3. - Proof. - move => t1 t2 t3 /andP [t1t2 t2t3]. - by rewrite /service_during -big_cat_nat /=. - Qed. + Proof. by move => ? ? ? /andP[? ?]; rewrite -big_cat_nat. Qed. (** Since [service] is just a special case of [service_during], the same holds for [service]. *) @@ -73,10 +62,7 @@ Section Composition. t1 <= t2 -> (service sched j t1) + (service_during sched j t1 t2) = service sched j t2. - Proof. - move=> t1 t2 t1t2. - by rewrite /service service_during_cat //. - Qed. + Proof. move=> ? ? ?; exact: service_during_cat. Qed. (** As a special case, we observe that the service during an interval can be decomposed into the first instant and the rest of the interval. *) @@ -86,10 +72,7 @@ Section Composition. (service_at sched j t1) + (service_during sched j t1.+1 t2) = service_during sched j t1 t2. Proof. - move => t1 t2 t1t2. - have TIMES: t1 <= t1.+1 <= t2 by rewrite /(_ && _) ifT //. - have SPLIT := service_during_cat t1 t1.+1 t2 TIMES. - by rewrite -service_during_instant //. + by move=> ? ? ?; rewrite -service_during_instant service_during_cat// leqnSn. Qed. (** Symmetrically, we have the same for the end of the interval. *) @@ -99,9 +82,8 @@ Section Composition. (service_during sched j t1 t2) + (service_at sched j t2) = service_during sched j t1 t2.+1. Proof. - move=> t1 t2 t1t2. - rewrite -(service_during_cat t1 t2 t2.+1); last by rewrite /(_ && _) ifT //. - by rewrite service_during_instant //. + move=> t1 t2 ?; rewrite -(service_during_cat t1 t2 t2.+1) ?leqnSn ?andbT//. + by rewrite service_during_instant. Qed. (** And hence also for [service]. *) @@ -109,10 +91,7 @@ Section Composition. forall t, (service sched j t) + (service_at sched j t) = service sched j t.+1. - Proof. - move=> t. - by rewrite /service -service_during_last_plus_before //. - Qed. + Proof. move=> ?; exact: service_during_last_plus_before. Qed. (** Finally, we deconstruct the service received during an interval <<[t1, t3)>> into the service at a midpoint t2 and the service in the intervals before @@ -123,9 +102,9 @@ Section Composition. (service_during sched j t1 t2) + (service_at sched j t2) + (service_during sched j t2.+1 t3) = service_during sched j t1 t3. Proof. - move => t1 t2 t3 /andP [t1t2 t2t3]. - rewrite -addnA service_during_first_plus_later// service_during_cat// /(_ && _) ifT//. - by exact: ltnW. + move => t1 t2 t3 /andP[t1t2 t2t3]. + rewrite -addnA service_during_first_plus_later// service_during_cat//. + by rewrite t1t2 ltnW. Qed. End Composition. @@ -150,18 +129,14 @@ Section UnitService. (** First, we prove that the instantaneous service cannot be greater than 1, ... *) Lemma service_at_most_one: forall t, service_at sched j t <= 1. - Proof. - by move=> t; rewrite /service_at. - Qed. + Proof. by rewrite /service_at. Qed. (** ... which implies that the instantaneous service always equals to 0 or 1. *) Corollary service_is_zero_or_one: forall t, service_at sched j t = 0 \/ service_at sched j t = 1. Proof. - intros. - have Lewf := service_at_most_one t. - remember (service_at sched j t) as Ï. - by destruct Ï; last destruct Ï; [left| right | exfalso]. + move=> t. + by case: service_at (service_at_most_one t) => [|[|//]] _; [left|right]. Qed. (** Next we prove that the cumulative service received by job [j] in @@ -169,10 +144,8 @@ Section UnitService. Lemma cumulative_service_le_delta: forall t delta, service_during sched j t (t + delta) <= delta. Proof. - unfold service_during; intros t delta. - apply leq_trans with (n := \sum_(t <= t0 < t + delta) 1); - last by rewrite sum_of_ones. - by apply: leq_sum => t' _; apply: service_at_most_one. + move=> t delta; rewrite -[X in _ <= X](sum_of_ones t). + apply: leq_sum => t' _; exact: service_at_most_one. Qed. (** Conversely, we prove that if the cumulative service received by @@ -182,28 +155,16 @@ Section UnitService. forall t delta Ï, Ï <= service_during sched j t (t + delta) -> Ï <= delta. - Proof. - induction delta; intros ? LE. - - by rewrite service_during_geq in LE; lia. - - rewrite addnS -service_during_last_plus_before in LE; last by lia. - destruct (service_is_zero_or_one (t + delta)) as [EQ|EQ]; rewrite EQ in LE. - + rewrite addn0 in LE. - by apply IHdelta in LE; rewrite (leqRW LE). - + rewrite addn1 in LE. - destruct Ï; first by done. - by rewrite ltnS in LE; apply IHdelta in LE; rewrite (leqRW LE). - Qed. - + Proof. move=> ??? /leq_trans; apply; exact: cumulative_service_le_delta. Qed. Section ServiceIsUnitGrowthFunction. (** We show that the service received by any job [j] is a unit growth function. *) - Lemma service_is_unit_growth_function: + Lemma service_is_unit_growth_function : unit_growth_function (service sched j). Proof. - rewrite /unit_growth_function => t. - rewrite addn1 -service_last_plus_before leq_add2l. - by apply service_at_most_one. + move=> t; rewrite addn1 -service_last_plus_before leq_add2l. + exact: service_at_most_one. Qed. (** Next, consider any time [t]... *) @@ -221,15 +182,12 @@ Section UnitService. t' < t /\ service sched j t' = s. Proof. - feed (exists_intermediate_point (service sched j)); - [by apply service_is_unit_growth_function | intros EX]. - feed (EX 0 t); first by done. - feed (EX s); first by rewrite /service /service_during big_geq //. - by move: EX => /= [x_mid EX]; exists x_mid. + apply: (exists_intermediate_point _ service_is_unit_growth_function 0) => //. + by rewrite service0. Qed. End ServiceIsUnitGrowthFunction. - + End UnitService. (** We establish a basic fact about the monotonicity of service. *) @@ -250,10 +208,7 @@ Section Monotonicity. forall t1 t2, t1 <= t2 -> service sched j t1 <= service sched j t2. - Proof. - move=> t1 t2 let1t2. - by rewrite -(service_cat sched j t1 t2 let1t2); apply: leq_addr. - Qed. + Proof. by move=> t1 t2 ?; rewrite -(service_cat _ _ t1 t2)// leq_addr. Qed. End Monotonicity. @@ -271,37 +226,29 @@ Section RelationToScheduled. (** We observe that a job that isn't scheduled in a given processor state cannot possibly receive service in that state. *) - Lemma service_in_implies_scheduled_in : forall s, - ~~ scheduled_in j s -> service_in j s = 0. + Lemma service_in_implies_scheduled_in : + forall s, + ~~ scheduled_in j s -> service_in j s = 0. Proof. - move=> s /existsP Hsched. - apply/eqP. - rewrite sum_nat_eq0. - apply/forallP => c /=. - rewrite service_on_implies_scheduled_on => //. - apply/negP => Hsch. - apply: Hsched. - by exists c. + move=> s. + move=> /existsP Hsched; apply/eqP; rewrite sum_nat_eq0; apply/forallP => c. + rewrite service_on_implies_scheduled_on//. + by apply/negP => ?; apply: Hsched; exists c. Qed. (** In particular, it cannot receive service at any given time. *) Corollary not_scheduled_implies_no_service: forall t, ~~ scheduled_at sched j t -> service_at sched j t = 0. - Proof. - rewrite /service_at /scheduled_at. - move=> t NOT_SCHED. - by rewrite service_in_implies_scheduled_in. - Qed. + Proof. move=> ?; exact: service_in_implies_scheduled_in. Qed. (** Conversely, if a job receives service, then it must be scheduled. *) - Lemma service_at_implies_scheduled_at: + Lemma service_at_implies_scheduled_at : forall t, service_at sched j t > 0 -> scheduled_at sched j t. Proof. - move=> t. - destruct (scheduled_at sched j t) eqn:SCHEDULED; first trivial. - by rewrite not_scheduled_implies_no_service // negbT. + move=> t; case SCHEDULED: scheduled_at => //. + by rewrite not_scheduled_implies_no_service// negbT. Qed. (** Thus, if the cumulative amount of service changes, then it must be @@ -310,9 +257,8 @@ Section RelationToScheduled. forall t, service sched j t < service sched j t.+1 -> scheduled_at sched j t. Proof. - move => t. - rewrite -service_last_plus_before -{1}(addn0 (service sched j t)) ltn_add2l. - by apply: service_at_implies_scheduled_at. + move=> t; rewrite -service_last_plus_before -ltn_subLR// subnn. + exact: service_at_implies_scheduled_at. Qed. (** We observe that a job receives cumulative service during some interval iff @@ -325,32 +271,10 @@ Section RelationToScheduled. t1 <= t < t2 /\ service_at sched j t > 0. Proof. - split. - { - move=> NONZERO. - case (boolP([exists t: 'I_t2, - (t >= t1) && (service_at sched j t > 0)])) => [EX | ALL]. - - move: EX => /existsP [x /andP [GE SERV]]. - exists x; split => //. - apply /andP; by split. - - rewrite negb_exists in ALL; move: ALL => /forallP ALL. - rewrite /service_during big_nat_cond in NONZERO. - rewrite big1 ?ltn0 // in NONZERO => i. - rewrite andbT; move => /andP [GT LT]. - specialize (ALL (Ordinal LT)); simpl in ALL. - rewrite GT andTb -eqn0Ngt in ALL. - by apply /eqP. - } - { - move=> [t [TT SERVICE]]. - case (boolP (0 < service_during sched j t1 t2)) => // NZ. - exfalso. - rewrite -eqn0Ngt in NZ. move/eqP: NZ. - rewrite big_nat_eq0 => IS_ZERO. - have NO_SERVICE := IS_ZERO t TT. - apply lt0n_neq0 in SERVICE. - by move/neqP in SERVICE; contradiction. - } + move=> t1 t2. + split=> [|[t titv_nz_serv]]. + - by move=> /sum_seq_gt0P[t]; rewrite mem_index_iota => ?; exists t. + - by apply/sum_seq_gt0P; exists t; rewrite mem_index_iota. Qed. (** Thus, any job that receives some service during an interval must be @@ -362,12 +286,9 @@ Section RelationToScheduled. t1 <= t < t2 /\ scheduled_at sched j t. Proof. - move=> t1 t2. - rewrite service_during_service_at. - move=> [t' [TIMES SERVICED]]. - exists t'; split => //. - by apply: service_at_implies_scheduled_at. - Qed. + move=> t1 t2; rewrite service_during_service_at => -[t' [TIMES SERVICED]]. + exists t'; split=> //; exact: service_at_implies_scheduled_at. + Qed. (** ...which implies that any job with positive cumulative service must have been scheduled at some point. *) @@ -375,12 +296,9 @@ Section RelationToScheduled. forall t, service sched j t > 0 -> exists t', (t' < t /\ scheduled_at sched j t'). Proof. - move=> t2. - rewrite /service => NONZERO. - have EX_SCHED := cumulative_service_implies_scheduled 0 t2 NONZERO. - by move: EX_SCHED => [t [TIMES SCHED_AT]]; exists t; split. + by move=> t /cumulative_service_implies_scheduled[t' ?]; exists t'. Qed. - + (** If we can assume that a scheduled job always receives service, we can further prove the converse. *) Section GuaranteedService. @@ -394,11 +312,10 @@ Section RelationToScheduled. forall t, ~~ scheduled_at sched j t <-> service_at sched j t = 0. Proof. - move=> t. rewrite /scheduled_at /service_at. - split => [NOT_SCHED | NO_SERVICE]. - - by rewrite service_in_implies_scheduled_in. - - apply (contra (H_scheduled_implies_serviced j (sched t))). - by rewrite -eqn0Ngt; apply /eqP. + move=> t. + split => [|NO_SERVICE]; first exact: service_in_implies_scheduled_in. + apply: (contra (H_scheduled_implies_serviced j (sched t))). + by rewrite -eqn0Ngt -NO_SERVICE. Qed. (** Then, if a job does not receive any service during an interval, it @@ -409,13 +326,10 @@ Section RelationToScheduled. forall t, t1 <= t < t2 -> ~~ scheduled_at sched j t. Proof. - move=> t1 t2 ZERO_SUM t /andP [GT_t1 LT_t2]. - rewrite no_service_not_scheduled. - move: ZERO_SUM. - rewrite /service_during big_nat_eq0 => IS_ZERO. - by apply (IS_ZERO t); apply/andP. + move=> t1 t2. + by move=> + t titv; rewrite no_service_not_scheduled big_nat_eq0; apply. Qed. - + (** Conversely, if a job is not scheduled during an interval, then it does not receive any service in that interval *) Lemma not_scheduled_during_implies_zero_service: @@ -423,9 +337,8 @@ Section RelationToScheduled. (forall t, t1 <= t < t2 -> ~~ scheduled_at sched j t) -> service_during sched j t1 t2 = 0. Proof. - intros t1 t2 NSCHED. - apply big_nat_eq0; move=> t NEQ. - by apply no_service_not_scheduled, NSCHED. + move=> t1 t2; rewrite big_nat_eq0 => + t titv => /(_ t titv). + by rewrite no_service_not_scheduled. Qed. (** If a job is scheduled at some point in an interval, it receives @@ -437,11 +350,8 @@ Section RelationToScheduled. scheduled_at sched j t) -> service_during sched j t1 t2 > 0. Proof. - move=> t1 t2 [t' [TIMES SCHED]]. - rewrite service_during_service_at. - exists t'; split => //. - move: SCHED. rewrite /scheduled_at /service_at. - by apply (H_scheduled_implies_serviced j (sched t')). + move=> t1 t2 [t [titv sch]]; rewrite service_during_service_at. + exists t; split=> //; exact: H_scheduled_implies_serviced. Qed. (** ...which again applies to total service, too. *) @@ -452,9 +362,8 @@ Section RelationToScheduled. scheduled_at sched j t') -> service sched j t > 0. Proof. - move=> t [t' [TT SCHED]]. - rewrite /service. apply scheduled_implies_cumulative_service. - by exists t'. + move=> t. + by move=> [t' ?]; apply: scheduled_implies_cumulative_service; exists t'. Qed. End GuaranteedService. @@ -476,22 +385,15 @@ Section RelationToScheduled. service sched j t > 0 -> exists t', (job_arrival j <= t' < t /\ scheduled_at sched j t'). Proof. - move=> t SERVICE. - have EX_SCHED := positive_service_implies_scheduled_before t SERVICE. - inversion EX_SCHED as [t'' [TIMES SCHED_AT]]. - exists t''; split; last by done. - rewrite /(_ && _) ifT //. - move: H_jobs_must_arrive. rewrite /jobs_must_arrive_to_execute /has_arrived => ARR. - by apply: ARR. + move=> t /positive_service_implies_scheduled_before[t' [t't sch]]. + exists t'; split=> //; rewrite t't andbT; exact: H_jobs_must_arrive. Qed. Lemma not_scheduled_before_arrival: forall t, t < job_arrival j -> ~~ scheduled_at sched j t. Proof. - move=> t EARLY. - apply: (contra (H_jobs_must_arrive j t)). - by rewrite /has_arrived -ltnNge. - Qed. + by move=> t ?; apply: (contra (H_jobs_must_arrive j t)); rewrite -ltnNge. + Qed. (** We show that job [j] does not receive service at any time [t] prior to its arrival. *) @@ -500,8 +402,8 @@ Section RelationToScheduled. t < job_arrival j -> service_at sched j t = 0. Proof. - move=> t NOT_ARR. - by rewrite not_scheduled_implies_no_service // not_scheduled_before_arrival. + move=> t NOT_ARR; rewrite not_scheduled_implies_no_service//. + exact: not_scheduled_before_arrival. Qed. (** Note that the same property applies to the cumulative service. *) @@ -510,14 +412,8 @@ Section RelationToScheduled. t2 <= job_arrival j -> service_during sched j t1 t2 = 0. Proof. - move=> t1 t2 EARLY. - rewrite /service_during. - have ZERO_SUM: \sum_(t1 <= t < t2) service_at sched j t = \sum_(t1 <= t < t2) 0; - last by rewrite ZERO_SUM sum0. - rewrite big_nat_cond [in RHS]big_nat_cond. - apply: eq_bigr => i /andP [TIMES _]. move: TIMES => /andP [le_t1_i lt_i_t2]. - apply (service_before_job_arrival_zero i). - by apply leq_trans with (n := t2). + move=> t1 t2 early; rewrite big_nat_eq0 => t /andP[_ t_lt_t2]. + apply: service_before_job_arrival_zero; exact: leq_trans early. Qed. (** Hence, one can ignore the service received by a job before its arrival @@ -528,20 +424,16 @@ Section RelationToScheduled. t2 >= job_arrival j -> service_during sched j t1 t2 = service_during sched j (job_arrival j) t2. Proof. - move=> t1 t2 le_t1 le_t2. - rewrite -(service_during_cat sched j t1 (job_arrival j) t2). - rewrite cumulative_service_before_job_arrival_zero //. - by apply/andP. + move=> t1 t2 t1_le t2_ge. + rewrite -(service_during_cat sched _ _ (job_arrival j)); last exact/andP. + by rewrite cumulative_service_before_job_arrival_zero. Qed. (** ... which we can also state in terms of cumulative service. *) Corollary no_service_before_arrival: forall t, t <= job_arrival j -> service sched j t = 0. - Proof. - move=> t EARLY. - by rewrite /service cumulative_service_before_job_arrival_zero. - Qed. + Proof. exact: cumulative_service_before_job_arrival_zero. Qed. End AfterArrival. @@ -563,9 +455,8 @@ Section RelationToScheduled. Lemma constant_service_implies_no_service_during: service_during sched j t1 t2 = 0. Proof. - move: H_same_service. - rewrite -(service_cat sched j t1 t2) // -[service sched j t1 in LHS]addn0 => /eqP. - by rewrite eqn_add2l => /eqP. + move: H_same_service; rewrite -(service_cat _ _ t1 t2)// => /eqP. + by rewrite -[X in X == _]addn0 eqn_add2l => /eqP. Qed. (** ...which of course implies that it does not receive service at any @@ -574,11 +465,9 @@ Section RelationToScheduled. forall t, t1 <= t < t2 -> service_at sched j t = 0. Proof. - move=> t /andP [GE_t1 LT_t2]. - move: constant_service_implies_no_service_during. - rewrite /service_during big_nat_eq0 => IS_ZERO. - apply IS_ZERO. - by apply /andP. + move=> t titv. + have := constant_service_implies_no_service_during. + rewrite big_nat_eq0; exact. Qed. (** We show that job [j] receives service at some point [t < t1] @@ -587,23 +476,14 @@ Section RelationToScheduled. [exists t: 'I_t1, service_at sched j t > 0] = [exists t': 'I_t2, service_at sched j t' > 0]. Proof. - apply /idP/idP => /existsP [t SERVICED]. - { - have LE: t < t2 by apply: (leq_trans _ H_t1_le_t2) => //. - by apply /existsP; exists (Ordinal LE). - } - { - case (boolP (t < t1)) => LE. - - by apply /existsP; exists (Ordinal LE). - - exfalso. - have TIMES: t1 <= t < t2 - by apply /andP; split => //; rewrite leqNgt //. - have NO_SERVICE := constant_service_implies_not_scheduled t TIMES. - by rewrite NO_SERVICE in SERVICED. - } + apply/idP/idP => /existsP[t serv]. + { by apply/existsP; exists (widen_ord H_t1_le_t2 t). } + have [t_lt_t1|t1_le_t] := ltnP t t1. + { by apply/existsP; exists (Ordinal t_lt_t1). } + exfalso; move: serv; apply/negP; rewrite -eqn0Ngt. + by apply/eqP/constant_service_implies_not_scheduled; rewrite t1_le_t /=. Qed. - (** Then, under the assumption that scheduled jobs receives service, we can translate this into a claim about scheduled_at. *) @@ -616,18 +496,14 @@ Section RelationToScheduled. [exists t: 'I_t1, scheduled_at sched j t] = [exists t': 'I_t2, scheduled_at sched j t']. Proof. - have CONV: forall B, [exists b: 'I_B, scheduled_at sched j b] - = [exists b: 'I_B, service_at sched j b > 0]. - { - move=> B. apply/idP/idP => /existsP [b P]; apply /existsP; exists b. - - by move: P; rewrite /scheduled_at /service_at; - apply (H_scheduled_implies_serviced j (sched b)). - - by apply service_at_implies_scheduled_at. - } - rewrite !CONV. - by apply same_service_implies_serviced_at_earlier_times. + have CONV B : [exists b: 'I_B, scheduled_at sched j b] + = [exists b: 'I_B, service_at sched j b > 0]. + { apply/idP/idP => /existsP[b P]; apply/existsP; exists b. + - exact: H_scheduled_implies_serviced. + - exact: service_at_implies_scheduled_at. } + by rewrite !CONV same_service_implies_serviced_at_earlier_times. Qed. - + End TimesWithSameService. End RelationToScheduled. @@ -662,11 +538,7 @@ Section ServiceInTwoSchedules. is also the same. *) Lemma same_service_during: service_during sched1 j t1 t2 = service_during sched2 j t1 t2. - Proof. - rewrite /service_during. - apply eq_big_nat. - by apply H_sched1_sched2_same_service_at. - Qed. + Proof. exact/eq_big_nat/H_sched1_sched2_same_service_at. Qed. End ServiceDuringEquivalentInterval. @@ -678,9 +550,8 @@ Section ServiceInTwoSchedules. (forall t, t1 <= t < t2 -> sched1 t = sched2 t) -> forall j, service_during sched1 j t1 t2 = service_during sched2 j t1 t2. Proof. - move=> t1 t2 SCHED_EQ j. - apply same_service_during => t' RANGE. - by rewrite /service_at SCHED_EQ. + move=> t1 t2 sch j; apply: same_service_during => t' t'itv. + by rewrite /service_at sch. Qed. (** For convenience, we restate the corollary also at the level of @@ -689,8 +560,6 @@ Section ServiceInTwoSchedules. forall h, identical_prefix sched1 sched2 h -> forall j, service sched1 j h = service sched2 j h. - Proof. - by move=> h IDENT j; apply equal_prefix_implies_same_service_during. - Qed. + Proof. move=> ? ? ?; exact: equal_prefix_implies_same_service_during. Qed. End ServiceInTwoSchedules. diff --git a/analysis/facts/edf_definitions.v b/analysis/facts/edf_definitions.v index f7d992c2fdc738424fcb811f9bd6eda1a375f6a8..a17c05415ce1d2e4d65a2e20e8a6d3b4d84e1fd9 100644 --- a/analysis/facts/edf_definitions.v +++ b/analysis/facts/edf_definitions.v @@ -85,8 +85,7 @@ Section Equivalence. { apply /andP; split => //. - apply /andP; split => //. apply (incompletion_monotonic _ j _ _ LEQ). - apply scheduled_implies_not_completed => //. - by apply ideal_proc_model_ensures_ideal_progress. + by apply scheduled_implies_not_completed. - apply /negP; move => SCHED''. by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). } Qed. diff --git a/analysis/facts/job_index.v b/analysis/facts/job_index.v index b12e0041585a1f270b21cd9e7c537c72d048586d..66d44bda9ac4ce8f5d74434cb97b203815a38894 100644 --- a/analysis/facts/job_index.v +++ b/analysis/facts/job_index.v @@ -148,14 +148,14 @@ Section JobIndexLemmas. Proof. intros * IN1 IN2 LE. move_neq_up LT; move_neq_down LE. - rewrite -> arrivals_P_cat with (t := job_arrival j1); last by apply job_arrival_between in IN1 => //. + rewrite -> arrivals_P_cat with (t := job_arrival j1); last by apply job_arrival_between_P in IN1 => //. rewrite !index_cat ifT; last by eapply arrival_lt_implies_job_in_arrivals_between_P; eauto. rewrite ifF. - - eapply leq_trans; [ | now erewrite leq_addr]. + - eapply leq_trans; [ | by erewrite leq_addr]. rewrite index_mem. - now eapply arrival_lt_implies_job_in_arrivals_between_P; eauto. + by eapply arrival_lt_implies_job_in_arrivals_between_P; eauto. - apply Bool.not_true_is_false; intro T. - now apply job_arrival_between in T; try lia. + by apply job_arrival_between_P in T; try lia. Qed. (** We observe that index of job [j1] is same in the @@ -168,7 +168,8 @@ Section JobIndexLemmas. rewrite leq_eqVlt => /orP [/eqP LT|LT]; first by rewrite /task_arrivals_up_to_job_arrival LT H_same_task. specialize (arrival_lt_implies_strict_prefix _ H_consistent_arrivals (job_task j1) j1 j2) => SUB. feed_n 5 SUB => //; move: SUB => [xs2 [NEMPT2 CAT2]]. - now rewrite -CAT2 index_cat ifT; last by apply arrives_in_task_arrivals_up_to => //. + rewrite -CAT2 index_cat ifT //=. + by apply arrives_in_task_arrivals_up_to => //. Qed. (** We show that the [job_index] of a job [j1] is strictly less than @@ -177,7 +178,7 @@ Section JobIndexLemmas. job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1). Proof. rewrite /job_index index_mem. - now apply arrives_in_task_arrivals_up_to. + exact: arrives_in_task_arrivals_up_to. Qed. (** Finally, we show that a lower job index implies an earlier arrival time. *) @@ -195,7 +196,7 @@ Section JobIndexLemmas. - now eapply leq_trans; [apply index_job_lt_size_task_arrivals_up_to_job | rewrite leq_addr]. - apply Bool.not_true_is_false; intro T. - now apply job_arrival_between in T; try lia. + now apply job_arrival_between_P in T; try lia. Qed. (** We show that if job [j1] arrives earlier than job [j2] diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v index 952163fbc261f7157a4040fbfa66e34402683691..e0b3a5adfe6d3d325962e7f149ca3bd4bef12722 100644 --- a/analysis/facts/transform/edf_opt.v +++ b/analysis/facts/transform/edf_opt.v @@ -196,9 +196,8 @@ Section MakeEDFAtFacts. job_deadline j > t. Proof. move=> j t SCHED. - apply (scheduled_at_implies_later_deadline sched) => //. - - by apply ideal_proc_model_ensures_ideal_progress. - - by apply (H_no_deadline_misses _ t). + apply: (scheduled_at_implies_later_deadline sched) => //. + exact: (H_no_deadline_misses _ t). Qed. (** We analyze [make_edf_at] applied to an arbitrary point in time, @@ -244,7 +243,6 @@ Section MakeEDFAtFacts. by rewrite scheduled_at_def; apply /eqP. move: (scheduled_job_in_sched_has_later_deadline _ _ SCHED') => DL_orig. apply edf_swap_no_deadline_misses_introduced => //. - - by apply ideal_proc_model_ensures_ideal_progress. - by apply fsc_range1 => //. - move=> j1 j2 SCHED_j1 SCHED_j2. apply: (fsc_found_job_deadline sched _ j_orig t_edf _ _ _ _ _ t_edf) => //. @@ -274,7 +272,6 @@ Section MakeEDFAtFacts. move=> j t SCHED. apply (scheduled_at_implies_later_deadline sched') => //. - by apply mea_completed_jobs. - - by apply ideal_proc_model_ensures_ideal_progress. - by apply mea_no_deadline_misses with (t := t). Qed. @@ -579,8 +576,7 @@ Section EDFPrefixFacts. move=> j t SCHED. move: edf_prefix_well_formedness => [COMP [ARR DL_MET]]. apply (scheduled_at_implies_later_deadline sched') => //. - - by apply ideal_proc_model_ensures_ideal_progress. - - by apply (DL_MET j t). + exact: (DL_MET j t). Qed. (** Since no jobs are lost or added to the schedule by diff --git a/analysis/facts/transform/edf_wc.v b/analysis/facts/transform/edf_wc.v index d61aed00766e7986ec70de35c990d088fb999233..f04c2e50c6e72a979c1450221044b66257719d5e 100644 --- a/analysis/facts/transform/edf_wc.v +++ b/analysis/facts/transform/edf_wc.v @@ -267,7 +267,6 @@ Section MakeEDFWorkConservationLemmas. apply fsc_swap_maintains_work_conservation => //. - by rewrite scheduled_at_def; apply /eqP => //. - apply (scheduled_at_implies_later_deadline sched) => //. - + by apply ideal_proc_model_ensures_ideal_progress. + rewrite /all_deadlines_met in (H_no_deadline_misses). now apply (H_no_deadline_misses s t_edf); rewrite scheduled_at_def; apply /eqP. + by rewrite scheduled_at_def; apply/eqP => //. @@ -380,4 +379,3 @@ Section EDFTransformWorkConservationLemmas. Qed. End EDFTransformWorkConservationLemmas. - diff --git a/model/preemption/parameter.v b/model/preemption/parameter.v index 46e04302acc05d665dd2aca6c021439ae9940bdd..c92656e23bb5d2c9942b2e533eaeb9865792262a 100644 --- a/model/preemption/parameter.v +++ b/model/preemption/parameter.v @@ -35,29 +35,11 @@ Section MaxAndLastNonpreemptiveSegment. (** We observe that the conversion indeed is an equivalent way of representing the set of preemption points. *) - Remark conversion_preserves_equivalence: + Remark conversion_preserves_equivalence : forall (j : Job) (Ï : work), Ï <= job_cost j -> job_preemptable j Ï <-> Ï \in job_preemption_points j. - Proof. - intros ? ? LE. - case: (posnP (job_cost j)) => [ZERO|POS]. - { unfold job_preemption_points. - split; intros PP. - - move: LE; rewrite ZERO leqn0; move => /eqP EQ; subst. - by simpl; rewrite PP. - - rewrite ZERO in PP; simpl in PP. - destruct (job_preemptable j 0) eqn:EQ; last by done. - by move: PP => /orP [/eqP A1| FF]; subst. - } - have F: job_cost j == 0 = false. - { by apply/eqP/neqP; rewrite -lt0n. } - split; intros PP. - all: unfold job_preemption_points in *. - - rewrite mem_filter; apply/andP; split; first by done. - by rewrite mem_iota subn0 add0n //; apply/andP; split. - - by move: PP; rewrite mem_filter; move => /andP [PP _]. - Qed. + Proof. by move=> j rho le; rewrite mem_filter mem_index_iota ltnS le/= andbT. Qed. (** We further define a function that, for a given job, yields the sequence of lengths of its nonpreemptive segments. *)