simplify `conversion_preserves_equivalence` proof

...and many other proofs:

- Simplify proof of conversion_preserves_equivalence
- Simplify proofs in analysis/facts/behavior/service.v
- Simplify proofs in analysis/facts/behavior/deadlines.v
- Simplify proofs in analysis/facts/behavior/arrivals.v
- Fix order of arguments in identical_prefix_inclusion
- Simplify proofs in analysis/facts/behavior/completion.v

analysis/definitions/schedule_prefix.v

@@ -20,7 +20,7 @@ Section PrefixDefinition.
 
   (** In other words, two schedules with a shared prefix are completely
       interchangeable w.r.t. whether a job is scheduled (in the prefix). *)
-  Fact identical_prefix_scheduled_at:
+  Fact identical_prefix_scheduled_at :
     forall sched sched' h,
       identical_prefix sched sched' h ->
       forall j t,
@@ -33,16 +33,10 @@ Section PrefixDefinition.
 
   (** Trivially, any prefix of an identical prefix is also an identical
       prefix. *)
-  Fact identical_prefix_inclusion:
-    forall sched sched' h,
-      identical_prefix sched sched' h ->
-      forall h',
-        h' <= h ->
-        identical_prefix sched sched' h'.
-  Proof.
-    move=> sched sched' h IDENT h' INCL t LT_h'.
-    apply IDENT.
-    now apply (leq_trans LT_h').
-  Qed.
+  Fact identical_prefix_inclusion :
+    forall sched sched' h h',
+      h' <= h ->
+      identical_prefix sched sched' h -> identical_prefix sched sched' h'.
+  Proof. by move=> sched sched' h h' h'_le_h + t t_lt_h'; apply; apply: leq_trans h'_le_h. Qed.
 
 End PrefixDefinition.

analysis/facts/behavior/arrivals.v

@@ -16,10 +16,7 @@ Section ArrivalPredicates.
     forall j t1 t2,
       arrived_between j t1 t2 ->
       arrived_before j t2.
-  Proof.
-    move=> j t1 t2.
-    now rewrite /arrived_before /arrived_between => /andP [_ CLAIM].
-  Qed.
+  Proof. by move=> ? ? ? /andP[]. Qed.
 
   (** A job that arrives before a time [t] certainly has arrived by time
       [t]. *)
@@ -27,17 +24,13 @@ Section ArrivalPredicates.
     forall j t,
       arrived_before j t ->
       has_arrived j t.
-  Proof.
-    move=> j t.
-    rewrite /arrived_before /has_arrived.
-    now apply ltnW.
-  Qed.
+  Proof. move=> ? ?; exact: ltnW. Qed.
 
 End ArrivalPredicates.
 
 (** In this section, we relate job readiness to [has_arrived]. *)
 Section Arrived.
-  
+
   (** Consider any kinds of jobs and any kind of processor state. *)
   Context {Job : JobType} {PState : ProcessorState Job}.
 
@@ -55,65 +48,36 @@ Section Arrived.
   Lemma any_ready_job_is_pending:
     forall j t,
       job_ready sched j t -> pending sched j t.
-  Proof.
-    move: jr => [is_ready CONSISTENT].
-    move=> j t READY.
-    apply CONSISTENT.
-    by exact READY.
-  Qed.
+  Proof. move: jr => [? +] /= ?; exact. Qed.
 
   (** Next, we observe that a given job must have arrived to be ready... *)
-  Lemma ready_implies_arrived:
+  Lemma ready_implies_arrived :
     forall j t, job_ready sched j t -> has_arrived j t.
-  Proof.
-    move=> j t READY.
-    move: (any_ready_job_is_pending j t READY).
-    by rewrite /pending => /andP [ARR _].
-  Qed.
+  Proof. by move=> ? ? /any_ready_job_is_pending => /andP[]. Qed.
 
   (** ...and lift this observation also to the level of whole schedules. *)
   Lemma jobs_must_arrive_to_be_ready:
-    jobs_must_be_ready_to_execute sched ->
-    jobs_must_arrive_to_execute sched.
-  Proof.
-    rewrite /jobs_must_be_ready_to_execute /jobs_must_arrive_to_execute.
-    move=> READY_IF_SCHED j t SCHED.
-    move: (READY_IF_SCHED j t SCHED) => READY.
-    by apply ready_implies_arrived.
-  Qed.
+    jobs_must_be_ready_to_execute sched -> jobs_must_arrive_to_execute sched.
+  Proof. move=> READY ? ? ?; exact/ready_implies_arrived/READY. Qed.
 
   (** Furthermore, in a valid schedule, jobs must arrive to execute. *)
-  Corollary valid_schedule_implies_jobs_must_arrive_to_execute:
-    forall arr_seq, 
-    valid_schedule sched arr_seq ->
-    jobs_must_arrive_to_execute sched.
-  Proof.
-    move=> arr_seq [??].
-    by apply jobs_must_arrive_to_be_ready.
-  Qed.
-  
+  Corollary valid_schedule_implies_jobs_must_arrive_to_execute :
+    forall arr_seq,
+      valid_schedule sched arr_seq -> jobs_must_arrive_to_execute sched.
+  Proof. move=> ? [? ?]; exact: jobs_must_arrive_to_be_ready. Qed.
+
   (** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
   Corollary backlogged_implies_arrived:
     forall j t,
       backlogged sched j t -> has_arrived j t.
-  Proof.
-    rewrite /backlogged.
-    move=> j t /andP [READY _].
-    now apply ready_implies_arrived.
-  Qed.
+  Proof. move=> ? ? /andP[? ?]; exact: ready_implies_arrived. Qed.
 
   (** Similarly, since backlogged jobs are by definition pending, any
       backlogged job must be incomplete. *)
   Lemma backlogged_implies_incomplete:
     forall j t,
       backlogged sched j t -> ~~ completed_by sched j t.
-  Proof.
-    move=> j t BACK.
-    have suff: pending sched j t.
-    - by move /andP => [_ INCOMP].
-    - apply; move: BACK => /andP [READY _].
-      by apply any_ready_job_is_pending.
-  Qed.
+  Proof. by move=> ? ? /andP[/any_ready_job_is_pending /andP[]]. Qed.
 
 End Arrived.
 
@@ -147,12 +111,9 @@ Section ArrivalSequencePrefix.
         t <= t2 ->
         arrivals_between arr_seq t1 t2 =
         arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
-    Proof.
-      unfold arrivals_between; intros t1 t t2 GE LE.
-        by rewrite (@big_cat_nat _ _ _ t).
-    Qed.
+    Proof. by move=> ? ? ? ? ?; rewrite -big_cat_nat. Qed.
 
-    (** We also prove a stronger version of the above lemma 
+    (** We also prove a stronger version of the above lemma
      in the case of arrivals that satisfy a predicate [P]. *)
     Lemma arrivals_P_cat:
       forall P t t1 t2,
@@ -160,11 +121,10 @@ Section ArrivalSequencePrefix.
         arrivals_between_P arr_seq P t1 t2 =
         arrivals_between_P arr_seq P t1 t ++ arrivals_between_P arr_seq P t t2.
     Proof.
-      intros P t t1 t2 INEQ.
-      rewrite -filter_cat.
-      now rewrite -arrivals_between_cat => //; lia.
+      move=> P t t1 t2.
+      by move=> /andP[? ?]; rewrite -filter_cat -arrivals_between_cat// ltnW.
     Qed.
-    
+
     (** The same observation applies to membership in the set of
          arrived jobs. *)
     Lemma arrivals_between_mem_cat:
@@ -173,63 +133,77 @@ Section ArrivalSequencePrefix.
         t <= t2 ->
         j \in arrivals_between arr_seq t1 t2 =
         (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
-    Proof.
-        by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
-    Qed.
+    Proof. by move=> ? ? ? ? ? ?; rewrite -arrivals_between_cat. Qed.
 
     (** We observe that we can grow the considered interval without
          "losing" any arrived jobs, i.e., membership in the set of arrived jobs
          is monotonic. *)
-    Lemma arrivals_between_sub:
+    Lemma arrivals_between_sub :
       forall j t1 t1' t2 t2',
         t1' <= t1 ->
         t2 <= t2' ->
         j \in arrivals_between arr_seq t1 t2 ->
         j \in arrivals_between arr_seq t1' t2'.
     Proof.
-      intros j t1 t1' t2 t2' GE1 LE2 IN.
-      move: (leq_total t1 t2) => /orP [BEFORE | AFTER];
-                                  last by rewrite /arrivals_between big_geq // in IN.
-      rewrite /arrivals_between.
-      rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].
-      rewrite mem_cat; apply/orP; right.
-      rewrite -> big_cat_nat with (n := t2); [simpl | by done | by done].
-        by rewrite mem_cat; apply/orP; left.
+      move=> j t1 t1' t2 t2' t1'_le_t1 t2_le_t2' j_in.
+      have /orP[t2_le_t1|t1_le_t2] := leq_total t2 t1.
+      { by move: j_in; rewrite /arrivals_between big_geq. }
+      rewrite (arrivals_between_mem_cat _ _ t1)// ?mem_cat.
+      2:{ exact: leq_trans t2_le_t2'. }
+      rewrite [X in _ || X](arrivals_between_mem_cat _ _ t2)// mem_cat.
+      by rewrite j_in orbT.
     Qed.
 
   End Composition.
-  
+
   (** Next, we relate the arrival prefixes with job arrival times. *)
   Section ArrivalTimes.
 
     (** Assume that job arrival times are consistent. *)
-    Hypothesis H_consistent_arrival_times:
-      consistent_arrival_times arr_seq.
-
-    (** First, we prove that if a job belongs to the prefix
-         (jobs_arrived_before t), then it arrives in the arrival sequence. *)
+    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. *)
+    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)>>. *)
+    Lemma job_arrival_between :
+      forall {j t1 t2},
+        j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j < t2.
+    Proof. by move=> ? ? ? /mem_bigcat_nat_exists[i [/job_arrival_at <-]]. Qed.
+
+    (** For convenience, we restate the left bound of the above lemma... *)
+    Corollary job_arrival_between_ge :
+      forall {j t1 t2},
+        j \in arrivals_between arr_seq t1 t2 -> t1 <= job_arrival j.
+    Proof. by move=> ? ? ? /job_arrival_between/andP[]. Qed.
+
+    (** ... as well as the right bound separately as corollaries. *)
+    Corollary job_arrival_between_lt :
+      forall {j t1 t2},
+        j \in arrivals_between arr_seq t1 t2 -> job_arrival j < t2.
+    Proof. by move=> ? ? ? /job_arrival_between/andP[]. Qed.
+
+    (** Second, we prove that if a job belongs to the prefix
+        (jobs_arrived_before t), then it arrives in the arrival
+        sequence. *)
     Lemma in_arrivals_implies_arrived:
       forall j t1 t2,
         j \in arrivals_between arr_seq t1 t2 ->
         arrives_in arr_seq j.
-    Proof.
-      rename H_consistent_arrival_times into CONS.
-      intros j t1 t2 IN.
-      apply mem_bigcat_nat_exists in IN.
-      move: IN => [arr [IN _]].
-        by exists arr.
-    Qed.
-    
+    Proof. by move=> ? ? ? /mem_bigcat_nat_exists[arr [? _]]; exists arr. Qed.
+
     (** We also prove a weaker version of the above lemma. *)
     Lemma in_arrseq_implies_arrives:
       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 ? ?; 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
@@ -238,13 +212,7 @@ Section ArrivalSequencePrefix.
       forall j t1 t2,
         j \in arrivals_between arr_seq t1 t2 ->
         arrived_between j t1 t2.
-    Proof.
-      rename H_consistent_arrival_times into CONS.
-      intros j t1 t2 IN.
-      apply mem_bigcat_nat_exists in IN.
-      move: IN => [t0 [IN /= LT]].
-        by apply CONS in IN; rewrite /arrived_between IN.
-    Qed.
+    Proof. by move=> ? ? ? /mem_bigcat_nat_exists[t0 [/job_arrival_at <-]]. Qed.
 
     (** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
            then it indeed arrives before time t. *)
@@ -252,11 +220,7 @@ Section ArrivalSequencePrefix.
       forall j t,
         j \in arrivals_before arr_seq t ->
         arrived_before j t.
-    Proof.
-      intros j t IN.
-      have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
-        by rewrite /arrived_between /=.
-    Qed.
+    Proof. by move=> ? ? /in_arrivals_implies_arrived_between. Qed.
 
     (** Similarly, we prove that if a job from the arrival sequence arrives
         before t, then it belongs to the sequence (jobs_arrived_before t). *)
@@ -266,27 +230,22 @@ Section ArrivalSequencePrefix.
         arrived_between j t1 t2 ->
         j \in arrivals_between arr_seq t1 t2.
     Proof.
-      rename H_consistent_arrival_times into CONS.
-      move => j t1 t2 [a_j ARRj] BEFORE.
-      have SAME := ARRj; apply CONS in SAME; subst a_j.
-      now apply mem_bigcat_nat with (j := (job_arrival j)).
+      move=> j t1 t2 [a_j arrj] before; apply: mem_bigcat_nat (arrj).
+      by rewrite -(job_arrival_at arrj).
     Qed.
-    
+
     (** Any job in arrivals between time instants [t1] and [t2] must arrive
        in the interval <<[t1,t2)>>. *)
-    Lemma job_arrival_between:
+    Lemma job_arrival_between_P:
       forall j P t1 t2,
         j \in arrivals_between_P arr_seq P t1 t2 ->
         t1 <= job_arrival j < t2.
     Proof.
-      intros * ARR.
-      move: ARR; rewrite mem_filter => /andP [PJ JARR].
-      apply mem_bigcat_nat_exists in JARR.
-      move : JARR => [i [ARR INEQ]].
-      apply H_consistent_arrival_times in ARR.
-      now rewrite ARR.
+      move=> j P t1 t2.
+      rewrite mem_filter => /andP[Pj /mem_bigcat_nat_exists[i [+ iitv]]].
+      by move=> /job_arrival_at ->.
     Qed.
-    
+
     (** Any job [j] is in the sequence [arrivals_between t1 t2] given
      that [j] arrives in the interval <<[t1,t2)>>. *)
     Lemma job_in_arrivals_between:
@@ -295,23 +254,18 @@ Section ArrivalSequencePrefix.
         t1 <= job_arrival j < t2 ->
         j \in arrivals_between arr_seq t1 t2.
     Proof.
-      intros * ARR INEQ.
-      apply mem_bigcat_nat with (j := job_arrival j) => //.
-      move : ARR => [t J_IN].
-      now rewrite -> H_consistent_arrival_times with (t := t).
+      move=> j t1 t2 [t jarr] jitv; apply: mem_bigcat_nat (jarr).
+      by rewrite -(job_arrival_at jarr).
     Qed.
-    
+
     (** 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.
-      intros x t t' IN1 IN2.
-        by apply CONS in IN1; apply CONS in IN2; subst.
+      move=> SET t1 t2; apply: bigcat_nat_uniq => // j t1' t2'.
+      by move=> /job_arrival_at <- /job_arrival_at <-.
     Qed.
 
     (** Also note that there can't by any arrivals in an empty time interval. *)
@@ -319,27 +273,23 @@ Section ArrivalSequencePrefix.
       forall t1 t2,
         t1 >= t2 ->
         arrivals_between arr_seq t1 t2  = [::].
-    Proof.
-        by intros ? ? GE; rewrite /arrivals_between big_geq.
-    Qed.
-    
+    Proof. by move=> ? ? ?; rewrite /arrivals_between big_geq. Qed.
+
     (** Given jobs [j1] and [j2] in [arrivals_between_P arr_seq P t1 t2], the fact that
         [j2] arrives strictly before [j1] implies that [j2] also belongs in the sequence
         [arrivals_between_P arr_seq P t1 (job_arrival j1)]. *)
-    Lemma arrival_lt_implies_job_in_arrivals_between_P:
+    Lemma arrival_lt_implies_job_in_arrivals_between_P :
       forall (j1 j2 : Job) (P : Job -> bool) (t1 t2 : instant),
-        (j1 \in arrivals_between_P arr_seq P t1 t2) -> 
-        (j2 \in arrivals_between_P arr_seq P t1 t2) ->
+        j1 \in arrivals_between_P arr_seq P t1 t2 ->
+        j2 \in arrivals_between_P arr_seq P t1 t2 ->
         job_arrival j2 < job_arrival j1 ->
         j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1).
     Proof.
-      intros * J1_IN J2_IN ARR_LT.
-      rewrite mem_filter in J2_IN; move : J2_IN => /andP [PJ2 J2ARR] => //.
-      rewrite mem_filter; apply /andP; split => //.
-      apply mem_bigcat_nat_exists in J2ARR; move : J2ARR => [i [J2_IN INEQ]].
-      apply mem_bigcat_nat with (j := i) => //.
-      apply H_consistent_arrival_times in J2_IN; rewrite J2_IN in ARR_LT.
-      now lia.
+      move=> j1 j2 P t1 t2.
+      rewrite !mem_filter => /andP[_ j1arr] /andP[Pj2 j2arr] arr_lt.
+      rewrite Pj2/=; apply: job_in_arrivals_between.
+      - exact: in_arrivals_implies_arrived j2arr.
+      - by rewrite (job_arrival_between_ge j2arr).
     Qed.
 
   End ArrivalTimes.

analysis/facts/behavior/completion.v

@@ -28,11 +28,7 @@ Section CompletionFacts.
       t <= t' ->
       completed_by sched j t ->
       completed_by sched j t'.
-  Proof.
-    move => t t' LE. rewrite /completed_by /service => COMP.
-    apply leq_trans with (n := service_during sched j 0 t); auto.
-      by apply service_monotonic.
-  Qed.
+  Proof. move=> ? ? ? /leq_trans; apply; exact: service_monotonic. Qed.
 
   (** We prove that if [j] is not completed by [t'], then it's also not
       completed by any earlier instant. *)
@@ -41,11 +37,7 @@ Section CompletionFacts.
       t <= t' ->
       ~~ completed_by sched j t' ->
       ~~ completed_by sched j t.
-  Proof.
-    move => t t' LE.
-    apply contra.
-    by apply completion_monotonic.
-  Qed.
+  Proof. move=> ? ? ?; exact/contra/completion_monotonic. Qed.
 
   (** We observe that being incomplete is the same as not having received
      sufficient service yet... *)
@@ -53,9 +45,7 @@ Section CompletionFacts.
     forall t,
       service sched j t < job_cost j
       <-> ~~ completed_by sched j t.
-  Proof.
-    move=> t. by split; rewrite /completed_by; [rewrite -ltnNge // | rewrite ltnNge //].
-  Qed.
+  Proof. by move=> ?; rewrite -ltnNge. Qed.
 
   (** ...which is also the same as having positive remaining cost. *)
   Lemma incomplete_is_positive_remaining_cost:
@@ -63,7 +53,7 @@ Section CompletionFacts.
       ~~ completed_by sched j t
       <-> remaining_cost sched j t > 0.
   Proof.
-    move=> t. by split; rewrite /remaining_cost -less_service_than_cost_is_incomplete subn_gt0 //.
+    by move=> ?; rewrite -less_service_than_cost_is_incomplete subn_gt0.
   Qed.
 
   (** Trivially, it follows that an incomplete job has a positive cost. *)
@@ -72,11 +62,8 @@ Section CompletionFacts.
       ~~ completed_by sched j t ->
       job_cost_positive j.
   Proof.
-    move=> t INCOMP.
-    apply: (leq_trans _);
-      last by apply leq_subr.
-    apply incomplete_is_positive_remaining_cost.
-    exact INCOMP.
+    move=> t INCOMP; apply: leq_trans (leq_subr (service sched j t) _).
+    by rewrite -incomplete_is_positive_remaining_cost.
   Qed.
 
 
@@ -86,13 +73,20 @@ Section CompletionFacts.
   Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
   Hypothesis H_completed_jobs : completed_jobs_dont_execute sched.
 
+  (** To simplify subsequent proofs, we restate the assumption
+      [H_completed_jobs] as a trivial corollary. *)
+  Corollary service_lt_cost :
+    forall t,
+      scheduled_at sched j t -> service sched j t < job_cost j.
+  Proof. exact: H_completed_jobs. Qed.
+
   (** We observe that a job that is completed at the instant of its
       arrival has a cost of zero. *)
   Lemma completed_on_arrival_implies_zero_cost :
     completed_by sched j (job_arrival j) ->
     job_cost j = 0.
   Proof.
-    by rewrite /completed_by no_service_before_arrival // leqn0 => /eqP.
+    by rewrite /completed_by no_service_before_arrival// leqn0 => /eqP.
   Qed.
 
   (** Further, we note that if a job receives service at some time t, then its
@@ -103,9 +97,9 @@ Section CompletionFacts.
       remaining_cost sched j t > 0.
   Proof.
     move=> t SERVICE.
-    rewrite -incomplete_is_positive_remaining_cost -less_service_than_cost_is_incomplete.
-    apply H_completed_jobs.
-    by apply service_at_implies_scheduled_at.
+    rewrite -incomplete_is_positive_remaining_cost.
+    rewrite -less_service_than_cost_is_incomplete.
+    exact/service_lt_cost/service_at_implies_scheduled_at.
   Qed.
 
   (** Consequently, if we have a have processor model where scheduled jobs
@@ -115,47 +109,44 @@ Section CompletionFacts.
   (** Assume a scheduled job always receives some positive service. *)
   Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
 
+  (** To simplify subsequent proofs, we restate the assumption
+      [H_scheduled_implies_serviced] as a trivial corollary. *)
+  Corollary scheduled_implies_serviced :
+    forall s,
+      scheduled_in j s -> 0 < service_in j s.
+  Proof. exact: H_scheduled_implies_serviced. Qed.
+
   (** Then a scheduled job has positive remaining cost. *)
   Corollary scheduled_implies_positive_remaining_cost:
     forall t,
       scheduled_at sched j t ->
       remaining_cost sched j t > 0.
   Proof.
-    rewrite /scheduled_at => t SCHEDULED.
-      by apply: serviced_implies_positive_remaining_cost; rewrite /service_at; apply: H_scheduled_implies_serviced.
+    move=> t sch.
+    exact/serviced_implies_positive_remaining_cost/scheduled_implies_serviced.
   Qed.
 
-  (** We also prove that a completed job cannot be scheduled... *)
-  Lemma completed_implies_not_scheduled:
+  (** We also prove that a scheduled job cannot be completed... *)
+  Lemma scheduled_implies_not_completed :
     forall t,
-      completed_by sched j t ->
-      ~~ scheduled_at sched j t.
+      scheduled_at sched j t -> ~~ completed_by sched j t.
   Proof.
-    move=> t COMP.
-    apply contra with (b := ~~ completed_by sched j t);
-      last by apply /negPn.
-    move=> SCHED. move: (H_completed_jobs j t SCHED).
-    by rewrite less_service_than_cost_is_incomplete.
+    move=> t sch.
+    by rewrite -less_service_than_cost_is_incomplete service_lt_cost.
   Qed.
 
-  (** ... and that a scheduled job cannot be completed. *)
-  Lemma scheduled_implies_not_completed:
+  (** ... and that a completed job cannot be scheduled. *)
+  Lemma completed_implies_not_scheduled :
     forall t,
-      scheduled_at sched j t ->
-      ~~ completed_by sched j t.
-  Proof.
-    move=> t SCHED.
-    have REMPOS := scheduled_implies_positive_remaining_cost t SCHED.
-    rewrite /remaining_cost subn_gt0 in REMPOS.
-      by rewrite -less_service_than_cost_is_incomplete.
-  Qed.
+      completed_by sched j t -> ~~ scheduled_at sched j t.
+  Proof. move=> ? /negPn; exact/contra/scheduled_implies_not_completed. Qed.
 
 End CompletionFacts.
 
 (** In this section, we establish some facts that are really about service,
     but are also related to completion and rely on some of the above lemmas.
     Hence they are in this file rather than in the service facts file. *)
-Section ServiceAndCompletionFacts.  
+Section ServiceAndCompletionFacts.
 
   (** Consider any job type,...*)
   Context {Job: JobType}.
@@ -177,6 +168,13 @@ Section ServiceAndCompletionFacts.
   (** Assume that a scheduled job receives exactly one time unit of service. *)
   Hypothesis H_unit_service: unit_service_proc_model PState.
 
+  (** To simplify subsequent proofs, we restate the assumption
+      [H_unit_service] as a trivial corollary. *)
+  Lemma unit_service :
+    forall s,
+      service_in j s <= 1.
+  Proof. exact: H_unit_service. Qed.
+
   (** To begin with, we establish that the cumulative service never exceeds a
      job's total cost if service increases only by one at each step since
      completed jobs don't execute. *)
@@ -184,18 +182,15 @@ Section ServiceAndCompletionFacts.
     forall t,
       service sched j t <= job_cost j.
   Proof.
-    move=> t.
-    elim: t => [|t]; first by rewrite service0.
+    elim=> [|t]; first by rewrite service0.
     rewrite -service_last_plus_before.
-    rewrite leq_eqVlt => /orP [/eqP EQ|LT].
-    - rewrite not_scheduled_implies_no_service;
-        first by rewrite addn0 EQ.
-      apply completed_implies_not_scheduled => //.
+    rewrite leq_eqVlt => /orP[/eqP EQ|LT].
+    - rewrite not_scheduled_implies_no_service ?EQ ?addn0//.
+      apply: completed_implies_not_scheduled => //.
       by rewrite /completed_by EQ.
-    - apply leq_trans with (n := service sched j t + 1);
-        last by rewrite addn1.
-      rewrite leq_add2l.
-      by apply H_unit_service.
+    - have: service_at sched j t <= 1 by exact: unit_service.
+      rewrite -(leq_add2l (service sched j t)) => /leq_trans; apply.
+      by rewrite addn1.
   Qed.
 
   (** This lets us conclude that [service] and [remaining_cost] are complements
@@ -203,11 +198,7 @@ Section ServiceAndCompletionFacts.
   Lemma service_cost_invariant:
     forall t,
       (service sched j t) + (remaining_cost sched j t) = job_cost j.
-  Proof.
-    move=> t.
-    rewrite /remaining_cost subnKC //.
-    by apply service_at_most_cost.
-  Qed.
+  Proof. by move=> ?; rewrite subnKC// service_at_most_cost. Qed.
 
   (** We show that the service received by job [j] in any interval is no larger
      than its cost. *)
@@ -216,9 +207,9 @@ Section ServiceAndCompletionFacts.
       service_during sched j t t' <= job_cost j.
   Proof.
     move=> t t'.
-    case/orP: (leq_total t t') => [tt'|tt']; last by rewrite service_during_geq //.
-    apply leq_trans with (n := service sched j t'); last by apply: service_at_most_cost.
-    rewrite /service. rewrite -(service_during_cat sched j 0 t t') // leq_addl //.
+    have [t'_le_t|t_lt_t'] := leqP t' t; first by rewrite service_during_geq.
+    apply: leq_trans (service_at_most_cost t').
+    by rewrite -(service_cat _ _ _ _ (ltnW t_lt_t')) leq_addl.
   Qed.
 
   (** If a job isn't complete at time [t], it can't be completed at time [t +
@@ -228,15 +219,14 @@ Section ServiceAndCompletionFacts.
       ~~ completed_by sched j t ->
       ~~ completed_by sched j (t + remaining_cost sched j t - 1).
   Proof.
-    move=> t.
-    rewrite incomplete_is_positive_remaining_cost => REMCOST.
+    move=> t; rewrite incomplete_is_positive_remaining_cost => rem_cost.
     rewrite -less_service_than_cost_is_incomplete -(service_cat sched j t);
-    last by rewrite -addnBA //; apply: leq_addr.
-    apply leq_ltn_trans with (n := service sched j t + remaining_cost sched j t - 1).
-    - by rewrite -!addnBA //; rewrite leq_add2l; apply cumulative_service_le_delta; exact.
-    - rewrite service_cost_invariant // -subn_gt0 subKn //.
-      move: REMCOST. rewrite /remaining_cost subn_gt0 => SERVICE.
-        by apply leq_ltn_trans with (n := service sched j t).
+      last by rewrite -addnBA//; exact: leq_addr.
+    have: service sched j t + remaining_cost sched j t - 1 < job_cost j.
+    { rewrite service_cost_invariant -subn_gt0 subKn//.
+      exact/(leq_trans rem_cost)/leq_subr. }
+    apply: leq_ltn_trans.
+    by rewrite -!addnBA// leq_add2l cumulative_service_le_delta.
   Qed.
 
   Section GuaranteedService.
@@ -248,17 +238,21 @@ Section ServiceAndCompletionFacts.
     Context `{JobArrival Job}.
     Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched.
 
+    (** To simplify subsequent proofs, we restate the assumption
+        [H_jobs_must_arrive] as a trivial corollary. *)
+    Corollary has_arrived_scheduled :
+      forall t,
+        scheduled_at sched j t -> has_arrived j t.
+    Proof. exact: H_jobs_must_arrive. Qed.
+
     (** We show that if job j is scheduled, then it must be pending. *)
     Lemma scheduled_implies_pending:
       forall t,
         scheduled_at sched j t ->
         pending sched j t.
     Proof.
-      move=> t SCHED.
-      rewrite /pending.
-      apply /andP; split;
-        first by apply: H_jobs_must_arrive => //.
-      by apply: scheduled_implies_not_completed => //.
+      move=> t sch; apply/andP; split; first exact: has_arrived_scheduled.
+      exact: scheduled_implies_not_completed.
     Qed.
 
   End GuaranteedService.
@@ -300,27 +294,23 @@ Section PositiveCost.
         job_arrival j <= t' < t
         /\ scheduled_at sched j t'.
   Proof.
-    rewrite /completed_by.
-    move=> t COMPLETE.
-    have POSITIVE_SERVICE: 0 < service sched j t
-      by apply leq_trans with (n := job_cost j); auto.
-      by apply: positive_service_implies_scheduled_since_arrival; assumption.
+    move=> t comp.
+    have: 0 < service sched j t by exact: leq_trans comp.
+    exact: positive_service_implies_scheduled_since_arrival.
   Qed.
 
   (** We also prove that the job is pending at the moment of its arrival. *)
   Lemma job_pending_at_arrival:
     pending sched j (job_arrival j).
   Proof.
-    rewrite /pending.
-    apply/andP; split;
-    first by rewrite /has_arrived //.
-    rewrite /completed_by no_service_before_arrival // -ltnNge //.
+    apply/andP; split; first by rewrite /has_arrived.
+    by rewrite /completed_by no_service_before_arrival// -ltnNge.
   Qed.
 
 End PositiveCost.
 
 Section CompletedJobs.
-  
+
   (** Consider any kinds of jobs and any kind of processor state. *)
   Context {Job : JobType} {PState : ProcessorState Job}.
 
@@ -336,22 +326,15 @@ Section CompletedJobs.
   (** We observe that a given job is ready only if it is also incomplete... *)
   Lemma ready_implies_incomplete:
     forall j t, job_ready sched j t -> ~~ completed_by sched j t.
-  Proof.
-    move=> j t READY.
-    move: (any_ready_job_is_pending sched j t READY).
-    by rewrite /pending => /andP [_ INCOMPLETE].
-  Qed.
+  Proof. by move=> ? ? /any_ready_job_is_pending /andP[]. Qed.
 
   (** ...and lift this observation also to the level of whole schedules. *)
   Lemma completed_jobs_are_not_ready:
     jobs_must_be_ready_to_execute sched ->
     completed_jobs_dont_execute sched.
   Proof.
-    rewrite /jobs_must_be_ready_to_execute /completed_jobs_dont_execute.
-    move=> READY_IF_SCHED j t SCHED.
-    move: (READY_IF_SCHED j t SCHED) => READY.
-    rewrite less_service_than_cost_is_incomplete.
-    by apply ready_implies_incomplete.
+    move=> + j t sch => /(_ j t sch) ready.
+    by rewrite less_service_than_cost_is_incomplete ready_implies_incomplete.
   Qed.
 
   (** Furthermore, in a valid schedule, completed jobs don't execute. *)
@@ -359,10 +342,7 @@ Section CompletedJobs.
     forall arr_seq, 
     valid_schedule sched arr_seq ->
     completed_jobs_dont_execute sched.
-  Proof.
-    move=> arr_seq [??].
-    by apply completed_jobs_are_not_ready.
-  Qed.
+  Proof. move=> ? [? ?]; exact: completed_jobs_are_not_ready. Qed.
 
   (** We further observe that completed jobs don't execute if scheduled jobs
      always receive non-zero service and cumulative service never exceeds job
@@ -373,11 +353,8 @@ Section CompletedJobs.
     completed_jobs_dont_execute sched.
   Proof.
     move=> IDEAL SERVICE_BOUND j t SCHED.
-    have UB := SERVICE_BOUND j t.+1.
-    have POS := IDEAL _ _ SCHED.
-    apply leq_trans with (n := service sched j t.+1) => //.
-    rewrite -service_last_plus_before /service_at.
-    by rewrite -{1}(addn0 (service sched j t)) ltn_add2l.
+    apply: leq_trans (SERVICE_BOUND j t.+1).
+    by rewrite -service_last_plus_before -addn1 leq_add2l IDEAL.
   Qed.
 
 End CompletedJobs.
@@ -402,9 +379,8 @@ Section CompletionInTwoSchedules.
         completed_by sched1 j t = completed_by sched2 j t.
   Proof.
     move=> sched1 sched2 h PREFIX j t LE_h.
-    rewrite /completed_by.
-    rewrite (identical_prefix_service sched1 sched2) //.
-    now apply (identical_prefix_inclusion _ _ h).
+    rewrite /completed_by (identical_prefix_service sched1 sched2)//.
+    exact: identical_prefix_inclusion PREFIX.
   Qed.
 
   (** For convenience, we restate the previous lemma in terms of [pending]. *)
@@ -415,9 +391,8 @@ Section CompletionInTwoSchedules.
         t <= h ->
         pending sched1 j t = pending sched2 j t.
   Proof.
-    move=> sched1 sched2 h PREFIX j t LE_h.
-    now rewrite /pending (identical_prefix_completed_by _ sched2 h).
+    move=> sched1 sched2 h PREFIX j t t_le_h.
+    by rewrite /pending (identical_prefix_completed_by _ sched2 h).
   Qed.
 
-
 End CompletionInTwoSchedules.

analysis/facts/behavior/deadlines.v

@@ -27,11 +27,9 @@ Section DeadlineFacts.
         ~~ completed_by sched j t ->
         t < job_deadline j.
     Proof.
-      move=> j t MET INCOMP.
-      apply contraT; rewrite -leqNgt => PAST_DL.
-      have DL_MISS: ~~ completed_by sched j (job_deadline j)
-        by apply incompletion_monotonic with (t' := t) => //.
-      by move: DL_MISS => /negP.
+      move=> j t MET INCOMP; apply: contraT; rewrite -leqNgt => PAST_DL.
+      have /negP// : ~~ completed_by sched j (job_deadline j).
+      exact: incompletion_monotonic INCOMP.
     Qed.
 
     (** Furthermore, a job that both meets its deadline and is incomplete at a
@@ -46,11 +44,8 @@ Section DeadlineFacts.
       move=> j t MET INCOMP.
       apply: cumulative_service_implies_scheduled.
       rewrite -(ltn_add2l (service sched j t)) addn0.
-      rewrite service_cat;
-        last by (apply ltnW; apply incomplete_implies_later_deadline).
-      apply leq_trans with (n := job_cost j);
-        first by rewrite less_service_than_cost_is_incomplete.
-      by apply MET.
+      rewrite service_cat; last exact/ltnW/incomplete_implies_later_deadline.
+      by apply: leq_trans MET; rewrite less_service_than_cost_is_incomplete.
     Qed.
 
   End Incompletion.
@@ -77,8 +72,8 @@ Section DeadlineFacts.
         t < job_deadline j.
     Proof.
       move=> j t MET SCHED_AT.
-      apply (incomplete_implies_later_deadline sched) => //.
-      by apply scheduled_implies_not_completed.
+      apply: (incomplete_implies_later_deadline sched) => //.
+      exact: scheduled_implies_not_completed.
     Qed.
 
   End IdealProgressSchedules.
@@ -101,8 +96,7 @@ Section DeadlineFacts.
         (job_meets_deadline sched j <-> job_meets_deadline sched' j).
     Proof.
       move=> j SERVICE.
-      split;
-        by rewrite /job_meets_deadline /completed_by -SERVICE.
+      by split; rewrite /job_meets_deadline /completed_by -SERVICE.
     Qed.
 
   End EqualProgress.

analysis/facts/edf_definitions.v

@@ -85,8 +85,7 @@ Section Equivalence.
     { apply /andP; split => //.
       - apply /andP; split => //.
         apply (incompletion_monotonic _ j _ _ LEQ).
-        apply scheduled_implies_not_completed => //.
-        by apply ideal_proc_model_ensures_ideal_progress.
+        by apply scheduled_implies_not_completed.
       - apply /negP; move => SCHED''.
         by exploit (ideal_proc_model_is_a_uniprocessor_model j j_hp sched t). }
   Qed.

analysis/facts/job_index.v

@@ -148,14 +148,14 @@ Section JobIndexLemmas.
   Proof.
     intros * IN1 IN2 LE.
     move_neq_up LT; move_neq_down LE.
-    rewrite -> arrivals_P_cat with (t := job_arrival j1); last by apply job_arrival_between in IN1 => //.
+    rewrite -> arrivals_P_cat with (t := job_arrival j1); last by apply job_arrival_between_P in IN1 => //.
     rewrite !index_cat ifT; last by eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.
     rewrite ifF.
-    - eapply leq_trans; [ | now erewrite leq_addr].
+    - eapply leq_trans; [ | by erewrite leq_addr].
       rewrite index_mem.
-      now eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.
+      by eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.
     - apply Bool.not_true_is_false; intro T.
-      now apply job_arrival_between in T; try lia.
+      by apply job_arrival_between_P in T; try lia.
   Qed.
   
   (** We observe that index of job [j1] is same in the 
@@ -168,7 +168,8 @@ Section JobIndexLemmas.
     rewrite leq_eqVlt => /orP [/eqP LT|LT]; first by rewrite /task_arrivals_up_to_job_arrival LT H_same_task.
     specialize (arrival_lt_implies_strict_prefix _ H_consistent_arrivals (job_task j1) j1 j2) => SUB.
     feed_n 5 SUB => //; move: SUB => [xs2 [NEMPT2 CAT2]].
-    now rewrite -CAT2 index_cat ifT; last by apply arrives_in_task_arrivals_up_to => //.
+    rewrite -CAT2 index_cat ifT //=.
+    by apply arrives_in_task_arrivals_up_to => //.
   Qed.
 
   (** We show that the [job_index] of a job [j1] is strictly less than
@@ -177,7 +178,7 @@ Section JobIndexLemmas.
     job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1).
   Proof.
     rewrite /job_index index_mem.
-    now apply arrives_in_task_arrivals_up_to.
+    exact: arrives_in_task_arrivals_up_to.
   Qed.
 
   (** Finally, we show that a lower job index implies an earlier arrival time. *)
@@ -195,7 +196,7 @@ Section JobIndexLemmas.
     - now eapply leq_trans;
         [apply index_job_lt_size_task_arrivals_up_to_job | rewrite leq_addr].
     - apply Bool.not_true_is_false; intro T.
-      now apply job_arrival_between in T; try lia.
+      now apply job_arrival_between_P in T; try lia.
   Qed.
 
   (** We show that if job [j1] arrives earlier than job [j2]

analysis/facts/transform/edf_opt.v

@@ -196,9 +196,8 @@ Section MakeEDFAtFacts.
       job_deadline j > t.
   Proof.
     move=> j t SCHED.
-    apply (scheduled_at_implies_later_deadline sched) => //.
-    - by apply ideal_proc_model_ensures_ideal_progress.
-    - by apply (H_no_deadline_misses _ t).
+    apply: (scheduled_at_implies_later_deadline sched) => //.
+    exact: (H_no_deadline_misses _ t).
   Qed.
 
   (** We analyze [make_edf_at] applied to an arbitrary point in time,
@@ -244,7 +243,6 @@ Section MakeEDFAtFacts.
         by rewrite scheduled_at_def; apply /eqP.
       move: (scheduled_job_in_sched_has_later_deadline _ _ SCHED') => DL_orig.
       apply edf_swap_no_deadline_misses_introduced => //.
-      - by apply ideal_proc_model_ensures_ideal_progress.
       - by apply fsc_range1 => //.
       - move=> j1 j2 SCHED_j1 SCHED_j2.
         apply: (fsc_found_job_deadline sched _ j_orig t_edf _ _ _ _ _ t_edf) => //.
@@ -274,7 +272,6 @@ Section MakeEDFAtFacts.
     move=> j t SCHED.
     apply (scheduled_at_implies_later_deadline sched') => //.
     - by apply mea_completed_jobs.
-    - by apply ideal_proc_model_ensures_ideal_progress.
     - by apply mea_no_deadline_misses with (t := t).
   Qed.
 
@@ -579,8 +576,7 @@ Section EDFPrefixFacts.
     move=> j t SCHED.
     move: edf_prefix_well_formedness => [COMP [ARR DL_MET]].
     apply (scheduled_at_implies_later_deadline sched') => //.
-    - by apply ideal_proc_model_ensures_ideal_progress.
-    - by apply (DL_MET j t).
+    exact: (DL_MET j t).
   Qed.
 
   (** Since no jobs are lost or added to the schedule by

analysis/facts/transform/edf_wc.v

@@ -267,7 +267,6 @@ Section MakeEDFWorkConservationLemmas.
          apply fsc_swap_maintains_work_conservation => //.
          -  by rewrite scheduled_at_def; apply /eqP => //.
          - apply (scheduled_at_implies_later_deadline sched) => //.
-           + by apply ideal_proc_model_ensures_ideal_progress.
            + rewrite /all_deadlines_met in  (H_no_deadline_misses).
              now apply (H_no_deadline_misses s t_edf); rewrite scheduled_at_def; apply /eqP.
            + by rewrite scheduled_at_def; apply/eqP => //.
@@ -380,4 +379,3 @@ Section EDFTransformWorkConservationLemmas.
   Qed.
 
 End EDFTransformWorkConservationLemmas.
-

model/preemption/parameter.v

@@ -35,29 +35,11 @@ Section MaxAndLastNonpreemptiveSegment.
 
   (** We observe that the conversion indeed is an equivalent way of
       representing the set of preemption points. *)
-  Remark conversion_preserves_equivalence:
+  Remark conversion_preserves_equivalence :
     forall (j : Job) (ρ : work),
       ρ <= job_cost j ->
       job_preemptable j ρ <-> ρ \in job_preemption_points j.
-  Proof.
-    intros ? ? LE.
-    case: (posnP (job_cost j)) => [ZERO|POS].
-    { unfold job_preemption_points.
-      split; intros PP.
-      - move: LE; rewrite ZERO leqn0; move => /eqP EQ; subst.
-        by simpl; rewrite PP.
-      - rewrite ZERO in PP; simpl in PP.
-        destruct (job_preemptable j 0) eqn:EQ; last by done.
-        by move: PP => /orP [/eqP A1| FF]; subst.
-    }
-    have F: job_cost j == 0 = false.
-    { by apply/eqP/neqP; rewrite -lt0n. }
-    split; intros PP.
-    all: unfold job_preemption_points in *.
-    - rewrite mem_filter; apply/andP; split; first by done.
-      by rewrite mem_iota subn0 add0n //; apply/andP; split.
-    - by move: PP; rewrite mem_filter; move => /andP [PP _].
-  Qed.
+  Proof. by move=> j rho le; rewrite mem_filter mem_index_iota ltnS le/= andbT. Qed.
 
   (** We further define a function that, for a given job, yields the sequence
       of lengths of its nonpreemptive segments. *)