Library prosa.util.unit_growth

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat zify.zify.
Require Import prosa.util.tactics prosa.util.notation prosa.util.rel.

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.

Section ExistsIntermediateValue.

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.

Section ExistsIntermediateValueLEQ.

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.

Section ExistsIntermediateValuePredicates.

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.

    Lemma exists_first_intermediate_point :
      ∃ t , (t1 < t ≤ t2 ) ∧ (∀ x, t1 ≤ x < t → ~~ P x ) ∧ P t.

  End ExistsIntermediateValuePredicates.

End Lemmas.

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'.+1 ⇒ minn (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).

The slowed version of a function never exceeds the original function.

Lemma slowed_never_exceeds :
∀ (f : nat → nat) (x : nat),
slowed f x ≤ f x.

If some value A is bounded by F - f δ for a function f, then it is also bounded above by F - slowed f δ.

Corollary bound_preserved_under_slowed :
  ∀ (f : nat → nat) (δ : nat) (A F : nat),
    A ≤ F - f δ →
    A ≤ F - slowed f δ.

Consider a monotone function f and the derived function Δ ↦ Δ - f Δ. We show that whenever this derived function attains a value at some interval length Δ, there exists a (possibly smaller) interval length δ ≤ Δ at which the same value is obtained after applying the "slowing" transformation slowed f.

Intuitively, this lemma justifies replacing f by its slowed version without losing any possible output of Δ - f Δ, because for any Δ we can find a suitable δ where the slowed version matches.

Lemma slowed_subtraction_value_preservation :
  ∀ (f : nat → nat) (Δ : nat),
    monotone leq f →
    ∃ (δ : nat ),
      δ ≤ Δ
      ∧ Δ - f Δ = δ - slowed f δ.