From 9227bdb40408ded5514c98e408695404b982f237 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Tue, 2 Nov 2021 10:57:48 +0100
Subject: [PATCH] clean up in util/unit_growth.v * rename [step_function] to
[unit_growth] * restructure file
---
analysis/facts/behavior/service.v | 16 +--
classic/model/schedule/uni/schedule.v | 16 +--
.../model/schedule/uni/susp/last_execution.v | 4 +-
classic/util/step_function.v | 2 +-
util/all.v | 2 +-
util/step_function.v | 127 ------------------
util/unit_growth.v | 118 ++++++++++++++++
7 files changed, 138 insertions(+), 147 deletions(-)
delete mode 100644 util/step_function.v
create mode 100644 util/unit_growth.v
diff --git a/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
index 8afab05fe..c09e5f98e 100644
--- a/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -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. *)
diff --git a/classic/model/schedule/uni/schedule.v b/classic/model/schedule/uni/schedule.v
index f225f802a..6966f04c0 100644
--- a/classic/model/schedule/uni/schedule.v
+++ b/classic/model/schedule/uni/schedule.v
@@ -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.
diff --git a/classic/model/schedule/uni/susp/last_execution.v b/classic/model/schedule/uni/susp/last_execution.v
index 5a2458fd6..1cb8db6dc 100644
--- a/classic/model/schedule/uni/susp/last_execution.v
+++ b/classic/model/schedule/uni/susp/last_execution.v
@@ -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.
diff --git a/classic/util/step_function.v b/classic/util/step_function.v
index 4a567bdaa..a34d56f34 100644
--- a/classic/util/step_function.v
+++ b/classic/util/step_function.v
@@ -1,4 +1,4 @@
-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.
diff --git a/util/all.v b/util/all.v
index 2b76862d0..7d5fd95d0 100644
--- a/util/all.v
+++ b/util/all.v
@@ -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.
diff --git a/util/step_function.v b/util/step_function.v
deleted file mode 100644
index 9d02d75a7..000000000
--- a/util/step_function.v
+++ /dev/null
@@ -1,127 +0,0 @@
-Require Import prosa.util.tactics prosa.util.notation.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
-
-Section StepFunction.
-
- Section Defs.
-
- (* We say that a function [f]... *)
- Variable f : nat -> nat.
-
- (* ...is a step function iff the following holds. *)
- Definition is_step_function :=
- forall t, f (t + 1) <= f t + 1.
-
- End Defs.
-
- Section Lemmas.
-
- (* 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.
- 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 (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.
-
- End Lemmas.
-
- (* In this section, we prove an analogue of the intermediate
- value theorem, but for predicates of natural numbers. *)
- Section ExistsIntermediateValuePredicates.
-
- (* Let [P] be any predicate on natural numbers. *)
- Variable P : nat -> bool.
-
- (* 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] ... *)
- Hypothesis H_not_P_at_t1 : ~~ P t1.
-
- (* ... 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. *)
- Lemma exists_first_intermediate_point :
- exists t, (t1 < t <= t2) /\ (forall x, t1 <= x < t -> ~~ P x) /\ P t.
- Proof.
- have EX: exists x, P x && (t1 < x <= t2).
- { exists t2.
- apply/andP; split; first by done.
- apply/andP; split; last by done.
- move: H_t1_le_t2; rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
- by exfalso; subst t2; move: H_not_P_at_t1 => /negP NPt1.
- }
- have MIN := ex_minnP EX.
- move: MIN => [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.
- exists x; repeat split; [ apply/andP; split | | ]; try done.
- move => y /andP [NEQ1 NEQ2]; apply/negPn; intros Py.
- feed (MIN y).
- { apply/andP; split; first by done.
- apply/andP; split.
- - move: NEQ1. rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
- by exfalso; subst y; move: H_not_P_at_t1 => /negP NPt1.
- - by apply ltnW, leq_trans with x.
- }
- by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
- Qed.
-
- End ExistsIntermediateValuePredicates.
-
-End StepFunction.
diff --git a/util/unit_growth.v b/util/unit_growth.v
new file mode 100644
index 000000000..d29f82ac1
--- /dev/null
+++ b/util/unit_growth.v
@@ -0,0 +1,118 @@
+Require Import prosa.util.tactics prosa.util.notation.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
+
+(** 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.
+
+(** In this section, we prove a few useful lemmas about unit growth functions. *)
+Section Lemmas.
+
+ (** Let [f] be any unit growth function over natural numbers. *)
+ Variable f : nat -> nat.
+ Hypothesis H_unit_growth_function : unit_growth_function f.
+
+ (** In the following 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_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].
+ }
+ { 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.
+
+ (** 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. *)
+ Variable P : nat -> bool.
+
+ (** 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] ... *)
+ Hypothesis H_not_P_at_t1 : ~~ P t1.
+
+ (** ... 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. *)
+ Lemma exists_first_intermediate_point :
+ exists t, (t1 < t <= t2) /\ (forall x, t1 <= x < t -> ~~ P x) /\ P t.
+ Proof.
+ have EX: exists x, P x && (t1 < x <= t2).
+ { exists t2.
+ apply/andP; split; first by done.
+ apply/andP; split; last by done.
+ move: H_t1_le_t2; rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
+ by exfalso; subst t2; move: H_not_P_at_t1 => /negP NPt1.
+ }
+ have MIN := ex_minnP EX.
+ move: MIN => [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.
+ exists x; repeat split; [ apply/andP; split | | ]; try done.
+ move => y /andP [NEQ1 NEQ2]; apply/negPn; intros Py.
+ feed (MIN y).
+ { apply/andP; split; first by done.
+ apply/andP; split.
+ - move: NEQ1. rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
+ by exfalso; subst y; move: H_not_P_at_t1 => /negP NPt1.
+ - by apply ltnW, leq_trans with x.
+ }
+ by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
+ Qed.
+
+ End ExistsIntermediateValuePredicates.
+
+End Lemmas.
--
GitLab