enable periodic->RBF auto conversion

NB: This requires bumping up the "depth" parameter of `rt_auto` and `rt_eauto`.

As a benefit, it becomes possible to automatically use RBFs in the
context of periodic tasks, sporadic tasks, and tasks with arrival
curves. 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.
Require Import prosa.model.task.arrival.curve_as_rbf.

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.

  Context `{JobCost Job} `{TaskCost Task}.
  Hypothesis H_valid_costs : jobs_have_valid_job_costs.

  (** Interpret as an RBF. *)

  Goal valid_taskset_request_bound_function ts (task_max_rbf max_arrivals).
  Proof. by rt_auto. Qed.

  Goal taskset_respects_max_request_bound arr_seq ts.
  Proof. rt_eauto. Qed.

End AutoArrivalModelConversion.
```

model/task/arrival/curve_as_rbf.v

@@ -172,3 +172,12 @@ Section ArrivalCurveToRBF.
   End Facts.
   
 End ArrivalCurveToRBF.
+
+(** We add the lemmas into the "Hint Database" basic_rt_facts so that
+    they become available for proof automation. *)
+Global Hint Resolve
+  valid_arrival_curve_to_max_rbf
+  respects_arrival_curve_to_max_rbf
+  valid_taskset_arrival_curve_to_max_rbf
+  taskset_respects_arrival_curve_to_max_rbf
+  : basic_rt_facts.

util/tactics.v

@@ -87,15 +87,17 @@ Ltac feed_n n H := match constr:(n) with
     [(e)auto with basic_rt_facts] to facilitate automation. Here, we
     use scope [basic_rt_facts] that contains a collection of basic
     real-time theory lemmas. *)
-(** Note: constant [3] was chosen because most of the basic rt facts
+(** Note: constant [4] was chosen because most of the basic rt facts
     have the structure [A1 -> A2 -> ... B], where [Ai] is a hypothesis
     usually present in the context, which gives the depth of the
-    search which is equal to two. One additional level of depth (3)
-    was added to support rare exceptions to this rule. At the same
-    time, the constant should not be too large to avoid slowdowns in
-    case of an unsuccessful application of automation. *)
-Ltac rt_auto := auto 3 with basic_rt_facts.
-Ltac rt_eauto := eauto 3 with basic_rt_facts.
+    search which is equal to two. Two additional levels of depth (4)
+    was added to support rare exceptions to this rule. In particular,
+    depth 4 is needed for automatic periodic->RBF arrival model
+    conversion. At the same time, the constant should not be too large
+    to avoid slowdowns in case of an unsuccessful application of
+    automation. *)
+Ltac rt_auto := auto 4 with basic_rt_facts.
+Ltac rt_eauto := eauto 4 with basic_rt_facts.
 
 (* ************************************************************************** *)
 (** * Handier movement of inequalities. *)