Add basic lemmas to exploit hypotheses in behavior

analysis/facts/behavior/arrivals.v

@@ -10,6 +10,18 @@ Section ArrivalPredicates.
   (** Consider any kinds of jobs with arrival times. *)
   Context {Job : JobType} `{JobArrival Job}.
 
+  (** Make hypothesis more easier to discover. *)
+  Lemma consistent_times_valid_arrival :
+    forall arr_seq,
+      valid_arrival_sequence arr_seq -> consistent_arrival_times arr_seq.
+  Proof. by move=> ? []. Qed.
+
+  (** Make hypothesis more easier to discover. *)
+  Lemma uniq_valid_arrival :
+    forall arr_seq,
+      valid_arrival_sequence arr_seq -> arrival_sequence_uniq arr_seq.
+  Proof. by move=> ? []. Qed.
+
   (** A job that arrives in some interval <<[t1, t2)>> certainly arrives before
       time [t2]. *)
   Lemma arrived_between_before:
@@ -79,6 +91,26 @@ Section Arrived.
       backlogged sched j t -> ~~ completed_by sched j t.
   Proof. by move=> ? ? /andP[/any_ready_job_is_pending /andP[]]. Qed.
 
+  (** Make hypothesis more easier to discover. *)
+  Lemma job_scheduled_implies_ready :
+    jobs_must_be_ready_to_execute sched ->
+    forall j t,
+      scheduled_at sched j t -> job_ready sched j t.
+  Proof. exact. Qed.
+
+  (** Make hypothesis more easier to discover. *)
+  Lemma valid_schedule_jobs_come_from_arrival_sequence :
+    forall arr_seq,
+      valid_schedule sched arr_seq ->
+      jobs_come_from_arrival_sequence sched arr_seq.
+  Proof. by move=> ? []. Qed.
+
+  (** Make hypothesis more easier to discover. *)
+  Lemma valid_schedule_jobs_must_be_ready_to_execute :
+    forall arr_seq,
+      valid_schedule sched arr_seq -> jobs_must_be_ready_to_execute sched.
+  Proof. by move=> ? []. Qed.
+
 End Arrived.
 
 (** We add some of the above lemmas to the "Hint Database"
@@ -162,6 +194,12 @@ Section ArrivalSequencePrefix.
     (** Assume that job arrival times are consistent. *)
     Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
 
+    (** Make hypothesis more easier to discover. *)
+    Lemma job_arrival_arrives_at :
+      forall {j t},
+        arrives_at arr_seq j t -> job_arrival j = t.
+    Proof. exact: H_consistent_arrival_times. Qed.
+
     (** To simplify subsequent proofs, we restate the
         [H_consistent_arrival_times] assumption as a trivial corollary. *)
     Lemma job_arrival_at :

analysis/facts/readiness/sequential.v

@@ -65,7 +65,8 @@ Section SequentialTasksReadiness.
     - move: READY => /andP [PEND /allP ALL]; apply: ALL.
       rewrite mem_filter; apply/andP; split; first by done.
       by apply arrived_between_implies_in_arrivals => //.
-    - by apply H_valid_schedule in SCHED; rewrite SCHED in NREADY.
+    - exfalso; apply/(negP NREADY)/job_scheduled_implies_ready => //.
+      exact: (valid_schedule_jobs_must_be_ready_to_execute sched arr_seq).
   Qed.
 
   (* Finally, we show that the sequential readiness model is a

analysis/facts/transform/wc_correctness.v

@@ -84,10 +84,9 @@ Section AuxiliaryLemmasWorkConservingTransformation.
       move=> j t.
       rewrite /find_swap_candidate.
       destruct search_arg eqn:RES; last first.
-      { move: (H_jobs_must_be_ready j t).
-        rewrite /scheduled_at scheduled_in_def => READY SCHED_J.
-        apply READY in SCHED_J.
-        by apply (ready_implies_arrived sched). }
+      { rewrite -scheduled_in_def => sched_j.
+        apply: (ready_implies_arrived sched).
+        exact: job_scheduled_implies_ready. }
       { move=> /eqP SCHED_J.
         move: RES => /search_arg_pred.
         rewrite SCHED_J //. }
@@ -100,8 +99,8 @@ Section AuxiliaryLemmasWorkConservingTransformation.
     Proof.
       move=> j t SCHED_AT.
       move: (swap_job_scheduled_cases _ _ _ _ _ SCHED_AT)=> [OTHER |[AT_T1 | AT_T2]].
-      { have READY: job_ready sched j t by apply H_jobs_must_be_ready; rewrite -OTHER //.
-          by apply (ready_implies_arrived sched). }
+      { apply: (ready_implies_arrived sched).
+        by apply: job_scheduled_implies_ready; rewrite // -OTHER. }
       { set t2 := find_swap_candidate arr_seq sched t1 in AT_T1.
         move: AT_T1 => [EQ_T1 SCHED_AT'].
         apply fsc_respects_has_arrived.
@@ -110,18 +109,18 @@ Section AuxiliaryLemmasWorkConservingTransformation.
         rewrite EQ_T1 in SCHED_AT'.
         rewrite SCHED_AT' /scheduled_at.
         by rewrite scheduled_in_def. }
-      { set t2 := find_swap_candidate arr_seq sched t1 in AT_T2.
-        move: AT_T2 => [EQ_T2 SCHED_AT'].
-        have ORDER: t1<=t2 by apply swap_candidate_is_in_future.
-        have READY: job_ready sched j t1 by apply H_jobs_must_be_ready; rewrite -SCHED_AT' //.
-        rewrite /job_ready /basic_ready_instance /pending /completed_by in READY.
-        move: READY => /andP [ARR _].
-        rewrite EQ_T2.
-        rewrite /has_arrived in ARR.
-        apply leq_trans with (n := t1) => //. }
+      set t2 := find_swap_candidate arr_seq sched t1 in AT_T2.
+      move: AT_T2 => [EQ_T2 SCHED_AT'].
+      have ORDER: t1<=t2 by apply swap_candidate_is_in_future.
+      have READY: job_ready sched j t1.
+      { by apply: job_scheduled_implies_ready; rewrite // -SCHED_AT'. }
+      rewrite /job_ready /basic_ready_instance /pending /completed_by in READY.
+      move: READY => /andP [ARR _].
+      rewrite EQ_T2.
+      exact: (leq_trans ARR).
     Qed.
 
-    (** Finally we show that, in the transformed schedule, jobs are scheduled 
+    (** Finally we show that, in the transformed schedule, jobs are scheduled
         only if they are ready. *)
     Lemma fsc_jobs_must_be_ready_to_execute:
       jobs_must_be_ready_to_execute sched'.

results/fifo/rta.v

@@ -163,8 +163,9 @@ Section AbstractRTAforFIFOwithArrivalCurves.
       { rewrite negb_or /is_priority_inversion /is_priority_inversion
                 /is_interference_from_another_hep_job => /andP [HYP1 HYP2].
         ideal_proc_model_sched_case_analysis_eq sched t jo.
-        { exfalso; clear HYP1 HYP2.
-          destruct H_valid_schedule as [A B].
+        { exfalso=> {HYP1 HYP2}.
+          have A : jobs_come_from_arrival_sequence sched arr_seq.
+          { exact: valid_schedule_jobs_come_from_arrival_sequence. }
           eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try by eauto 2 with basic_facts.
           move: BUSY => [PREF _].
           by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. }
@@ -194,7 +195,8 @@ Section AbstractRTAforFIFOwithArrivalCurves.
       busy_intervals_are_bounded_by arr_seq sched tsk interference interfering_workload L.
     Proof.
       intros j ARR TSK POS.
-      destruct H_valid_schedule as [COME MUST ].
+      have COME : jobs_come_from_arrival_sequence sched arr_seq.
+      { exact: valid_schedule_jobs_come_from_arrival_sequence. }
       edestruct exists_busy_interval_from_total_workload_bound
         with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; eauto 2 with basic_facts.
       { by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
@@ -202,7 +204,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
         split; first by done.
         by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts. }
     Qed.
-    
+
     (** In this section, we prove that, under FIFO scheduling, the cumulative priority inversion experienced
         by a job [j] in any interval within its busy window is always [0]. We later use this fact to prove the bound on 
         the cumulative interference. *)
@@ -238,39 +240,39 @@ Section AbstractRTAforFIFOwithArrivalCurves.
           { apply /negP.
             eapply (FIFO_implies_no_priority_inversion arr_seq); eauto with basic_facts.
             by apply /andP; split; [| rewrite COMPL]. }
-          { rewrite scheduled_at_def in INTER.
-            rewrite /is_priority_inversion. 
-            move: INTER => /eqP INTER; rewrite INTER.
-            apply /negP; rewrite Bool.negb_involutive /hep_job /FIFO.
-            move_neq_up CONTR.
-             have QTIme' : quiet_time arr_seq sched j t.
-            { move => j_hp ARRjhp HEP ARRbef.
-              eapply (scheduled_implies_higher_priority_completed arr_seq _ _ _ _ s); try by done.
-              - 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.
-            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.
-              by move: (H_job_cost_positive); rewrite /job_cost_positive COMPL. }
-            { specialize (QUIET t); feed QUIET.
-              - apply /andP; split; first by done.
-                by apply leq_trans with (t1 +  Δ) ; [| apply ltnW].
-              - by contradict QUIET. }
-            by destruct H_valid_schedule as [COME MUST]. } }
-        { destruct H_valid_schedule as [READY MUST].
-          have HAS : has_arrived s t by eapply (jobs_must_arrive_to_be_ready  sched).
           rewrite scheduled_at_def in INTER.
-          unfold is_priority_inversion.
-          move: INTER => /eqP ->.
-          apply /negP; rewrite Bool.negb_involutive.
-          by apply leq_trans with t; [apply HAS | apply ltnW]. }
+          rewrite /is_priority_inversion.
+          move: INTER => /eqP INTER; rewrite INTER.
+          apply /negP; rewrite Bool.negb_involutive /hep_job /FIFO.
+          move_neq_up CONTR.
+          have QTIme' : quiet_time arr_seq sched j t.
+          { move => j_hp ARRjhp HEP ARRbef.
+            eapply (scheduled_implies_higher_priority_completed arr_seq _ _ _ _ s); try by done.
+            - 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 [];
+            last exact: valid_schedule_jobs_come_from_arrival_sequence.
+          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.
+            by move: (H_job_cost_positive); rewrite /job_cost_positive COMPL. }
+          specialize (QUIET t); feed QUIET.
+          - apply /andP; split; first by done.
+            by apply leq_trans with (t1 +  Δ) ; [| apply ltnW].
+          - by contradict QUIET. }
+        have MUST : jobs_must_be_ready_to_execute sched.
+        { exact: (valid_schedule_jobs_must_be_ready_to_execute sched arr_seq). }
+        have HAS : has_arrived s t by eapply (jobs_must_arrive_to_be_ready  sched).
+        rewrite scheduled_at_def in INTER.
+        unfold is_priority_inversion.
+        move: INTER => /eqP ->; apply /negP; rewrite Bool.negb_involutive.
+        by apply leq_trans with t; [apply HAS | apply ltnW].
         Unshelve.
-        all: try by done.
+        all: by [].
       Qed.
-      
+
     End PriorityInversion.
 
     (** Using the above lemma, we prove that IBF is indeed an interference bound. *)
@@ -278,7 +280,8 @@ Section AbstractRTAforFIFOwithArrivalCurves.
       job_interference_is_bounded_by arr_seq sched tsk interference interfering_workload  IBF.
     Proof.
       move => t1 t2 Δ j ARRj TSKj BUSY IN_BUSY NCOMPL.
-      move: H_valid_schedule => [READY MUST ].
+      have COME : jobs_come_from_arrival_sequence sched arr_seq.
+      { exact: valid_schedule_jobs_come_from_arrival_sequence. }
       rewrite /cumul_interference cumulative_interference_split.
       have JPOS: job_cost_positive j by rewrite -ltnNge in NCOMPL; unfold job_cost_positive; lia.
       move: (BUSY) => [ [ /andP [LE GT] [QUIETt1 _ ] ] [QUIETt2 EQNs]].
@@ -294,27 +297,27 @@ Section AbstractRTAforFIFOwithArrivalCurves.
           ( try ( apply (task_rbf_1_ge_task_cost arr_seq) with (j0 := j) => //= ) ||
           apply (task_rbf_1_ge_task_cost arr_seq) with (j := j) => //=); first by auto.
           by apply task_rbf_monotone; [apply H_valid_arrival_curve | lia]. }
-        { eapply leq_trans; last first.
-          by erewrite leq_add2l; eapply task_rbf_excl_tsk_bounds_task_workload_excl_j; eauto 1.
-          rewrite addnBA.
-          { rewrite leq_sub2r //; eapply leq_trans.
-            - apply sum_over_partitions_le => j' inJOBS.
-              by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS). 
-            - rewrite (big_rem tsk) //= addnC leq_add //; last by rewrite subnKC.
-              rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=. 
-              apply leq_sum => tsk' _; rewrite andbC //=.
-              destruct (tsk' \in rem (T:=Task) tsk ts) eqn:IN; last by done.
-              apply rem_in in IN.
-              eapply leq_trans; last first.
-              + by apply (task_workload_le_task_rbf _ _ _ IN H_valid_job_cost H_is_arrival_curve t1).
-              + by rewrite addnBAC //= subnKC //= addn1; apply leqW. } 
-          { rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=.
-            - by rewrite TSKj; apply leq_addr.
-            - apply job_in_arrivals_between => //.
-              by apply /andP; split; [| rewrite subnKC; [rewrite addn1 |]].  } } }
+        eapply leq_trans; last first.
+        by erewrite leq_add2l; eapply task_rbf_excl_tsk_bounds_task_workload_excl_j; eauto 1.
+        rewrite addnBA.
+        { rewrite leq_sub2r //; eapply leq_trans.
+          - apply sum_over_partitions_le => j' inJOBS.
+            by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS). 
+          - rewrite (big_rem tsk) //= addnC leq_add //; last by rewrite subnKC.
+            rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=. 
+            apply leq_sum => tsk' _; rewrite andbC //=.
+            destruct (tsk' \in rem (T:=Task) tsk ts) eqn:IN; last by [].
+            apply rem_in in IN.
+            eapply leq_trans; last first.
+            + by apply (task_workload_le_task_rbf _ _ _ IN H_valid_job_cost H_is_arrival_curve t1).
+            + by rewrite addnBAC //= subnKC //= addn1; apply leqW. }
+        rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=.
+        - by rewrite TSKj; apply leq_addr.
+        - apply job_in_arrivals_between => //.
+          by apply /andP; split; [| rewrite subnKC; [rewrite addn1 |]].  }
       apply: arrivals_uniq => //.
       apply: job_in_arrivals_between => //.
-      by apply /andP; split; [ | rewrite addn1]. 
+      by apply /andP; split; [ | rewrite addn1].
     Qed.
 
     (** Finally, we show that there exists a solution for the response-time equation. *)