# 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 δ.