Library prosa.util.unit_growth

We say that a function f is a unit growth function iff for any time instant t it holds that f (t + 1) f t + 1.
Definition unit_growth_function (f : nat nat) :=
   t, f (t + 1) f t + 1.

In this section, we prove a few useful lemmas about unit growth functions.
Section Lemmas.

Let f be any unit growth function over natural numbers.
  Variable f : nat nat.
  Hypothesis H_unit_growth_function : unit_growth_function f.

Since f is a unit-growth function, the value of f after k steps is at most k greater than its value at the starting point.
  Lemma unit_growth_function_k_steps_bounded :
     (x k : nat),
      f (x + k) k + f x.
In the following section, we prove a result similar to the intermediate value theorem for continuous functions.
Consider any interval [x1, x2].
    Variable x1 x2 : nat.
    Hypothesis H_is_interval : x1 x2.

Let y be any value such that f x1 y < f x2.
    Variable y : nat.
    Hypothesis H_between : f x1 y < f x2.

Then, we prove that there exists an intermediate point x_mid such that f x_mid = y.
    Lemma exists_intermediate_point :
       x_mid,
        x1 x_mid < x2 f x_mid = y.

  End ExistsIntermediateValue.

Next, we prove the same lemma with slightly different boundary conditions.
Consider any interval [x1, x2].
    Variable x1 x2 : nat.
    Hypothesis H_is_interval : x1 x2.

Let y be any value such that f x1 y f x2. Note that y is allowed to be equal to f x2.
    Variable y : nat.
    Hypothesis H_between : f x1 y f x2.

Then, we prove that there exists an intermediate point x_mid such that f x_mid = y.
    Corollary exists_intermediate_point_leq :
       x_mid,
        x1 x_mid x2 f x_mid = y.

  End ExistsIntermediateValueLEQ.

In this section, we, again, prove an analogue of the intermediate value theorem, but for predicates over natural numbers.
Let P be any predicate on natural numbers.
    Variable P : nat bool.

Consider a time interval [t1,t2] such that ...
    Variables t1 t2 : nat.
    Hypothesis H_t1_le_t2 : t1 t2.

... P doesn't hold for t1 ...
    Hypothesis H_not_P_at_t1 : ~~ P t1.

... but holds for t2.
    Hypothesis H_P_at_t2 : P t2.

Then we prove that within time interval [t1,t2] there exists time instant t such that t is the first time instant when P holds.

Slowing Functions to Unit-Step Growth

Next, we define and prove a few properties about a function that converts any function into a unit-step function. This construction will be used later to define Supply-Bound Functions (SBFs), which must satisfy this growth constraint in some of the RTAs.

Slowed Function

Given a function F : nat nat, we define a slowed version slowed F such that slowed F n grows no faster than one unit per input increment. Intuitively, slowed F matches F when slowed F n = F n, and otherwise "lags behind" F to enforce the unit-growth constraint.
The definition is recursive: slowed F n is the minimum of F n and 1 + slowed F (n-1).
Fixpoint slowed (F : nat nat) (n : nat) : nat :=
  match n with
  | 0 ⇒ F 0
  | n'.+1minn (F n'.+1) (slowed F n').+1
  end.

Given two functions f and F, if f is a unit-growth function and f F pointwise up to Δ, then f Δ slowed F Δ.
Lemma slowed_respects_pointwise_leq :
   (f F : nat nat) (Δ : nat),
    unit_growth_function f
    ( x, x Δ f x F x)
    f Δ slowed F Δ.

The slowed function grows at most by 1 per step (i.e., it's unit-growth).
Lemma slowed_is_unit_step :
   (f : nat nat),
    unit_growth_function (slowed f).

If f is monotone, then slowed f is also monotone.
Lemma slowed_respects_monotone :
   (f : nat nat),
    monotone leq f
    monotone leq (slowed f).