Implicit arguments
It seems that I found a way to (partially) solve the problem with let-blocks boilerplate.
Coq supports typeclasses and can even find an appropriate instance of a typeclass automatically. We just need to wrap the problematic parameters into typeclasses, so Coq can guess which parameter to use.
I have a bit too much code, but it shows all basic situations.
I'm going to start from the parameters of jobs and tasks (i.e. job_cost, job_arrival, task_cost, task_deadline, etc.). And later we can agree on whether we need to do this for arr_seq and sched.
Require Import rt.util.all.
Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job
rt.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module NewUniprocessorSchedule.
Import SporadicTaskset.
Export Time ArrivalSequence.
Section Schedule.
(* Skip this section. *)
Section ScheduleDef.
Variable Job: eqType.
Definition schedule := time -> option Job.
End ScheduleDef.
(* This is the code that we need to write once.
I don't think it's worth explaining to a Prosa-reader. *)
Section SectionWithTechnicalDetails.
Variable Job: eqType.
Class JobArrival : Type := job_arrival: Job -> time.
Class JobCost : Type := job_cost : Job -> time.
Class Sched : Type := sched : schedule Job.
End SectionWithTechnicalDetails.
(* The drawback of this approach is that we no longer use the keyword "Variable"
for job_arrival, job_cost and so on. However, we no longer have to tug
parameters for definitions. Besides that, the code is completely indistinguishable
from the previous versions. *)
Section ScheduleProperties.
Context {Job: eqType}.
(* Now we use "Context" instead of "Variable". *)
Context {job_arrival : JobArrival Job}.
Context {job_cost : JobCost Job}.
(* Consider any uniprocessor schedule. *)
Context {sched : Sched Job}.
(* This section is no different from the original version. *)
Section JobProperties.
(* For parameters that we want to explicitly specify
further we continue to use the keyword Variable. *)
Variable j: Job.
Definition scheduled_at (t: time) := sched t == Some j.
Definition service_at (t: time) : time := scheduled_at t.
Definition service_during (t1 t2: time) :=
\sum_(t1 <= t < t2) service_at t.
Definition service (t: time) := service_during 0 t.
Definition completed_by (t: time) := service t == job_cost j.
End JobProperties.
End ScheduleProperties.
(* This section is no different from the original version. *)
Section ValidSchedules.
Context {Job: eqType}.
Context {job_arrival: JobArrival Job}.
Context {job_cost: JobCost Job}.
Context {sched: Sched Job}.
Definition jobs_must_arrive_to_execute :=
forall j t, scheduled_at j t -> has_arrived job_arrival j t.
Definition completed_jobs_dont_execute :=
forall j t, service j t <= job_cost j.
End ValidSchedules.
(* Let's prove something. *)
Section Lemmas.
Context {Job: eqType}.
Context {job_arrival: JobArrival Job}.
Context {job_cost: JobCost Job}.
Context {sched: Sched Job}.
Section Completion.
(* No additional arguments. *)
Hypothesis H_completed_jobs: completed_jobs_dont_execute.
Variable j: Job.
(* This proof is no different from the original one. *)
Lemma completed_implies_not_scheduled :
forall t,
completed_by j t -> (* No additional arguments. *)
~~ scheduled_at j t. (* No additional arguments. *)
Proof.
rename H_completed_jobs into COMP.
unfold completed_jobs_dont_execute in *.
intros t COMPLETED.
apply/negP; red; intro SCHED.
have BUG := COMP j t.+1.
rewrite leqNgt in BUG; move: BUG => /negP BUG; apply BUG.
unfold service, service_during; rewrite big_nat_recr // /= -addn1.
apply leq_add; first by move: COMPLETED => /eqP <-.
by rewrite /service_at SCHED.
Qed.
End Completion.
End Lemmas.
(* Now suppose that we need to consider two different schedulers. *)
Section TwoSchedulers.
Context {Job: eqType}.
Context {job_arrival: JobArrival Job}.
Context {job_cost: JobCost Job}.
(* As before, we just create two different schedulers. *)
Context {sched1: Sched Job}.
Context {sched2: Sched Job}.
(* I think in this case Coq picks an arbitrary instance. *)
(* Hypothesis H_completed_jobs: completed_jobs_dont_execute. *)
(* But we can explicitly specify the scheduler. *)
Hypothesis H_sched1: @completed_jobs_dont_execute _ _ sched1.
Hypothesis H_sched2: @completed_jobs_dont_execute _ _ sched2.
(* ... *)
End TwoSchedulers.
End Schedule.
End NewUniprocessorSchedule.
(* Still works fine in a new module. *)
Module SomeNewModule.
Import SporadicTaskset.
Export Time ArrivalSequence.
Import NewUniprocessorSchedule.
Section NewSection.
Context {Job: eqType}.
Context {job_arrival: JobArrival Job}.
Context {job_cost: JobCost Job}.
Context {sched: Sched Job}.
Section Completion.
Hypothesis H_completed_jobs: completed_jobs_dont_execute.
Variable j: Job.
Lemma completed_implies_not_scheduled :
forall t,
completed_by j t ->
~~ scheduled_at j t.
Proof.
rename H_completed_jobs into COMP.
unfold completed_jobs_dont_execute in *.
intros t COMPLETED.
apply/negP; red; intro SCHED.
have BUG := COMP j t.+1.
rewrite leqNgt in BUG; move: BUG => /negP BUG; apply BUG.
unfold service, service_during; rewrite big_nat_recr // /= -addn1.
apply leq_add; first by move: COMPLETED => /eqP <-.
by rewrite /service_at SCHED.
Qed.
End Completion.
End NewSection.
End SomeNewModule.