Add basic lemmas to exploit hypotheses in behavior

This ensures all hypotheses in behavior have corresponding trivial lemmas in analysis/facts/all that enable to exploit them. This also makes the code more robust to potential changes in the precise way these hypotheses are stated.

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.
 
 (** In this section, we establish useful facts about arrival sequence prefixes. *)
@@ -155,6 +187,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 :