add lemmas to exploit basic behavior hypotheses

This ensures all hypotheses in behavior have corresponding trivial lemmas
in `analysis.facts.all` that enable to exploit them, which makes them 
easier to discover with `Search`.

This also makes the code more robust to potential changes in the precise way
these hypotheses are stated.

analysis/facts/behavior/arrivals.v

@@ -26,6 +26,20 @@ Section ArrivalPredicates.
       has_arrived j t.
   Proof. move=> ? ?; exact: ltnW. Qed.
 
+  (** Furthermore, we restate a common hypothesis to make its
+      implication 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.
+
+  (** We restate another common hypothesis to make its implication
+      easier to discover. *)
+  Lemma uniq_valid_arrival :
+    forall arr_seq,
+      valid_arrival_sequence arr_seq -> arrival_sequence_uniq arr_seq.
+  Proof. by move=> ? []. Qed.
+
 End ArrivalPredicates.
 
 (** In this section, we relate job readiness to [has_arrived]. *)
@@ -79,6 +93,28 @@ Section Arrived.
       backlogged sched j t -> ~~ completed_by sched j t.
   Proof. by move=> ? ? /andP[/any_ready_job_is_pending /andP[]]. Qed.
 
+  (** Finally, we restate common hypotheses on the well-formedness of
+      schedules to make their implications more easily
+      discoverable. First, on the readiness of scheduled jobs, ... *)
+  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.
+
+  (** ... second, on the origin of scheduled jobs, and ... *)
+  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.
+
+  (** ... third, on the readiness of jobs in valid schedules. *)
+  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.
 
 (** In this section, we establish useful facts about arrival sequence prefixes. *)
@@ -155,16 +191,24 @@ Section ArrivalSequencePrefix.
     (** Assume that job arrival times are consistent. *)
     Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
 
-    (** To simplify subsequent proofs, we restate the
-        [H_consistent_arrival_times] assumption as a trivial corollary. *)
+    (** To make the hypothesis and its implication easier to discover,
+        we restate it as a trivial lemma. *)
+    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.
+
+    (** Similarly, to simplify subsequent proofs, we restate the
+        [H_consistent_arrival_times] assumption as a trivial
+        corollary. *)
     Lemma job_arrival_at :
       forall {j t},
         j \in arrivals_at arr_seq t -> job_arrival j = t.
     Proof. exact: H_consistent_arrival_times. Qed.
 
-    (** First, we observe that any job in the set of all arrivals
-        between time instants [t1] and [t2] must arrive in the
-        interval <<[t1,t2)>>. *)
+    (** To begin with actual properties, we observe that any job in
+        the set of all arrivals between time instants [t1] and [t2]
+        must arrive in the interval <<[t1,t2)>>. *)
     Lemma job_arrival_between :
       forall {j t1 t2},
         j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j < t2.

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 rt_eauto.
           move: BUSY => [PREF _].
           by eapply not_quiet_implies_not_idle; rt_eauto. }
@@ -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]]]]; rt_eauto.
       { 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; rt_eauto. }
     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. *)
@@ -249,7 +251,7 @@ 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;
-              rt_eauto;last by done.
+              rt_eauto; last by [].
             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.
@@ -260,17 +262,17 @@ Section AbstractRTAforFIFOwithArrivalCurves.
                 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 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.
+          move: INTER => /eqP ->; apply /negP; rewrite Bool.negb_involutive.
+          by apply leq_trans with t; [apply HAS | apply ltnW].
+          Unshelve.
+          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. *)

scripts/wordlist.pws

@@ -73,4 +73,6 @@ Gonthier
 setoid
 Leontyev
 et
-al
+al
\ No newline at end of file
+discoverable
+formedness