enable automatic arrival-model conversion

This commit makes it possible to transparently interpret periodic
tasks as sporadic tasks, and sporadic tasks as tasks with an arrival
curve, such that all proof obligations can satisfied by `rt_auto` and
`rt_eauto`. Full example:

```
Require Import prosa.model.task.arrival.periodic.
Require Import prosa.model.task.arrival.periodic_as_sporadic.
Require Import prosa.model.task.arrival.sporadic_as_curve.

Section AutoArrivalModelConversion.

  Context {Job : JobType} `{JobArrival Job}.
  Context {Task : TaskType} `{PeriodicModel Task} `{JobTask Job Task}.

  Variable ts : TaskSet Task.

  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
  Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.

  Hypothesis H_valid_periods : valid_periods ts.

  Hypothesis H_respects : taskset_respects_periodic_task_model arr_seq ts.

  (** 1. Interpret as sporadic: *)
  Goal valid_taskset_inter_arrival_times ts.
  Proof. by rt_auto. Qed.

  Goal taskset_respects_sporadic_task_model ts arr_seq.
  Proof. by rt_auto. Qed.

  (** 2. Interpret as an arrival curve. *)
  Goal valid_taskset_arrival_curve ts max_arrivals.
  Proof. by rt_auto. Qed.

  Goal taskset_respects_max_arrivals arr_seq ts.
  Proof. by rt_eauto. Qed.

End AutoArrivalModelConversion.

```

model/task/arrival/periodic_as_sporadic.v

@@ -67,13 +67,13 @@ Section PeriodicTasksAsSporadicTasks.
 
   (** First, we show that all tasks in a task set with valid periods
       also have valid min inter-arrival times. *)
-  Remark valid_periods_are_valid_inter_arrival_times:
+  Remark valid_periods_are_valid_inter_arrival_times :
     forall ts, valid_periods ts -> valid_taskset_inter_arrival_times ts.
   Proof. trivial. Qed.
 
   (** Second, we show that each task in a periodic task set respects
       the sporadic task model. *)
-  Remark periodic_task_sets_respect_sporadic_task_model:
+  Remark periodic_task_sets_respect_sporadic_task_model :
     forall ts,
       valid_periods ts ->
       taskset_respects_periodic_task_model arr_seq ts ->
@@ -87,6 +87,11 @@ Section PeriodicTasksAsSporadicTasks.
   
 End PeriodicTasksAsSporadicTasks.
 
-(** We add the [periodic_task_respects_sporadic_task_model] lemma into a "Hint Database" basic_rt_facts,
-    so Coq will be able to apply it automatically. *)
-Global Hint Extern 1 => apply periodic_task_respects_sporadic_task_model : basic_rt_facts.
+(** We add the lemmas into the "Hint Database" basic_rt_facts so that
+    they become available for proof automation. *)
+Global Hint Resolve
+  periodic_task_respects_sporadic_task_model
+  valid_period_is_valid_inter_arrival_time
+  valid_periods_are_valid_inter_arrival_times
+  periodic_task_sets_respect_sporadic_task_model
+  : basic_rt_facts.

model/task/arrival/sporadic_as_curve.v

@@ -27,6 +27,13 @@ Section SporadicArrivalCurve.
     exact: div_ceil_monotone1.
   Qed.
 
+  (** For convenience, we lift the preceding observation to the level
+      of entire task sets. *)
+  Remark sporadic_task_sets_arrival_curve_valid :
+    forall ts,
+      valid_taskset_arrival_curve ts max_arrivals.
+  Proof. move=> ? ? ?; exact: sporadic_arrival_curve_valid. Qed.
+
    (** Next, we note that it is indeed an arrival bound. To this end,
        consider any type of jobs stemming from these tasks ... *)
   Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
@@ -36,16 +43,43 @@ Section SporadicArrivalCurve.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
   Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
-  (** Let [tsk] denote any valid sporadic task to be analyzed. *)
-  Variable tsk : Task.
-  Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
-  Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
+  (** We establish the validity of the defined curve. *)
+  Section Validity.
+
+    (** Let [tsk] denote any valid sporadic task to be analyzed. *)
+    Variable tsk : Task.
+    Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
+    Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
+
+    (** We observe that [max_sporadic_arrivals] is indeed an upper bound
+        on the maximum number of arrivals. *)
+    Lemma sporadic_arrival_curve_respects_max_arrivals :
+      respects_max_arrivals arr_seq tsk (max_sporadic_arrivals tsk).
+    Proof. move=> t1 t2 LEQ. exact: sporadic_task_arrivals_bound. Qed.
 
-  (** We observe that [max_sporadic_arrivals] is indeed an upper bound
-      on the maximum number of arrivals. *)
-  Lemma sporadic_arrival_curve_respects_max_arrivals :
-    respects_max_arrivals arr_seq tsk (max_sporadic_arrivals tsk).
-  Proof. move=> t1 t2 LEQ. exact: sporadic_task_arrivals_bound. Qed.
+  End Validity.
+
+  (** For convenience, we lift the preceding observation to the level
+      of entire task sets. *)
+  Remark sporadic_task_sets_respects_max_arrivals :
+    forall ts,
+      valid_taskset_inter_arrival_times ts ->
+      taskset_respects_sporadic_task_model ts arr_seq ->
+      taskset_respects_max_arrivals arr_seq ts.
+  Proof.
+    move=> ts VAL SPO tsk IN.
+    apply: sporadic_arrival_curve_respects_max_arrivals.
+    - by apply: SPO.
+    - by apply: VAL.
+  Qed.
 
 End SporadicArrivalCurve.
 
+(** We add the lemmas into the "Hint Database" basic_rt_facts so that
+    they become available for proof automation. *)
+Global Hint Resolve
+  sporadic_arrival_curve_valid
+  sporadic_task_sets_arrival_curve_valid
+  sporadic_arrival_curve_respects_max_arrivals
+  sporadic_task_sets_respects_max_arrivals
+  : basic_rt_facts.