From af4fb1dbf290c22abb4f3cc0f514d8f8967909ac Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 7 Mar 2022 16:04:35 +0100
Subject: [PATCH] introduce [rt_auto] and [rt_eauto] tactics
This commit renames scope [basic_facts] into [basic_rt_facts] to
highlight the that lemmas collected in the scope are real-time (rt)
theory lemmas.
These new tactics are just shorthand for [(e)auto with basic_rt_facts].
---
analysis/abstract/ideal_jlfp_rta.v | 2 +-
analysis/facts/behavior/arrivals.v | 79 +++++++++++++++++--
analysis/facts/behavior/completion.v | 4 +-
analysis/facts/busy_interval/busy_interval.v | 28 +++----
analysis/facts/busy_interval/carry_in.v | 7 +-
.../facts/busy_interval/priority_inversion.v | 18 ++---
analysis/facts/model/ideal_schedule.v | 4 +-
analysis/facts/model/preemption.v | 2 +-
analysis/facts/model/rbf.v | 2 +-
analysis/facts/periodic/arrival_separation.v | 8 +-
analysis/facts/periodic/sporadic.v | 4 +-
analysis/facts/periodic/task_arrivals_size.v | 4 +-
analysis/facts/preemption/job/limited.v | 2 +-
analysis/facts/preemption/job/nonpreemptive.v | 6 +-
analysis/facts/preemption/job/preemptive.v | 2 +-
.../facts/preemption/rtc_threshold/floating.v | 4 +-
.../rtc_threshold/job_preemptable.v | 4 +-
.../facts/preemption/rtc_threshold/limited.v | 2 +-
.../preemption/rtc_threshold/nonpreemptive.v | 2 +-
.../preemption/rtc_threshold/preemptive.v | 4 +-
analysis/facts/preemption/task/floating.v | 4 +-
analysis/facts/preemption/task/limited.v | 4 +-
.../facts/preemption/task/nonpreemptive.v | 4 +-
analysis/facts/preemption/task/preemptive.v | 4 +-
analysis/facts/priority/edf.v | 6 +-
analysis/facts/priority/fifo.v | 12 +--
analysis/facts/readiness/basic.v | 4 +-
model/priority/classes.v | 4 +-
model/priority/deadline_monotonic.v | 4 +-
model/priority/edf.v | 4 +-
model/priority/fifo.v | 4 +-
model/priority/gel.v | 4 +-
model/priority/numeric_fixed_priority.v | 4 +-
model/priority/rate_monotonic.v | 4 +-
results/edf/rta/bounded_nps.v | 6 +-
results/edf/rta/bounded_pi.v | 24 +++---
results/edf/rta/floating_nonpreemptive.v | 2 +-
results/edf/rta/fully_nonpreemptive.v | 2 +-
results/edf/rta/fully_preemptive.v | 2 +-
results/edf/rta/limited_preemptive.v | 2 +-
results/fifo/rta.v | 26 +++---
results/fixed_priority/rta/bounded_nps.v | 6 +-
results/fixed_priority/rta/bounded_pi.v | 20 ++---
.../rta/floating_nonpreemptive.v | 2 +-
.../fixed_priority/rta/fully_nonpreemptive.v | 2 +-
results/fixed_priority/rta/fully_preemptive.v | 2 +-
.../fixed_priority/rta/limited_preemptive.v | 2 +-
util/tactics.v | 14 ++++
48 files changed, 221 insertions(+), 145 deletions(-)
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index ddfadd5c8..839ad64b9 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -514,7 +514,7 @@ Section JLFPInstantiation.
rewrite eqn_add2r; unfold hep_job.
erewrite H_priority_is_reflexive; eauto 2.
rewrite eqn_leq; apply/andP; split; try eauto 2.
- by apply service_at_most_cost; eauto with basic_facts.
+ by apply service_at_most_cost; rt_eauto.
Qed.
(** The equivalence trivially follows from the lemmas above. *)
diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 05335ff2b..27461995c 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -81,13 +81,6 @@ Section Arrived.
End Arrived.
-(** We add some of the above lemmas to the "Hint Database"
- [basic_facts], so the [auto] tactic will be able to use them. *)
-Global Hint Resolve
- valid_schedule_implies_jobs_must_arrive_to_execute
- jobs_must_arrive_to_be_ready
- : basic_facts.
-
(** In this section, we establish useful facts about arrival sequence prefixes. *)
Section ArrivalSequencePrefix.
@@ -295,3 +288,75 @@ Section ArrivalSequencePrefix.
End ArrivalTimes.
End ArrivalSequencePrefix.
+
+(** In this section, we establish a few auxiliary facts about the
+ relation between the property of being scheduled and arrival
+ predicates to facilitate automation. *)
+Section ScheduledImpliesArrives.
+
+ (** Consider any type of jobs. *)
+ Context {Job : JobType}.
+ Context `{JobArrival Job}.
+
+ (** Consider any kind of processor state model, ... *)
+ Context {PState : ProcessorState Job}.
+
+ (** ... any job arrival sequence with consistent arrivals, .... *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+
+ (** ... and 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. *)
+ Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+
+
+ (** Next, consider a job [j] ... *)
+ Variable j : Job.
+
+ (** ... which is scheduled at a time instant [t]. *)
+ Variable t : instant.
+ Hypothesis H_scheduled_at : scheduled_at sched j t.
+
+ (** Then we show that [j] arrives in [arr_seq]. *)
+ Lemma arrives_in_jobs_come_from_arrival_sequence :
+ arrives_in arr_seq j.
+ Proof.
+ by apply: H_jobs_come_from_arrival_sequence H_scheduled_at.
+ Qed.
+
+ (** Job [j] has arrived by time instant [t]. *)
+ Lemma arrived_between_jobs_must_arrive_to_execute :
+ has_arrived j t.
+ Proof.
+ by apply: H_jobs_must_arrive_to_execute H_scheduled_at.
+ Qed.
+
+ (** Finally, for any future time [t'], job [j] arrives before [t']. *)
+ Lemma arrivals_before_scheduled_at :
+ forall t',
+ t < t' ->
+ j \in arrivals_before arr_seq t'.
+ Proof.
+ move=> t' LTtt'.
+ apply: arrived_between_implies_in_arrivals => //.
+ - by apply: arrives_in_jobs_come_from_arrival_sequence.
+ - apply: leq_ltn_trans LTtt'.
+ by apply: arrived_between_jobs_must_arrive_to_execute.
+ Qed.
+
+End ScheduledImpliesArrives.
+
+(** We add some of the above lemmas to the "Hint Database"
+ [basic_rt_facts], so the [auto] tactic will be able to use them. *)
+Global Hint Resolve
+ arrivals_before_scheduled_at
+ arrivals_uniq
+ arrived_between_implies_in_arrivals
+ arrived_between_jobs_must_arrive_to_execute
+ arrives_in_jobs_come_from_arrival_sequence
+ jobs_must_arrive_to_be_ready
+ valid_schedule_implies_jobs_must_arrive_to_execute
+ : basic_rt_facts.
diff --git a/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v
index 29ff9170a..3caae12cf 100644
--- a/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ -359,9 +359,9 @@ Section CompletedJobs.
End CompletedJobs.
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
will be able to apply it automatically. *)
-Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_facts.
+Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_rt_facts.
(** Next, we relate the completion of jobs in schedules with identical prefixes. *)
Section CompletionInTwoSchedules.
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index 7cf5cd230..5f910fa80 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -46,7 +46,6 @@ Section ExistsBusyIntervalJLFP.
(** For simplicity, let's define some local names. *)
Let job_pending_at := pending sched.
Let job_completed_by := completed_by sched.
- Let arrivals_between := arrivals_between arr_seq.
(** Consider an arbitrary task [tsk]. *)
Variable tsk : Task.
@@ -107,7 +106,7 @@ Section ExistsBusyIntervalJLFP.
Proof.
rename H_quiet into QUIET, H_not_quiet into NOTQUIET.
destruct (has (fun j_hp => (~~ job_completed_by j_hp t2) && hep_job j_hp j)
- (arrivals_between t1 t2)) eqn:COMP.
+ (arrivals_between arr_seq t1 t2)) eqn:COMP.
{ move: COMP => /hasP [j_hp ARR /andP [NOTCOMP HP]].
move: (ARR) => INarr.
apply in_arrivals_implies_arrived_between in ARR; last by done.
@@ -189,7 +188,7 @@ Section ExistsBusyIntervalJLFP.
- by exfalso; move_neq_down CONTR; eapply leq_ltn_trans; eauto 2.
- have EX: exists hp__seq: seq Job,
forall j__hp, j__hp \in hp__seq <-> arrives_in arr_seq j__hp /\ job_pending_at j__hp t /\ hep_job j__hp j.
- { exists (filter (fun jo => (job_pending_at jo t) && (hep_job jo j)) (arrivals_between 0 t.+1)).
+ { exists (filter (fun jo => (job_pending_at jo t) && (hep_job jo j)) (arrivals_between arr_seq 0 t.+1)).
intros; split; intros T.
- move: T; rewrite mem_filter; move => /andP [/andP [PEN HP] IN].
repeat split; eauto using in_arrivals_implies_arrived.
@@ -260,7 +259,7 @@ Section ExistsBusyIntervalJLFP.
time interval <<[t1, t1 + Δ)>>. *)
Let service_received_by_hep_jobs_released_during t_beg t_end :=
service_of_higher_or_equal_priority_jobs
- sched (arrivals_between t_beg t_end) j t1 (t1 + Δ).
+ sched (arrivals_between arr_seq t_beg t_end) j t1 (t1 + Δ).
(** We prove that jobs with higher-than-or-equal priority that
released before time instant [t1] receive no service after time
@@ -271,12 +270,11 @@ Section ExistsBusyIntervalJLFP.
Proof.
intros.
rewrite /service_received_by_hep_jobs_released_during
- /service_of_higher_or_equal_priority_jobs
- /service_of_jobs /arrivals_between.
+ /service_of_higher_or_equal_priority_jobs /service_of_jobs.
rewrite [in X in _ = X](arrivals_between_cat _ _ t1);
[ | | rewrite leq_addr]; try done.
rewrite big_cat //=.
- rewrite -{1}[\sum_(j <- arrivals_between _ (t1 + Δ) | _)
+ rewrite -{1}[\sum_(j <- arrivals_between arr_seq _ (t1 + Δ) | _)
service_during sched j t1 (t1 + Δ)]add0n.
apply/eqP. rewrite eqn_add2r eq_sym exchange_big //=.
rewrite big1_seq //.
@@ -295,14 +293,14 @@ Section ExistsBusyIntervalJLFP.
(** Next we prove that the total service within a "non-quiet"
time interval <<[t1, t1 + Δ)>> is exactly [Δ]. *)
Lemma no_idle_time_within_non_quiet_time_interval:
- service_of_jobs sched predT (arrivals_between 0 (t1 + Δ)) t1 (t1 + Δ) = Δ.
+ service_of_jobs sched predT (arrivals_between arr_seq 0 (t1 + Δ)) t1 (t1 + Δ) = Δ.
Proof.
intros; unfold service_of_jobs, service_of_higher_or_equal_priority_jobs.
rewrite -{3}[Δ](sum_of_ones t1) exchange_big //=.
apply/eqP; rewrite eqn_leq; apply/andP; split.
{ rewrite leq_sum // => t' _.
- have SCH := @service_of_jobs_le_1 _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).
- by eapply leq_trans; last apply SCH; eauto using arrivals_uniq with basic_facts. }
+ have SCH := @service_of_jobs_le_1 _ _ _ _ sched predT (arrivals_between arr_seq 0 (t1 + Δ)).
+ by eapply leq_trans; last apply SCH; rt_eauto. }
{ rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=
leq_sum // => t' /andP [/andP [LT GT] _]; apply/sum_seq_gt0P.
ideal_proc_model_sched_case_analysis_eq sched t' jo.
@@ -355,14 +353,14 @@ Section ExistsBusyIntervalJLFP.
a given interval <<[t1, t2)>> that have higher-or-equal
priority w.r.t. the job [j] being analyzed. *)
Let hp_workload t1 t2 :=
- workload_of_higher_or_equal_priority_jobs j (arrivals_between t1 t2).
+ workload_of_higher_or_equal_priority_jobs j (arrivals_between arr_seq t1 t2).
(** With regard to the jobs with higher-or-equal priority that are released
in a given interval <<[t1, t2)>>, we also recall the service received by these
jobs in the same interval <<[t1, t2)>>. *)
Let hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs
- sched (arrivals_between t1 t2) j t1 t2.
+ sched (arrivals_between arr_seq t1 t2) j t1 t2.
(** Now we begin the proof. First, we show that the busy interval is bounded. *)
Section BoundingBusyInterval.
@@ -483,7 +481,7 @@ Section ExistsBusyIntervalJLFP.
{ rewrite leqn0 big1_seq // /service_at => i Hi.
by rewrite service_in_def SCHED. }
{ case PRIO1: (hep_job j1 j) => /=; first last.
- - apply service_of_jobs_le_1; auto with basic_facts.
+ - apply service_of_jobs_le_1; rt_auto.
by apply arrivals_uniq.
- rewrite leqn0 big1_seq; first by done.
move => j2 /andP [PRIO2 ARRj2].
@@ -515,11 +513,11 @@ Section ExistsBusyIntervalJLFP.
have PEND := not_quiet_implies_exists_pending_job.
rename H_no_quiet_time into NOTQUIET,
H_is_busy_prefix into PREFIX.
- set l := arrivals_between t1 (t1 + delta).
+ set l := arrivals_between arr_seq t1 (t1 + delta).
set hep := hep_job.
unfold hp_service, service_of_higher_or_equal_priority_jobs, service_of_jobs,
hp_workload, workload_of_higher_or_equal_priority_jobs, workload_of_jobs.
- fold arrivals_between l hep.
+ fold l hep.
move: (PREFIX) => [_ [QUIET _]].
move: (NOTQUIET) => NOTQUIET'.
feed (NOTQUIET' (t1 + delta)).
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index 2601666fd..708962c38 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -171,7 +171,7 @@ Section ExistsNoCarryIn.
Proof.
unfold total_service.
rewrite -{3}[Δ]addn0 -{2}(subnn t) addnBA // [in X in _ <= X]addnC.
- apply service_of_jobs_le_length_of_interval'; auto with basic_facts.
+ apply service_of_jobs_le_length_of_interval'; rt_auto.
by eapply arrivals_uniq; eauto 2.
Qed.
@@ -228,7 +228,7 @@ Section ExistsNoCarryIn.
H_jobs_must_arrive_to_execute
H_completed_jobs_dont_execute
predT 0 t t.
- feed_n 2 COMPL; auto with basic_facts.
+ feed_n 2 COMPL; rt_auto.
{ intros j A B; apply H_no_carry_in.
- eapply in_arrivals_implies_arrived; eauto 2.
- eapply in_arrivals_implies_arrived_between in A; eauto 2.
@@ -247,8 +247,7 @@ Section ExistsNoCarryIn.
by apply H_workload_is_bounded.
}
intros s ARR BEF.
- eapply workload_eq_service_impl_all_jobs_have_completed; eauto with basic_facts.
- by eapply arrived_between_implies_in_arrivals.
+ by eapply workload_eq_service_impl_all_jobs_have_completed; rt_eauto.
Qed.
End ProcessorIsNotTooBusyInduction.
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index d1a8964e4..88c90824a 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -125,7 +125,7 @@ Section PriorityInversionIsBounded.
~ is_idle sched t.
Proof.
intros IDLE.
- by exfalso; apply: not_quiet_implies_not_idle; eauto 2 with basic_facts.
+ by exfalso; apply: not_quiet_implies_not_idle; rt_eauto.
Qed.
(** Next we consider two cases: (1) when [t] is less than [t2 - 1] and (2) [t] is equal to [t2 - 1]. *)
@@ -202,7 +202,7 @@ Section PriorityInversionIsBounded.
now rewrite -pred_Sn.
}
have PEND: pending sched j t2.-1
- by rewrite -ARR; apply job_pending_at_arrival => //; eauto with basic_facts.
+ by rewrite -ARR; apply job_pending_at_arrival => //; rt_eauto.
apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].
eapply NOTHP, (H_priority_is_transitive 0); last by apply HEPhp.
apply (H_respects_policy _ _ t2.-1); auto.
@@ -259,13 +259,13 @@ Section PriorityInversionIsBounded.
move: (H_t_in_busy_interval) => /andP [GEt LEt].
have HP := scheduled_at_preemption_time_implies_higher_or_equal_priority _ Sched_jhp.
move: (Sched_jhp) => PENDING.
- eapply scheduled_implies_pending in PENDING; eauto 2 with basic_facts.
+ eapply scheduled_implies_pending in PENDING; rt_eauto.
apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _].
apply contraT; rewrite -ltnNge; intro LT; exfalso.
feed (QUIET jhp); first by eapply CONS, Sched_jhp.
specialize (QUIET HP LT).
have COMP: job_completed_by jhp t by apply: completion_monotonic QUIET.
- apply completed_implies_not_scheduled in COMP; eauto with basic_facts.
+ apply completed_implies_not_scheduled in COMP; rt_eauto.
by move: COMP => /negP COMP; apply COMP.
Qed.
@@ -331,14 +331,14 @@ Section PriorityInversionIsBounded.
}
repeat split; try done.
move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET EXj]]]; move: (Sched_jhp) => PENDING.
- eapply scheduled_implies_pending in PENDING; eauto with basic_facts.
+ eapply scheduled_implies_pending in PENDING; rt_eauto.
apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _].
apply contraT; rewrite -ltnNge; intro LT; exfalso.
feed (QUIET jhp); first by eapply H_jobs_come_from_arrival_sequence, Sched_jhp.
specialize (QUIET HP LT).
have COMP: job_completed_by jhp t.
{ apply: completion_monotonic QUIET; exact: leq_trans LEtp. }
- apply completed_implies_not_scheduled in COMP; eauto with basic_facts.
+ apply completed_implies_not_scheduled in COMP; rt_eauto.
by move : COMP => /negP COMP; apply : COMP.
Qed.
@@ -388,10 +388,10 @@ Section PriorityInversionIsBounded.
apply/negP; intros SCHED2.
specialize (QT jhp).
feed_n 3 QT; eauto.
- - have MATE: jobs_must_arrive_to_execute sched by eauto with basic_facts.
+ - have MATE: jobs_must_arrive_to_execute sched by rt_eauto.
have HA: has_arrived jhp t by apply MATE.
by done.
- apply completed_implies_not_scheduled in QT; eauto with basic_facts.
+ apply completed_implies_not_scheduled in QT; rt_eauto.
by move: QT => /negP NSCHED; apply: NSCHED.
Qed.
@@ -677,7 +677,7 @@ Section PriorityInversionIsBounded.
specialize (EXPP (service jlp t1)).
feed EXPP.
{ apply/andP; split; first by done.
- apply service_at_most_cost; eauto with basic_facts.
+ apply service_at_most_cost; rt_eauto.
}
move: EXPP => [pt [NEQ PP]].
exists pt; apply/andP; split; by done.
diff --git a/analysis/facts/model/ideal_schedule.v b/analysis/facts/model/ideal_schedule.v
index f3ce907d2..230402d36 100644
--- a/analysis/facts/model/ideal_schedule.v
+++ b/analysis/facts/model/ideal_schedule.v
@@ -247,11 +247,11 @@ Section IncrementalService.
End IncrementalService.
(** * Automation *)
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically. *)
Global Hint Resolve ideal_proc_model_is_a_uniprocessor_model
ideal_proc_model_ensures_ideal_progress
- ideal_proc_model_provides_unit_service : basic_facts.
+ ideal_proc_model_provides_unit_service : basic_rt_facts.
(** We also provide tactics for case analysis on ideal processor state. *)
diff --git a/analysis/facts/model/preemption.v b/analysis/facts/model/preemption.v
index f38a46af5..1ccd9e256 100644
--- a/analysis/facts/model/preemption.v
+++ b/analysis/facts/model/preemption.v
@@ -96,7 +96,7 @@ Section PreemptionFacts.
apply/allP; intros t'.
by rewrite mem_index_iota ltnS -eqn_leq; move => /eqP <-.
}
- have MATE : jobs_must_arrive_to_execute sched by eauto with basic_facts.
+ have MATE : jobs_must_arrive_to_execute sched by rt_eauto.
move : (H_sched_valid) => [COME_ARR READY].
have MIN := ex_minnP EX.
move: MIN => [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.
diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index 31df27fef..3508f44bd 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -319,7 +319,7 @@ Section RequestBoundFunctions.
Proof.
move => t GE.
destruct t; first by done.
- eapply leq_trans; first by apply task_rbf_1_ge_task_cost; eauto with basic_facts.
+ eapply leq_trans; first by apply task_rbf_1_ge_task_cost; rt_eauto.
rewrite /total_request_bound_function.
erewrite big_rem; last by exact H_tsk_in_ts.
apply leq_trans with (task_request_bound_function tsk t.+1); last by apply leq_addr.
diff --git a/analysis/facts/periodic/arrival_separation.v b/analysis/facts/periodic/arrival_separation.v
index 46af75dbf..89ed08c0e 100644
--- a/analysis/facts/periodic/arrival_separation.v
+++ b/analysis/facts/periodic/arrival_separation.v
@@ -103,7 +103,7 @@ Section JobArrivalSeparation.
move : BEFORE => [nj [NEQNJ [TSKNJ [ARRNJ INDNJ]]]]; rewrite TSKj2 in TSKNJ.
specialize (IHs nj j2); feed_n 6 IHs => //; first by lia.
{ by apply (lower_index_implies_earlier_arrival _ H_consistent_arrivals tsk);
- eauto with basic_facts; lia.
+ rt_eauto; lia.
}
move : IHs => [n [NZN ARRJ'NJ]].
move: (H_periodic_model nj) => PERIODIC; feed_n 3 PERIODIC => //; first by lia.
@@ -143,13 +143,13 @@ Section JobArrivalSeparation.
apply job_arrival_separation_when_index_diff_is_k with (k := (job_index arr_seq j2 - job_index arr_seq j1)); try done.
- apply subnKC.
move_neq_up IND.
- eapply lower_index_implies_earlier_arrival in IND; eauto with basic_facts.
+ eapply lower_index_implies_earlier_arrival in IND; rt_eauto.
now move_neq_down IND.
- case: (boolP (job_index arr_seq j1 == job_index arr_seq j2)) => [/eqP EQ_IND|NEQ_IND].
+ now apply equal_index_implies_equal_jobs in EQ_IND => //; rewrite H_j1_of_task.
+ move: NEQ_IND; rewrite neq_ltn => /orP [LT|LT].
- * now eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.
- * eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.
+ * now eapply (lower_index_implies_earlier_arrival) in LT; rt_eauto.
+ * eapply (lower_index_implies_earlier_arrival) in LT; rt_eauto.
now move_neq_down LT.
Qed.
diff --git a/analysis/facts/periodic/sporadic.v b/analysis/facts/periodic/sporadic.v
index 2a4f509e1..3fb575218 100644
--- a/analysis/facts/periodic/sporadic.v
+++ b/analysis/facts/periodic/sporadic.v
@@ -87,6 +87,6 @@ Section PeriodicTasksAsSporadicTasks.
End PeriodicTasksAsSporadicTasks.
-(** We add the [periodic_task_respects_sporadic_task_model] lemma into a "Hint Database" basic_facts,
+(** We add the [periodic_task_respects_sporadic_task_model] lemma into a "Hint Database" basic_rt_facts,
so Coq will be able to apply it automatically. *)
-Global Hint Extern 1 => apply periodic_task_respects_sporadic_task_model : basic_facts.
+Global Hint Extern 1 => apply periodic_task_respects_sporadic_task_model : basic_rt_facts.
diff --git a/analysis/facts/periodic/task_arrivals_size.v b/analysis/facts/periodic/task_arrivals_size.v
index 8d3b831fe..587383df7 100644
--- a/analysis/facts/periodic/task_arrivals_size.v
+++ b/analysis/facts/periodic/task_arrivals_size.v
@@ -67,7 +67,7 @@ Section TaskArrivalsSize.
move: A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
move: (ARRA); move: (ARRB); rewrite /arrivals_at => A_IN B_IN.
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
- have SPO : respects_sporadic_task_model arr_seq tsk; try by auto with basic_facts.
+ have SPO : respects_sporadic_task_model arr_seq tsk; try by rt_auto.
have EQ_ARR_A : (job_arrival a = t) by apply H_consistent_arrivals.
have EQ_ARR_B : (job_arrival b = t) by apply H_consistent_arrivals.
specialize (SPO a b); feed_n 6 SPO => //; try by lia.
@@ -129,7 +129,7 @@ Section TaskArrivalsSize.
move : (jobs_exists_later n) => [j' [ARR [TSK [ARRIVAL IND]]]].
apply (only_j_in_task_arrivals_at_j
arr_seq H_consistent_arrivals H_uniq_arr_seq tsk) in ARR => //;
- last by auto with basic_facts.
+ last by rt_auto.
rewrite /task_arrivals_at_job_arrival TSK in ARR.
now rewrite -ARRIVAL ARR.
Qed.
diff --git a/analysis/facts/preemption/job/limited.v b/analysis/facts/preemption/job/limited.v
index 6db85b504..d992e4620 100644
--- a/analysis/facts/preemption/job/limited.v
+++ b/analysis/facts/preemption/job/limited.v
@@ -225,4 +225,4 @@ Section ModelWithLimitedPreemptions.
Qed.
End ModelWithLimitedPreemptions.
-Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_facts.
+Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_rt_facts.
diff --git a/analysis/facts/preemption/job/nonpreemptive.v b/analysis/facts/preemption/job/nonpreemptive.v
index adb04aae5..b59ee9eb0 100644
--- a/analysis/facts/preemption/job/nonpreemptive.v
+++ b/analysis/facts/preemption/job/nonpreemptive.v
@@ -49,7 +49,7 @@ Section FullyNonPreemptiveModel.
+ rewrite /completed_by -ltnNge.
move: NCOMPL; rewrite neq_ltn; move => /orP [LE|GE]; [by done | exfalso].
move: GE; rewrite ltnNge; move => /negP GE; apply: GE.
- apply completion.service_at_most_cost; eauto 2 with basic_facts.
+ apply completion.service_at_most_cost; rt_eauto.
- intros t NSCHED SCHED.
rewrite /job_preemptable /fully_nonpreemptive_model.
apply/orP; left.
@@ -66,7 +66,7 @@ Section FullyNonPreemptiveModel.
have <-: (service_at sched j t.+1) = 1.
{ by apply/eqP; rewrite service_at_def eqb1 -scheduled_at_def. }
by rewrite -big_nat_recr //=.
- by apply completion.service_at_most_cost; eauto 2 with basic_facts.
+ by apply completion.service_at_most_cost; rt_eauto.
Qed.
(** We also prove that under the fully non-preemptive model
@@ -127,7 +127,7 @@ Section FullyNonPreemptiveModel.
Qed.
End FullyNonPreemptiveModel.
-Global Hint Resolve valid_fully_nonpreemptive_model : basic_facts.
+Global Hint Resolve valid_fully_nonpreemptive_model : basic_rt_facts.
(** In this section, we prove the equivalence between no preemptions and a non-preemptive schedule. *)
Section NoPreemptionsEquivalence.
diff --git a/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
index bb8fc1366..9df41b730 100644
--- a/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ -64,4 +64,4 @@ Section FullyPreemptiveModel.
Qed.
End FullyPreemptiveModel.
-Global Hint Resolve valid_fully_preemptive_model : basic_facts.
+Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
index cbfe9ce95..5cb883836 100644
--- a/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -35,9 +35,9 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
intros; split.
- by rewrite /task_rtc_bounded_by_cost.
- intros j ARR TSK.
- apply leq_trans with (job_cost j); eauto 2 with basic_facts.
+ apply leq_trans with (job_cost j); rt_eauto.
by move: TSK => /eqP <-; apply H_valid_job_cost.
Qed.
End TaskRTCThresholdFloatingNonPreemptiveRegions.
-Global Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 69778b68d..451319b8a 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -258,6 +258,6 @@ Section RunToCompletionThreshold.
End RunToCompletionThreshold.
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically. *)
-Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_facts.
+Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 4e560671a..a202b2916 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -140,4 +140,4 @@ Section TaskRTCThresholdLimitedPreemptions.
Qed.
End TaskRTCThresholdLimitedPreemptions.
-Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index 5fde74ce9..4fbcecd89 100644
--- a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -77,4 +77,4 @@ Section TaskRTCThresholdFullyNonPreemptive.
Qed.
End TaskRTCThresholdFullyNonPreemptive.
-Global Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/preemptive.v b/analysis/facts/preemption/rtc_threshold/preemptive.v
index 2a47fb546..f6495c33b 100644
--- a/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -33,9 +33,9 @@ Section TaskRTCThresholdFullyPreemptiveModel.
intros; split.
- by rewrite /task_rtc_bounded_by_cost.
- intros j ARR TSK.
- apply leq_trans with (job_cost j); eauto 2 with basic_facts.
+ apply leq_trans with (job_cost j); rt_eauto.
by move: TSK => /eqP <-; apply H_valid_job_cost.
Qed.
End TaskRTCThresholdFullyPreemptiveModel.
-Global Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_rt_facts.
diff --git a/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
index 92ced12af..0171bff61 100644
--- a/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ -106,8 +106,8 @@ Section FloatingNonPreemptiveRegionsModel.
End FloatingNonPreemptiveRegionsModel.
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
Global Hint Resolve
valid_fixed_preemption_points_model_lemma
floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
- floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
+ floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.
diff --git a/analysis/facts/preemption/task/limited.v b/analysis/facts/preemption/task/limited.v
index 983c8c61b..80ba93c84 100644
--- a/analysis/facts/preemption/task/limited.v
+++ b/analysis/facts/preemption/task/limited.v
@@ -108,8 +108,8 @@ Section LimitedPreemptionsModel.
End LimitedPreemptionsModel.
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
Global Hint Resolve
valid_fixed_preemption_points_model_lemma
fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
- fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
+ fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.
diff --git a/analysis/facts/preemption/task/nonpreemptive.v b/analysis/facts/preemption/task/nonpreemptive.v
index 286756642..bc3360d50 100644
--- a/analysis/facts/preemption/task/nonpreemptive.v
+++ b/analysis/facts/preemption/task/nonpreemptive.v
@@ -85,8 +85,8 @@ Section FullyNonPreemptiveModel.
End FullyNonPreemptiveModel.
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
Global Hint Resolve
valid_fully_nonpreemptive_model
fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions
- fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
+ fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.
diff --git a/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
index 512b68311..f82e5bcd6 100644
--- a/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -57,8 +57,8 @@ Section FullyPreemptiveModel.
End FullyPreemptiveModel.
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
Global Hint Resolve
valid_fully_preemptive_model
fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions
- fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments : basic_facts.
+ fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments : basic_rt_facts.
diff --git a/analysis/facts/priority/edf.v b/analysis/facts/priority/edf.v
index ed19b6a0a..a9d7d2ebb 100644
--- a/analysis/facts/priority/edf.v
+++ b/analysis/facts/priority/edf.v
@@ -29,9 +29,9 @@ Section PropertiesOfEDF.
End PropertiesOfEDF.
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
will be able to apply it automatically. *)
-Global Hint Resolve EDF_respects_sequential_tasks : basic_facts.
+Global Hint Resolve EDF_respects_sequential_tasks : basic_rt_facts.
Require Export prosa.model.task.sequentiality.
@@ -98,7 +98,7 @@ Section SequentialEDF.
Proof.
intros ? ? ? ARR1 ARR2 SAME LT.
eapply early_hep_job_is_scheduled => //; eauto 2.
- - by auto with basic_facts.
+ - by rt_auto.
- move : H_valid_model_with_bounded_nonpreemptive_segments => [VALID _]; apply VALID.
- clear t; intros ?.
move: SAME => /eqP SAME.
diff --git a/analysis/facts/priority/fifo.v b/analysis/facts/priority/fifo.v
index 3228d7e60..94941ff1d 100644
--- a/analysis/facts/priority/fifo.v
+++ b/analysis/facts/priority/fifo.v
@@ -56,7 +56,7 @@ Section BasicLemmas.
apply /negP; rewrite negb_and.
apply /orP; right; apply /negPn.
have -> : scheduled_at sched s t -> completed_by sched j t => //.
- eapply (early_hep_job_is_scheduled); try eauto 2 with basic_facts.
+ eapply (early_hep_job_is_scheduled); try rt_eauto.
- by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=].
Qed.
@@ -74,7 +74,7 @@ Section BasicLemmas.
move => j' t SCHED j_hp ARRjhp HEP.
have EARLIER: job_arrival j_hp < job_arrival j' by rewrite -ltnNge in HEP.
eapply (early_hep_job_is_scheduled arr_seq _ sched _ _ _ _ j_hp j' _ _ _ t).
- Unshelve. all : eauto with basic_facts.
+ Unshelve. all : rt_eauto.
move=> t'; apply /andP; split => //.
by apply ltnW.
Qed.
@@ -91,7 +91,7 @@ Section BasicLemmas.
Lemma tasks_execute_sequentially : sequential_tasks arr_seq sched.
Proof.
move => j1 j2 t ARRj1 ARRj2 SAME_TASKx LT => //.
- eapply (early_hep_job_is_scheduled); try eauto 2 with basic_facts.
+ eapply (early_hep_job_is_scheduled); try rt_eauto.
by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=].
Qed.
@@ -117,7 +117,7 @@ Section BasicLemmas.
{ specialize (H_work_conservation j t).
destruct H_work_conservation as [j_other SCHEDj_other]; first by eapply (COME j t.-1 SCHED1).
- do 2 (apply /andP; split; last by done).
- eapply scheduled_implies_pending in SCHED1; try eauto with basic_facts.
+ eapply scheduled_implies_pending in SCHED1; try rt_eauto.
move : SCHED1 => /andP [HAS COMPL].
by apply leq_trans with t.-1; [exact HAS| lia].
- move: SCHEDj_other IDLE.
@@ -130,8 +130,8 @@ Section BasicLemmas.
by repeat (apply /andP ; split; try by done).
}
rewrite /hep_job /fifo.FIFO -ltnNge in HEP.
- eapply (early_hep_job_is_scheduled arr_seq ) in SCHED1; try eauto 2 with basic_facts.
- - apply scheduled_implies_not_completed in INTER; eauto with basic_facts.
+ eapply (early_hep_job_is_scheduled arr_seq ) in SCHED1; try rt_eauto.
+ - apply scheduled_implies_not_completed in INTER; rt_eauto.
by eapply (incompletion_monotonic sched s t.-1 t) in INTER; [move: INTER => /negP|lia].
- by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=]. }
Qed.
diff --git a/analysis/facts/readiness/basic.v b/analysis/facts/readiness/basic.v
index c3e0d39f5..6b6f43775 100644
--- a/analysis/facts/readiness/basic.v
+++ b/analysis/facts/readiness/basic.v
@@ -67,6 +67,6 @@ Section LiuAndLaylandReadiness.
End LiuAndLaylandReadiness.
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
will be able to apply it automatically. *)
-Global Hint Resolve basic_readiness_is_work_bearing_readiness : basic_facts.
+Global Hint Resolve basic_readiness_is_work_bearing_readiness : basic_rt_facts.
diff --git a/model/priority/classes.v b/model/priority/classes.v
index ac48795dc..c7766865b 100644
--- a/model/priority/classes.v
+++ b/model/priority/classes.v
@@ -151,6 +151,6 @@ Section Priorities.
End Priorities.
-(** We add the above observation into the "Hint Database" basic_facts, so Coq
+(** We add the above observation into the "Hint Database" basic_rt_facts, so Coq
will be able to apply it automatically. *)
-Global Hint Resolve respects_sequential_tasks : basic_facts.
+Global Hint Resolve respects_sequential_tasks : basic_rt_facts.
diff --git a/model/priority/deadline_monotonic.v b/model/priority/deadline_monotonic.v
index 625606f0c..8e9ee8abd 100644
--- a/model/priority/deadline_monotonic.v
+++ b/model/priority/deadline_monotonic.v
@@ -35,11 +35,11 @@ Section Properties.
End Properties.
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically. *)
Global Hint Resolve
DM_is_reflexive
DM_is_transitive
DM_is_total
- : basic_facts.
+ : basic_rt_facts.
diff --git a/model/priority/edf.v b/model/priority/edf.v
index 24b052b46..ea18bac0b 100644
--- a/model/priority/edf.v
+++ b/model/priority/edf.v
@@ -35,11 +35,11 @@ Section PropertiesOfEDF.
End PropertiesOfEDF.
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically. *)
Global Hint Resolve
EDF_is_reflexive
EDF_is_transitive
EDF_is_total
- : basic_facts.
+ : basic_rt_facts.
diff --git a/model/priority/fifo.v b/model/priority/fifo.v
index a89e24c90..453f296f6 100644
--- a/model/priority/fifo.v
+++ b/model/priority/fifo.v
@@ -31,11 +31,11 @@ Section Properties.
End Properties.
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically. *)
Global Hint Resolve
FIFO_is_reflexive
FIFO_is_transitive
FIFO_is_total
- : basic_facts.
+ : basic_rt_facts.
diff --git a/model/priority/gel.v b/model/priority/gel.v
index 319574e09..7127b03b7 100644
--- a/model/priority/gel.v
+++ b/model/priority/gel.v
@@ -75,11 +75,11 @@ Section PropertiesOfGEL.
End PropertiesOfGEL.
-(** We add the above facts into a "Hint Database" basic_facts, so Coq
+(** We add the above facts into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically where needed. *)
Global Hint Resolve
GEL_is_reflexive
GEL_is_transitive
GEL_is_total
- : basic_facts.
+ : basic_rt_facts.
diff --git a/model/priority/numeric_fixed_priority.v b/model/priority/numeric_fixed_priority.v
index 7dfb26e93..7f5c73e10 100644
--- a/model/priority/numeric_fixed_priority.v
+++ b/model/priority/numeric_fixed_priority.v
@@ -46,11 +46,11 @@ Section Properties.
End Properties.
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically. *)
Global Hint Resolve
NFP_is_reflexive
NFP_is_transitive
NFP_is_total
- : basic_facts.
+ : basic_rt_facts.
diff --git a/model/priority/rate_monotonic.v b/model/priority/rate_monotonic.v
index 0af602c49..ca0895ed0 100644
--- a/model/priority/rate_monotonic.v
+++ b/model/priority/rate_monotonic.v
@@ -37,11 +37,11 @@ Section Properties.
End Properties.
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically. *)
Global Hint Resolve
RM_is_reflexive
RM_is_transitive
RM_is_total
- : basic_facts.
+ : basic_rt_facts.
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index ceec37fd4..123cb771c 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -208,7 +208,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
intros t _; case: (sched t); last by done.
by intros s; destruct (hep_job s j).
}
- edestruct @preemption_time_exists as [ppt [PPT NEQ2]]; eauto 2 with basic_facts.
+ edestruct @preemption_time_exists as [ppt [PPT NEQ2]]; rt_eauto.
move: NEQ2 => /andP [GE LE].
apply leq_trans with (cumulative_priority_inversion sched j t1 ppt);
last apply leq_trans with (ppt - t1).
@@ -222,7 +222,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
rewrite big_nat_cond big1 //; move => t /andP [/andP [GEt LTt] _ ].
case SCHED: (sched t) => [s | ]; last by done.
edestruct @not_quiet_implies_exists_scheduled_hp_job
- with (K := ppt - t1) (t := t) as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts.
+ with (K := ppt - t1) (t := t) as [j_hp [ARRB [HP SCHEDHP]]]; rt_eauto.
{ exists ppt; split. by done. by rewrite subnKC //; apply/andP; split. }
{ by rewrite subnKC //; apply/andP; split. }
apply/eqP; rewrite eqb0 Bool.negb_involutive.
@@ -273,7 +273,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Theorem uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments:
response_time_bounded_by tsk R.
Proof.
- eapply uniprocessor_response_time_bound_edf; eauto 2 with basic_facts.
+ eapply uniprocessor_response_time_bound_edf; rt_eauto.
- eapply EDF_implies_sequential_tasks; eauto 2.
+ by apply basic.basic_readiness_is_work_bearing_readiness, EDF_is_reflexive.
- by apply priority_inversion_is_bounded.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 793083c42..01fa39bfa 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -226,9 +226,9 @@ Section AbstractRTAforEDFwithArrivalCurves.
move => /andP [HYP1 HYP2].
ideal_proc_model_sched_case_analysis_eq sched t jo.
{ exfalso; clear HYP1 HYP2.
- eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
move: BUSY => [PREF _].
- by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. }
+ by eapply not_quiet_implies_not_idle; rt_eauto. }
{ clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move => /eqP EqSched_jo.
rewrite EqSched_jo in HYP1, HYP2.
move: HYP1 HYP2.
@@ -258,8 +258,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
unfold EDF in *.
intros j t1 t2 ARR TSK POS BUSY.
move: H_sched_valid => [CARR MBR].
- eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
- eapply all_jobs_have_completed_equiv_workload_eq_service; eauto 2 with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
+ eapply all_jobs_have_completed_equiv_workload_eq_service; rt_eauto.
intros s INs TSKs.
rewrite /arrivals_between in INs.
move: (INs) => NEQ.
@@ -286,11 +286,11 @@ Section AbstractRTAforEDFwithArrivalCurves.
intros j ARR TSK POS.
move: H_sched_valid => [CARR MBR].
edestruct exists_busy_interval_from_total_workload_bound
- with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; eauto 2 with basic_facts.
+ with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
{ by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
exists t1, t2; split; first by done.
split; first by done.
- by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts.
+ by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
Qed.
(** Next, we prove that [IBF_other] is indeed an interference bound. *)
@@ -346,7 +346,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
+ by rewrite /is_priority_inversion leq_addr.
+ by rewrite ltnW.
- apply H_priority_inversion_is_bounded; try done.
- eapply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval; eauto 2 with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval; rt_eauto.
by move: H_busy_interval => [PREF _].
Qed.
@@ -367,9 +367,9 @@ Section AbstractRTAforEDFwithArrivalCurves.
move: (H_busy_interval) => [[/andP [JINBI JINBI2] [QT _]] _].
move: H_sched_valid => [CARR MBR].
erewrite instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks;
- eauto 2 with basic_facts.
+ rt_eauto.
- by move: (H_job_of_tsk) => /eqP ->; rewrite /jobs.
- - by rewrite instantiated_quiet_time_equivalent_quiet_time; eauto 2 with basic_facts.
+ - by rewrite instantiated_quiet_time_equivalent_quiet_time; rt_eauto.
Qed.
(** By lemma [service_of_jobs_le_workload], the total
@@ -380,7 +380,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
service_of_jobs sched (EDF_not_from tsk) jobs t1 (t1 + Δ)
<= workload_of_jobs (EDF_not_from tsk) jobs.
Proof.
- by apply service_of_jobs_le_workload; eauto 2 with basic_facts.
+ by apply service_of_jobs_le_workload; rt_eauto.
Qed.
(** Next, we prove that the total workload of jobs
@@ -577,7 +577,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
by rewrite /completed_by /completed_by ZERO.
- move: (BUSY) => [[/andP [JINBI JINBI2] [QT _]] _].
rewrite (cumulative_task_interference_split arr_seq sched _ _ _ tsk j);
- eauto 2 with basic_facts; last first.
+ rt_eauto; last first.
{ by eapply arrived_between_implies_in_arrivals; eauto. }
rewrite /I leq_add //.
+ by apply cumulative_priority_inversion_is_bounded with t2.
@@ -683,7 +683,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
(task_interference_bound_function := fun tsk A R => IBF_other A R) (L0 := L) ) ||
eapply uniprocessor_response_time_bound_seq with
(interference := interference) (interfering_workload := interfering_workload)
- (task_interference_bound_function := fun tsk A R => IBF_other A R) (L := L)); eauto 2 with basic_facts.
+ (task_interference_bound_function := fun tsk A R => IBF_other A R) (L := L)); rt_eauto.
- by apply instantiated_i_and_w_are_coherent_with_schedule.
- by apply instantiated_interference_and_workload_consistent_with_sequential_tasks.
- by apply instantiated_busy_intervals_are_bounded.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 5b752d5c8..1c1bc8101 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -143,7 +143,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
move: (LIMJ) => [BEG [END _]].
try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L).
- all: eauto 2 with basic_facts.
+ all: rt_eauto.
rewrite subnn.
intros A SP.
apply H_R_is_maximum in SP.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index a828bdffa..ff4d924cc 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -141,7 +141,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
}
try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L).
- all: eauto 3 with basic_facts.
+ all: rt_eauto.
Qed.
End RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index 9be953143..aa060227e 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -129,7 +129,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
/fully_preemptive.fully_preemptive_model subnn big1_eq. }
try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L) .
- all: eauto 2 with basic_facts.
+ all: rt_eauto.
- move => A /andP [LT NEQ].
specialize (H_R_is_maximum A); feed H_R_is_maximum.
{ by apply/andP; split. }
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 061fab736..2004a0e5d 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -150,7 +150,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
}
try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L).
- all: eauto 2 with basic_facts.
+ all: rt_eauto.
rewrite subKn; first by done.
rewrite /task_last_nonpr_segment -(leq_add2r 1) subn1 !addn1 prednK; last first.
- rewrite /last0 -nth_last.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 59e285a0d..ec72b8f43 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -165,9 +165,9 @@ Section AbstractRTAforFIFOwithArrivalCurves.
ideal_proc_model_sched_case_analysis_eq sched t jo.
{ exfalso; clear HYP1 HYP2.
destruct H_valid_schedule as [A B].
- eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try by eauto 2 with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try by rt_eauto.
move: BUSY => [PREF _].
- by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. }
+ by eapply not_quiet_implies_not_idle; rt_eauto. }
{ clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move => /eqP EqSched_jo.
rewrite EqSched_jo in HYP1, HYP2.
move: HYP1 HYP2.
@@ -196,11 +196,11 @@ Section AbstractRTAforFIFOwithArrivalCurves.
intros j ARR TSK POS.
destruct H_valid_schedule as [COME MUST ].
edestruct exists_busy_interval_from_total_workload_bound
- with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; eauto 2 with basic_facts.
+ with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
{ by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
{ exists t1, t2; split; first by done.
split; first by done.
- by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts. }
+ by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto. }
Qed.
(** In this section, we prove that, under FIFO scheduling, the cumulative priority inversion experienced
@@ -236,7 +236,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
destruct (leqP (job_arrival j) t).
{ destruct (completed_by sched j t) eqn : COMPL; last first.
{ apply /negP.
- eapply (FIFO_implies_no_priority_inversion arr_seq); eauto with basic_facts.
+ eapply (FIFO_implies_no_priority_inversion arr_seq); rt_eauto.
by apply /andP; split; [| rewrite COMPL]. }
{ rewrite scheduled_at_def in INTER.
rewrite /is_priority_inversion.
@@ -249,11 +249,11 @@ Section AbstractRTAforFIFOwithArrivalCurves.
- by move : INTER => /eqP INTER; rewrite -scheduled_at_def in INTER.
- by rewrite -ltnNge; apply leq_ltn_trans with (job_arrival j). }
apply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval;
- eauto 2 with basic_facts;last by done.
+ rt_eauto;last by done.
move : H_busy_interval => [ [_ [_ [QUIET /andP [ARR _ ]]]] _].
destruct (leqP t t1) as [LE | LT].
{ have EQ : t = job_arrival j by apply eq_trans with t1; lia.
- rewrite EQ in COMPL; apply completed_on_arrival_implies_zero_cost in COMPL; eauto with basic_facts.
+ rewrite EQ in COMPL; apply completed_on_arrival_implies_zero_cost in COMPL; rt_eauto.
by move: (H_job_cost_positive); rewrite /job_cost_positive COMPL. }
{ specialize (QUIET t); feed QUIET.
- apply /andP; split; first by done.
@@ -284,9 +284,9 @@ Section AbstractRTAforFIFOwithArrivalCurves.
move: (BUSY) => [ [ /andP [LE GT] [QUIETt1 _ ] ] [QUIETt2 EQNs]].
erewrite (cumulative_priority_inversion_is_bounded j ARRj JPOS t1 t2); rewrite //= add0n.
rewrite (instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs arr_seq) //=;
- try by (try rewrite instantiated_quiet_time_equivalent_quiet_time); eauto 2 with basic_facts.
- eapply leq_trans; first by apply service_of_jobs_le_workload; eauto 2 with basic_facts.
- rewrite (leqRW (workload_equal_subset _ _ _ _ _ _ _)); eauto 2 with basic_facts.
+ try by (try rewrite instantiated_quiet_time_equivalent_quiet_time); rt_eauto.
+ eapply leq_trans; first by apply service_of_jobs_le_workload; rt_eauto.
+ rewrite (leqRW (workload_equal_subset _ _ _ _ _ _ _)); rt_eauto.
specialize (workload_minus_job_cost j) => ->.
{ rewrite /workload_of_jobs /IBF (big_rem tsk) //= (addnC (rbf tsk (job_arrival j - t1 + ε))).
rewrite -addnBA; last first.
@@ -386,12 +386,12 @@ Section AbstractRTAforFIFOwithArrivalCurves.
have GE: task_cost tsk <= R; last by lia.
rewrite !add0n in LE1.
rewrite -(leqRW LE2) -(leqRW LE1).
- by eapply (task_cost_le_sum_rbf arr_seq); eauto with basic_facts. }
+ by eapply (task_cost_le_sum_rbf arr_seq); rt_eauto. }
{ rewrite subnK; first by done.
rewrite !add0n in LE1. apply leq_trans with F; last by done.
apply leq_trans with (\sum_(tsko <- ts) rbf tsko ε); last by done.
apply leq_trans with (task_cost tsk); first by lia.
- eapply task_cost_le_sum_rbf; eauto with basic_facts. }
+ eapply task_cost_le_sum_rbf; rt_eauto. }
Qed.
End SolutionOfResponseTimeReccurenceExists.
@@ -412,7 +412,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
(interference_bound_function := fun tsk A R => IBF tsk A R) (L0 := L) ) ||
eapply uniprocessor_response_time_bound with
(interference := interference) (interfering_workload := interfering_workload)
- (interference_bound_function := fun tsk A R => IBF tsk A R) (L := L)); eauto 2 with basic_facts.
+ (interference_bound_function := fun tsk A R => IBF tsk A R) (L := L)); rt_eauto.
- by apply instantiated_i_and_w_are_coherent_with_schedule.
- by apply instantiated_busy_intervals_are_bounded.
- by apply instantiated_interference_is_bounded.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 40bce6903..1a7068ab5 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -173,7 +173,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
by intros s; case: (hep_job s j).
}
move: NEQ => /negP /negP; rewrite -ltnNge; move => BOUND.
- edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; eauto 2 with basic_facts.
+ edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; rt_eauto.
move: NEQ => /andP [GE LE].
apply leq_trans with (cumulative_priority_inversion sched j t1 ppt);
last apply leq_trans with (ppt - t1); first last.
@@ -196,7 +196,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
case SCHED: (sched t) => [s | ]; last by done.
edestruct (@not_quiet_implies_exists_scheduled_hp_job)
with (K := ppt - t1) (t1 := t1) (t2 := t2) (t := t)
- as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts.
+ as [j_hp [ARRB [HP SCHEDHP]]]; rt_eauto.
{ by exists ppt; split; [done | rewrite subnKC //; apply/andP]. }
{ by rewrite subnKC //; apply/andP; split. }
apply/eqP; rewrite eqb0 Bool.negb_involutive.
@@ -242,7 +242,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
response_time_bounded_by tsk R.
Proof.
eapply uniprocessor_response_time_bound_fp;
- eauto using priority_inversion_is_bounded with basic_facts.
+ eauto using priority_inversion_is_bounded with basic_rt_facts.
Qed.
End ResponseTimeBound.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 3f5966098..38f8f68c8 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -200,8 +200,8 @@ Section AbstractRTAforFPwithArrivalCurves.
* by exfalso.
* by subst s; rewrite scheduled_at_def //; apply/eqP.
+ exfalso; clear HYP1 HYP2.
- eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto with basic_facts.
- by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle; eauto 2 with basic_facts; apply/eqP.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
+ by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle; rt_eauto; apply/eqP.
- move: (HYP); rewrite scheduled_at_def; move => /eqP HYP2; apply/negP.
rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion
/is_interference_from_another_hep_job HYP2 negb_or.
@@ -219,8 +219,8 @@ Section AbstractRTAforFPwithArrivalCurves.
Proof.
intros j t1 t2 ARR TSK POS BUSY.
move: H_sched_valid => [CARR MBR].
- eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto with basic_facts.
- eapply all_jobs_have_completed_equiv_workload_eq_service; eauto with basic_facts.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
+ eapply all_jobs_have_completed_equiv_workload_eq_service; rt_eauto.
intros s ARRs TSKs.
move: (BUSY) => [[_ [QT _]] _].
apply QT.
@@ -243,11 +243,11 @@ Section AbstractRTAforFPwithArrivalCurves.
intros j ARR TSK POS.
move: H_sched_valid => [CARR MBR].
edestruct (exists_busy_interval) with (delta := L) as [t1 [t2 [T1 [T2 GGG]]]];
- eauto 2 with basic_facts.
+ rt_eauto.
{ by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_hep_rbf. }
exists t1, t2; split; first by done.
split; first by done.
- by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts.
+ by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
Qed.
(** Next, we prove that [IBF_other] is indeed an interference bound.
@@ -271,8 +271,8 @@ Section AbstractRTAforFPwithArrivalCurves.
move: H_sched_valid => [CARR MBR].
move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
{ by exfalso; rewrite /completed_by ZERO in NCOMPL. }
- eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
- rewrite /interference; erewrite cumulative_task_interference_split; eauto 2 with basic_facts; last first.
+ eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
+ rewrite /interference; erewrite cumulative_task_interference_split; rt_eauto; last first.
{ move: BUSY => [[_ [_ [_ /andP [GE LT]]]] _].
by eapply arrived_between_implies_in_arrivals; eauto 2. }
unfold IBF_other, interference.
@@ -297,7 +297,7 @@ Section AbstractRTAforFPwithArrivalCurves.
{ rewrite /workload_of_jobs /total_ohep_rbf /total_ohep_request_bound_function_FP.
move: (TSK) => /eqP <-; apply total_workload_le_total_ohep_rbf; try done.
by move: (TSK) => /eqP ->. }
- all: eauto 2 using arr_seq with basic_facts. }
+ all: eauto 2 using arr_seq with basic_rt_facts. }
Qed.
(** Finally, we show that there exists a solution for the response-time recurrence. *)
@@ -368,7 +368,7 @@ Section AbstractRTAforFPwithArrivalCurves.
move: H_sched_valid => [CARR MBR].
move: (posnP (@job_cost _ Cost js)) => [ZERO|POS].
{ by rewrite /job_response_time_bound /completed_by ZERO. }
- eapply uniprocessor_response_time_bound_seq; eauto 2 with basic_facts.
+ eapply uniprocessor_response_time_bound_seq; rt_eauto.
- by apply instantiated_i_and_w_are_consistent_with_schedule.
- by apply instantiated_interference_and_workload_consistent_with_sequential_tasks.
- by apply instantiated_busy_intervals_are_bounded.
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 469954409..73a987d3e 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -148,7 +148,7 @@ Section RTAforFloatingModelwithArrivalCurves.
move: (H_valid_task_model_with_floating_nonpreemptive_regions) => [LIMJ JMLETM].
move: (LIMJ) => [BEG [END _]].
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.
- all: eauto 2 with basic_facts.
+ all: rt_eauto.
- by apply sequential_readiness_implies_work_bearing_readiness.
- by apply sequential_readiness_implies_sequential_tasks.
- intros A SP.
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 925ad4882..e3d35cf10 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -154,7 +154,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
(L0 := L) ) ||
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
(L := L).
- all: eauto 3 with basic_facts.
+ all: rt_eauto.
- by apply sequential_readiness_implies_work_bearing_readiness.
- by apply sequential_readiness_implies_sequential_tasks.
Qed.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 28ceef67f..31574f38f 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -136,7 +136,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
{ by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
/fully_preemptive.fully_preemptive_model subnn big1_eq. }
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.
- all: eauto 2 with basic_facts.
+ all: rt_eauto.
rewrite /work_bearing_readiness.
- by apply sequential_readiness_implies_work_bearing_readiness.
- by apply sequential_readiness_implies_sequential_tasks => //.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 1dadfd26c..4d39b8f32 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -158,7 +158,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
with (L0 := L) ) ||
eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
with (L := L).
- all: eauto 2 with basic_facts.
+ all: rt_eauto.
- by apply sequential_readiness_implies_work_bearing_readiness.
- by apply sequential_readiness_implies_sequential_tasks.
- intros A SP.
diff --git a/util/tactics.v b/util/tactics.v
index 074cda81c..7f38418aa 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -83,6 +83,20 @@ Ltac feed_n n H := match constr:(n) with
| (S ?m) => feed H ; [| feed_n m H]
end.
+(** We introduce tactics [rt_auto] and [rt_eauto] as a shorthand for
+ [(e)auto with basic_rt_facts] to facilitate automation. Here, we
+ use scope [basic_rt_facts] that contains a collection of basic
+ real-time theory lemmas. *)
+(** Note: constant [3] was chosen because most of the basic rt facts
+ have the structure [A1 -> A2 -> ... B], where [Ai] is a hypothesis
+ usually present in the context, which gives the depth of the
+ search which is equal to two. One additional level of depth (3)
+ was added to support rare exceptions to this rule. At the same
+ time, the constant should not be too large to avoid slowdowns in
+ case of an unsuccessful application of automation. *)
+Ltac rt_auto := auto 3 with basic_rt_facts.
+Ltac rt_eauto := eauto 3 with basic_rt_facts.
+
(* ************************************************************************** *)
(** * Handier movement of inequalities. *)
(* ************************************************************************** *)
--
GitLab