clean up util/list.v

also, removed one assumption in [eq_ind_in_seq]

analysis/facts/job_index.v

@@ -51,7 +51,6 @@ Section JobIndexLemmas.
       apply eq_ind_in_seq with (xs := task_arrivals_up_to_job_arrival arr_seq j2) => //.
       - now rewrite -/(job_index _ _) -IND -ARR_CAT index_cat ifT;
           try apply arrives_in_task_arrivals_up_to.
-      - now apply uniq_task_arrivals.
       - rewrite -ARR_CAT mem_cat; apply /orP.
         now left; apply arrives_in_task_arrivals_up_to.
       - now apply arrives_in_task_arrivals_up_to.
@@ -69,7 +68,6 @@ Section JobIndexLemmas.
       apply (eq_ind_in_seq _ _ _ (task_arrivals_up_to_job_arrival arr_seq j1)) => //.
       - now rewrite -/(job_index _ _) IND -ARR_CAT index_cat ifT;
           try apply arrives_in_task_arrivals_up_to.
-      - now apply uniq_task_arrivals.
       - now apply arrives_in_task_arrivals_up_to.
       - rewrite -ARR_CAT mem_cat; apply /orP.
         now left; apply arrives_in_task_arrivals_up_to => //.
@@ -368,7 +366,7 @@ Section PreviousJob.
     { apply index_uniq => //.
       now apply uniq_task_arrivals => //. }
     repeat split => //.    
-    { rewrite -> diff_jobs_iff_diff_indices => //; last by auto.
+    { rewrite -> diff_jobs_iff_diff_indices => //; eauto.
       rewrite /job_index; rewrite [in X in _ <> X] (job_index_same_in_task_arrivals _ _ jk j) => //.
       - rewrite index_uniq -/(job_index arr_seq j)=> //; last by apply uniq_task_arrivals.
         now ssrlia.

analysis/facts/periodic/arrival_separation.v

@@ -102,8 +102,8 @@ Section JobArrivalSeparation.
         - feed BEFORE; first by ssrlia.
           move : BEFORE => [nj [NEQNJ [TSKNJ [ARRNJ INDNJ]]]]; rewrite TSKj2 in TSKNJ.
           specialize (IHs nj j2); feed_n 6 IHs => //; first by ssrlia.          
-          { now apply (lower_index_implies_earlier_arrival _ H_consistent_arrivals H_uniq_arrseq tsk);
-              auto with basic_facts; ssrlia.
+          { by apply (lower_index_implies_earlier_arrival _ H_consistent_arrivals tsk);
+              eauto with basic_facts; ssrlia.
           }
           move : IHs => [n [NZN ARRJ'NJ]].          
           move: (H_periodic_model nj) => PERIODIC; feed_n 3 PERIODIC => //; first by ssrlia. 

analysis/facts/periodic/sporadic.v

@@ -46,7 +46,7 @@ Section PeriodicTasksAsSporadicTasks.
     intros tsk VALID_PERIOD H_PERIODIC j1 j2 NEQ ARR ARR' TSK TSK' ARR_LT.
     rewrite /task_min_inter_arrival_time /periodic_as_sporadic.
     have IND_LT : job_index arr_seq j1 < job_index arr_seq j2.
-    { rewrite -> diff_jobs_iff_diff_indices in NEQ => //; auto; last by rewrite TSK.
+    { rewrite -> diff_jobs_iff_diff_indices in NEQ => //; eauto; last by rewrite TSK.
       move_neq_up IND_LTE; move_neq_down ARR_LT.
       specialize (H_PERIODIC j1); feed_n 3 H_PERIODIC => //; try by ssrlia.
       move : H_PERIODIC => [pj [ARR_PJ [IND_PJ [TSK_PJ PJ_ARR]]]].

analysis/facts/sporadic.v

@@ -45,10 +45,10 @@ Section SporadicModelIndexLemmas.
   Proof.
     intro IND.
     move: (H_sporadic_model j1 j2) => SPORADIC; feed_n 6 SPORADIC => //. 
-    - rewrite -> diff_jobs_iff_diff_indices => //; auto.
+    - rewrite -> diff_jobs_iff_diff_indices => //; eauto.
        + now ssrlia.
        + now rewrite H_j1_task. 
-    - apply (index_lte_implies_arrival_lte arr_seq); try auto.
+    - apply (index_lte_implies_arrival_lte arr_seq); try eauto.
       now rewrite H_j1_task.
     - have POS_IA : task_min_inter_arrival_time tsk > 0 by auto.
       now ssrlia.
@@ -95,7 +95,7 @@ Section DifferentJobsImplyDifferentArrivalTimes.
       job_arrival j1 <> job_arrival j2.
   Proof.
     intros UNEQ EQ_ARR.
-    rewrite -> diff_jobs_iff_diff_indices in UNEQ => //; auto; last by rewrite H_j1_task.
+    rewrite -> diff_jobs_iff_diff_indices in UNEQ => //; eauto; last by rewrite H_j1_task.
     move /neqP: UNEQ; rewrite neq_ltn => /orP [LT|LT].
     all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia.
   Qed.
@@ -110,7 +110,7 @@ Section DifferentJobsImplyDifferentArrivalTimes.
     split; first by apply congr1.
     intro EQ_ARR.
     case: (boolP (j1 == j2)) => [/eqP EQ | /eqP NEQ]; first by auto.
-    rewrite -> diff_jobs_iff_diff_indices in NEQ => //; auto; last by rewrite H_j1_task.
+    rewrite -> diff_jobs_iff_diff_indices in NEQ => //; eauto; last by rewrite H_j1_task.
     move /neqP: NEQ; rewrite neq_ltn => /orP [LT|LT].
     all: now apply lower_index_implies_earlier_arrival with (tsk0 := tsk) in LT => //; ssrlia.
   Qed.