Require Export prosa.analysis.facts.behavior.all.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]

(** 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: forall sched t, P sched -> P (f sched t).

    (** ...then so does a prefix map of [f]. *)
    Lemma prefix_map_property_invariance:
      forall sched h, P sched -> P (prefix_map sched f h).
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t : instant),
P sched -> P (f sched t)
forall (sched : schedule PState) (h : instant),
P sched -> P (prefix_map sched f h)
    Proof.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t : instant),
P sched -> P (f sched t)
forall (sched : schedule PState) (h : instant),
P sched -> P (prefix_map sched f h)
      move=> sched h P_sched.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t : instant),
P sched -> P (f sched t)
sched: schedule PState
h: instant
P_sched: P sched
P (prefix_map sched f h)
      induction h; first by rewrite /prefix_map.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t : instant),
P sched -> P (f sched t)
sched: schedule PState
h: nat
P_sched: P sched
IHh: P (prefix_map sched f h)
P (prefix_map sched f h.+1)
      rewrite /prefix_map -/prefix_map.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t : instant),
P sched -> P (f sched t)
sched: schedule PState
h: nat
P_sched: P sched
IHh: P (prefix_map sched f h)
P (f (prefix_map sched f h) h)
      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:
      forall sched t_ref,
        P sched -> P (f sched t_ref).

    (** ...and establishes [Q] (provided that [P] holds)... *)
    Hypothesis H_f_grows_Q:
      forall sched t_ref,
        P sched ->
        (forall t', t' <  t_ref -> Q sched t') ->
        forall 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:
      forall sched horizon,
        P sched ->
        forall t,
          t < horizon ->
          Q (prefix_map sched f horizon) t.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
Q: schedule PState -> instant -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t_ref : instant),
P sched -> P (f sched t_ref)
H_f_grows_Q: forall (sched : schedule PState)
  (t_ref : nat),
P sched ->
(forall t' : nat,
 t' < t_ref -> Q sched t') ->
forall t' : nat,
t' <= t_ref -> Q (f sched t_ref) t'
forall (sched : schedule PState) (horizon : nat),
P sched ->
forall t : nat,
t < horizon -> Q (prefix_map sched f horizon) t
    Proof.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
Q: schedule PState -> instant -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t_ref : instant),
P sched -> P (f sched t_ref)
H_f_grows_Q: forall (sched : schedule PState)
  (t_ref : nat),
P sched ->
(forall t' : nat,
 t' < t_ref -> Q sched t') ->
forall t' : nat,
t' <= t_ref -> Q (f sched t_ref) t'
forall (sched : schedule PState) (horizon : nat),
P sched ->
forall t : nat,
t < horizon -> Q (prefix_map sched f horizon) t
      move=> sched h P_holds.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
Q: schedule PState -> instant -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t_ref : instant),
P sched -> P (f sched t_ref)
H_f_grows_Q: forall (sched : schedule PState)
  (t_ref : nat),
P sched ->
(forall t' : nat,
 t' < t_ref -> Q sched t') ->
forall t' : nat,
t' <= t_ref -> Q (f sched t_ref) t'
sched: schedule PState
h: nat
P_holds: P sched
forall t : nat, t < h -> Q (prefix_map sched f h) t
      induction h as [|h Q_holds_before_h]; first by rewrite /prefix_map.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
Q: schedule PState -> instant -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t_ref : instant),
P sched -> P (f sched t_ref)
H_f_grows_Q: forall (sched : schedule PState)
  (t_ref : nat),
P sched ->
(forall t' : nat,
 t' < t_ref -> Q sched t') ->
forall t' : nat,
t' <= t_ref -> Q (f sched t_ref) t'
sched: schedule PState
h: nat
P_holds: P sched
Q_holds_before_h: forall t : nat,
t < h -> Q (prefix_map sched f h) t
forall t : nat,
t < h.+1 -> Q (prefix_map sched f h.+1) t
      rewrite /prefix_map -/prefix_map => t.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
Q: schedule PState -> instant -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t_ref : instant),
P sched -> P (f sched t_ref)
H_f_grows_Q: forall (sched : schedule PState)
  (t_ref : nat),
P sched ->
(forall t' : nat,
 t' < t_ref -> Q sched t') ->
forall t' : nat,
t' <= t_ref -> Q (f sched t_ref) t'
sched: schedule PState
h: nat
P_holds: P sched
Q_holds_before_h: forall t : nat,
t < h -> Q (prefix_map sched f h) t
t: nat
t < h.+1 -> Q (f (prefix_map sched f h) h) t
      rewrite ltnS => LE_t_h.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
Q: schedule PState -> instant -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t_ref : instant),
P sched -> P (f sched t_ref)
H_f_grows_Q: forall (sched : schedule PState)
  (t_ref : nat),
P sched ->
(forall t' : nat,
 t' < t_ref -> Q sched t') ->
forall t' : nat,
t' <= t_ref -> Q (f sched t_ref) t'
sched: schedule PState
h: nat
P_holds: P sched
Q_holds_before_h: forall t : nat,
t < h -> Q (prefix_map sched f h) t
t: nat
LE_t_h: t <= h
Q (f (prefix_map sched f h) h) t
      apply H_f_grows_Q => //.
Job: JobType
PState: ProcessorState Job
P: schedule PState -> Prop
Q: schedule PState -> instant -> Prop
f: schedule PState -> instant -> schedule PState
H_f_maintains_P: forall (sched : schedule PState)
  (t_ref : instant),
P sched -> P (f sched t_ref)
H_f_grows_Q: forall (sched : schedule PState)
  (t_ref : nat),
P sched ->
(forall t' : nat,
 t' < t_ref -> Q sched t') ->
forall t' : nat,
t' <= t_ref -> Q (f sched t_ref) t'
sched: schedule PState
h: nat
P_holds: P sched
Q_holds_before_h: forall t : nat,
t < h -> Q (prefix_map sched f h) t
t: nat
LE_t_h: t <= h
P (prefix_map sched f h)
      by apply prefix_map_property_invariance.
    Qed.
    
  End PointwiseProperty.

End SchedulePrefixMap.