Library prosa.util.step_function


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)


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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 9)
  
  f : nat -> nat
  H_step_function : is_step_function f
  x1, x2 : nat
  H_is_interval : x1 <= x2
  y : nat
  H_between : f x1 <= y < f x2
  ============================
  exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y

----------------------------------------------------------------------------- *)


      Proof.
        rename H_is_interval into INT, H_step_function into STEP, H_between into BETWEEN.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 10)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, x2 : nat
  INT : x1 <= x2
  y : nat
  BETWEEN : f x1 <= y < f x2
  ============================
  exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y

----------------------------------------------------------------------------- *)


        move: x2 INT BETWEEN; clear x2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 16)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y : nat
  ============================
  forall x2 : nat,
  x1 <= x2 ->
  f x1 <= y < f x2 -> exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y

----------------------------------------------------------------------------- *)


        suff DELTA:
           delta,
            f x1 y < f (x1 + delta)
             x_mid, x1 x_mid < x1 + delta f x_mid = y.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 23)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y : nat
  DELTA : forall delta : nat,
          f x1 <= y < f (x1 + delta) ->
          exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  ============================
  forall x2 : nat,
  x1 <= x2 ->
  f x1 <= y < f x2 -> exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y

subgoal 2 (ID 22) is:
 forall delta : nat,
 f x1 <= y < f (x1 + delta) ->
 exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y

----------------------------------------------------------------------------- *)


        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 23)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y : nat
  DELTA : forall delta : nat,
          f x1 <= y < f (x1 + delta) ->
          exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  ============================
  forall x2 : nat,
  x1 <= x2 ->
  f x1 <= y < f x2 -> exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y

----------------------------------------------------------------------------- *)


movex2 LE /andP [GEy LTy].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 64)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y : nat
  DELTA : forall delta : nat,
          f x1 <= y < f (x1 + delta) ->
          exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  x2 : nat
  LE : x1 <= x2
  GEy : f x1 <= y
  LTy : y < f x2
  ============================
  exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          exploit (DELTA (x2 - x1));
            first by apply/andP; split; last by rewrite addnBA // addKn.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 338)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y : nat
  DELTA : forall delta : nat,
          f x1 <= y < f (x1 + delta) ->
          exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  x2 : nat
  LE : x1 <= x2
  GEy : f x1 <= y
  LTy : y < f x2
  ============================
  (exists x_mid : nat, x1 <= x_mid < x1 + (x2 - x1) /\ f x_mid = y) ->
  exists x_mid : nat, x1 <= x_mid < x2 /\ f x_mid = y

----------------------------------------------------------------------------- *)


            by rewrite addnBA // addKn.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 22) is:
 forall delta : nat,
 f x1 <= y < f (x1 + delta) ->
 exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y

----------------------------------------------------------------------------- *)


        }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 22)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y : nat
  ============================
  forall delta : nat,
  f x1 <= y < f (x1 + delta) ->
  exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y

----------------------------------------------------------------------------- *)


        induction delta.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 448)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y : nat
  ============================
  f x1 <= y < f (x1 + 0) ->
  exists x_mid : nat, x1 <= x_mid < x1 + 0 /\ f x_mid = y

subgoal 2 (ID 451) is:
 f x1 <= y < f (x1 + delta.+1) ->
 exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 448)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y : nat
  ============================
  f x1 <= y < f (x1 + 0) ->
  exists x_mid : nat, x1 <= x_mid < x1 + 0 /\ f x_mid = y

----------------------------------------------------------------------------- *)


rewrite addn0; move ⇒ /andP [GE0 LT0].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 495)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y : nat
  GE0 : f x1 <= y
  LT0 : y < f x1
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


            by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 451) is:
 f x1 <= y < f (x1 + delta.+1) ->
 exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


        }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 451)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y, delta : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  ============================
  f x1 <= y < f (x1 + delta.+1) ->
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


        {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 451)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y, delta : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  ============================
  f x1 <= y < f (x1 + delta.+1) ->
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


move ⇒ /andP [GT LT].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 581)
  
  f : nat -> nat
  STEP : is_step_function f
  x1, y, delta : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta.+1)
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          specialize (STEP (x1 + delta)); rewrite leq_eqVlt in STEP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 602)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta.+1)
  STEP : (f (x1 + delta + 1) == f (x1 + delta) + 1)
         || (f (x1 + delta + 1) < f (x1 + delta) + 1)
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          have LE: y f (x1 + delta).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 603)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta.+1)
  STEP : (f (x1 + delta + 1) == f (x1 + delta) + 1)
         || (f (x1 + delta + 1) < f (x1 + delta) + 1)
  ============================
  y <= f (x1 + delta)

subgoal 2 (ID 605) is:
 exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 603)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta.+1)
  STEP : (f (x1 + delta + 1) == f (x1 + delta) + 1)
         || (f (x1 + delta + 1) < f (x1 + delta) + 1)
  ============================
  y <= f (x1 + delta)

----------------------------------------------------------------------------- *)


move: STEP ⇒ /orP [/eqP EQ | STEP];
              first by rewrite !addn1 in EQ; rewrite addnS EQ ltnS in LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 681)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta.+1)
  STEP : f (x1 + delta + 1) < f (x1 + delta) + 1
  ============================
  y <= f (x1 + delta)

----------------------------------------------------------------------------- *)


            rewrite [X in _ < X]addn1 ltnS in STEP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 754)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta.+1)
  STEP : f (x1 + delta + 1) <= f (x1 + delta)
  ============================
  y <= f (x1 + delta)

----------------------------------------------------------------------------- *)


            apply: (leq_trans _ STEP).

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 765)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta.+1)
  STEP : f (x1 + delta + 1) <= f (x1 + delta)
  ============================
  y <= f (x1 + delta + 1)

----------------------------------------------------------------------------- *)


              by rewrite addn1 -addnS ltnW.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 605) is:
 exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          }
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 605)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta.+1)
  STEP : (f (x1 + delta + 1) == f (x1 + delta) + 1)
         || (f (x1 + delta + 1) < f (x1 + delta) + 1)
  LE : y <= f (x1 + delta)
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


clear STEP LT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 779)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LE : y <= f (x1 + delta)
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          rewrite leq_eqVlt in LE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 797)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LE : (y == f (x1 + delta)) || (y < f (x1 + delta))
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          move: LE ⇒ /orP [/eqP EQy | LT].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 872)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  EQy : y = f (x1 + delta)
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

subgoal 2 (ID 873) is:
 exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 872)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  EQy : y = f (x1 + delta)
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


(x1 + delta); split; last by rewrite EQy.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 877)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  EQy : y = f (x1 + delta)
  ============================
  x1 <= x1 + delta < x1 + delta.+1

----------------------------------------------------------------------------- *)


              by apply/andP; split; [by apply leq_addr | by rewrite addnS].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 873) is:
 exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 873)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta)
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


          {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 873)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : f x1 <= y < f (x1 + delta) ->
            exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta)
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


feed (IHdelta); first by apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 917)
  
  f : nat -> nat
  x1, delta, y : nat
  IHdelta : exists x_mid : nat, x1 <= x_mid < x1 + delta /\ f x_mid = y
  GT : f x1 <= y
  LT : y < f (x1 + delta)
  ============================
  exists x_mid : nat, x1 <= x_mid < x1 + delta.+1 /\ f x_mid = y

----------------------------------------------------------------------------- *)


            move: IHdelta ⇒ [x_mid [/andP [GE0 LT0] EQ0]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1005)
  
  f : nat -> nat
  x1, delta, y : nat
  GT : f x1 <= y
  LT : y < f (x1 + delta)
  x_mid : nat
  GE0 : x1 <= x_mid
  LT0 : x_mid < x1 + delta
  EQ0 : f x_mid = y
  ============================
  exists x_mid0 : nat, x1 <= x_mid0 < x1 + delta.+1 /\ f x_mid0 = y

----------------------------------------------------------------------------- *)


             x_mid; split; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1009)
  
  f : nat -> nat
  x1, delta, y : nat
  GT : f x1 <= y
  LT : y < f (x1 + delta)
  x_mid : nat
  GE0 : x1 <= x_mid
  LT0 : x_mid < x1 + delta
  EQ0 : f x_mid = y
  ============================
  x1 <= x_mid < x1 + delta.+1

----------------------------------------------------------------------------- *)


            apply/andP; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1037)
  
  f : nat -> nat
  x1, delta, y : nat
  GT : f x1 <= y
  LT : y < f (x1 + delta)
  x_mid : nat
  GE0 : x1 <= x_mid
  LT0 : x_mid < x1 + delta
  EQ0 : f x_mid = y
  ============================
  x_mid < x1 + delta.+1

----------------------------------------------------------------------------- *)


              by apply: (leq_trans LT0); rewrite addnS.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


          }
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


 
        }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


      Qed.

    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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 9)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  ============================
  exists t : nat,
    t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t

----------------------------------------------------------------------------- *)


    Proof.
      have EX: x, P x && (t1 < x t2).

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 12)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  ============================
  exists x : nat, [&& P x, t1 < x & x <= t2]

subgoal 2 (ID 14) is:
 exists t : nat,
   t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 12)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  ============================
  exists x : nat, [&& P x, t1 < x & x <= t2]

----------------------------------------------------------------------------- *)


t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 16)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  ============================
  [&& P t2, t1 < t2 & t2 <= t2]

----------------------------------------------------------------------------- *)


        apply/andP; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 43)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  ============================
  t1 < t2 <= t2

----------------------------------------------------------------------------- *)


        apply/andP; split; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 69)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  ============================
  t1 < t2

----------------------------------------------------------------------------- *)


        move: H_t1_le_t2; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | NEQ1]; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 148)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  EQ : t1 = t2
  ============================
  t1 < t2

----------------------------------------------------------------------------- *)


          by exfalso; subst t2; move: H_not_P_at_t1 ⇒ /negP NPt1.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 14) is:
 exists t : nat,
   t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t

----------------------------------------------------------------------------- *)


      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 14)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  EX : exists x : nat, [&& P x, t1 < x & x <= t2]
  ============================
  exists t : nat,
    t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t

----------------------------------------------------------------------------- *)


      have MIN := ex_minnP EX.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 214)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  EX : exists x : nat, [&& P x, t1 < x & x <= t2]
  MIN : ex_minn_spec (fun x : nat => [&& P x, t1 < x & x <= t2])
          (ex_minn (P:=fun x : nat => [&& P x, t1 < x & x <= t2]) EX)
  ============================
  exists t : nat,
    t1 < t <= t2 /\ (forall x : nat, t1 <= x < t -> ~~ P x) /\ P t

----------------------------------------------------------------------------- *)


      move: MIN ⇒ [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 304)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  ============================
  exists t : nat,
    t1 < t <= t2 /\ (forall x0 : nat, t1 <= x0 < t -> ~~ P x0) /\ P t

----------------------------------------------------------------------------- *)


       x; repeat split; [ apply/andP; split | | ]; try done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 312)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  ============================
  forall x0 : nat, t1 <= x0 < x -> ~~ P x0

----------------------------------------------------------------------------- *)


      movey /andP [NEQ1 NEQ2]; apply/negPn; intros Py.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 447)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  y : nat
  NEQ1 : t1 <= y
  NEQ2 : y < x
  Py : P y
  ============================
  False

----------------------------------------------------------------------------- *)


      feed (MIN y).
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 448)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  y : nat
  NEQ1 : t1 <= y
  NEQ2 : y < x
  Py : P y
  ============================
  [&& P y, t1 < y & y <= t2]

subgoal 2 (ID 453) is:
 False

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 448)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  y : nat
  NEQ1 : t1 <= y
  NEQ2 : y < x
  Py : P y
  ============================
  [&& P y, t1 < y & y <= t2]

----------------------------------------------------------------------------- *)


apply/andP; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 480)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  y : nat
  NEQ1 : t1 <= y
  NEQ2 : y < x
  Py : P y
  ============================
  t1 < y <= t2

----------------------------------------------------------------------------- *)


        apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 506)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  y : nat
  NEQ1 : t1 <= y
  NEQ2 : y < x
  Py : P y
  ============================
  t1 < y

subgoal 2 (ID 507) is:
 y <= t2

----------------------------------------------------------------------------- *)


        - move: NEQ1.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 509)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  y : nat
  NEQ2 : y < x
  Py : P y
  ============================
  t1 <= y -> t1 < y

subgoal 2 (ID 507) is:
 y <= t2

----------------------------------------------------------------------------- *)


rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | NEQ1]; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 586)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  y : nat
  NEQ2 : y < x
  Py : P y
  EQ : t1 = y
  ============================
  t1 < y

subgoal 2 (ID 507) is:
 y <= t2

----------------------------------------------------------------------------- *)


            by exfalso; subst y; move: H_not_P_at_t1 ⇒ /negP NPt1.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 507)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  MIN : forall n : nat, [&& P n, t1 < n & n <= t2] -> x <= n
  y : nat
  NEQ1 : t1 <= y
  NEQ2 : y < x
  Py : P y
  ============================
  y <= t2

----------------------------------------------------------------------------- *)


        - by apply ltnW, leq_trans with x.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 453) is:
 False

----------------------------------------------------------------------------- *)


      }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 453)
  
  P : nat -> bool
  t1, t2 : nat
  H_t1_le_t2 : t1 <= t2
  H_not_P_at_t1 : ~~ P t1
  H_P_at_t2 : P t2
  x : nat
  Px : P x
  LT1 : t1 < x
  LT2 : x <= t2
  y : nat
  MIN : x <= y
  NEQ1 : t1 <= y
  NEQ2 : y < x
  Py : P y
  ============================
  False

----------------------------------------------------------------------------- *)


        by move: NEQ2; rewrite ltnNge; move ⇒ /negP NEQ2.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


    Qed.

  End ExistsIntermediateValuePredicates.

End StepFunction.