Skip to content
Snippets Groups Projects
Commit 9227bdb4 authored by Sergey Bozhko's avatar Sergey Bozhko :eyes: Committed by Björn Brandenburg
Browse files

clean up in util/unit_growth.v

* rename [step_function] to [unit_growth]
* restructure file
parent a0579b47
No related branches found
No related tags found
No related merge requests found
......@@ -197,13 +197,13 @@ Section UnitService.
Qed.
Section ServiceIsAStepFunction.
Section ServiceIsUnitGrowthFunction.
(** We show that the service received by any job [j] is a step function. *)
Lemma service_is_a_step_function:
is_step_function (service sched j).
(** We show that the service received by any job [j] is a unit growth function. *)
Lemma service_is_unit_growth_function:
unit_growth_function (service sched j).
Proof.
rewrite /is_step_function => t.
rewrite /unit_growth_function => t.
rewrite addn1 -service_last_plus_before leq_add2l.
by apply service_at_most_one.
Qed.
......@@ -224,14 +224,14 @@ Section UnitService.
service sched j t' = s.
Proof.
feed (exists_intermediate_point (service sched j));
[by apply service_is_a_step_function | intros EX].
[by apply service_is_unit_growth_function | intros EX].
feed (EX 0 t); first by done.
feed (EX s); first by rewrite /service /service_during big_geq //.
by move: EX => /= [x_mid EX]; exists x_mid.
Qed.
End ServiceIsAStepFunction.
End ServiceIsUnitGrowthFunction.
End UnitService.
(** We establish a basic fact about the monotonicity of service. *)
......
......@@ -492,15 +492,15 @@ Module UniprocessorSchedule.
End OnlyOneJobScheduled.
Section ServiceIsAStepFunction.
Section ServiceIsUnitGrowthFunction.
(* First, we show that the service received by any job j
is a step function. *)
Lemma service_is_a_step_function:
is a unit growth funciton. *)
Lemma service_is_unit_growth_function:
forall j,
is_step_function (service sched j).
unit_growth_function (service sched j).
Proof.
unfold is_step_function, service, service_during; intros j t.
unfold unit_growth_function, service, service_during; intros j t.
rewrite addn1 big_nat_recr //=.
by apply leq_add; last by apply leq_b1.
Qed.
......@@ -522,14 +522,14 @@ Module UniprocessorSchedule.
service sched j t0 = s0.
Proof.
feed (exists_intermediate_point (service sched j));
[by apply service_is_a_step_function | intros EX].
[by apply service_is_unit_growth_function | intros EX].
feed (EX 0 t); first by done.
feed (EX s0);
first by rewrite /service /service_during big_geq //.
by move: EX => /= [x_mid EX]; exists x_mid.
Qed.
End ServiceIsAStepFunction.
End ServiceIsUnitGrowthFunction.
Section ScheduledAtEarlierTime.
......@@ -641,4 +641,4 @@ Module UniprocessorSchedule.
End Schedule.
End UniprocessorSchedule.
\ No newline at end of file
End UniprocessorSchedule.
......@@ -335,7 +335,7 @@ Module LastExecution.
rename H_jobs_must_arrive_to_execute into ARR.
move: H_j_has_completed => COMP.
feed (exists_intermediate_point (service sched j));
first by apply service_is_a_step_function.
first by apply service_is_unit_growth_function.
move => EX; feed (EX (job_arrival j) t).
{ feed (cumulative_service_implies_scheduled sched j 0 t).
apply leq_ltn_trans with (n := s); first by done.
......@@ -408,4 +408,4 @@ Module LastExecution.
End TimeAfterLastExecution.
End LastExecution.
\ No newline at end of file
End LastExecution.
Require Export prosa.util.step_function.
Require Export prosa.util.unit_growth.
Require Import prosa.classic.util.tactics prosa.classic.util.notation prosa.classic.util.induction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
......@@ -7,7 +7,7 @@ Require Export prosa.util.nat.
Require Export prosa.util.ssrlia.
Require Export prosa.util.sum.
Require Export prosa.util.seqset.
Require Export prosa.util.step_function.
Require Export prosa.util.unit_growth.
Require Export prosa.util.epsilon.
Require Export prosa.util.search_arg.
Require Export prosa.util.rel.
......
Require Import prosa.util.tactics prosa.util.notation.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
Section StepFunction.
(** We say that a function [f] is a unit growth function iff for any
time instant [t] it holds that [f (t + 1) <= f t + 1]. *)
Definition unit_growth_function (f : nat -> nat) :=
forall t, f (t + 1) <= f t + 1.
Section Defs.
(** In this section, we prove a few useful lemmas about unit growth functions. *)
Section Lemmas.
(* We say that a function [f]... *)
Variable f : nat -> nat.
(** Let [f] be any unit growth function over natural numbers. *)
Variable f : nat -> nat.
Hypothesis H_unit_growth_function : unit_growth_function f.
(* ...is a step function iff the following holds. *)
Definition is_step_function :=
forall t, f (t + 1) <= f t + 1.
(** In the following section, we prove a result similar to the
intermediate value theorem for continuous functions. *)
Section ExistsIntermediateValue.
End Defs.
(** Consider any interval [x1, x2]. *)
Variable x1 x2 : nat.
Hypothesis H_is_interval : x1 <= x2.
Section Lemmas.
(** Let [t] be any value such that [f x1 <= y < f x2]. *)
Variable y : nat.
Hypothesis H_between : f x1 <= y < f x2.
(* Let [f] be any step function over natural numbers. *)
Variable f : nat -> nat.
Hypothesis H_step_function : is_step_function f.
(* In this section, we prove a result similar to the intermediate
value theorem for continuous functions. *)
Section ExistsIntermediateValue.
(* Consider any interval [x1, x2]. *)
Variable x1 x2 : nat.
Hypothesis H_is_interval : x1 <= x2.
(* Let [t] be any value such that [f x1 <= y < f x2]. *)
Variable y : nat.
Hypothesis H_between : f x1 <= y < f x2.
(* Then, we prove that there exists an intermediate point [x_mid] such that
[f x_mid = y]. *)
Lemma exists_intermediate_point :
exists x_mid, x1 <= x_mid < x2 /\ f x_mid = y.
Proof.
rename H_is_interval into INT, H_step_function into STEP, H_between into BETWEEN.
move: x2 INT BETWEEN; clear x2.
suff DELTA:
forall delta,
f x1 <= y < f (x1 + delta) ->
exists x_mid, x1 <= x_mid < x1 + delta /\ f x_mid = y.
{ move => x2 LE /andP [GEy LTy].
exploit (DELTA (x2 - x1));
first by apply/andP; split; last by rewrite addnBA // addKn.
(** Then, we prove that there exists an intermediate point [x_mid] such that [f x_mid = y]. *)
Lemma exists_intermediate_point :
exists x_mid, x1 <= x_mid < x2 /\ f x_mid = y.
Proof.
rename H_is_interval into INT, H_unit_growth_function into UNIT, H_between into BETWEEN.
move: x2 INT BETWEEN; clear x2.
suff DELTA:
forall delta,
f x1 <= y < f (x1 + delta) ->
exists x_mid, x1 <= x_mid < x1 + delta /\ f x_mid = y.
{ move => x2 LE /andP [GEy LTy].
exploit (DELTA (x2 - x1));
first by apply/andP; split; last by rewrite addnBA // addKn.
by rewrite addnBA // addKn.
}
induction delta.
{ rewrite addn0; move => /andP [GE0 LT0].
by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
}
{ move => /andP [GT LT].
specialize (UNIT (x1 + delta)); rewrite leq_eqVlt in UNIT.
have LE: y <= f (x1 + delta).
{ move: UNIT => /orP [/eqP EQ | UNIT]; first by rewrite !addn1 in EQ; rewrite addnS EQ ltnS in LT.
rewrite [X in _ < X]addn1 ltnS in UNIT.
apply: (leq_trans _ UNIT).
by rewrite addn1 -addnS ltnW.
} clear UNIT LT.
rewrite leq_eqVlt in LE.
move: LE => /orP [/eqP EQy | LT].
{ exists (x1 + delta); split; last by rewrite EQy.
by apply/andP; split; [apply leq_addr | rewrite addnS].
}
induction delta.
{ rewrite addn0; move => /andP [GE0 LT0].
by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
}
{ move => /andP [GT LT].
specialize (STEP (x1 + delta)); rewrite leq_eqVlt in STEP.
have LE: y <= f (x1 + delta).
{ move: STEP => /orP [/eqP EQ | STEP];
first by rewrite !addn1 in EQ; rewrite addnS EQ ltnS in LT.
rewrite [X in _ < X]addn1 ltnS in STEP.
apply: (leq_trans _ STEP).
by rewrite addn1 -addnS ltnW.
} clear STEP LT.
rewrite leq_eqVlt in LE.
move: LE => /orP [/eqP EQy | LT].
{ exists (x1 + delta); split; last by rewrite EQy.
by apply/andP; split; [apply leq_addr | rewrite addnS].
}
{ feed (IHdelta); first by apply/andP; split.
move: IHdelta => [x_mid [/andP [GE0 LT0] EQ0]].
exists x_mid; split; last by done.
apply/andP; split; first by done.
by apply: (leq_trans LT0); rewrite addnS.
}
}
Qed.
End ExistsIntermediateValue.
{ feed (IHdelta); first by apply/andP; split.
move: IHdelta => [x_mid [/andP [GE0 LT0] EQ0]].
exists x_mid; split; last by done.
apply/andP; split; first by done.
by apply: (leq_trans LT0); rewrite addnS.
}
}
Qed.
End Lemmas.
End ExistsIntermediateValue.
(* In this section, we prove an analogue of the intermediate
value theorem, but for predicates of natural numbers. *)
(** In this section, we, again, prove an analogue of the
intermediate value theorem, but for predicates over natural
numbers. *)
Section ExistsIntermediateValuePredicates.
(* Let [P] be any predicate on natural numbers. *)
(** Let [P] be any predicate on natural numbers. *)
Variable P : nat -> bool.
(* Consider a time interval [t1,t2] such that ... *)
(** Consider a time interval <<[t1,t2]>> such that ... *)
Variables t1 t2 : nat.
Hypothesis H_t1_le_t2 : t1 <= t2.
(* ... [P] doesn't hold for [t1] ... *)
(** ... [P] doesn't hold for [t1] ... *)
Hypothesis H_not_P_at_t1 : ~~ P t1.
(* ... but holds for [t2]. *)
(** ... but holds for [t2]. *)
Hypothesis H_P_at_t2 : P t2.
(* Then we prove that within time interval [t1,t2] there exists time
instant [t] such that [t] is the first time instant when [P] holds. *)
(** Then we prove that within time interval <<[t1,t2]>> there exists
time instant [t] such that [t] is the first time instant when
[P] holds. *)
Lemma exists_first_intermediate_point :
exists t, (t1 < t <= t2) /\ (forall x, t1 <= x < t -> ~~ P x) /\ P t.
Proof.
......@@ -122,6 +113,6 @@ Section StepFunction.
by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
Qed.
End ExistsIntermediateValuePredicates.
End ExistsIntermediateValuePredicates.
End StepFunction.
End Lemmas.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment