Library prosa.analysis.transform.prefix


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)


From mathcomp Require Import ssrnat ssrbool fintype.
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.
For any type of jobs and...
  Context {Job : JobType}.

... any given type of processor states ...
  Context {PState: eqType}.
  Context `{ProcessorState Job PState}.

... 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).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 229)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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.
      movesched h P_sched.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 232)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 240)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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 (succn h))

----------------------------------------------------------------------------- *)


      rewrite /prefix_map -/prefix_map.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 243)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 234)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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.
      movesched h P_holds.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 237)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 245)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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 < succn h -> Q (prefix_map sched f (succn h)) t

----------------------------------------------------------------------------- *)


      rewrite /prefix_map -/prefix_mapt.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 280)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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 < succn h -> Q (f (prefix_map sched f h) h) t

----------------------------------------------------------------------------- *)


      rewrite ltnSLE_t_h.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 285)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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 ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 286)
  
  Job : JobType
  PState : eqType
  H : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

  End PointwiseProperty.

End SchedulePrefixMap.