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...
... any given type of processor states ...
... 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.
(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.
Given any property of schedules...
...and a point-wise transformation [f],...
...if [f] maintains property [P],...
...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.
move⇒ sched 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.
∀ 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.
move⇒ sched 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.
Given any property of schedules [P],...
...any point-wise property [Q],...
...and a point-wise transformation [f],...
...if [f] maintains [P]...
...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'.
∀ 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.
move⇒ sched 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_map ⇒ t.
(* ----------------------------------[ 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 ltnS ⇒ LE_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.
∀ 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.
move⇒ sched 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_map ⇒ t.
(* ----------------------------------[ 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 ltnS ⇒ LE_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.