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.
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.
In this section, we prove a few useful lemmas about unit growth functions.
Let f be any unit growth function over natural numbers.
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.
In the following section, we prove a result similar to the
intermediate value theorem for continuous functions.
Consider any interval
[x1, x2]
.
Lemma exists_intermediate_point :
∃ x_mid,
x1 ≤ x_mid < x2 ∧ f x_mid = y.
End ExistsIntermediateValue.
∃ 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]
.
Corollary exists_intermediate_point_leq :
∃ x_mid,
x1 ≤ x_mid ≤ x2 ∧ f x_mid = y.
End ExistsIntermediateValueLEQ.
∃ 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.
Consider a time interval
[t1,t2]
such that ...
... but holds for 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.
∃ t, (t1 < t ≤ t2) ∧ (∀ x, t1 ≤ x < t → ~~ P x) ∧ P t.
End ExistsIntermediateValuePredicates.
End Lemmas.
Slowing Functions to Unit-Step Growth
Slowed Function
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.
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 Δ.
∀ (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).