From af370ec8ff6756ca1bd5f003db4cc9841878da9d Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Tue, 26 Jul 2016 17:00:13 +0200
Subject: [PATCH] Simplify definition of the JobIn type
---
implementation/apa/arrival_sequence.v | 2 +-
implementation/basic/arrival_sequence.v | 2 +-
implementation/jitter/arrival_sequence.v | 2 +-
model/basic/arrival_sequence.v | 33 ++++++++--------
model/basic/jobin_eqdec.v | 49 ++++++++++++------------
5 files changed, 42 insertions(+), 46 deletions(-)
diff --git a/implementation/apa/arrival_sequence.v b/implementation/apa/arrival_sequence.v
index 21adb133c..ef341ef73 100644
--- a/implementation/apa/arrival_sequence.v
+++ b/implementation/apa/arrival_sequence.v
@@ -42,7 +42,7 @@ Module ConcreteArrivalSequence.
(* ... every job comes from the task set, ... *)
Theorem periodic_arrivals_all_jobs_from_taskset:
forall (j: JobIn arr_seq),
- job_task (_job_in arr_seq j) \in ts. (* TODO: fix coercion. *)
+ job_task (job_of_job_in j) \in ts. (* TODO: fix coercion. *)
Proof.
intros j.
destruct j as [j arr ARRj]; simpl.
diff --git a/implementation/basic/arrival_sequence.v b/implementation/basic/arrival_sequence.v
index 17920ae1e..8e17a0d7c 100644
--- a/implementation/basic/arrival_sequence.v
+++ b/implementation/basic/arrival_sequence.v
@@ -38,7 +38,7 @@ Module ConcreteArrivalSequence.
(* ... every job comes from the task set, ... *)
Theorem periodic_arrivals_all_jobs_from_taskset:
forall (j: JobIn arr_seq),
- job_task (_job_in arr_seq j) \in ts. (* TODO: fix coercion. *)
+ job_task (job_of_job_in j) \in ts. (* TODO: fix coercion. *)
Proof.
intros j.
destruct j as [j arr ARRj]; simpl.
diff --git a/implementation/jitter/arrival_sequence.v b/implementation/jitter/arrival_sequence.v
index b8b7f4e35..4fb3a3c96 100644
--- a/implementation/jitter/arrival_sequence.v
+++ b/implementation/jitter/arrival_sequence.v
@@ -38,7 +38,7 @@ Module ConcreteArrivalSequence.
(* ... every job comes from the task set, ... *)
Theorem periodic_arrivals_all_jobs_from_taskset:
forall (j: JobIn arr_seq),
- job_task (_job_in arr_seq j) \in ts. (* TODO: fix coercion *)
+ job_task (job_of_job_in j) \in ts. (* TODO: fix coercion *)
Proof.
intros j.
destruct j as [j arr ARRj]; simpl.
diff --git a/model/basic/arrival_sequence.v b/model/basic/arrival_sequence.v
index d84e7664d..dcb43d387 100644
--- a/model/basic/arrival_sequence.v
+++ b/model/basic/arrival_sequence.v
@@ -1,4 +1,4 @@
-Require Import rt.util.all rt.model.basic.job rt.model.basic.task rt.model.basic.time.
+Require Import rt.util.all rt.model.basic.task rt.model.basic.time.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(* Definitions and properties of job arrival sequences. *)
@@ -24,26 +24,23 @@ Module ArrivalSequence.
Context {Job: eqType}.
- (* Whether a job arrives in a particular sequence at time t *)
+ (* First we define whether a job arrives in a particular sequence at time t. *)
Definition arrives_at (j: Job) (arr_seq: arrival_sequence Job) (t: time) :=
j \in arr_seq t.
- (* A job j of type (JobIn arr_seq) is a job that arrives at some particular
- time in arr_seq. It holds the arrival time and a proof of arrival. *)
- Record JobIn (arr_seq: arrival_sequence Job) : Type :=
- {
- _job_in: Job;
- _arrival_time: time; (* arrival time *)
- _: arrives_at _job_in arr_seq _arrival_time (* proof of arrival *)
- }.
+ (* Next, we define the type (JobIn arr_seq) to represent a job that belongs to arr_seq.
+ (Note: The notation might seem complicated, but it just means that the type JobIn is
+ constructed using a Job j, a time t, and a proof of arrival. *)
+ Inductive JobIn (arr_seq: arrival_sequence Job) :=
+ Build_JobIn j t of (arrives_at j arr_seq t).
- (* Define a coercion that states that every JobIn is a Job. *)
- Coercion JobIn_is_Job {arr_seq: arrival_sequence Job} (j: JobIn arr_seq) :=
- _job_in arr_seq j.
+ (* Next, we define a coercion that returns the Job contained in the type JobIn. *)
+ Coercion job_of_job_in {arr_seq} (j: JobIn arr_seq) : Job :=
+ let: Build_JobIn actual_job _ _ := j in actual_job.
- (* Define job arrival time as that time that the job arrives (only works for JobIn). *)
+ (* Similarly, we define a function that returns the arrival time of the job. *)
Definition job_arrival {arr_seq: arrival_sequence Job} (j: JobIn arr_seq) :=
- _arrival_time arr_seq j.
+ let: Build_JobIn _ arr _ := j in arr.
(* Finally, we define a decidable equality for JobIn, in order to make
it compatible with ssreflect (see jobin_eqdec.v). *)
@@ -56,7 +53,7 @@ Module ArrivalSequence.
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
-
+
(* The same job j cannot arrive at two different times. *)
Definition no_multiple_arrivals :=
forall (j: Job) t1 t2,
@@ -113,7 +110,7 @@ Module ArrivalSequence.
(* There's an inverse function for recovering the original Job from JobIn. *)
Lemma is_JobIn_inverse :
forall t,
- ocancel (is_JobIn t) (_job_in arr_seq).
+ ocancel (is_JobIn t) job_of_job_in.
Proof.
by intros t; red; intros x; unfold is_JobIn; des_eqrefl.
Qed.
@@ -157,7 +154,7 @@ Module ArrivalSequence.
apply bigcat_ord_uniq.
{
intros i; unfold jobs_arriving_at.
- apply pmap_uniq with (g := (_job_in arr_seq)); first by apply is_JobIn_inverse.
+ apply pmap_uniq with (g := job_of_job_in); first by apply is_JobIn_inverse.
by apply SET.
}
{
diff --git a/model/basic/jobin_eqdec.v b/model/basic/jobin_eqdec.v
index 0d78e334f..7b36dda60 100644
--- a/model/basic/jobin_eqdec.v
+++ b/model/basic/jobin_eqdec.v
@@ -1,30 +1,29 @@
(* The decidable equality for JobIn checks whether the Job
and the arrival times are the same. *)
-Definition jobin_eqdef (arr_seq: arrival_sequence Job) :=
- (fun j1 j2: JobIn arr_seq =>
- (_job_in arr_seq j1 == _job_in arr_seq j2) &&
- (_arrival_time arr_seq j1 == _arrival_time arr_seq j2)).
- Lemma eqn_jobin : forall arr_seq, Equality.axiom (jobin_eqdef arr_seq).
- Proof.
- unfold Equality.axiom; intros arr_seq x y.
- destruct (jobin_eqdef arr_seq x y) eqn:EQ.
- {
- apply ReflectT.
- unfold jobin_eqdef in *.
- move: EQ => /andP [/eqP EQjob /eqP EQarr].
- destruct x, y; ins; subst.
- f_equal; apply bool_irrelevance.
- }
- {
- apply ReflectF.
- unfold jobin_eqdef, not in *; intro BUG.
- apply negbT in EQ; rewrite negb_and in EQ.
- destruct x, y.
- move: EQ => /orP [/negP DIFFjob | /negP DIFFarr].
- by apply DIFFjob; inversion BUG; subst; apply/eqP.
- by apply DIFFarr; inversion BUG; subst; apply/eqP.
- }
- Qed.
+Definition jobin_eqdef arr_seq (j1 j2: JobIn arr_seq) :=
+ (job_of_job_in j1 == job_of_job_in j2) && (job_arrival j1 == job_arrival j2).
+
+Lemma eqn_jobin : forall arr_seq, Equality.axiom (jobin_eqdef arr_seq).
+Proof.
+ unfold Equality.axiom; intros arr_seq x y.
+ destruct (jobin_eqdef arr_seq x y) eqn:EQ.
+ {
+ apply ReflectT.
+ unfold jobin_eqdef in *.
+ move: EQ => /andP [/eqP EQjob /eqP EQarr].
+ destruct x, y; ins; subst.
+ f_equal; apply bool_irrelevance.
+ }
+ {
+ apply ReflectF.
+ unfold jobin_eqdef, not in *; intro BUG.
+ apply negbT in EQ; rewrite negb_and in EQ.
+ destruct x, y.
+ move: EQ => /orP [/negP DIFFjob | /negP DIFFarr].
+ by apply DIFFjob; inversion BUG; subst; apply/eqP.
+ by apply DIFFarr; inversion BUG; subst; apply/eqP.
+ }
+Qed.
Canonical jobin_eqMixin arr_seq := EqMixin (eqn_jobin arr_seq).
Canonical jobin_eqType arr_seq := Eval hnf in EqType (JobIn arr_seq) (jobin_eqMixin arr_seq).
\ No newline at end of file
--
GitLab