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.

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.

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.

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.