Embeds arrival_uniq into arrival sequences

This avoid having to state arrival_uniq again and again almost each
time an arrival sequence is used, since arrival sequence without
uniq_arrival aren't really a thing.

analysis/abstract/abstract_rta.v

@@ -33,8 +33,7 @@ Section Abstract_RTA.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
-  
+
   (** Next, consider 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.

analysis/abstract/abstract_seq_rta.v

@@ -32,7 +32,6 @@ Section Sequential_Abstract_RTA.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** Next, consider any ideal uniprocessor schedule of this arrival sequence...*)
   Variable sched : schedule (ideal.processor_state Job).
@@ -584,7 +583,7 @@ Section Sequential_Abstract_RTA.
         { apply arrived_between_implies_in_arrivals; try done.
           apply/andP; split; rewrite /A subnKC //.
           by rewrite addn1 ltnSn //. }
-        have Fact4: j \in arrivals_at arr_seq (t1 + A).
+        have Fact4: j \in arr_seq (t1 + A).
         { by move: ARR => [t ARR]; rewrite subnKC //; feed (H_arrival_times_are_consistent j t); try (subst t). }
         have Fact1: 1 <= number_of_task_arrivals arr_seq tsk (t1 + A) (t1 + A + ε).
         { rewrite /number_of_task_arrivals /task_arrivals_between /arrival_sequence.arrivals_between.

analysis/abstract/ideal_jlfp_rta.v

@@ -25,8 +25,7 @@ Section JLFPInstantiation.
   (** Consider any arrival sequence with consistent arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq. 
-  
+
   (** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_jobs_come_from_arrival_sequence:
@@ -117,7 +116,7 @@ Section JLFPInstantiation.
       workload are generated by jobs with higher or equal priority
       released at time [t]. *)
   Definition interfering_workload_of_hep_jobs (j : Job) (t : instant) :=
-    \sum_(jhp <- arrivals_at arr_seq t | another_hep_job jhp j) job_cost jhp.
+    \sum_(jhp <- arr_seq t | another_hep_job jhp j) job_cost jhp.
 
   (** Instantiation of Interference *)
   (** We say that job [j] incurs interference at time [t] iff it

analysis/definitions/completion_sequence.v

 From mathcomp Require Export ssreflect seq ssrnat ssrbool eqtype.
-Require Import prosa.behavior.service.
+Require Import prosa.behavior.service prosa.analysis.facts.behavior.arrivals.
 
 (** This module contains basic definitions and properties of job
     completion sequences. *)
@@ -11,18 +11,28 @@ Section CompletionSequence.
 
   (** Consider any kind of jobs with a cost
      and any kind of processor state. *)
-  Context {Job : JobType} `{JobCost Job} {PState : Type}.
+  Context {Job : JobType} `{JobCost Job} `{JobArrival Job} {PState : Type}.
   Context `{ProcessorState Job PState}.
 
   (** Consider any job arrival sequence. *)
   Variable arr_seq: arrival_sequence Job.
 
+  Variable consistent_JobArrival : consistent_arrival_times arr_seq.
+
   (** Consider any schedule. *)
   Variable sched : schedule PState.
 
+  Definition completion_sequence_subdef :=
+    fun t => [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
+
+  Lemma completion_sequence_subproof t : uniq (completion_sequence_subdef t).
+  Proof. exact/filter_uniq/arrivals_uniq. Qed.
+
   (** For each instant [t], the completion sequence returns all
      arrived jobs that have completed at [t]. *)
-  Definition completion_sequence : arrival_sequence Job :=
-    fun t => [seq j <- arrivals_up_to arr_seq t | completes_at sched j t].
+  Definition completion_sequence : arrival_sequence Job := {|
+    arrival_sequence_seq := completion_sequence_subdef;
+    arrival_sequence_uniq := completion_sequence_subproof
+  |}.
 
 End CompletionSequence.

analysis/facts/behavior/arrivals.v

@@ -226,11 +226,7 @@ Section ArrivalSequencePrefix.
       forall t j,
         j \in arr_seq t ->
         arrives_in arr_seq j.
-    Proof.
-      move => t j J_ARR.
-      exists t.
-      now rewrite /arrivals_at.
-    Qed.
+    Proof. by move=> t j J_ARR; exists t. Qed.
 
     (** Next, we prove that if a job belongs to the prefix
          (jobs_arrived_between t1 t2), then it indeed arrives between t1 and
@@ -305,12 +301,11 @@ Section ArrivalSequencePrefix.
     (** Next, we prove that if the arrival sequence doesn't contain duplicate
         jobs, the same applies for any of its prefixes. *)
     Lemma arrivals_uniq:
-      arrival_sequence_uniq arr_seq ->
       forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
     Proof.
       rename H_consistent_arrival_times into CONS.
-      unfold arrivals_up_to; intros SET t1 t2.
-      apply bigcat_nat_uniq; first by done.
+      unfold arrivals_up_to; intros t1 t2.
+      apply bigcat_nat_uniq; first exact: arrival_sequence_uniq.
       intros x t t' IN1 IN2.
         by apply CONS in IN1; apply CONS in IN2; subst.
     Qed.

analysis/facts/busy_interval/busy_interval.v

@@ -243,10 +243,6 @@ Section ExistsBusyIntervalJLFP.
     (** Assume that the schedule is work-conserving ... *)
     Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
-    (** ... and there are no duplicate job arrivals. *)
-    Hypothesis H_arrival_sequence_is_a_set:
-      arrival_sequence_uniq arr_seq.
-
     (** Let [t1] be a quiet time. *)
     Variable t1 : instant.
     Hypothesis H_quiet_time : quiet_time t1.
@@ -341,10 +337,6 @@ Section ExistsBusyIntervalJLFP.
     (** Assume that the schedule is work-conserving, ... *)
     Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
-    (** ... and there are no duplicate job arrivals, ... *)
-    Hypothesis H_arrival_sequence_is_a_set:
-      arrival_sequence_uniq arr_seq.        
-
     (** ... and the priority relation is reflexive and transitive. *)
     Hypothesis H_priority_is_reflexive: reflexive_priorities.
     Hypothesis H_priority_is_transitive: transitive_priorities.

analysis/facts/busy_interval/carry_in.v

@@ -56,10 +56,6 @@ Section ExistsNoCarryIn.
   (** Assume that the schedule is work-conserving, ... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
-  (** ... and there are no duplicate job arrivals. *)
-  Hypothesis H_arrival_sequence_is_a_set:
-    arrival_sequence_uniq arr_seq.
-  
   (** The fact that there is no carry-in at time instant [t] trivially
       implies that [t] is a quiet time. *)
   Lemma no_carry_in_implies_quiet_time :

analysis/facts/hyperperiod.v

@@ -66,8 +66,7 @@ Section PeriodicLemmas.
   (** ... and a consistent arrival sequence with non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
-  
+
   (** Consider a task set [ts] such that all tasks in
       [ts] have valid periods. *)
   Variable ts : TaskSet Task.

analysis/facts/job_index.v

@@ -14,8 +14,7 @@ Section JobIndexLemmas.
   (** Consider any arrival sequence with consistent and non-duplicate arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq. 
-  Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq.
-  
+
   (** ... and any two jobs [j1] and [j2] from this arrival sequence
    that stem from the same task. *)
   Variable j1 j2 : Job.
@@ -245,8 +244,7 @@ Section PreviousJob.
   (** Consider any unique arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq. 
-  Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq.
-  
+
   (** ... and an arbitrary job with a positive [job_index]. *)
   Variable j : Job.
   Hypothesis H_arrives_in_arr_seq: arrives_in arr_seq j.
@@ -268,9 +266,9 @@ Section PreviousJob.
   Lemma prev_job_index:
     index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1.
   Proof.
-    apply index_uniq; last by apply uniq_task_arrivals.
+    apply: index_uniq; last exact: uniq_task_arrivals.
     apply leq_ltn_trans with (n := job_index arr_seq j); try by ssrlia.
-    now apply index_job_lt_size_task_arrivals_up_to_job.
+    exact: index_job_lt_size_task_arrivals_up_to_job.
   Qed.
 
   (** Observe that job [j] and [prev_job j] stem from the same task. *)
@@ -288,7 +286,7 @@ Section PreviousJob.
   Proof.
     rewrite /prev_job -index_mem index_uniq;
       try by apply job_index_minus_one_lt_size_task_arrivals_up_to.
-    now apply uniq_task_arrivals.
+    exact: uniq_task_arrivals.
   Qed.       
 
   (** We observe that for any job [j] the arrival time of [prev_job j] is 
@@ -364,7 +362,7 @@ Section PreviousJob.
     have JK_ARR : (arrives_in arr_seq jk) by apply in_arrseq_implies_arrives with (t := i) => //.
     have INDJK : (index jk (task_arrivals_up_to_job_arrival arr_seq j) = k).
     { apply index_uniq => //.
-      now apply uniq_task_arrivals => //. }
+      exact: uniq_task_arrivals. }
     repeat split => //.    
     { rewrite -> diff_jobs_iff_diff_indices => //; eauto.
       rewrite /job_index; rewrite [in X in _ <> X] (job_index_same_in_task_arrivals _ _ jk j) => //.

analysis/facts/model/offset.v

@@ -16,7 +16,6 @@ Section OffsetLemmas.
   (** Consider any arrival sequence with consistent and non-duplicate arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** ... and any job [j] (that stems from the arrival sequence) of any 
       task [tsk] with a valid offset. *)

analysis/facts/model/rbf.v

@@ -25,7 +25,6 @@ Section ProofWorkloadBound.
   (** Consider any arrival sequence with consistent, non-duplicate arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
-  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
   (** ... any schedule corresponding to this arrival sequence, ... *)
   Context {PState : Type} `{ProcessorState Job PState}.

analysis/facts/model/task_arrivals.v

@@ -71,7 +71,7 @@ Section TaskArrivals.
     split; first by apply /eqP => //. 
     move : ARR => [t ARR]; move : (ARR) => EQ.
     apply H_consistent_arrivals in EQ.
-    rewrite (mem_bigcat_nat _ (fun t => arrivals_at arr_seq t) j 0 _ (job_arrival j)) // EQ //.
+    rewrite (mem_bigcat_nat _ (fun t => arr_seq t) j 0 _ (job_arrival j)) // EQ //.
     now ssrlia.
   Qed.
 
@@ -85,7 +85,6 @@ Section TaskArrivals.
     intros j ARR.
     rewrite mem_filter; apply /andP.
     split; first by apply /eqP => //. 
-    rewrite /arrivals_at.
     move : ARR => [t ARR].
     now rewrite (H_consistent_arrivals j t ARR).
   Qed.
@@ -173,13 +172,8 @@ Section TaskArrivals.
       task arrivals also contain non-duplicate arrivals. *)
   Lemma uniq_task_arrivals:
     forall t,
-      arrival_sequence_uniq arr_seq ->
       uniq (task_arrivals_up_to arr_seq tsk t).
-  Proof.
-    intros * UNQ_SEQ.
-    apply filter_uniq.
-    now apply arrivals_uniq.
-  Qed.
+  Proof. move=> t; exact/filter_uniq/arrivals_uniq. Qed.
   
   (** A job cannot arrive before it's arrival time. *) 
   Lemma job_notin_task_arrivals_before:

analysis/facts/model/workload.v

@@ -69,7 +69,6 @@ Section WorkloadFacts.
 
     (** Assume that arrival times are consistent and that arrivals are unique. *)
     Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
-    Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
 
     (** Consider a time interval <<[t1, t2)>> and a time instant [t]. *)
     Variable t1 t2 t : instant.
@@ -88,7 +87,8 @@ Section WorkloadFacts.
     Proof.
       rewrite /workload_of_jobs big_seq_cond.
       rewrite -[in X in X <= _]big_filter -[in X in _ <= X]big_filter.
-      apply leq_sum_sub_uniq; first by apply filter_uniq, arrivals_uniq.
+      apply leq_sum_sub_uniq.
+      { apply/filter_uniq/arrivals_uniq => //; exact: arrival_sequence_uniq. }
       move => j'; rewrite mem_filter => [/andP [/andP [A /andP [C D]] _]].
       rewrite mem_filter; apply/andP; split; first by done.
       apply job_in_arrivals_between; eauto.

analysis/facts/periodic/arrival_separation.v

@@ -18,7 +18,6 @@ Section JobArrivalSeparation.
   (** Consider any unique arrival sequence with consistent arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
 
   (** ... and any task [tsk] that is to be analyzed. *)
   Variable tsk : Task.
@@ -95,7 +94,7 @@ Section JobArrivalSeparation.
       }
       { intros j1 j2 TSKj1 TSKj2 STEP LT ARRj2 ARRj1.
         specialize (exists_jobs_before_j
-                      arr_seq H_consistent_arrivals H_uniq_arrseq j2 ARRj2 (job_index arr_seq j2 - s)) => BEFORE.
+                      arr_seq H_consistent_arrivals j2 ARRj2 (job_index arr_seq j2 - s)) => BEFORE.
         destruct s.
         - exists 1; repeat split.
           now rewrite (consecutive_job_separation j1) //; ssrlia.

analysis/facts/periodic/arrival_times.v

@@ -19,7 +19,6 @@ Section PeriodicArrivalTimes.
   (** Consider any unique arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** ... and any periodic task [tsk] with a valid offset and period. *)
     Variable tsk : Task.

analysis/facts/periodic/sporadic.v

@@ -22,8 +22,7 @@ Section PeriodicTasksAsSporadicTasks.
 
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
-  
+
   (** ... may be interpreted as a type of sporadic tasks by using each task's
       period as its minimum inter-arrival time ... *)
   Global Instance periodic_as_sporadic : SporadicModel Task :=

analysis/facts/periodic/task_arrivals_size.v

@@ -18,7 +18,6 @@ Section TaskArrivalsSize.
   (** Consider any unique arrival sequence with consistent arrivals ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** ... and any periodic task [tsk] with a valid offset and period. *)
   Variable tsk : Task.
@@ -43,7 +42,7 @@ Section TaskArrivalsSize.
     destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] => //.
     rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN => /andP [/eqP TSK A_ARR].
     move : (A_ARR) => A_IN; apply H_consistent_arrivals in A_IN.
-    rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.
+    rewrite -A_IN in T.
     apply in_arrseq_implies_arrives in A_ARR.
     have EXISTS_N : exists n, job_arrival a = task_offset tsk + n * task_period tsk by
           apply job_arrival_times with (arr_seq0 := arr_seq) => //.
@@ -62,10 +61,12 @@ Section TaskArrivalsSize.
     case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) => [LT|GT|EQ]; try by auto.
     destruct (size (task_arrivals_at arr_seq tsk t)); now left.
     specialize (exists_two (task_arrivals_at arr_seq tsk t)) => EXISTS_TWO.
-    destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].
+    have uniq_task : uniq (task_arrivals_at arr_seq tsk t).
+    { exact/filter_uniq/arrival_sequence_uniq. }
+    have [a [b [NEQ [A_IN B_IN]]]] := EXISTS_TWO GT uniq_task.
     rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
     move: A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
-    move: (ARRA); move: (ARRB); rewrite /arrivals_at => A_IN B_IN.
+    move: (ARRA) (ARRB) => 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 EQ_ARR_A : (job_arrival a = t) by apply H_consistent_arrivals.

analysis/facts/shifted_job_costs.v

@@ -23,7 +23,6 @@ Section ValidJobCostsShifted.
   (** Consider a consistent arrival sequence with non-duplicate arrivals. *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** Furthermore, assume that arrivals have valid job costs. *) 
   Hypothesis H_arrivals_have_valid_job_costs: arrivals_have_valid_job_costs arr_seq.

analysis/facts/sporadic.v

@@ -21,8 +21,7 @@ Section SporadicModelIndexLemmas.
   (** Consider any unique arrival sequence with consistent arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
-  
+
   (** ... and any sporadic task [tsk] that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
@@ -73,8 +72,7 @@ Section DifferentJobsImplyDifferentArrivalTimes.
   (** Consider any unique arrival sequence with consistent arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arrseq: arrival_sequence_uniq arr_seq.
-  
+
   (** ... and any sporadic task [tsk] that is to be analyzed. *)
   Variable tsk : Task.
   Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
@@ -135,7 +133,6 @@ Section SporadicArrivals.
   (** Consider any unique arrival sequence with consistent arrivals, ... *)
   Variable arr_seq : arrival_sequence Job.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
-  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
   (** ... and any sporadic task [tsk] to be analyzed. *)
   Variable tsk : Task.
@@ -165,10 +162,12 @@ Section SporadicArrivals.
   Proof.
     move => [j [SIZE_G [PERIODIC VALID_TMIA]]].
     specialize (exists_two (task_arrivals_at_job_arrival arr_seq j)) => EXISTS_TWO.
-    destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].
+    have uniq_tasks : uniq (task_arrivals_at_job_arrival arr_seq j).
+    { exact/filter_uniq/arrival_sequence_uniq. }
+    have [a [b [NEQ [A_IN B_IN]]]] := EXISTS_TWO SIZE_G uniq_tasks.
     rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
     move: A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
-    move: (ARRA); move: (ARRB); rewrite /arrivals_at => A_IN B_IN.
+    move: (ARRA) (ARRB) => A_IN B_IN.
     apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
     have EQ_ARR_A : (job_arrival a = job_arrival j) by apply H_consistent_arrivals.
     have EQ_ARR_B : (job_arrival b = job_arrival j) by apply H_consistent_arrivals.

analysis/facts/transform/wc_correctness.v

@@ -208,9 +208,7 @@ Section AuxiliaryLemmasWorkConservingTransformation.
       move=> j t' ARR_IN ARR.
       rewrite /max_deadline_for_jobs_arrived_before.
       apply in_max0_le; apply map_f.
-      rewrite /arrivals_up_to.
-      apply arrived_between_implies_in_arrivals;
-        by move:H_arr_seq_valid => [CONS UNIQ].
+      exact: arrived_between_implies_in_arrivals.
     Qed.
 
     (** Next, we want to show that, if a job arriving from the arrival