From 58d8d0ab91e61ad59bdb3bfe960a2647d0484615 Mon Sep 17 00:00:00 2001
From: Sergey Bozhko <sbozhko@sws-mpi.org>
Date: Thu, 20 Sep 2018 22:34:10 +0200
Subject: [PATCH] Add lemmas about arrivals_between
---
model/arrival/basic/arrival_sequence.v | 33 +++++++++-----------------
model/arrival/basic/task_arrival.v | 22 +++++++++++++++--
2 files changed, 31 insertions(+), 24 deletions(-)
diff --git a/model/arrival/basic/arrival_sequence.v b/model/arrival/basic/arrival_sequence.v
index cc12c8599..78e67106d 100644
--- a/model/arrival/basic/arrival_sequence.v
+++ b/model/arrival/basic/arrival_sequence.v
@@ -110,6 +110,16 @@ Module ArrivalSequence.
(* First, we show that the set of arriving jobs can be split
into disjoint intervals. *)
+ Lemma job_arrived_between_cat:
+ forall t1 t t2,
+ t1 <= t ->
+ t <= t2 ->
+ jobs_arrived_between t1 t2 = jobs_arrived_between t1 t ++ jobs_arrived_between t t2.
+ Proof.
+ unfold jobs_arrived_between; intros t1 t t2 GE LE.
+ by rewrite (@big_cat_nat _ _ _ t).
+ Qed.
+
Lemma jobs_arrived_between_mem_cat:
forall j t1 t t2,
t1 <= t ->
@@ -117,28 +127,7 @@ Module ArrivalSequence.
j \in jobs_arrived_between t1 t2 =
(j \in jobs_arrived_between t1 t ++ jobs_arrived_between t t2).
Proof.
- unfold jobs_arrived_between; intros j t1 t t2 GE LE.
- apply/idP/idP.
- {
- intros IN.
- apply mem_bigcat_nat_exists in IN; move: IN => [arr [IN /andP [GE1 LT2]]].
- rewrite mem_cat; apply/orP.
- by destruct (ltnP arr t); [left | right];
- apply mem_bigcat_nat with (j := arr); try (by apply/andP; split).
- }
- {
- rewrite mem_cat; move => /orP [LEFT | RIGHT].
- {
- apply mem_bigcat_nat_exists in LEFT; move: LEFT => [t0 [IN0 /andP [GE0 LT0]]].
- apply mem_bigcat_nat with (j := t0); last by done.
- by rewrite GE0 /=; apply: (leq_trans LT0).
- }
- {
- apply mem_bigcat_nat_exists in RIGHT; move: RIGHT => [t0 [IN0 /andP [GE0 LT0]]].
- apply mem_bigcat_nat with (j := t0); last by done.
- by rewrite LT0 andbT; apply: (leq_trans _ GE0).
- }
- }
+ by intros j t1 t t2 GE LE; rewrite (job_arrived_between_cat _ t).
Qed.
Lemma jobs_arrived_between_sub:
diff --git a/model/arrival/basic/task_arrival.v b/model/arrival/basic/task_arrival.v
index d9cb85399..a68188634 100644
--- a/model/arrival/basic/task_arrival.v
+++ b/model/arrival/basic/task_arrival.v
@@ -1,6 +1,6 @@
Require Import rt.util.all.
Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.job.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path bigop.
(* Properties of job arrival. *)
Module TaskArrival.
@@ -59,6 +59,24 @@ Module TaskArrival.
Definition num_arrivals_of_task (t1 t2: time) :=
size (arrivals_of_task_between t1 t2).
+ (* In this section we prove some basic lemmas about number of arrivals of task. *)
+ Section Lemmas.
+
+ (* We show that the number of arrivals of task can be split into disjoint intervals. *)
+ Lemma num_arrivals_of_task_cat:
+ forall t t1 t2,
+ t1 <= t <= t2 ->
+ num_arrivals_of_task t1 t2 = num_arrivals_of_task t1 t + num_arrivals_of_task t t2.
+ Proof.
+ move => t t1 t2 /andP [GE LE].
+ rewrite /num_arrivals_of_task /arrivals_of_task_between
+ /arrivals_between /jobs_arrived_between.
+ rewrite (@big_cat_nat _ _ _ t) //=.
+ by rewrite filter_cat size_cat.
+ Qed.
+
+ End Lemmas.
+
End NumberOfArrivals.
(* In this section, we prove some basic results regarding the
@@ -72,7 +90,7 @@ Module TaskArrival.
Variable job_arrival: Job -> time.
Variable job_task: Job -> Task.
- (* Consider any arrival sequence with consistent, duplicate-free arrivals, ... *)
+ (* Consider any arrival sequence with consistent, non-duplicate arrivals, ... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_consistent_arrivals: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
--
GitLab