Library prosa.util.step_function
Require Import prosa.util.tactics prosa.util.notation.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
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.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
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.