Library prosa.implementation.facts.generic_schedule
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
Require Export prosa.implementation.definitions.generic_scheduler.
Require Export prosa.analysis.facts.transform.replace_at.
Properties of the Generic Reference Scheduler
For any type of jobs and type of schedule, ...
... any scheduling policy, and ...
... any notion of idleness.
For notational convenience, we define [prefix t] to denote the finite
prefix considered when scheduling a job at time [t].
Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.
To begin with, we establish two simple rewriting lemmas for unrolling
[schedule_up_to]. First, we observe that the allocation is indeed
determined by the policy based on the preceding prefix.
Lemma schedule_up_to_def:
∀ t,
schedule_up_to policy idle_state t t = policy (prefix t) t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 572)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall t : instant,
schedule_up_to policy idle_state t t = policy (prefix t) t
----------------------------------------------------------------------------- *)
Proof. by elim⇒ [|n IH]; rewrite [LHS]/schedule_up_to -/(schedule_up_to _) /replace_at; apply ifT.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
schedule_up_to policy idle_state t t = policy (prefix t) t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 572)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall t : instant,
schedule_up_to policy idle_state t t = policy (prefix t) t
----------------------------------------------------------------------------- *)
Proof. by elim⇒ [|n IH]; rewrite [LHS]/schedule_up_to -/(schedule_up_to _) /replace_at; apply ifT.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Second, we note how to replace [schedule_up_to] in the general case with
its definition.
Lemma schedule_up_to_unfold:
∀ h t,
schedule_up_to policy idle_state h t = replace_at (prefix h) h (policy (prefix h) h) t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 579)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall h t : instant,
schedule_up_to policy idle_state h t =
replace_at (prefix h) h (policy (prefix h) h) t
----------------------------------------------------------------------------- *)
Proof. by move⇒ h t; rewrite [LHS]/schedule_up_to /prefix; elim: h.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ h t,
schedule_up_to policy idle_state h t = replace_at (prefix h) h (policy (prefix h) h) t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 579)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall h t : instant,
schedule_up_to policy idle_state h t =
replace_at (prefix h) h (policy (prefix h) h) t
----------------------------------------------------------------------------- *)
Proof. by move⇒ h t; rewrite [LHS]/schedule_up_to /prefix; elim: h.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Next, we observe that we can increase a prefix's horizon by one
time unit without changing any allocations in the prefix.
Lemma schedule_up_to_widen:
∀ h t,
t ≤ h →
schedule_up_to policy idle_state h t = schedule_up_to policy idle_state h.+1 t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 586)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall h t : nat,
t <= h ->
schedule_up_to policy idle_state h t =
schedule_up_to policy idle_state (succn h) t
----------------------------------------------------------------------------- *)
Proof.
move⇒ h t RANGE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 589)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h, t : nat
RANGE : t <= h
============================
schedule_up_to policy idle_state h t =
schedule_up_to policy idle_state (succn h) t
----------------------------------------------------------------------------- *)
rewrite [RHS]schedule_up_to_unfold rest_of_schedule_invariant // ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 640)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h, t : nat
RANGE : t <= h
EQ : t = succn h
============================
False
----------------------------------------------------------------------------- *)
now move: RANGE; rewrite EQ ltnn.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ h t,
t ≤ h →
schedule_up_to policy idle_state h t = schedule_up_to policy idle_state h.+1 t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 586)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall h t : nat,
t <= h ->
schedule_up_to policy idle_state h t =
schedule_up_to policy idle_state (succn h) t
----------------------------------------------------------------------------- *)
Proof.
move⇒ h t RANGE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 589)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h, t : nat
RANGE : t <= h
============================
schedule_up_to policy idle_state h t =
schedule_up_to policy idle_state (succn h) t
----------------------------------------------------------------------------- *)
rewrite [RHS]schedule_up_to_unfold rest_of_schedule_invariant // ⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 640)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h, t : nat
RANGE : t <= h
EQ : t = succn h
============================
False
----------------------------------------------------------------------------- *)
now move: RANGE; rewrite EQ ltnn.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
After the horizon of a prefix, the schedule is still "empty", meaning
that all instants are idle.
Lemma schedule_up_to_empty:
∀ h t,
h < t →
schedule_up_to policy idle_state h t = idle_state.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 592)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall h t : nat,
h < t -> schedule_up_to policy idle_state h t = idle_state
----------------------------------------------------------------------------- *)
Proof.
move⇒ h t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 594)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h, t : nat
============================
h < t -> schedule_up_to policy idle_state h t = idle_state
----------------------------------------------------------------------------- *)
elim: h ⇒ [LT|h IH LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 604)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t : nat
LT : 0 < t
============================
schedule_up_to policy idle_state 0 t = idle_state
subgoal 2 (ID 607) is:
schedule_up_to policy idle_state (succn h) t = idle_state
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 604)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t : nat
LT : 0 < t
============================
schedule_up_to policy idle_state 0 t = idle_state
----------------------------------------------------------------------------- *)
rewrite /schedule_up_to rest_of_schedule_invariant // ⇒ ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 649)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t : nat
LT : 0 < t
ZERO : t = 0
============================
False
----------------------------------------------------------------------------- *)
now subst.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 607)
subgoal 1 (ID 607) is:
schedule_up_to policy idle_state (succn h) t = idle_state
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 607)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
LT : succn h < t
============================
schedule_up_to policy idle_state (succn h) t = idle_state
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 607)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
LT : succn h < t
============================
schedule_up_to policy idle_state (succn h) t = idle_state
----------------------------------------------------------------------------- *)
rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ h t);
first by apply IH ⇒ //; apply ltn_trans with (n := h.+1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 691)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
LT : succn h < t
============================
t <> succn h
----------------------------------------------------------------------------- *)
move⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 718)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
LT : succn h < t
EQ : t = succn h
============================
False
----------------------------------------------------------------------------- *)
move: LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 720)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
EQ : t = succn h
============================
succn h < t -> False
----------------------------------------------------------------------------- *)
now rewrite EQ ltnn.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ h t,
h < t →
schedule_up_to policy idle_state h t = idle_state.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 592)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall h t : nat,
h < t -> schedule_up_to policy idle_state h t = idle_state
----------------------------------------------------------------------------- *)
Proof.
move⇒ h t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 594)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h, t : nat
============================
h < t -> schedule_up_to policy idle_state h t = idle_state
----------------------------------------------------------------------------- *)
elim: h ⇒ [LT|h IH LT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 604)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t : nat
LT : 0 < t
============================
schedule_up_to policy idle_state 0 t = idle_state
subgoal 2 (ID 607) is:
schedule_up_to policy idle_state (succn h) t = idle_state
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 604)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t : nat
LT : 0 < t
============================
schedule_up_to policy idle_state 0 t = idle_state
----------------------------------------------------------------------------- *)
rewrite /schedule_up_to rest_of_schedule_invariant // ⇒ ZERO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 649)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t : nat
LT : 0 < t
ZERO : t = 0
============================
False
----------------------------------------------------------------------------- *)
now subst.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 607)
subgoal 1 (ID 607) is:
schedule_up_to policy idle_state (succn h) t = idle_state
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 607)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
LT : succn h < t
============================
schedule_up_to policy idle_state (succn h) t = idle_state
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 607)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
LT : succn h < t
============================
schedule_up_to policy idle_state (succn h) t = idle_state
----------------------------------------------------------------------------- *)
rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ h t);
first by apply IH ⇒ //; apply ltn_trans with (n := h.+1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 691)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
LT : succn h < t
============================
t <> succn h
----------------------------------------------------------------------------- *)
move⇒ EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 718)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
LT : succn h < t
EQ : t = succn h
============================
False
----------------------------------------------------------------------------- *)
move: LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 720)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
t, h : nat
IH : h < t -> schedule_up_to policy idle_state h t = idle_state
EQ : t = succn h
============================
succn h < t -> False
----------------------------------------------------------------------------- *)
now rewrite EQ ltnn.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
A crucial fact is that a prefix up to horizon [h1] is identical to a
prefix up to a later horizon [h2] at times up to [h1].
Lemma schedule_up_to_prefix_inclusion:
∀ h1 h2,
h1 ≤ h2 →
∀ t,
t ≤ h1 →
schedule_up_to policy idle_state h1 t = schedule_up_to policy idle_state h2 t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 600)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall h1 h2 : nat,
h1 <= h2 ->
forall t : nat,
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state h2 t
----------------------------------------------------------------------------- *)
Proof.
move⇒ h1 h2 LEQ t BEFORE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 605)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, h2 : nat
LEQ : h1 <= h2
t : nat
BEFORE : t <= h1
============================
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state h2 t
----------------------------------------------------------------------------- *)
elim: h2 LEQ BEFORE; first by rewrite leqn0 ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 618)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, t : nat
============================
forall n : nat,
(h1 <= n ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state n t) ->
h1 <= succn n ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state (succn n) t
----------------------------------------------------------------------------- *)
move⇒ t' IH.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 661)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, t, t' : nat
IH : h1 <= t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t' t
============================
h1 <= succn t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state (succn t') t
----------------------------------------------------------------------------- *)
rewrite leq_eqVlt ltnS ⇒ /orP [/eqP <-|LEQ] // t_H1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 773)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, t, t' : nat
IH : h1 <= t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t' t
LEQ : h1 <= t'
t_H1 : t <= h1
============================
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state (succn t') t
----------------------------------------------------------------------------- *)
rewrite IH // schedule_up_to_widen //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 807)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, t, t' : nat
IH : h1 <= t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t' t
LEQ : h1 <= t'
t_H1 : t <= h1
============================
t <= t'
----------------------------------------------------------------------------- *)
now apply (leq_trans t_H1).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End GenericScheduleProperties.
∀ h1 h2,
h1 ≤ h2 →
∀ t,
t ≤ h1 →
schedule_up_to policy idle_state h1 t = schedule_up_to policy idle_state h2 t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 600)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
============================
forall h1 h2 : nat,
h1 <= h2 ->
forall t : nat,
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state h2 t
----------------------------------------------------------------------------- *)
Proof.
move⇒ h1 h2 LEQ t BEFORE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 605)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, h2 : nat
LEQ : h1 <= h2
t : nat
BEFORE : t <= h1
============================
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state h2 t
----------------------------------------------------------------------------- *)
elim: h2 LEQ BEFORE; first by rewrite leqn0 ⇒ /eqP →.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 618)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, t : nat
============================
forall n : nat,
(h1 <= n ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state n t) ->
h1 <= succn n ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state (succn n) t
----------------------------------------------------------------------------- *)
move⇒ t' IH.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 661)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, t, t' : nat
IH : h1 <= t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t' t
============================
h1 <= succn t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state (succn t') t
----------------------------------------------------------------------------- *)
rewrite leq_eqVlt ltnS ⇒ /orP [/eqP <-|LEQ] // t_H1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 773)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, t, t' : nat
IH : h1 <= t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t' t
LEQ : h1 <= t'
t_H1 : t <= h1
============================
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state (succn t') t
----------------------------------------------------------------------------- *)
rewrite IH // schedule_up_to_widen //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 807)
Job : JobType
PState : Type
H : ProcessorState Job PState
policy : PointwisePolicy PState
idle_state : PState
prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| succn t' => schedule_up_to policy idle_state t'
end : nat -> schedule PState
h1, t, t' : nat
IH : h1 <= t' ->
t <= h1 ->
schedule_up_to policy idle_state h1 t =
schedule_up_to policy idle_state t' t
LEQ : h1 <= t'
t_H1 : t <= h1
============================
t <= t'
----------------------------------------------------------------------------- *)
now apply (leq_trans t_H1).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End GenericScheduleProperties.