Library prosa.util.search_arg


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

Welcome to Coq 8.11.2 (June 2020)

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


From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
Require Import prosa.util.tactics.

This file introduces a function called [search_arg] that allows finding the argument within a given range for which a function is minimal w.r.t. to a given order while satisfying a given predicate, along with lemmas establishing the basic properties of [search_arg].
Note that while this is quite similar to [arg min ...] / [arg max ...] in [ssreflect] ([fintype]), this function is subtly different in that it possibly returns None and that it does not require the last element in the given range to satisfy the predicate. In contrast, [ssreflect]'s notion of extremum in [fintype] uses the upper bound of the search space as the default value, which is rather unnatural when searching through a schedule.

Section ArgSearch.

  (* Given a function [f] that maps the naturals to elements of type [T]... *)
  Context {T : Type}.
  Variable f: nat T.

  (* ... a predicate [P] on [T] ... *)
  Variable P: pred T.

  (* ... and an order [R] on [T] ... *)
  Variable R: rel T.

  (* ... we define the procedure [search_arg] to iterate a given search space
     [a, b), while checking each element whether [f] satisfies [P] at that
     point and returning the extremum as defined by [R]. *)

  Fixpoint search_arg (a b : nat) : option nat :=
    if a < b then
      match b with
      | 0 ⇒ None
      | S b'match search_arg a b' with
                | Noneif P (f b') then Some b' else None
                | Some xif P (f b') && R (f b') (f x) then Some b' else Some x
                end
      end
    else None.

In the following, we establish basic properties of [search_arg].

  (* To begin, we observe that the search yields [None] iff predicate [P] does
     not hold for any of the points in the search interval. *)

  Lemma search_arg_none:
     a b,
      search_arg a b = None x, a x < b ~~ P (f x).

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

1 subgoal (ID 41)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  ============================
  forall a b : nat,
  search_arg a b = None <-> (forall x : nat, a <= x < b -> ~~ P (f x))

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


  Proof.
    split.

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

2 subgoals (ID 45)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  ============================
  search_arg a b = None -> forall x : nat, a <= x < b -> ~~ P (f x)

subgoal 2 (ID 46) is:
 (forall x : nat, a <= x < b -> ~~ P (f x)) -> search_arg a b = None

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


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

1 subgoal (ID 45)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  ============================
  search_arg a b = None -> forall x : nat, a <= x < b -> ~~ P (f x)

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


(* if *)
      elim: b ⇒ [ _ | b' HYP]; first by move_ /andP [_ FALSE] //.

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

1 subgoal (ID 58)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  HYP : search_arg a b' = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  ============================
  search_arg a b'.+1 = None -> forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


      rewrite /search_arg -/search_arg.

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

1 subgoal (ID 123)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  HYP : search_arg a b' = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  ============================
  (if a < b'.+1
   then
    match search_arg a b' with
    | Some x => if P (f b') && R (f b') (f x) then Some b' else Some x
    | None => if P (f b') then Some b' else None
    end
   else None) = None -> forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


      case: (boolP (a < b'.+1)) ⇒ [a_lt_b | not_a_lt_b' TRIV].

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

2 subgoals (ID 134)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  HYP : search_arg a b' = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  a_lt_b : a < b'.+1
  ============================
  match search_arg a b' with
  | Some x => if P (f b') && R (f b') (f x) then Some b' else Some x
  | None => if P (f b') then Some b' else None
  end = None -> forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

subgoal 2 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


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

2 subgoals (ID 138)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  ============================
  (search_arg a b' = None -> forall x : nat, a <= x < b' -> ~~ P (f x)) ->
  match search_arg a b' with
  | Some x => if P (f b') && R (f b') (f x) then Some b' else Some x
  | None => if P (f b') then Some b' else None
  end = None -> forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

subgoal 2 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


case: (search_arg a b') ⇒ [y | HYP NIL x].

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

3 subgoals (ID 147)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  y : nat
  ============================
  (Some y = None -> forall x : nat, a <= x < b' -> ~~ P (f x)) ->
  (if P (f b') && R (f b') (f y) then Some b' else Some y) = None ->
  forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

subgoal 2 (ID 150) is:
 a <= x < b'.+1 -> ~~ P (f x)
subgoal 3 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


        + case: (P (f b') && R (f b') (f y)) ⇒ //.

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

2 subgoals (ID 150)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  HYP : None = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  NIL : (if P (f b') then Some b' else None) = None
  x : nat
  ============================
  a <= x < b'.+1 -> ~~ P (f x)

subgoal 2 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


        + move⇒ /andP[a_le_x x_lt_b'].

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

2 subgoals (ID 257)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  HYP : None = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  NIL : (if P (f b') then Some b' else None) = None
  x : nat
  a_le_x : a <= x
  x_lt_b' : x < b'.+1
  ============================
  ~~ P (f x)

subgoal 2 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


          move: x_lt_b'.

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

2 subgoals (ID 259)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  HYP : None = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  NIL : (if P (f b') then Some b' else None) = None
  x : nat
  a_le_x : a <= x
  ============================
  x < b'.+1 -> ~~ P (f x)

subgoal 2 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


          rewrite ltnS leq_eqVlt ⇒ /orP [/eqP EQ|LT].

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

3 subgoals (ID 342)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  HYP : None = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  NIL : (if P (f b') then Some b' else None) = None
  x : nat
  a_le_x : a <= x
  EQ : x = b'
  ============================
  ~~ P (f x)

subgoal 2 (ID 343) is:
 ~~ P (f x)
subgoal 3 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


          × rewrite EQ.

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

3 subgoals (ID 345)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  HYP : None = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  NIL : (if P (f b') then Some b' else None) = None
  x : nat
  a_le_x : a <= x
  EQ : x = b'
  ============================
  ~~ P (f b')

subgoal 2 (ID 343) is:
 ~~ P (f x)
subgoal 3 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


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

3 subgoals (ID 347)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  HYP : None = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  x : nat
  a_le_x : a <= x
  EQ : x = b'
  ============================
  (if P (f b') then Some b' else None) = None -> ~~ P (f b')

subgoal 2 (ID 343) is:
 ~~ P (f x)
subgoal 3 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


case: (P (f b')) ⇒ //.

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

2 subgoals (ID 343)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  HYP : None = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  NIL : (if P (f b') then Some b' else None) = None
  x : nat
  a_le_x : a <= x
  LT : x < b'
  ============================
  ~~ P (f x)

subgoal 2 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


          × feed HYP ⇒ //.

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

2 subgoals (ID 385)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  HYP : forall x : nat, a <= x < b' -> ~~ P (f x)
  NIL : (if P (f b') then Some b' else None) = None
  x : nat
  a_le_x : a <= x
  LT : x < b'
  ============================
  ~~ P (f x)

subgoal 2 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


            apply: (HYP x).

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

2 focused subgoals
(shelved: 1) (ID 412)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  a_lt_b : a < b'.+1
  HYP : forall x : nat, a <= x < b' -> ~~ P (f x)
  NIL : (if P (f b') then Some b' else None) = None
  x : nat
  a_le_x : a <= x
  LT : x < b'
  ============================
  a <= x < b'

subgoal 2 (ID 136) is:
 forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


            by apply /andP; split.

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

1 subgoal (ID 136)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  HYP : search_arg a b' = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  not_a_lt_b' : ~~ (a < b'.+1)
  TRIV : None = None
  ============================
  forall x : nat, a <= x < b'.+1 -> ~~ P (f x)

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


      - movex /andP [a_le_x b_lt_b'].

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

1 subgoal (ID 480)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  HYP : search_arg a b' = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  not_a_lt_b' : ~~ (a < b'.+1)
  TRIV : None = None
  x : nat
  a_le_x : a <= x
  b_lt_b' : x < b'.+1
  ============================
  ~~ P (f x)

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


        exfalso.

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

1 subgoal (ID 481)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  HYP : search_arg a b' = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  not_a_lt_b' : ~~ (a < b'.+1)
  TRIV : None = None
  x : nat
  a_le_x : a <= x
  b_lt_b' : x < b'.+1
  ============================
  False

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


        move: not_a_lt_b'.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 483)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  HYP : search_arg a b' = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  TRIV : None = None
  x : nat
  a_le_x : a <= x
  b_lt_b' : x < b'.+1
  ============================
  ~~ (a < b'.+1) -> False

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


rewrite -leqNgt ltnNge ⇒ /negP b'_lt_a.

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

1 subgoal (ID 517)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  HYP : search_arg a b' = None -> forall x : nat, a <= x < b' -> ~~ P (f x)
  TRIV : None = None
  x : nat
  a_le_x : a <= x
  b_lt_b' : x < b'.+1
  b'_lt_a : ~ a <= b'
  ============================
  False

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


        by move: (leq_ltn_trans a_le_x b_lt_b').

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

1 subgoal (ID 46)

subgoal 1 (ID 46) is:
 (forall x : nat, a <= x < b -> ~~ P (f x)) -> search_arg a b = None

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


    }

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

1 subgoal (ID 46)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  ============================
  (forall x : nat, a <= x < b -> ~~ P (f x)) -> search_arg a b = None

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


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

1 subgoal (ID 46)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  ============================
  (forall x : nat, a <= x < b -> ~~ P (f x)) -> search_arg a b = None

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


(* only if *)
      rewrite /search_arg.

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

1 subgoal (ID 522)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  ============================
  (forall x : nat, a <= x < b -> ~~ P (f x)) ->
  (fix search_arg (a0 b0 : nat) {struct b0} : option nat :=
     if a0 < b0
     then
      match b0 with
      | 0 => None
      | b'.+1 =>
          match search_arg a0 b' with
          | Some x => if P (f b') && R (f b') (f x) then Some b' else Some x
          | None => if P (f b') then Some b' else None
          end
      end
     else None) a b = None

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


      elim: b ⇒ [//|b'].

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

1 subgoal (ID 533)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  ============================
  ((forall x : nat, a <= x < b' -> ~~ P (f x)) ->
   (fix search_arg (a0 b : nat) {struct b} : option nat :=
      if a0 < b
      then
       match b with
       | 0 => None
       | b'0.+1 =>
           match search_arg a0 b'0 with
           | Some x =>
               if P (f b'0) && R (f b'0) (f x) then Some b'0 else Some x
           | None => if P (f b'0) then Some b'0 else None
           end
       end
      else None) a b' = None) ->
  (forall x : nat, a <= x < b'.+1 -> ~~ P (f x)) ->
  (if a < b'.+1
   then
    match
      (fix search_arg (a0 b : nat) {struct b} : option nat :=
         if a0 < b
         then
          match b with
          | 0 => None
          | b'0.+1 =>
              match search_arg a0 b'0 with
              | Some x =>
                  if P (f b'0) && R (f b'0) (f x) then Some b'0 else Some x
              | None => if P (f b'0) then Some b'0 else None
              end
          end
         else None) a b'
    with
    | Some x => if P (f b') && R (f b') (f x) then Some b' else Some x
    | None => if P (f b') then Some b' else None
    end
   else None) = None

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


      rewrite -/search_argIND NOT_SAT.

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

1 subgoal (ID 536)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  ============================
  (if a < b'.+1
   then
    match search_arg a b' with
    | Some x => if P (f b') && R (f b') (f x) then Some b' else Some x
    | None => if P (f b') then Some b' else None
    end
   else None) = None

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


      have ->: search_arg a b' = None.

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

2 subgoals (ID 540)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  ============================
  search_arg a b' = None

subgoal 2 (ID 545) is:
 (if a < b'.+1 then if P (f b') then Some b' else None else None) = None

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


      {

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

1 subgoal (ID 540)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  ============================
  search_arg a b' = None

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


        apply INDx /andP [a_le_x x_lt_n].

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

1 subgoal (ID 587)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  x : nat
  a_le_x : a <= x
  x_lt_n : x < b'
  ============================
  ~~ P (f x)

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


        apply: (NOT_SAT x).

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

1 focused subgoal
(shelved: 1) (ID 592)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  x : nat
  a_le_x : a <= x
  x_lt_n : x < b'
  ============================
  a <= x < b'.+1

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


        apply /andP; split ⇒ //.

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

1 subgoal (ID 619)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  x : nat
  a_le_x : a <= x
  x_lt_n : x < b'
  ============================
  x < b'.+1

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


        by rewrite ltnS; apply ltnW.

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

1 subgoal (ID 545)

subgoal 1 (ID 545) is:
 (if a < b'.+1 then if P (f b') then Some b' else None else None) = None

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


      }

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

1 subgoal (ID 545)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  ============================
  (if a < b'.+1 then if P (f b') then Some b' else None else None) = None

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


      case: (boolP (a < b'.+1)) ⇒ [a_lt_b | //].

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

1 subgoal (ID 657)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  a_lt_b : a < b'.+1
  ============================
  (if P (f b') then Some b' else None) = None

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


      apply ifF.

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

1 subgoal (ID 659)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  a_lt_b : a < b'.+1
  ============================
  P (f b') = false

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


      apply negbTE.

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

1 subgoal (ID 660)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  a_lt_b : a < b'.+1
  ============================
  ~~ P (f b')

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


      apply (NOT_SAT b').

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

1 subgoal (ID 661)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b' : nat
  IND : (forall x : nat, a <= x < b' -> ~~ P (f x)) -> search_arg a b' = None
  NOT_SAT : forall x : nat, a <= x < b'.+1 -> ~~ P (f x)
  a_lt_b : a < b'.+1
  ============================
  a <= b' < b'.+1

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


        by apply /andP; split.

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

No more subgoals.

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


    }

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

No more subgoals.

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


  Qed.

  (* Conversely, if we know that [f] satisfies [P] for at least one point in
     the search space, then [search_arg] yields some point. *)

  Lemma search_arg_not_none:
     a b,
      ( x, (a x < b) P (f x))
       y, search_arg a b = Some y.

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

1 subgoal (ID 52)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  ============================
  forall a b : nat,
  (exists x : nat, a <= x < b /\ P (f x)) ->
  exists y : nat, search_arg a b = Some y

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


  Proof.
    movea b H_exists.

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

1 subgoal (ID 55)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  H_exists : exists x : nat, a <= x < b /\ P (f x)
  ============================
  exists y : nat, search_arg a b = Some y

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


    destruct (search_arg a b) eqn:SEARCH; first by n.

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

1 subgoal (ID 69)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  H_exists : exists x : nat, a <= x < b /\ P (f x)
  SEARCH : search_arg a b = None
  ============================
  exists y : nat, None = Some y

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


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

1 subgoal (ID 73)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  H_exists : exists x : nat, a <= x < b /\ P (f x)
  ============================
  search_arg a b = None -> exists y : nat, None = Some y

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


rewrite search_arg_noneNOT_exists.

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

1 subgoal (ID 99)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  H_exists : exists x : nat, a <= x < b /\ P (f x)
  NOT_exists : forall x : nat, a <= x < b -> ~~ P (f x)
  ============================
  exists y : nat, None = Some y

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


    exfalso.

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

1 subgoal (ID 100)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  H_exists : exists x : nat, a <= x < b /\ P (f x)
  NOT_exists : forall x : nat, a <= x < b -> ~~ P (f x)
  ============================
  False

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


    move: H_exists ⇒ [x [RANGE Pfx]].

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

1 subgoal (ID 123)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b : nat
  NOT_exists : forall x : nat, a <= x < b -> ~~ P (f x)
  x : nat
  RANGE : a <= x < b
  Pfx : P (f x)
  ============================
  False

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


    by move: (NOT_exists x RANGE) ⇒ /negP not_Pfx.

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

No more subgoals.

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


  Qed.

  (* Since [search_arg] considers only points at which [f] satisfies [P], if it
     returns a point, then that point satisfies [P]. *)

  Lemma search_arg_pred:
     a b x,
      search_arg a b = Some x P (f x).

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

1 subgoal (ID 60)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  ============================
  forall a b x : nat, search_arg a b = Some x -> P (f x)

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


  Proof.
    movea b x.

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

1 subgoal (ID 63)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b, x : nat
  ============================
  search_arg a b = Some x -> P (f x)

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


    elim: b ⇒ [| n IND]; first by rewrite /search_arg // ifN.

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

1 subgoal (ID 74)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> P (f x)
  ============================
  search_arg a n.+1 = Some x -> P (f x)

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


    rewrite /search_arg -/search_arg.

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

1 subgoal (ID 101)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> P (f x)
  ============================
  (if a < n.+1
   then
    match search_arg a n with
    | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
    | None => if P (f n) then Some n else None
    end
   else None) = Some x -> P (f x)

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


    destruct (a < n.+1) eqn:a_lt_Sn; last by trivial.

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

1 subgoal (ID 113)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> P (f x)
  a_lt_Sn : (a < n.+1) = true
  ============================
  match search_arg a n with
  | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
  | None => if P (f n) then Some n else None
  end = Some x -> P (f x)

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


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

1 subgoal (ID 141)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> P (f x)
  ============================
  (a < n.+1) = true ->
  match search_arg a n with
  | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
  | None => if P (f n) then Some n else None
  end = Some x -> P (f x)

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


rewrite ltnSa_lt_Sn.

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

1 subgoal (ID 146)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> P (f x)
  a_lt_Sn : (a <= n) = true
  ============================
  match search_arg a n with
  | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
  | None => if P (f n) then Some n else None
  end = Some x -> P (f x)

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


    destruct (search_arg a n) as [q|] eqn:REC;
      destruct (P (f n)) eqn:Pfn ⇒ //=;
      [elim: (R (f n) (f q)) ⇒ // |];
      by movex_is; injection x_is ⇒ <-.

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

No more subgoals.

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


  Qed.

  (* Since [search_arg] considers only points within a given range, if it
     returns a point, then that point lies within the given range. *)

  Lemma search_arg_in_range:
     a b x,
      search_arg a b = Some x a x < b.

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

1 subgoal (ID 68)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  ============================
  forall a b x : nat, search_arg a b = Some x -> a <= x < b

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


  Proof.
    movea b x.

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

1 subgoal (ID 71)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, b, x : nat
  ============================
  search_arg a b = Some x -> a <= x < b

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


    elim: b ⇒ [| n IND]; first by rewrite /search_arg // ifN.

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

1 subgoal (ID 82)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> a <= x < n
  ============================
  search_arg a n.+1 = Some x -> a <= x < n.+1

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


    rewrite /search_arg -/search_arg.

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

1 subgoal (ID 109)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> a <= x < n
  ============================
  (if a < n.+1
   then
    match search_arg a n with
    | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
    | None => if P (f n) then Some n else None
    end
   else None) = Some x -> a <= x < n.+1

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


    destruct (a < n.+1) eqn:a_lt_Sn; last by trivial.

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

1 subgoal (ID 121)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> a <= x < n
  a_lt_Sn : (a < n.+1) = true
  ============================
  match search_arg a n with
  | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
  | None => if P (f n) then Some n else None
  end = Some x -> a <= x < n.+1

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


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

1 subgoal (ID 149)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> a <= x < n
  ============================
  (a < n.+1) = true ->
  match search_arg a n with
  | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
  | None => if P (f n) then Some n else None
  end = Some x -> a <= x < n.+1

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


rewrite ltnSa_lt_Sn.

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

1 subgoal (ID 154)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  IND : search_arg a n = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  ============================
  match search_arg a n with
  | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
  | None => if P (f n) then Some n else None
  end = Some x -> a <= x < n.+1

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


    destruct (search_arg a n) as [q|] eqn:REC;
      elim: (P (f n)) ⇒ //=.

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

3 subgoals (ID 187)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n, q : nat
  REC : search_arg a n = Some q
  IND : Some q = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  ============================
  (if R (f n) (f q) then Some n else Some q) = Some x -> a <= x < n.+1

subgoal 2 (ID 212) is:
 Some q = Some x -> a <= x < n.+1
subgoal 3 (ID 244) is:
 Some n = Some x -> a <= x < n.+1

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


    - elim: (R (f n) (f q)) ⇒ //= x_is;
        first by injection x_is ⇒ <-; apply /andP; split.

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

3 subgoals (ID 352)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n, q : nat
  REC : search_arg a n = Some q
  IND : Some q = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  x_is : Some q = Some x
  ============================
  a <= x < n.+1

subgoal 2 (ID 212) is:
 Some q = Some x -> a <= x < n.+1
subgoal 3 (ID 244) is:
 Some n = Some x -> a <= x < n.+1

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


      move: (IND x_is) ⇒ /andP [a_le_x x_lt_n].

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

3 subgoals (ID 426)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n, q : nat
  REC : search_arg a n = Some q
  IND : Some q = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  x_is : Some q = Some x
  a_le_x : a <= x
  x_lt_n : x < n
  ============================
  a <= x < n.+1

subgoal 2 (ID 212) is:
 Some q = Some x -> a <= x < n.+1
subgoal 3 (ID 244) is:
 Some n = Some x -> a <= x < n.+1

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


      apply /andP; split ⇒ //.

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

3 subgoals (ID 453)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n, q : nat
  REC : search_arg a n = Some q
  IND : Some q = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  x_is : Some q = Some x
  a_le_x : a <= x
  x_lt_n : x < n
  ============================
  x < n.+1

subgoal 2 (ID 212) is:
 Some q = Some x -> a <= x < n.+1
subgoal 3 (ID 244) is:
 Some n = Some x -> a <= x < n.+1

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


      by rewrite ltnS ltnW.

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

2 subgoals (ID 212)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n, q : nat
  REC : search_arg a n = Some q
  IND : Some q = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  ============================
  Some q = Some x -> a <= x < n.+1

subgoal 2 (ID 244) is:
 Some n = Some x -> a <= x < n.+1

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


    - movex_is.

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

2 subgoals (ID 486)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n, q : nat
  REC : search_arg a n = Some q
  IND : Some q = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  x_is : Some q = Some x
  ============================
  a <= x < n.+1

subgoal 2 (ID 244) is:
 Some n = Some x -> a <= x < n.+1

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


      move: (IND x_is) ⇒ /andP [a_le_x x_lt_n].

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

2 subgoals (ID 527)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n, q : nat
  REC : search_arg a n = Some q
  IND : Some q = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  x_is : Some q = Some x
  a_le_x : a <= x
  x_lt_n : x < n
  ============================
  a <= x < n.+1

subgoal 2 (ID 244) is:
 Some n = Some x -> a <= x < n.+1

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


      apply /andP; split ⇒ //.

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

2 subgoals (ID 554)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n, q : nat
  REC : search_arg a n = Some q
  IND : Some q = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  x_is : Some q = Some x
  a_le_x : a <= x
  x_lt_n : x < n
  ============================
  x < n.+1

subgoal 2 (ID 244) is:
 Some n = Some x -> a <= x < n.+1

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


      by rewrite ltnS ltnW.

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

1 subgoal (ID 244)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  REC : search_arg a n = None
  IND : None = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  ============================
  Some n = Some x -> a <= x < n.+1

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


    - movex_is.

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

1 subgoal (ID 587)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  a, x, n : nat
  REC : search_arg a n = None
  IND : None = Some x -> a <= x < n
  a_lt_Sn : (a <= n) = true
  x_is : Some n = Some x
  ============================
  a <= x < n.+1

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


      by injection x_is ⇒ <-; apply /andP; split.

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

No more subgoals.

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


  Qed.

  (* Let us assume that [R] is a reflexive and transitive total order... *)
  Hypothesis R_reflexive: reflexive R.
  Hypothesis R_transitive: transitive R.
  Hypothesis R_total: total R.

  (* ...then [search_arg] yields an extremum w.r.t. to [a, b), that is, if
     [search_arg] yields a point x, then [R (f x) (f y)] holds for any [y] in the
     search range [a, b) that satisfies [P]. *)

  Lemma search_arg_extremum:
     a b x,
      search_arg a b = Some x
       y,
        a y < b
        P (f y)
        R (f x) (f y).

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

1 subgoal (ID 80)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  ============================
  forall a b x : nat,
  search_arg a b = Some x ->
  forall y : nat, a <= y < b -> P (f y) -> R (f x) (f y)

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


  Proof.
    movea b x SEARCH.

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

1 subgoal (ID 84)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, b, x : nat
  SEARCH : search_arg a b = Some x
  ============================
  forall y : nat, a <= y < b -> P (f y) -> R (f x) (f y)

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


    elim: b x SEARCHn IND x; first by rewrite /search_arg.

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

1 subgoal (ID 103)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  ============================
  search_arg a n.+1 = Some x ->
  forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


    rewrite /search_arg -/search_arg.

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

1 subgoal (ID 132)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  ============================
  (if a < n.+1
   then
    match search_arg a n with
    | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
    | None => if P (f n) then Some n else None
    end
   else None) = Some x ->
  forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


    destruct (a < n.+1) eqn:a_lt_Sn; last by trivial.

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

1 subgoal (ID 144)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a < n.+1) = true
  ============================
  match search_arg a n with
  | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
  | None => if P (f n) then Some n else None
  end = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


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

1 subgoal (ID 181)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  ============================
  (a < n.+1) = true ->
  match search_arg a n with
  | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
  | None => if P (f n) then Some n else None
  end = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


rewrite ltnSa_lt_Sn.

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

1 subgoal (ID 186)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  ============================
  match search_arg a n with
  | Some x0 => if P (f n) && R (f n) (f x0) then Some n else Some x0
  | None => if P (f n) then Some n else None
  end = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


    destruct (search_arg a n) as [q|] eqn:REC;
      destruct (P (f n)) eqn:Pfn ⇒ //=.

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

3 subgoals (ID 227)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  ============================
  (if R (f n) (f q) then Some n else Some q) = Some x ->
  forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

subgoal 2 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 3 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


    - rewrite <- REC in IND.

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

3 subgoals (ID 364)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  ============================
  (if R (f n) (f q) then Some n else Some q) = Some x ->
  forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

subgoal 2 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 3 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


      destruct (R (f n) (f q)) eqn:RELsome_x_is;
        movey /andP [a_le_y y_lt_Sn] Pfy;
        injection some_x_isx_is; rewrite -{}x_is //;
        move: y_lt_Sn; rewrite ltnS;
        rewrite leq_eqVlt ⇒ /orP [/eqP EQ | y_lt_n].

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

6 subgoals (ID 611)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = true
  some_x_is : Some n = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  EQ : y = n
  ============================
  R (f n) (f y)

subgoal 2 (ID 612) is:
 R (f n) (f y)
subgoal 3 (ID 691) is:
 R (f q) (f y)
subgoal 4 (ID 692) is:
 R (f q) (f y)
subgoal 5 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 6 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


      + by rewrite EQ; apply (R_reflexive (f n)).

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

5 subgoals (ID 612)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = true
  some_x_is : Some n = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  ============================
  R (f n) (f y)

subgoal 2 (ID 691) is:
 R (f q) (f y)
subgoal 3 (ID 692) is:
 R (f q) (f y)
subgoal 4 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 5 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


      + apply (R_transitive (f q)) ⇒ //.

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

5 subgoals (ID 696)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = true
  some_x_is : Some n = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  ============================
  R (f q) (f y)

subgoal 2 (ID 691) is:
 R (f q) (f y)
subgoal 3 (ID 692) is:
 R (f q) (f y)
subgoal 4 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 5 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


        move: (IND q REC y) ⇒ HOLDS.

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

5 subgoals (ID 720)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = true
  some_x_is : Some n = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  HOLDS : a <= y < n -> P (f y) -> R (f q) (f y)
  ============================
  R (f q) (f y)

subgoal 2 (ID 691) is:
 R (f q) (f y)
subgoal 3 (ID 692) is:
 R (f q) (f y)
subgoal 4 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 5 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


        apply HOLDS ⇒ //.

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

5 subgoals (ID 721)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = true
  some_x_is : Some n = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  HOLDS : a <= y < n -> P (f y) -> R (f q) (f y)
  ============================
  a <= y < n

subgoal 2 (ID 691) is:
 R (f q) (f y)
subgoal 3 (ID 692) is:
 R (f q) (f y)
subgoal 4 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 5 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


        by apply /andP; split.

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

4 subgoals (ID 691)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = false
  some_x_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  EQ : y = n
  ============================
  R (f q) (f y)

subgoal 2 (ID 692) is:
 R (f q) (f y)
subgoal 3 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 4 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


      + rewrite EQ.

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

4 subgoals (ID 773)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = false
  some_x_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  EQ : y = n
  ============================
  R (f q) (f n)

subgoal 2 (ID 692) is:
 R (f q) (f y)
subgoal 3 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 4 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


        move: (R_total (f q) (f n)) ⇒ /orP [R_qn | R_nq] //.

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

4 subgoals (ID 839)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = false
  some_x_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  EQ : y = n
  R_nq : R (f n) (f q)
  ============================
  R (f q) (f n)

subgoal 2 (ID 692) is:
 R (f q) (f y)
subgoal 3 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 4 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


        by move: REL ⇒ /negP.

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

3 subgoals (ID 692)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = false
  some_x_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  ============================
  R (f q) (f y)

subgoal 2 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 3 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


      + move: (IND q REC y) ⇒ HOLDS.

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

3 subgoals (ID 904)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = false
  some_x_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  HOLDS : a <= y < n -> P (f y) -> R (f q) (f y)
  ============================
  R (f q) (f y)

subgoal 2 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 3 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


        apply HOLDS ⇒ //.

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

3 subgoals (ID 905)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        search_arg a n = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  REL : R (f n) (f q) = false
  some_x_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  HOLDS : a <= y < n -> P (f y) -> R (f q) (f y)
  ============================
  a <= y < n

subgoal 2 (ID 258) is:
 Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 3 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


        by apply /andP; split.

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

2 subgoals (ID 258)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = false
  ============================
  Some q = Some x ->
  forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

subgoal 2 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


    - movesome_q_is y /andP [a_le_y y_lt_Sn] Pfy.

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

2 subgoals (ID 998)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = false
  some_q_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  y_lt_Sn : y < n.+1
  Pfy : P (f y)
  ============================
  R (f x) (f y)

subgoal 2 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


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

2 subgoals (ID 1000)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = false
  some_q_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  ============================
  y < n.+1 -> R (f x) (f y)

subgoal 2 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


rewrite ltnS.

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

2 subgoals (ID 1004)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = false
  some_q_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  ============================
  y <= n -> R (f x) (f y)

subgoal 2 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


      rewrite leq_eqVlt ⇒ /orP [/eqP EQ | y_lt_n].

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

3 subgoals (ID 1083)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = false
  some_q_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  EQ : y = n
  ============================
  R (f x) (f y)

subgoal 2 (ID 1084) is:
 R (f x) (f y)
subgoal 3 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


      + exfalso.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 1085)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = false
  some_q_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  EQ : y = n
  ============================
  False

subgoal 2 (ID 1084) is:
 R (f x) (f y)
subgoal 3 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


move: Pfn ⇒ /negP Pfn.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 1127)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  some_q_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  EQ : y = n
  Pfn : ~ P (f n)
  ============================
  False

subgoal 2 (ID 1084) is:
 R (f x) (f y)
subgoal 3 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


by subst.

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

2 subgoals (ID 1084)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = false
  some_q_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  ============================
  R (f x) (f y)

subgoal 2 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


      + apply IND ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1162)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n, q : nat
  REC : search_arg a n = Some q
  IND : forall x : nat,
        Some q = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = false
  some_q_is : Some q = Some x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  ============================
  a <= y < n

subgoal 2 (ID 302) is:
 Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


by apply /andP; split.

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

1 subgoal (ID 302)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  REC : search_arg a n = None
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  ============================
  Some n = Some x ->
  forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


    - movesome_n_is.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1213)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  REC : search_arg a n = None
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  ============================
  forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


injection some_n_isn_is.

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

1 subgoal (ID 1216)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  REC : search_arg a n = None
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  ============================
  forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)

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


      movey /andP [a_le_y y_lt_Sn] Pfy.

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

1 subgoal (ID 1258)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  REC : search_arg a n = None
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  y_lt_Sn : y < n.+1
  Pfy : P (f y)
  ============================
  R (f x) (f y)

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


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

1 subgoal (ID 1260)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  REC : search_arg a n = None
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  ============================
  y < n.+1 -> R (f x) (f y)

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


rewrite ltnS.

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

1 subgoal (ID 1264)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  REC : search_arg a n = None
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  ============================
  y <= n -> R (f x) (f y)

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


      rewrite leq_eqVlt ⇒ /orP [/eqP EQ | y_lt_n].

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

2 subgoals (ID 1343)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  REC : search_arg a n = None
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  EQ : y = n
  ============================
  R (f x) (f y)

subgoal 2 (ID 1344) is:
 R (f x) (f y)

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


      + by rewrite -n_is EQ; apply (R_reflexive (f n)).

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

1 subgoal (ID 1344)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  REC : search_arg a n = None
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  ============================
  R (f x) (f y)

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


      + exfalso.

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

1 subgoal (ID 1349)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  REC : search_arg a n = None
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  ============================
  False

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


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

1 subgoal (ID 1351)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  ============================
  search_arg a n = None -> False

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


rewrite search_arg_noneNONE.

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

1 subgoal (ID 1376)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  NONE : forall x : nat, a <= x < n -> ~~ P (f x)
  ============================
  False

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


        move: (NONE y) ⇒ not_Pfy.

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

1 subgoal (ID 1378)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  NONE : forall x : nat, a <= x < n -> ~~ P (f x)
  not_Pfy : a <= y < n -> ~~ P (f y)
  ============================
  False

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


        feed not_Pfy; first by apply /andP; split.

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

1 subgoal (ID 1384)
  
  T : Type
  f : nat -> T
  P : pred T
  R : rel T
  R_reflexive : reflexive (T:=T) R
  R_transitive : transitive (T:=T) R
  R_total : total (T:=T) R
  a, n : nat
  IND : forall x : nat,
        None = Some x ->
        forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
  x : nat
  a_lt_Sn : (a <= n) = true
  Pfn : P (f n) = true
  some_n_is : Some n = Some x
  n_is : n = x
  y : nat
  a_le_y : a <= y
  Pfy : P (f y)
  y_lt_n : y < n
  NONE : forall x : nat, a <= x < n -> ~~ P (f x)
  not_Pfy : ~~ P (f y)
  ============================
  False

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


        by move: not_Pfy ⇒ /negP.

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

No more subgoals.

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


  Qed.

End ArgSearch.

Section ExMinn.

  (* We show that the fact that the minimal satisfying argument [ex_minn ex] of 
     a predicate [pred] satisfies another predicate [P] implies the existence
     of a minimal element that satisfies both [pred] and [P]. *)

  Lemma prop_on_ex_minn:
     (P : nat Prop) (pred : nat bool) (ex : n, pred n),
      P (ex_minn ex)
       n, P n pred n ( n', pred n' n n').

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

1 subgoal (ID 24)
  
  ============================
  forall (P : nat -> Prop) (pred : nat -> bool) (ex : exists n : nat, pred n),
  P (ex_minn (P:=pred) ex) ->
  exists n : nat, P n /\ pred n /\ (forall n' : nat, pred n' -> n <= n')

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


  Proof.
    intros.

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

1 subgoal (ID 28)
  
  P : nat -> Prop
  pred : nat -> bool
  ex : exists n : nat, pred n
  H : P (ex_minn (P:=pred) ex)
  ============================
  exists n : nat, P n /\ pred n /\ (forall n' : nat, pred n' -> n <= n')

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


     (ex_minn ex); repeat split; auto.

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

2 subgoals (ID 36)
  
  P : nat -> Prop
  pred : nat -> bool
  ex : exists n : nat, pred n
  H : P (ex_minn (P:=pred) ex)
  ============================
  pred (ex_minn (P:=pred) ex)

subgoal 2 (ID 37) is:
 forall n' : nat, pred n' -> ex_minn (P:=pred) ex <= n'

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


    all: have MIN := ex_minnP ex; move: MIN ⇒ [n Pn MIN]; auto.

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

No more subgoals.

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


  Qed.

  (* As a corollary, we show that if there is a constant [c] such 
     that [P c], then the minimal satisfying argument [ex_minn ex] 
     of a predicate [P] is less than or equal to [c]. *)

  Corollary ex_minn_le_ex:
     (P : nat bool) (exP : n, P n) (c : nat),
      P c
      ex_minn exP c.

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

1 subgoal (ID 28)
  
  ============================
  forall (P : nat -> bool) (exP : exists n : nat, P n) (c : nat),
  P c -> ex_minn (P:=P) exP <= c

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


  Proof.
    intros ? ? ? EX.

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

1 subgoal (ID 32)
  
  P : nat -> bool
  exP : exists n : nat, P n
  c : nat
  EX : P c
  ============================
  ex_minn (P:=P) exP <= c

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


    rewrite leqNgt; apply/negP; intros GT.

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

1 subgoal (ID 58)
  
  P : nat -> bool
  exP : exists n : nat, P n
  c : nat
  EX : P c
  GT : c < ex_minn (P:=P) exP
  ============================
  False

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


    pattern (ex_minn (P:=P) exP) in GT;
      apply prop_on_ex_minn in GT; move: GT ⇒ [n [LT [Pn MIN]]].

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

1 subgoal (ID 94)
  
  P : nat -> bool
  exP : exists n : nat, P n
  c : nat
  EX : P c
  n : nat
  LT : c < n
  Pn : P n
  MIN : forall n' : nat, P n' -> n <= n'
  ============================
  False

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


    specialize (MIN c EX).

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

1 subgoal (ID 96)
  
  P : nat -> bool
  exP : exists n : nat, P n
  c : nat
  EX : P c
  n : nat
  LT : c < n
  Pn : P n
  MIN : n <= c
  ============================
  False

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


      by move: MIN; rewrite leqNgt; move ⇒ /negP MIN; apply: MIN.

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

No more subgoals.

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


  Qed.

End ExMinn.