# Library prosa.analysis.transform.prefix

Require Export prosa.analysis.facts.behavior.all.
This file provides an operation that transforms a finite prefix of a given schedule by applying a point-wise transformation to each instant up to a given horizon.
Section SchedulePrefixMap.
For any type of jobs and...
Context {Job : JobType}.
... any given type of processor states ...
Context {PState : ProcessorState Job}.
... we define a procedure that applies a given function to every point in a given finite prefix of the schedule.
The point-wise transformation f is given a schedule and the point to transform, and must yield a transformed schedule that is used in subsequent operations.
Fixpoint prefix_map
(sched : schedule PState)
(f : schedule PState → instant → schedule PState)
(horizon : instant) :=
match horizon with
| 0 ⇒ sched
| S t ⇒
let
prefix := prefix_map sched f t
in f prefix t
end.
We provide a utility lemma that establishes that, if the point-wise transformation maintains a given property of the original schedule, then the prefix_map does so as well.
Section PropertyPreservation.
Given any property of schedules...
Variable P : schedule PState → Prop.
...and a point-wise transformation f,...
Variable f : schedule PState → instant → schedule PState.
...if f maintains property P,...
Hypothesis H_f_maintains_P : ∀ sched t, P sched → P (f sched t).
...then so does a prefix map of f.
Lemma prefix_map_property_invariance :
∀ sched h, P sched → P (prefix_map sched f h).
Proof.
move⇒ sched h P_sched.
induction h; first by rewrite /prefix_map.
rewrite /prefix_map -/prefix_map.
by apply: H_f_maintains_P.
Qed.
End PropertyPreservation.
Next, we consider the case where the point-wise transformation establishes a new property step-by-step.
Section PointwiseProperty.
Given any property of schedules P,...
Variable P : schedule PState → Prop.
...any point-wise property Q,...
Variable Q : schedule PState → instant → Prop.
...and a point-wise transformation f,...
Variable f : schedule PState → instant → schedule PState.
...if f maintains P...
Hypothesis H_f_maintains_P :
∀ sched t_ref,
P sched → P (f sched t_ref).
...and establishes Q (provided that P holds)...
Hypothesis H_f_grows_Q :
∀ sched t_ref,
P sched →
(∀ t', t' < t_ref → Q sched t') →
∀ t', t' ≤ t_ref → Q (f sched t_ref) t'.
...then the prefix-map operation will "grow" Q up to the horizon.
Lemma prefix_map_pointwise_property :
∀ sched horizon,
P sched →
∀ t,
t < horizon →
Q (prefix_map sched f horizon) t.
Proof.
move⇒ sched h P_holds.
induction h as [|h Q_holds_before_h]; first by rewrite /prefix_map.
rewrite /prefix_map -/prefix_map ⇒ t.
rewrite ltnS ⇒ LE_t_h.
apply H_f_grows_Q ⇒ //.
by apply prefix_map_property_invariance.
Qed.
End PointwiseProperty.
End SchedulePrefixMap.