From 3743b14e75f156dc9901ff0c6d459cd54fd600cb Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <f20171026@goa.bits-pilani.ac.in>
Date: Tue, 23 Nov 2021 15:28:33 +0000
Subject: [PATCH] add rewriting lemma on the workload of "all other jobs"
---
analysis/facts/model/workload.v | 31 ++++++++++++++++++++++++++++++-
1 file changed, 30 insertions(+), 1 deletion(-)
diff --git a/analysis/facts/model/workload.v b/analysis/facts/model/workload.v
index 1959eee73..667e3bbbd 100644
--- a/analysis/facts/model/workload.v
+++ b/analysis/facts/model/workload.v
@@ -34,4 +34,33 @@ Section WorkloadFacts.
by rewrite (arrivals_between_cat _ _ t) // big_cat.
Qed.
-End WorkloadFacts.
\ No newline at end of file
+ (** Consider a job [j] ... *)
+ Variable j : Job.
+
+ (** ... and a duplicate-free sequence of jobs [jobs]. *)
+ Variable jobs : seq Job.
+ Hypothesis H_jobs_uniq : uniq jobs.
+
+ (** Further, assume that [j] is contained in [jobs]. *)
+ Hypothesis H_j_in_jobs : j \in jobs.
+
+ (** To help with rewriting, we prove that the workload of [jobs]
+ minus the job cost of [j] is equal to the workload of all jobs
+ except [j]. To define the workload of all jobs, since
+ [workload_of_jobs] expects a predicate, we use [predT], which
+ is the always-true predicate. *)
+ Lemma workload_minus_job_cost :
+ workload_of_jobs (fun jhp : Job => jhp != j) jobs =
+ workload_of_jobs predT jobs - job_cost j.
+ Proof.
+ rewrite /workload_of_jobs (big_rem j) //= eq_refl //= add0n.
+ rewrite [in RHS](big_rem j) //= addnC -subnBA //= subnn subn0.
+ rewrite [in LHS]big_seq_cond [in RHS]big_seq_cond.
+ apply eq_bigl => j'.
+ rewrite Bool.andb_true_r.
+ destruct (j' \in rem (T:=Job) j jobs) eqn:INjobs; last by done.
+ apply /negP => /eqP EQUAL.
+ by rewrite EQUAL mem_rem_uniqF in INjobs.
+ Qed.
+
+End WorkloadFacts.
--
GitLab