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.

End StepFunction.