Library prosa.util.unit_growth

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

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.

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 t 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.
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.