From d1fd3867af5a68e18d8934e281c1840de83b8ed0 Mon Sep 17 00:00:00 2001
From: Marco Maida <mmaida@mpi-sws.org>
Date: Mon, 6 Sep 2021 14:42:57 +0200
Subject: [PATCH] automatically use implications of `valid_schedule`

Added helper lemmas relating `valid_schedule` to job execution hps with hint.
Removed useless hps in aRTA.
---
 analysis/facts/behavior/arrivals.v            | 14 ++++++++++++++
 analysis/facts/behavior/completion.v          | 14 ++++++++++++++
 results/edf/rta/bounded_nps.v                 |  6 +-----
 results/edf/rta/bounded_pi.v                  | 10 ++--------
 results/edf/rta/floating_nonpreemptive.v      |  4 ----
 results/edf/rta/fully_nonpreemptive.v         |  6 +-----
 results/edf/rta/fully_preemptive.v            |  4 ----
 results/edf/rta/limited_preemptive.v          |  4 ----
 results/fixed_priority/rta/bounded_nps.v      | 12 +++++-------
 results/fixed_priority/rta/bounded_pi.v       | 19 ++++++++-----------
 .../rta/floating_nonpreemptive.v              |  4 ----
 .../fixed_priority/rta/fully_nonpreemptive.v  |  6 +-----
 results/fixed_priority/rta/fully_preemptive.v |  4 ----
 .../fixed_priority/rta/limited_preemptive.v   |  4 ----
 14 files changed, 46 insertions(+), 65 deletions(-)

diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 31612165f..3ff7f9739 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -83,6 +83,16 @@ Section Arrived.
     by apply ready_implies_arrived.
   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.
+  
   (** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
   Corollary backlogged_implies_arrived:
     forall j t,
@@ -108,6 +118,10 @@ Section Arrived.
 
 End Arrived.
 
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+    will be able to apply it automatically. *)
+Global Hint Resolve valid_schedule_implies_jobs_must_arrive_to_execute : basic_facts.
+
 (** In this section, we establish useful facts about arrival sequence prefixes. *)
 Section ArrivalSequencePrefix.
 
diff --git a/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v
index eaf7c733f..00b864885 100644
--- a/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ -345,6 +345,16 @@ Section CompletedJobs.
     by apply ready_implies_incomplete.
   Qed.
 
+  (** Furthermore, in a valid schedule, completed jobs don't execute. *)
+  Corollary valid_schedule_implies_completed_jobs_dont_execute:
+    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.
+
   (** We further observe that completed jobs don't execute if scheduled jobs
      always receive non-zero service and cumulative service never exceeds job
      costs. *)
@@ -363,6 +373,10 @@ Section CompletedJobs.
 
 End CompletedJobs.
 
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+    will be able to apply it automatically. *)
+Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_facts.
+
 (** Next, we relate the completion of jobs in schedules with identical prefixes. *)
 Section CompletionInTwoSchedules.
   (** Consider any processor model and any type of jobs with costs, arrival times, and a notion of readiness. *)
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 0249c7616..724872487 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -58,10 +58,6 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
   
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-  
   (** In addition, we assume the existence of a function mapping jobs
       to their preemption points ... *)
   Context `{JobPreemptable Job}.
@@ -277,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.
+      eapply uniprocessor_response_time_bound_edf; eauto 2 with basic_facts.
       - 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 965e25fc0..4df6367f7 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -67,10 +67,6 @@ Section AbstractRTAforEDFwithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Note that we differentiate between abstract and 
      classical notions of work conserving schedule. *)
   Let work_conserving_ab := definitions.work_conserving arr_seq sched.
@@ -370,9 +366,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
           erewrite instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks;
             eauto 2 with basic_facts.
           - by rewrite -H_job_of_tsk /jobs.
-          - rewrite /edf.EDF /EDF instantiated_quiet_time_equivalent_quiet_time //.
-            + by apply EDF_is_reflexive.
-            + by apply EDF_respects_sequential_tasks.
+          - rewrite instantiated_quiet_time_equivalent_quiet_time; eauto 2 with basic_facts.
         Qed.
 
         (** By lemma [service_of_jobs_le_workload], the total
@@ -689,7 +683,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
     { by rewrite /job_response_time_bound /completed_by ZERO. }    
     eapply uniprocessor_response_time_bound_seq with
         (interference0 := interference) (interfering_workload0 := interfering_workload)
-        (task_interference_bound_function := fun tsk A R => IBF A R) (L0 := L); eauto 3.
+        (task_interference_bound_function := fun tsk A R => IBF A R) (L0 := L); eauto 2 with basic_facts.
     - 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 d12eb4c3d..d8e0a6935 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -74,10 +74,6 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   Hypothesis H_sched_valid: valid_schedule sched arr_seq.
   Hypothesis H_schedule_with_limited_preemptions:
     schedule_respects_preemption_model arr_seq sched.
-  
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 2d8d78d56..8b1c16ddf 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -64,10 +64,6 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_sched_valid: valid_schedule sched arr_seq.
   Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
-  
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.  
@@ -141,7 +137,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
         by rewrite /job_response_time_bound /completed_by ZEROj.
     }
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L).
-    all: eauto 2 with basic_facts.
+    all: eauto 3 with basic_facts.
   Qed.
   
 End RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index e7f66b7b2..4b1bf311c 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -65,10 +65,6 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Hypothesis H_jobs_come_from_arrival_sequence:
     jobs_come_from_arrival_sequence sched arr_seq.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 7bf011585..07c3c9fa7 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -75,10 +75,6 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Hypothesis H_sched_valid: valid_schedule sched arr_seq.
   Hypothesis H_schedule_with_limited_preemptions:
     schedule_respects_preemption_model arr_seq sched.
-  
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 7224726f0..019dbefa3 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -54,10 +54,6 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
 
   (** ... and assume that the schedule is valid.  *)
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
-
-  (** We also assume that jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
   
   (** In addition, we assume the existence of a function mapping jobs
       to their preemption points ... *)
@@ -177,7 +173,8 @@ 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; move: NEQ => /andP [GE LE].
+      edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; eauto 2 with basic_facts.
+      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.
       - rewrite leq_subLR.
@@ -198,7 +195,8 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         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) (t1 := t1) (t2 := t2) (t := t) as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2.
+          with (K := ppt - t1) (t1 := t1) (t2 := t2) (t := t)
+          as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts.
         { by exists ppt; split; [done | rewrite subnKC //; apply/andP]. } 
         { by rewrite subnKC //; apply/andP; split. }
         apply/eqP; rewrite eqb0 Bool.negb_involutive.
@@ -244,7 +242,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
       response_time_bounded_by tsk R.
     Proof.
       eapply uniprocessor_response_time_bound_fp;
-        eauto using priority_inversion_is_bounded. 
+        eauto using priority_inversion_is_bounded with basic_facts. 
     Qed.
     
   End ResponseTimeBound.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index c78811bd0..2489c3064 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -60,10 +60,6 @@ Section AbstractRTAforFPwithArrivalCurves.
   (** ... and assume that the schedule is valid.  *)
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
 
-  (** We also assume that jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-  
   (** Note that we differentiate between abstract and 
      classical notions of work conserving schedule. *)
   Let work_conserving_ab := definitions.work_conserving arr_seq sched.
@@ -205,7 +201,7 @@ Section AbstractRTAforFPwithArrivalCurves.
         + exfalso; clear HYP1 HYP2.
           eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto with basic_facts.
             by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle;
-                              eauto 2 using eqprop_to_eqbool.
+                              eauto 2 using eqprop_to_eqbool with basic_facts.
       - 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.
@@ -246,7 +242,8 @@ Section AbstractRTAforFPwithArrivalCurves.
     Proof.
       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.
+      edestruct (exists_busy_interval) with (delta := L) as [t1 [t2 [T1 [T2 GGG]]]];
+        eauto 2 with basic_facts.
       { by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_rbf'. }
       exists t1, t2; split; first by done.
       split; first by done.
@@ -295,11 +292,11 @@ Section AbstractRTAforFPwithArrivalCurves.
             (workload_of_jobs
                (fun jhp : Job => (FP_to_JLFP _ _) jhp j && (job_task jhp != job_task j))
                (arrivals_between arr_seq t1 (t1 + R0))).
-        { by apply service_of_jobs_le_workload; first apply ideal_proc_model_provides_unit_service. } 
+        { apply service_of_jobs_le_workload; first apply ideal_proc_model_provides_unit_service.
+          by apply (valid_schedule_implies_completed_jobs_dont_execute sched arr_seq). } 
         { rewrite /workload_of_jobs /total_ohep_rbf /total_ohep_request_bound_function_FP.
-          by rewrite -TSK; apply total_workload_le_total_rbf.
-        }
-      }
+          by rewrite -TSK; apply total_workload_le_total_rbf. } 
+        all: eauto 2 using arr_seq with basic_facts. }
     Qed.
 
     (** Finally, we show that there exists a solution for the response-time recurrence. *)
@@ -370,7 +367,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 3.
+    eapply uniprocessor_response_time_bound_seq; eauto 2 with basic_facts.
     - 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 a420c2cfe..10396808f 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -75,10 +75,6 @@ Section RTAforFloatingModelwithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
   Hypothesis H_schedule_with_limited_preemptions : schedule_respects_preemption_model arr_seq sched.
-  
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
       and assume that the relation is reflexive and transitive. *)
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 1f4f18249..0ba1115e8 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -68,10 +68,6 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
   Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule  sched.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
   Context `{FP_policy Task}.
@@ -153,7 +149,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
     }
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
         (L0 := L).
-    all: eauto 2 with basic_facts.
+    all: eauto 3 with basic_facts.
     - 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 1f1913a83..15e1f4670 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -68,10 +68,6 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   Hypothesis H_jobs_come_from_arrival_sequence:
     jobs_come_from_arrival_sequence sched arr_seq.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
   Context `{FP_policy Task}.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 4707900dc..a3d0b71da 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -76,10 +76,6 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Hypothesis H_schedule_respects_preemption_model:
     schedule_respects_preemption_model arr_seq sched.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
   Context `{FP_policy Task}.
-- 
GitLab