diff git a/analysis/definitions/busy_interval.v b/analysis/definitions/busy_interval.v
index 9031e12579ac9e3f2ec1aa70a7f3ce605a78923a..87c413a2b219e91c2f25cde31f73288246f0ccb1 100644
 a/analysis/definitions/busy_interval.v
+++ b/analysis/definitions/busy_interval.v
@@ 59,11 +59,11 @@ Section BusyIntervalJLFP.
End BusyInterval.
(** In this section we define the computational
 version of the notion of quiet time. *)
+ version of the notion of quiet time. *)
Section DecidableQuietTime.
(** We say that t is a quiet time for j iff every higherpriority job from
 the arrival sequence that arrived before t has completed by that time. *)
+ the arrival sequence that arrived before t has completed by that time. *)
Definition quiet_time_dec (j : Job) (t : instant) :=
all
(fun j_hp => hep_job j_hp j ==> (completed_by sched j_hp t))
diff git a/analysis/definitions/job_properties.v b/analysis/definitions/job_properties.v
index 3a0ee27759cf9ce036ccc32ea7225d66dbe7d766..78443d3efde7ec863779d8f556b85dc69ce9ef42 100644
 a/analysis/definitions/job_properties.v
+++ b/analysis/definitions/job_properties.v
@@ 1,5 +1,4 @@
Require Export prosa.behavior.all.
From mathcomp Require Export eqtype ssrnat.
(** In this section, we introduce properties of a job. *)
Section PropertiesOfJob.
diff git a/analysis/definitions/priority_inversion.v b/analysis/definitions/priority_inversion.v
index 21d93352591f2d32822b488ff7404b2764fae844..073333a9d885067c340163657cbf1a21d1050a71 100644
 a/analysis/definitions/priority_inversion.v
+++ b/analysis/definitions/priority_inversion.v
@@ 1,7 +1,5 @@
Require Export prosa.analysis.definitions.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(** * Cumulative Priority Inversion for JLFPmodels *)
(** In this module we define the notion of cumulative priority inversion for uniprocessor for JLFP schedulers. *)
Section CumulativePriorityInversion.
diff git a/analysis/definitions/progress.v b/analysis/definitions/progress.v
index ec8d847d7fac12d2bb025aa3611134595306ed14..ce5480af5b8d2d2f1fb4d51fd29dc38244ffdd21 100644
 a/analysis/definitions/progress.v
+++ b/analysis/definitions/progress.v
@@ 6,6 +6,7 @@ Require Export prosa.analysis.facts.behavior.service.
conversely a notion of a lack of progress. *)
Section Progress.
+
(** Consider any type of jobs with a known cost... *)
Context {Job : JobType}.
Context `{JobCost Job}.
diff git a/analysis/definitions/request_bound_function.v b/analysis/definitions/request_bound_function.v
index 4d8d877b15932d8c912b42c73ade3b4deac3195a..009cdb7c24d87906947761307e10e416e2da113f 100644
 a/analysis/definitions/request_bound_function.v
+++ b/analysis/definitions/request_bound_function.v
@@ 6,8 +6,6 @@ Require Export prosa.model.priority.classes.
could be generalized in future work. *)
Require Import prosa.analysis.facts.model.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

(** * Request Bound Function (RBF) *)
(** We define the notion of a task's requestbound function (RBF), as well as
@@ 47,7 +45,8 @@ Section TaskWorkloadBoundedByArrivalCurves.
Variable delta : duration.
(** We define the following workload bound for the task. *)
 Definition task_request_bound_function := task_cost tsk * max_arrivals tsk delta.
+ Definition task_request_bound_function :=
+ task_cost tsk * max_arrivals tsk delta.
End SingleTask.
diff git a/analysis/definitions/schedulability.v b/analysis/definitions/schedulability.v
index e879d848e93758dc2430a915ea717c20ef7a7b06..fb0a2874348c4ea25b769b31002478b6f648b085 100644
 a/analysis/definitions/schedulability.v
+++ b/analysis/definitions/schedulability.v
@@ 1,13 +1,23 @@
Require Export prosa.analysis.facts.behavior.completion.
Require Import prosa.model.task.absolute_deadline.
+(** * Schedulability *)
+
+(** In the following section we define the notion of schedulable
+ task. *)
Section Task.
+
+ (** Consider any type of tasks, ... *)
Context {Task : TaskType}.
 Context {Job: JobType}.
 Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
+ (** ... any type of jobs associated with these tasks, ... *)
+ Context {Job: JobType}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
Context `{JobDeadline Job}.
+ Context `{JobTask Job Task}.
+ (** ... and any kind of processor state. *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
@@ 37,43 +47,27 @@ Section Task.
arrives_in arr_seq j >
job_task j = tsk >
job_meets_deadline sched j.
+
End Task.
Section TaskSet.
 Context {Task : TaskType}.
 Context {Job: JobType}.

 Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
 Context `{JobDeadline Job}.

 Context {PState : Type}.
 Context `{ProcessorState Job PState}.

 Variable ts : {set Task}.

 (** Consider any job arrival sequence... *)
 Variable arr_seq: arrival_sequence Job.

 (** ...and any schedule of these jobs. *)
 Variable sched: schedule PState.

 (** We say that a task set is schedulable if all its tasks are schedulable *)
 Definition schedulable_taskset :=
 forall tsk, tsk \in ts > schedulable_task arr_seq sched tsk.
End TaskSet.

Section Schedulability.
 (** We can infer schedulability from a responsetime bound of a task. *)
+(** In this section we infer schedulability from a responsetime bound
+ of a task. *)
+Section Schedulability.
+ (** Consider any type of tasks, ... *)
Context {Task : TaskType}.
 Context {Job: JobType}.

Context `{TaskDeadline Task}.
 Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
+ (** ... any type of jobs associated with these tasks, ... *)
+ Context {Job: JobType}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+ Context `{JobTask Job Task}.
+
+ (** ... and any kind of processor state. *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.

+
(** Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
@@ 112,9 +106,12 @@ End Schedulability.
given schedule and one w.r.t. all jobs that arrive in a given
arrival sequence. *)
Section AllDeadlinesMet.

+
(** Consider any given type of jobs... *)
 Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
+ Context {Job : JobType}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+ Context `{JobDeadline Job}.
(** ... any given type of processor states. *)
Context {PState: eqType}.
@@ 151,8 +148,8 @@ Section AllDeadlinesMet.
End DeadlinesOfArrivals.
(** We observe that the latter definition, assuming a schedule in
 which all jobs come from the arrival sequence, implies the former
 definition. *)
+ which all jobs come from the arrival sequence, implies the
+ former definition. *)
Lemma all_deadlines_met_in_valid_schedule:
forall arr_seq sched,
jobs_come_from_arrival_sequence sched arr_seq >
diff git a/analysis/definitions/task_schedule.v b/analysis/definitions/task_schedule.v
index 351412278b25875329d557007d9fcbb6e317cdc6..f69f2ca2d7d9d7482e5fb5fc3a20efbc2426759d 100644
 a/analysis/definitions/task_schedule.v
+++ b/analysis/definitions/task_schedule.v
@@ 1,9 +1,10 @@
Require Export prosa.model.task.concept.
Require Export prosa.model.processor.ideal.
(** Due to historical reasons this file defines the notion of a schedule of
 a task for the ideal uniprocessor model. This is not a fundamental limitation
 and the notion can be further generalized to an arbitrary model. *)
+(** Due to historical reasons this file defines the notion of a
+ schedule of a task for the ideal uniprocessor model. This is not
+ a fundamental limitation and the notion can be further generalized
+ to an arbitrary model. *)
+Require Export prosa.model.processor.ideal.
(** * Schedule of task *)
(** In this section we define properties of schedule of a task *)
@@ 22,29 +23,25 @@ Section ScheduleOfTask.
(** Let [sched] be any ideal uniprocessor schedule. *)
Variable sched : schedule (ideal.processor_state Job).
 Section TaskProperties.

 (** Let [tsk] be any task. *)
 Variable tsk : Task.

 (** Next we define whether a task is scheduled at time [t], ... *)
 Definition task_scheduled_at (t : instant) :=
 if sched t is Some j then
 job_task j == tsk
 else false.
+ (** Let [tsk] be any task. *)
+ Variable tsk : Task.
+
+ (** Next we define whether a task is scheduled at time [t], ... *)
+ Definition task_scheduled_at (t : instant) :=
+ if sched t is Some j then
+ job_task j == tsk
+ else false.
 (** ...which also corresponds to the instantaneous service it receives. *)
 Definition task_service_at (t : instant) := task_scheduled_at t.
+ (** ...which also corresponds to the instantaneous service it receives. *)
+ Definition task_service_at (t : instant) := task_scheduled_at t.
 (** Based on the notion of instantaneous service, we define the
+ (** Based on the notion of instantaneous service, we define the
cumulative service received by [tsk] during any interval [t1, t2)... *)
 Definition task_service_during (t1 t2 : instant) :=
 \sum_(t1 <= t < t2) task_service_at t.
+ Definition task_service_during (t1 t2 : instant) :=
+ \sum_(t1 <= t < t2) task_service_at t.
 (** ...and the cumulative service received by [tsk] up to time t2,
+ (** ...and the cumulative service received by [tsk] up to time t2,
i.e., in the interval [0, t2). *)
 Definition task_service (t2 : instant) := task_service_during 0 t2.

 End TaskProperties.
+ Definition task_service (t2 : instant) := task_service_during 0 t2.
End ScheduleOfTask.
diff git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 5703fedef30e6937d66690489db6f107c19bdbbf..06fda1968e227ba16f91457c643af7d981e94176 100644
 a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ 1,6 +1,8 @@
Require Export prosa.behavior.all.
Require Export prosa.util.all.
+(** * Arrival Sequence *)
+
(** In this section, we relate job readiness to [has_arrived]. *)
Section Arrived.
@@ 11,8 +13,8 @@ Section Arrived.
(** Consider any schedule... *)
Variable sched : schedule PState.
 (** ...and suppose that jobs have a cost, an arrival time, and a notion of
 readiness. *)
+ (** ...and suppose that jobs have a cost, an arrival time, and a
+ notion of readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context `{JobReady Job PState}.
@@ 61,144 +63,140 @@ Section ArrivalSequencePrefix.
(** Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
 (** In this section, we prove some lemmas about arrival sequence prefixes. *)
 Section Lemmas.

 (** We begin with basic lemmas for manipulating the sequences. *)
 Section Composition.
+ (** We begin with basic lemmas for manipulating the sequences. *)
+ Section Composition.
 (** First, we show that the set of arriving jobs can be split
+ (** First, we show that the set of arriving jobs can be split
into disjoint intervals. *)
 Lemma arrivals_between_cat:
 forall t1 t t2,
 t1 <= t >
 t <= t2 >
 arrivals_between arr_seq t1 t2 = arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
 Proof.
 unfold arrivals_between; intros t1 t t2 GE LE.
 by rewrite (@big_cat_nat _ _ _ t).
 Qed.

 (** Second, the same observation applies to membership in the set of
+ Lemma arrivals_between_cat:
+ forall t1 t t2,
+ t1 <= t >
+ t <= t2 >
+ arrivals_between arr_seq t1 t2 =
+ arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
+ Proof.
+ unfold arrivals_between; intros t1 t t2 GE LE.
+ by rewrite (@big_cat_nat _ _ _ t).
+ Qed.
+
+ (** Second, the same observation applies to membership in the set of
arrived jobs. *)
 Lemma arrivals_between_mem_cat:
 forall j t1 t t2,
 t1 <= t >
 t <= t2 >
 j \in arrivals_between arr_seq t1 t2 =
 (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
 Proof.
 by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
 Qed.

 (** Third, we observe that we can grow the considered interval without
+ Lemma arrivals_between_mem_cat:
+ forall j t1 t t2,
+ t1 <= t >
+ t <= t2 >
+ j \in arrivals_between arr_seq t1 t2 =
+ (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
+ Proof.
+ by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
+ Qed.
+
+ (** Third, we observe that we can grow the considered interval without
"losing" any arrived jobs, i.e., membership in the set of arrived jobs
is monotonic. *)
 Lemma arrivals_between_sub:
 forall j t1 t1' t2 t2',
 t1' <= t1 >
 t2 <= t2' >
 j \in arrivals_between arr_seq t1 t2 >
 j \in arrivals_between arr_seq t1' t2'.
 Proof.
 intros j t1 t1' t2 t2' GE1 LE2 IN.
 move: (leq_total t1 t2) => /orP [BEFORE  AFTER];
 last by rewrite /arrivals_between big_geq // in IN.
 rewrite /arrivals_between.
 rewrite > big_cat_nat with (n := t1); [simpl  by done  by apply: (leq_trans BEFORE)].
 rewrite mem_cat; apply/orP; right.
 rewrite > big_cat_nat with (n := t2); [simpl  by done  by done].
 by rewrite mem_cat; apply/orP; left.
 Qed.

 End Composition.

 (** Next, we relate the arrival prefixes with job arrival times. *)
 Section ArrivalTimes.

 (** Assume that job arrival times are consistent. *)
 Hypothesis H_consistent_arrival_times:
 consistent_arrival_times arr_seq.

 (** First, we prove that if a job belongs to the prefix
+ Lemma arrivals_between_sub:
+ forall j t1 t1' t2 t2',
+ t1' <= t1 >
+ t2 <= t2' >
+ j \in arrivals_between arr_seq t1 t2 >
+ j \in arrivals_between arr_seq t1' t2'.
+ Proof.
+ intros j t1 t1' t2 t2' GE1 LE2 IN.
+ move: (leq_total t1 t2) => /orP [BEFORE  AFTER];
+ last by rewrite /arrivals_between big_geq // in IN.
+ rewrite /arrivals_between.
+ rewrite > big_cat_nat with (n := t1); [simpl  by done  by apply: (leq_trans BEFORE)].
+ rewrite mem_cat; apply/orP; right.
+ rewrite > big_cat_nat with (n := t2); [simpl  by done  by done].
+ by rewrite mem_cat; apply/orP; left.
+ Qed.
+
+ End Composition.
+
+ (** Next, we relate the arrival prefixes with job arrival times. *)
+ Section ArrivalTimes.
+
+ (** Assume that job arrival times are consistent. *)
+ Hypothesis H_consistent_arrival_times:
+ consistent_arrival_times arr_seq.
+
+ (** First, we prove that if a job belongs to the prefix
(jobs_arrived_before t), then it arrives in the arrival sequence. *)
 Lemma in_arrivals_implies_arrived:
 forall j t1 t2,
 j \in arrivals_between arr_seq t1 t2 >
 arrives_in arr_seq j.
 Proof.
 rename H_consistent_arrival_times into CONS.
 intros j t1 t2 IN.
 apply mem_bigcat_nat_exists in IN.
 move: IN => [arr [IN _]].
 by exists arr.
 Qed.

 (** Next, we prove that if a job belongs to the prefix
+ Lemma in_arrivals_implies_arrived:
+ forall j t1 t2,
+ j \in arrivals_between arr_seq t1 t2 >
+ arrives_in arr_seq j.
+ Proof.
+ rename H_consistent_arrival_times into CONS.
+ intros j t1 t2 IN.
+ apply mem_bigcat_nat_exists in IN.
+ move: IN => [arr [IN _]].
+ by exists arr.
+ Qed.
+
+ (** Next, we prove that if a job belongs to the prefix
(jobs_arrived_between t1 t2), then it indeed arrives between t1 and
t2. *)
 Lemma in_arrivals_implies_arrived_between:
 forall j t1 t2,
 j \in arrivals_between arr_seq t1 t2 >
 arrived_between j t1 t2.
 Proof.
 rename H_consistent_arrival_times into CONS.
 intros j t1 t2 IN.
 apply mem_bigcat_nat_exists in IN.
 move: IN => [t0 [IN /= LT]].
 by apply CONS in IN; rewrite /arrived_between IN.
 Qed.

 (** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
+ Lemma in_arrivals_implies_arrived_between:
+ forall j t1 t2,
+ j \in arrivals_between arr_seq t1 t2 >
+ arrived_between j t1 t2.
+ Proof.
+ rename H_consistent_arrival_times into CONS.
+ intros j t1 t2 IN.
+ apply mem_bigcat_nat_exists in IN.
+ move: IN => [t0 [IN /= LT]].
+ by apply CONS in IN; rewrite /arrived_between IN.
+ Qed.
+
+ (** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
then it indeed arrives before time t. *)
 Lemma in_arrivals_implies_arrived_before:
 forall j t,
 j \in arrivals_before arr_seq t >
 arrived_before j t.
 Proof.
 intros j t IN.
 have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
 by rewrite /arrived_between /=.
 Qed.

 (** Similarly, we prove that if a job from the arrival sequence arrives
+ Lemma in_arrivals_implies_arrived_before:
+ forall j t,
+ j \in arrivals_before arr_seq t >
+ arrived_before j t.
+ Proof.
+ intros j t IN.
+ have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
+ by rewrite /arrived_between /=.
+ Qed.
+
+ (** Similarly, we prove that if a job from the arrival sequence arrives
before t, then it belongs to the sequence (jobs_arrived_before t). *)
 Lemma arrived_between_implies_in_arrivals:
 forall j t1 t2,
 arrives_in arr_seq j >
 arrived_between j t1 t2 >
 j \in arrivals_between arr_seq t1 t2.
 Proof.
 rename H_consistent_arrival_times into CONS.
 move => j t1 t2 [a_j ARRj] BEFORE.
 have SAME := ARRj; apply CONS in SAME; subst a_j.
 by apply mem_bigcat_nat with (j := (job_arrival j)).
 Qed.

 (** Next, we prove that if the arrival sequence doesn't contain duplicate
+ Lemma arrived_between_implies_in_arrivals:
+ forall j t1 t2,
+ arrives_in arr_seq j >
+ arrived_between j t1 t2 >
+ j \in arrivals_between arr_seq t1 t2.
+ Proof.
+ rename H_consistent_arrival_times into CONS.
+ move => j t1 t2 [a_j ARRj] BEFORE.
+ have SAME := ARRj; apply CONS in SAME; subst a_j.
+ by apply mem_bigcat_nat with (j := (job_arrival j)).
+ Qed.
+
+ (** Next, we prove that if the arrival sequence doesn't contain duplicate
jobs, the same applies for any of its prefixes. *)
 Lemma arrivals_uniq :
 arrival_sequence_uniq arr_seq >
 forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
 Proof.
 rename H_consistent_arrival_times into CONS.
 unfold arrivals_up_to; intros SET t1 t2.
 apply bigcat_nat_uniq; first by done.
 intros x t t' IN1 IN2.
 by apply CONS in IN1; apply CONS in IN2; subst.
 Qed.

 (** Also note there can't by any arrivals in an empty time interval. *)
 Lemma arrivals_between_geq:
 forall t1 t2,
 t1 >= t2 >
 arrivals_between arr_seq t1 t2 = [::].
 Proof.
 by intros ? ? GE; rewrite /arrivals_between big_geq.
 Qed.

 End ArrivalTimes.

 End Lemmas.
+ Lemma arrivals_uniq :
+ arrival_sequence_uniq arr_seq >
+ forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
+ Proof.
+ rename H_consistent_arrival_times into CONS.
+ unfold arrivals_up_to; intros SET t1 t2.
+ apply bigcat_nat_uniq; first by done.
+ intros x t t' IN1 IN2.
+ by apply CONS in IN1; apply CONS in IN2; subst.
+ Qed.
+
+ (** Also note there can't by any arrivals in an empty time interval. *)
+ Lemma arrivals_between_geq:
+ forall t1 t2,
+ t1 >= t2 >
+ arrivals_between arr_seq t1 t2 = [::].
+ Proof.
+ by intros ? ? GE; rewrite /arrivals_between big_geq.
+ Qed.
+
+ End ArrivalTimes.
End ArrivalSequencePrefix.
\ No newline at end of file
diff git a/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v
index bc30ecc10452966e0cf7430fe497788dc5abbcdf..eb2c2a86b0fc3b8deac264675507d493469f696f 100644
 a/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ 1,9 +1,11 @@
Require Export prosa.analysis.facts.behavior.service.
Require Export prosa.analysis.facts.behavior.arrivals.
(** In this file, we establish basic facts about job completions. *)
+(** * Completion *)
+(** In this file, we establish basic facts about job completions. *)
Section CompletionFacts.
+
(** Consider any job type,...*)
Context {Job: JobType}.
Context `{JobCost Job}.
@@ 35,8 +37,7 @@ Section CompletionFacts.
Lemma less_service_than_cost_is_incomplete:
forall t,
service sched j t < job_cost j
 <>
 ~~ completed_by sched j t.
+ <> ~~ completed_by sched j t.
Proof.
move=> t. by split; rewrite /completed_by; [rewrite ltnNge //  rewrite ltnNge //].
Qed.
@@ 45,8 +46,7 @@ Section CompletionFacts.
Lemma incomplete_is_positive_remaining_cost:
forall t,
~~ completed_by sched j t
 <>
 remaining_cost sched j t > 0.
+ <> remaining_cost sched j t > 0.
Proof.
move=> t. by split; rewrite /remaining_cost less_service_than_cost_is_incomplete subn_gt0 //.
Qed.
@@ 112,11 +112,10 @@ Section CompletionFacts.
End CompletionFacts.

Section ServiceAndCompletionFacts.
 (** In this section, we establish some facts that are really about service,
 but are also related to completion and rely on some of the above lemmas.
 Hence they are in this file rather than in the service facts file. *)
+(** In this section, we establish some facts that are really about service,
+ but are also related to completion and rely on some of the above lemmas.
+ Hence they are in this file rather than in the service facts file. *)
+Section ServiceAndCompletionFacts.
(** Consider any job type,...*)
Context {Job: JobType}.
@@ 133,7 +132,7 @@ Section ServiceAndCompletionFacts.
Hypothesis H_completed_jobs:
completed_jobs_dont_execute sched.
 (** Let j be any job that is to be scheduled. *)
+ (** Let [j] be any job that is to be scheduled. *)
Variable j: Job.
(** Assume that a scheduled job receives exactly one time unit of service. *)
@@ 171,7 +170,7 @@ Section ServiceAndCompletionFacts.
by apply service_at_most_cost.
Qed.
 (** We show that the service received by job j in any interval is no larger
+ (** We show that the service received by job [j] in any interval is no larger
than its cost. *)
Lemma cumulative_service_le_job_cost:
forall t t',
@@ 183,8 +182,8 @@ Section ServiceAndCompletionFacts.
rewrite /service. rewrite (service_during_cat sched j 0 t t') // leq_addl //.
Qed.
 (** If a job isn't complete at time t, it can't be completed at time (t +
 remaining_cost j t  1). *)
+ (** If a job isn't complete at time [t], it can't be completed at time [t +
+ remaining_cost j t  1]. *)
Lemma job_doesnt_complete_before_remaining_cost:
forall t,
~~ completed_by sched j t >
@@ 227,9 +226,9 @@ Section ServiceAndCompletionFacts.
End ServiceAndCompletionFacts.
+(** In this section, we establish facts that on jobs with nonzero costs that
+ must arrive to execute. *)
Section PositiveCost.
 (** In this section, we establish facts that on jobs with nonzero costs that
 must arrive to execute. *)
(** Consider any type of jobs with cost and arrivaltime attributes,...*)
Context {Job: JobType}.
@@ 243,11 +242,11 @@ Section PositiveCost.
(** ...and a given schedule. *)
Variable sched: schedule PState.
 (** Let j be any job that is to be scheduled. *)
+ (** Let [j] be any job that is to be scheduled. *)
Variable j: Job.
 (** We assume that job j has positive cost, from which we can
 infer that there always is a time in which j is pending, ... *)
+ (** We assume that job [j] has positive cost, from which we can
+ infer that there always is a time in which [j] is pending, ... *)
Hypothesis H_positive_cost: job_cost j > 0.
(** ...and that jobs must arrive to execute. *)
@@ 283,6 +282,7 @@ Section PositiveCost.
End PositiveCost.
Section CompletedJobs.
+
(** Consider any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
diff git a/analysis/facts/behavior/deadlines.v b/analysis/facts/behavior/deadlines.v
index 0a75dbabd73fee41509ef06ba6e15d489eb3cdf4..a657981925d24ea609c1f8bded4711ab2e35124b 100644
 a/analysis/facts/behavior/deadlines.v
+++ b/analysis/facts/behavior/deadlines.v
@@ 1,11 +1,14 @@
Require Export prosa.analysis.facts.behavior.completion.
+(** * Deadlines *)
+
(** In this file, we observe basic properties of the behavioral job
model w.r.t. deadlines. *)

Section DeadlineFacts.
+
(** Consider any given type of jobs with costs and deadlines... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
+
(** ... any given type of processor states. *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
diff git a/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
index 9184a4b91a24aae4b6f8e64050327bd52b8b4c51..9c3fd40100c6e696a0788961927ce16a8be0a7d6 100644
 a/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ 2,15 +2,15 @@ Require Export prosa.util.all.
Require Export prosa.behavior.all.
Require Export prosa.model.processor.platform_properties.
From mathcomp Require Import ssrnat ssrbool fintype.
+(** * Service *)
(** In this file, we establish basic facts about the service received by
jobs. *)
Section Composition.
 (** To begin with, we provide some simple but handy rewriting rules for
+(** To begin with, we provide some simple but handy rewriting rules for
[service] and [service_during]. *)

+Section Composition.
+
(** Consider any job type and any processor state. *)
Context {Job: JobType}.
Context {PState: Type}.
@@ 130,10 +130,9 @@ Section Composition.
End Composition.

+(** As a common special case, we establish facts about schedules in which a
+ job receives either 1 or 0 service units at all times. *)
Section UnitService.
 (** As a common special case, we establish facts about schedules in which a
 job receives either 1 or 0 service units at all times. *)
(** Consider any job type and any processor state. *)
Context {Job: JobType}.
@@ 146,7 +145,7 @@ Section UnitService.
(** ...and a given schedule. *)
Variable sched: schedule PState.
 (** Let j be any job that is to be scheduled. *)
+ (** Let [j] be any job that is to be scheduled. *)
Variable j: Job.
(** First, we prove that the instantaneous service cannot be greater than 1, ... *)
@@ 156,7 +155,7 @@ Section UnitService.
by move=> t; rewrite /service_at.
Qed.
 (** ...which implies that the cumulative service received by job j in any
+ (** ...which implies that the cumulative service received by job [j] in any
interval of length delta is at most delta. *)
Lemma cumulative_service_le_delta:
forall t delta,
@@ 170,7 +169,7 @@ Section UnitService.
Section ServiceIsAStepFunction.
 (** We show that the service received by any job j is a step function. *)
+ (** 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).
Proof.
@@ 179,15 +178,15 @@ Section UnitService.
apply service_at_most_one.
Qed.
 (** Next, consider any time t... *)
+ (** Next, consider any time [t]... *)
Variable t: instant.
 (** ...and let s0 be any value less than the service received
 by job j by time t. *)
+ (** ...and let [s0] be any value less than the service received
+ by job [j] by time [t]. *)
Variable s0: duration.
Hypothesis H_less_than_s: s0 < service sched j t.
 (** Then, we show that there exists an earlier time t0 where job j had s0
+ (** Then, we show that there exists an earlier time [t0] where job [j] had [s0]
units of service. *)
Corollary exists_intermediate_service:
exists t0,
@@ 205,8 +204,8 @@ Section UnitService.
End UnitService.
+(** We establish a basic fact about the monotonicity of service. *)
Section Monotonicity.
 (** We establish a basic fact about the monotonicity of service. *)
(** Consider any job type and any processor model. *)
Context {Job: JobType}.
@@ 231,8 +230,9 @@ Section Monotonicity.
End Monotonicity.
+(** Consider any job type and any processor model. *)
Section RelationToScheduled.
 (** Consider any job type and any processor model. *)
+
Context {Job: JobType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
@@ 313,7 +313,7 @@ Section RelationToScheduled.
Qed.
(** Thus, any job that receives some service during an interval must be
 scheduled at some point during the interval... *)
+ scheduled at some point during the interval... *)
Corollary cumulative_service_implies_scheduled:
forall t1 t2,
service_during sched j t1 t2 > 0 >
@@ 339,12 +339,12 @@ Section RelationToScheduled.
have EX_SCHED := cumulative_service_implies_scheduled 0 t2 NONZERO.
by move: EX_SCHED => [t [TIMES SCHED_AT]]; exists t; split.
Qed.

+
+ (** If we can assume that a scheduled job always receives service,
+ we can further prove the converse. *)
Section GuaranteedService.
 (** If we can assume that a scheduled job always receives service, we can
 further prove the converse. *)
 (** Assume j always receives some positive service. *)
+ (** Assume [j] always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
(** In other words, not being scheduled is equivalent to receiving zero
@@ 406,9 +406,9 @@ Section RelationToScheduled.
End GuaranteedService.
+ (** Furthermore, if we know that jobs are not released early, then we can
+ narrow the interval during which they must have been scheduled. *)
Section AfterArrival.
 (** Furthermore, if we know that jobs are not released early, then we can
 narrow the interval during which they must have been scheduled. *)
Context `{JobArrival Job}.
@@ 440,8 +440,8 @@ Section RelationToScheduled.
rewrite /has_arrived ltnNge //.
Qed.
 (** We show that job j does not receive service at any time t prior to its
 arrival. *)
+ (** We show that job [j] does not receive service at any time [t] prior to its
+ arrival. *)
Lemma service_before_job_arrival_zero:
forall t,
t < job_arrival j >
@@ 492,17 +492,17 @@ Section RelationToScheduled.
End AfterArrival.
+ (** In this section, we prove some lemmas about time instants with same
+ service. *)
Section TimesWithSameService.
 (** In this section, we prove some lemmas about time instants with same
 service. *)
 (** Consider any time instants t1 and t2... *)
+ (** Consider any time instants [t1] and [t2]... *)
Variable t1 t2: instant.
 (** ...where t1 is no later than t2... *)
+ (** ...where [t1] is no later than [t2]... *)
Hypothesis H_t1_le_t2: t1 <= t2.
 (** ...and where job j has received the same amount of service. *)
+ (** ...and where job [j] has received the same amount of service. *)
Hypothesis H_same_service: service sched j t1 = service sched j t2.
(** First, we observe that this means that the job receives no service
@@ 527,8 +527,8 @@ Section RelationToScheduled.
apply IS_ZERO. apply /andP; split => //.
Qed.
 (** We show that job j receives service at some point t < t1 iff j receives
 service at some point t' < t2. *)
+ (** We show that job [j] receives service at some point [t < t1]
+ iff [j] receives service at some point [t' < t2]. *)
Lemma same_service_implies_serviced_at_earlier_times:
[exists t: 'I_t1, service_at sched j t > 0] =
[exists t': 'I_t2, service_at sched j t' > 0].
@@ 550,14 +550,15 @@ Section RelationToScheduled.
}
Qed.
+
(** Then, under the assumption that scheduled jobs receives service,
 we can translate this into a claim about scheduled_at. *)
+ we can translate this into a claim about scheduled_at. *)
 (** Assume j always receives some positive service. *)
+ (** Assume [j] always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.
 (** We show that job j is scheduled at some point t < t1 iff j is scheduled
 at some point t' < t2. *)
+ (** We show that job [j] is scheduled at some point [t < t1] iff [j] is scheduled
+ at some point [t' < t2]. *)
Lemma same_service_implies_scheduled_at_earlier_times:
[exists t: 'I_t1, scheduled_at sched j t] =
[exists t': 'I_t2, scheduled_at sched j t'].
diff git a/analysis/facts/edf.v b/analysis/facts/edf.v
index a5107a2df596c60ce3ade96efc3076cba7944197..7f3948983186c7ecfdd457947b5584a71ee38478 100644
 a/analysis/facts/edf.v
+++ b/analysis/facts/edf.v
@@ 31,5 +31,4 @@ End PropertiesOfEDF.
(** We add the above lemma into a "Hint Database" basic_facts, so Coq
will be able to apply them automatically. *)
Hint Resolve
 EDF_respects_sequential_tasks : basic_facts.
+Hint Resolve EDF_respects_sequential_tasks : basic_facts.
diff git a/analysis/facts/model/ideal_schedule.v b/analysis/facts/model/ideal_schedule.v
index 63a4bff261b5dedf37458b8719df91eea6b03f00..3f6178e6b1e9927b9751ded9e2df6e29c047246d 100644
 a/analysis/facts/model/ideal_schedule.v
+++ b/analysis/facts/model/ideal_schedule.v
@@ 1,4 +1,3 @@
From mathcomp Require Import all_ssreflect.
Require Export prosa.util.all.
Require Export prosa.model.processor.platform_properties.
Require Export prosa.analysis.facts.behavior.service.
@@ 87,33 +86,6 @@ Section ScheduleClass.
End ScheduleClass.
(** * Automation *)
(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
 will be able to apply them automatically. *)
Hint Resolve ideal_proc_model_is_a_uniprocessor_model
 ideal_proc_model_ensures_ideal_progress
 ideal_proc_model_provides_unit_service : basic_facts.

(** We also provide tactics for case analysis on ideal processor state. *)

(** The first tactic generates two subgoals: one with idle processor and
 the other with processor executing a job named [JobName]. *)
Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
 let Idle := fresh "Idle" in
 let Sched := fresh "Sched_" JobName in
 destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle  [JobName Sched]].

(** The second tactic is similar to the first, but it additionally generates
 two equalities: [sched t = None] and [sched t = Some j]. *)
Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
 let Idle := fresh "Idle" in
 let IdleEq := fresh "Eq" Idle in
 let Sched := fresh "Sched_" JobName in
 let SchedEq := fresh "Eq" Sched in
 destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle  [JobName Sched]];
 [move: (Idle) => /eqP IdleEq; rewrite ?IdleEq
  move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].

(** * Incremental Service in Ideal Schedule *)
(** In the following section we prove a few facts about service in ideal schedule. *)
(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
@@ 220,3 +192,30 @@ Section IncrementalService.
Qed.
End IncrementalService.
+
+(** * Automation *)
+(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+ will be able to apply them automatically. *)
+Hint Resolve ideal_proc_model_is_a_uniprocessor_model
+ ideal_proc_model_ensures_ideal_progress
+ ideal_proc_model_provides_unit_service : basic_facts.
+
+(** We also provide tactics for case analysis on ideal processor state. *)
+
+(** The first tactic generates two subgoals: one with idle processor and
+ the other with processor executing a job named [JobName]. *)
+Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
+ let Idle := fresh "Idle" in
+ let Sched := fresh "Sched_" JobName in
+ destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle  [JobName Sched]].
+
+(** The second tactic is similar to the first, but it additionally generates
+ two equalities: [sched t = None] and [sched t = Some j]. *)
+Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
+ let Idle := fresh "Idle" in
+ let IdleEq := fresh "Eq" Idle in
+ let Sched := fresh "Sched_" JobName in
+ let SchedEq := fresh "Eq" Sched in
+ destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle  [JobName Sched]];
+ [move: (Idle) => /eqP IdleEq; rewrite ?IdleEq
+  move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].
\ No newline at end of file
diff git a/analysis/facts/model/sequential.v b/analysis/facts/model/sequential.v
index a7141a718455781983e98b92b900cbd1086ef5f3..0dee672dac12e2959c590c586b0f0c909fd3de57 100644
 a/analysis/facts/model/sequential.v
+++ b/analysis/facts/model/sequential.v
@@ 1,6 +1,7 @@
Require Export prosa.model.task.sequentiality.
Section ExecutionOrder.
+
(** Consider any type of job associated with any type of tasks... *)
Context {Job: JobType}.
Context {Task: TaskType}.
@@ 22,7 +23,7 @@ Section ExecutionOrder.
(** A simple corollary of this hypothesis is that the scheduler
 executes a job with the earliest arrival time. *)
+ executes a job with the earliest arrival time. *)
Corollary scheduler_executes_job_with_earliest_arrival:
forall j1 j2 t,
same_task j1 j2 >
diff git a/analysis/facts/model/workload.v b/analysis/facts/model/workload.v
index 8de3db9336f104ffc594c832dc76253fc542b0cf..1959eee73164b6e5666b4e11d8b84e8b2300eab1 100644
 a/analysis/facts/model/workload.v
+++ b/analysis/facts/model/workload.v
@@ 1,8 +1,6 @@
Require Export prosa.model.aggregate.workload.
Require Export prosa.analysis.facts.behavior.arrivals.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(** * Lemmas about Workload of Sets of Jobs *)
(** In this file, we establish basic facts about the workload of sets of jobs. *)
Section WorkloadFacts.
diff git a/analysis/facts/preemption/job/limited.v b/analysis/facts/preemption/job/limited.v
index ce9c55b300edc66a57835d9161eac02634967d07..b78c8890a29d77e98bf00c88ae0a54a71994ad73 100644
 a/analysis/facts/preemption/job/limited.v
+++ b/analysis/facts/preemption/job/limited.v
@@ 4,7 +4,8 @@ Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.analysis.facts.model.ideal_schedule.
(** *)
+(** Throughout this file, we assume the job model with limited
+ preemption points. *)
Require Import prosa.model.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
diff git a/analysis/facts/preemption/job/nonpreemptive.v b/analysis/facts/preemption/job/nonpreemptive.v
index c683bf60fe686afe681de7cc544deb5312344b14..a0d723ea0b117804ed6a0aa18dbc29bf3d923586 100644
 a/analysis/facts/preemption/job/nonpreemptive.v
+++ b/analysis/facts/preemption/job/nonpreemptive.v
@@ 3,6 +3,7 @@ Require Export prosa.analysis.facts.model.ideal_schedule.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.nonpreemptive.
+(** Furthermore, we assume the fully nonpreemptive job model. *)
Require Import prosa.model.preemption.fully_nonpreemptive.
(** * Platform for Fully NonPreemptive model *)
diff git a/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
index 8600afd01294612a322c75ab9300bd54992d34f7..30c83ac5d8cb7180c2e11028ef4da6cecf4967e6 100644
 a/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ 1,4 +1,6 @@
Require Export prosa.model.task.preemption.parameters.
+
+(** Furthermore, we assume the fully preemptive job model. *)
Require Import prosa.model.preemption.fully_preemptive.
(** * Preemptions in Fully Preemptive Model *)
diff git a/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
index 7c17ea26f8fd6a23552416e73a5cf3832073828d..70503f20727232df9da7aab97296b18f47218e34 100644
 a/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ 1,8 +1,10 @@
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.floating_nonpreemptive.
Require Export prosa.analysis.facts.preemption.task.floating.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
+(** Furthermore, we assume the task model with floating nonpreemptive regions. *)
+Require Import prosa.model.preemption.limited_preemptive.
+Require Import prosa.model.task.preemption.floating_nonpreemptive.
+
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
threshold] for the model with floating nonpreemptive regions. *)
diff git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index c57a0bc0915358d96116cbb246c3ea57ff48a3bc..b35e55b2a256ed8327c2309ad38a5db6e40baf1f 100644
 a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ 1,6 +1,7 @@
Require Export prosa.analysis.facts.preemption.task.limited.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
+(** Furthermore, we assume the task model with fixed preemption points. *)
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.limited_preemptive.
diff git a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index 185a19ea62315e1f0c62e9963468cdd482397a60..f90fb3b1fd5a4ee50880dce79d3791bd13d9491a 100644
 a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ 1,9 +1,8 @@
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
+(** Furthermore, we assume the fully nonpreemptive task model. *)
Require Import prosa.model.preemption.fully_nonpreemptive.
Require Import prosa.model.task.preemption.fully_nonpreemptive.

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Task's Run to Completion Threshold *)
(** In this section, we prove that instantiation of function [task run
diff git a/analysis/facts/preemption/rtc_threshold/preemptive.v b/analysis/facts/preemption/rtc_threshold/preemptive.v
index 8e0e4eb80dbbef007916bea46f01a0dc794bdc97..8f6b0632a45ee32d87b5dd243ca69b8fdfd35f0d 100644
 a/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ 1,3 +1,4 @@
+(** Furthermore, we assume the fully preemptive task model. *)
Require Import prosa.model.preemption.fully_preemptive.
Require Import prosa.model.task.preemption.fully_preemptive.
Require Import prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
diff git a/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
index a17eac874684403d39c259810f50a2be881d4ae4..fa828062e89ab2ba72d252b4ddffc4b637d650d7 100644
 a/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ 1,10 +1,9 @@
Require Export prosa.analysis.facts.preemption.job.limited.
+(** Furthermore, we assume the task model with floating nonpreemptive regions. *)
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.floating_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

(** * Platform for Floating NonPreemptive Regions Model *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_max_nonpreemptive_segment] to the model
@@ 107,6 +106,7 @@ Section FloatingNonPreemptiveRegionsModel.
End FloatingNonPreemptiveRegionsModel.
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
Hint Resolve
valid_fixed_preemption_points_model_lemma
floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
diff git a/analysis/facts/preemption/task/limited.v b/analysis/facts/preemption/task/limited.v
index a29c2d827bcf8519d4637cb3dbd31b8dd680737a..40ecb21cbb818ac9b75019d764d17d54b3af6a05 100644
 a/analysis/facts/preemption/task/limited.v
+++ b/analysis/facts/preemption/task/limited.v
@@ 1,5 +1,6 @@
Require Export prosa.analysis.facts.preemption.job.limited.
+(** Furthermore, we assume the task model with fixed preemption points. *)
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.limited_preemptive.
@@ 107,6 +108,7 @@ Section LimitedPreemptionsModel.
End LimitedPreemptionsModel.
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
Hint Resolve
valid_fixed_preemption_points_model_lemma
fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
diff git a/analysis/facts/preemption/task/nonpreemptive.v b/analysis/facts/preemption/task/nonpreemptive.v
index f3d44c934134975aa9112795d41ac96c69eaab03..affb46ccb35c21ec5148de9cb41c573105a89122 100644
 a/analysis/facts/preemption/task/nonpreemptive.v
+++ b/analysis/facts/preemption/task/nonpreemptive.v
@@ 1,10 +1,9 @@
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
+(** Furthermore, we assume the fully nonpreemptive task model. *)
Require Import prosa.model.preemption.fully_nonpreemptive.
Require Import prosa.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

(** * Platform for Fully NonPreemptive Model *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_max_nonpreemptive_segment] to the fully
@@ 86,6 +85,7 @@ Section FullyNonPreemptiveModel.
End FullyNonPreemptiveModel.
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
Hint Resolve
valid_fully_nonpreemptive_model
fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions
diff git a/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
index 92a7102afbeb560dfa520135cf89ce663f84fb82..5f91aee5416c095e07a403375aeea1257f4bb13f 100644
 a/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ 1,6 +1,7 @@
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.preemption.job.preemptive.
+(** Furthermore, we assume the fully nonpreemptive task model. *)
Require Import prosa.model.task.preemption.fully_preemptive.
(** * Platform for Fully Preemptive Model *)
@@ 57,6 +58,7 @@ Section FullyPreemptiveModel.
End FullyPreemptiveModel.
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
Hint Resolve
valid_fully_preemptive_model
fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions
diff git a/analysis/transform/prefix.v b/analysis/transform/prefix.v
index c2f7b1e8faaedf714c21c140ea5ccf05fbfb7519..99670dad18b11d97f4e8df0a4706323fe4676fb3 100644
 a/analysis/transform/prefix.v
+++ b/analysis/transform/prefix.v
@@ 6,6 +6,7 @@ Require Export prosa.analysis.facts.behavior.all.
instant up to a given horizon. *)
Section SchedulePrefixMap.
+
(** For any type of jobs and... *)
Context {Job : JobType}.
diff git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index e5c1fd6cec14eb13800abbfeadd195fb213d883c..a92e599ebd253c63b1267a91b52a297e1865e7e5 100644
 a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ 2,6 +2,7 @@ Require Import prosa.model.priority.edf.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.results.edf.rta.bounded_pi.
+Require Export prosa.analysis.facts.busy_interval.priority_inversion.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import prosa.model.processor.ideal.
diff git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index b50dec91061f306cc67c375ecc465520a91cb6a4..db70e08a234b147c6e5c8d03f164a21e47652e07 100644
 a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ 1,6 +1,5 @@
Require Export prosa.analysis.facts.edf.
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.busy_interval.priority_inversion.
Require Export prosa.analysis.facts.busy_interval.carry_in.
Require Export prosa.analysis.definitions.schedulability.
Require Import prosa.model.priority.edf.