Library rt.util.step_function
Require Import rt.util.tactics rt.util.notation rt.util.induction.
Section StepFunction.
Section Defs.
(* We say that a function f... *)
Variable f: nat → nat.
(* ...is a step function iff the following holds. *)
Definition is_step_function :=
∀ t, f (t + 1) ≤ f t + 1.
End Defs.
Section Lemmas.
(* Let f be any step function over natural numbers. *)
Variable f: nat → nat.
Hypothesis H_step_function: is_step_function f.
(* In this 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 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. *)
Lemma exists_intermediate_point:
∃ x_mid, x1 ≤ x_mid < x2 ∧ f x_mid = y.
End ExistsIntermediateValue.
End Lemmas.
(* In this section, we prove an analogue of the intermediate
value theorem, but for predicates of 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 StepFunction.
Section StepFunction.
Section Defs.
(* We say that a function f... *)
Variable f: nat → nat.
(* ...is a step function iff the following holds. *)
Definition is_step_function :=
∀ t, f (t + 1) ≤ f t + 1.
End Defs.
Section Lemmas.
(* Let f be any step function over natural numbers. *)
Variable f: nat → nat.
Hypothesis H_step_function: is_step_function f.
(* In this 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 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. *)
Lemma exists_intermediate_point:
∃ x_mid, x1 ≤ x_mid < x2 ∧ f x_mid = y.
End ExistsIntermediateValue.
End Lemmas.
(* In this section, we prove an analogue of the intermediate
value theorem, but for predicates of 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 StepFunction.