note some trivial facts about schedules with a shared prefix

analysis/definitions/schedule_prefix.v

 Require Export prosa.behavior.ready.
+Require Export prosa.util.nat.
 
 (** We define the notion of prefix-equivalence of schedules. *)
 
@@ -17,4 +18,31 @@ Section PrefixDefinition.
       t < horizon ->
       sched t = sched' t.
 
+  (** 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:
+    forall sched sched' h,
+      identical_prefix sched sched' h ->
+      forall j t,
+        t < h ->
+        scheduled_at sched j t = scheduled_at sched' j t.
+  Proof.
+    move=> sched sched' h IDENT j t LT_h.
+    now rewrite /scheduled_at (IDENT t LT_h).
+  Qed.
+
+  (** 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 (ltn_leq_trans LT_h').
+  Qed.
+
 End PrefixDefinition.

analysis/facts/behavior/completion.v

 Require Export prosa.analysis.facts.behavior.service.
 Require Export prosa.analysis.facts.behavior.arrivals.
+Require Export prosa.analysis.definitions.schedule_prefix.
 
 (** * Completion *)
 
@@ -334,3 +335,40 @@ Section CompletedJobs.
   Qed.
 
 End CompletedJobs.
+
+(** Next, we relate the completion of jobs in schedules with identical prefixes. *)
+Section CompletionInTwoSchedules.
+  (** Consider any processor model and any type of jobs with costs, arrival times, and a notion of readiness. *)
+  Context {PState: Type} {Job: JobType} `{ProcessorState Job PState} `{JobReady Job PState}.
+
+  (** If two schedules share a common prefix, then (in the prefix) jobs
+      complete in one schedule iff they complete in the other. *)
+  Lemma identical_prefix_completed_by:
+    forall sched1 sched2 h,
+      identical_prefix sched1 sched2 h ->
+      forall j t,
+        t <= h ->
+        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).
+  Qed.
+
+  (** For convenience, we restate the previous lemma in terms of [pending]. *)
+  Corollary identical_prefix_pending:
+    forall sched1 sched2 h,
+      identical_prefix sched1 sched2 h ->
+      forall j t,
+        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).
+  Qed.
+
+
+End CompletionInTwoSchedules.
+
+

analysis/facts/behavior/service.v

 Require Export prosa.util.all.
 Require Export prosa.behavior.all.
 Require Export prosa.model.processor.platform_properties.
+Require Export prosa.analysis.definitions.schedule_prefix.
 
 (** * Service *)
 
@@ -599,19 +600,19 @@ Section ServiceInTwoSchedules.
 
   (** Consider any two given schedules... *)
   Variable sched1 sched2: schedule PState.
-  
-  (** Given an interval in which the schedules provide the same service 
-      to a job at each instant, we can prove that the cumulative service 
+
+  (** Given an interval in which the schedules provide the same service
+      to a job at each instant, we can prove that the cumulative service
       received during the interval has to be the same. *)
   Section ServiceDuringEquivalentInterval.
-    
+
     (** Consider two time instants...  *)
     Variable t1 t2 : instant.
 
     (** ...and a given job that is to be scheduled. *)
     Variable j: Job.
 
-    (** Assume that, in any instant between [t1] and [t2] the service 
+    (** Assume that, in any instant between [t1] and [t2] the service
         provided to [j] from the two schedules is the same. *)
     Hypothesis H_sched1_sched2_same_service_at:
       forall t, t1 <= t < t2 ->
@@ -642,4 +643,13 @@ Section ServiceInTwoSchedules.
     by rewrite /service_at SCHED_EQ.
   Qed.
 
+  (** For convenience, we restate the corollary also at the level of
+      [service] for identical prefixes. *)
+  Corollary identical_prefix_service:
+    forall h,
+      identical_prefix sched1 sched2 h ->
+      forall j, service sched1 j h = service sched2 j h.
+  Proof.
+    move=> h IDENT j; by apply equal_prefix_implies_same_service_during. Qed.
+
 End ServiceInTwoSchedules.