From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export mathcomp.zify.zify.
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
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.
*)


(** First, we show that, given an interval <<[t1, t2)>> and a
    predicate [P], either no element in the interval satisfy [P] or
    there is an element that satisfies [P]. *)
Lemma earliest_pred_element_exists_case :
  forall (P : pred nat) (t1 t2 : nat),
    (forall t, t1 <= t < t2 -> ~~ P t)
    \/ (exists t,
          t1 <= t < t2
          /\ P t
          /\ forall t', t1 <= t' -> P t' -> t <= t').
forall (P : pred nat) (t1 t2 : nat),
(forall t : nat, t1 <= t < t2 -> ~~ P t) \/
(exists t : nat,
   t1 <= t < t2 /\
   P t /\
   (forall t' : nat, t1 <= t' -> P t' -> t <= t'))
Proof.
forall (P : pred nat) (t1 t2 : nat),
(forall t : nat, t1 <= t < t2 -> ~~ P t) \/
(exists t : nat,
   t1 <= t < t2 /\
   P t /\
   (forall t' : nat, t1 <= t' -> P t' -> t <= t'))
  move=> P t1 t2.
P: pred nat
t1, t2: nat
(forall t : nat, t1 <= t < t2 -> ~~ P t) \/
(exists t : nat,
   t1 <= t < t2 /\
   P t /\
   (forall t' : nat, t1 <= t' -> P t' -> t <= t'))
  have [/allP ALL|/allPn [x /[!mem_index_iota] IN /negPn Px]]:=
    boolP(all (fun x => ~~ P x) (index_iota t1 t2)).
P: pred nat
t1, t2: nat
ALL: {in index_iota t1 t2,
 forall x : Datatypes_nat__canonical__eqtype_Equality, ~~ P x}
(forall t : nat, t1 <= t < t2 -> ~~ P t) \/
(exists t : nat,
   t1 <= t < t2 /\
   P t /\
   (forall t' : nat, t1 <= t' -> P t' -> t <= t'))
P: pred nat
t1, t2: nat
x: Datatypes_nat__canonical__eqtype_Equality
IN: t1 <= x < t2
Px: P x
(forall t : nat, t1 <= t < t2 -> ~~ P t) \/
(exists t : nat,
   t1 <= t < t2 /\
   P t /\
   (forall t' : nat, t1 <= t' -> P t' -> t <= t'))
  {
P: pred nat
t1, t2: nat
ALL: {in index_iota t1 t2,
 forall x : Datatypes_nat__canonical__eqtype_Equality, ~~ P x}
(forall t : nat, t1 <= t < t2 -> ~~ P t) \/
(exists t : nat,
   t1 <= t < t2 /\
   P t /\
   (forall t' : nat, t1 <= t' -> P t' -> t <= t')) by left => t IN; apply: ALL; rewrite mem_index_iota. }
P: pred nat
t1, t2: nat
x: Datatypes_nat__canonical__eqtype_Equality
IN: t1 <= x < t2
Px: P x
(forall t : nat, t1 <= t < t2 -> ~~ P t) \/
(exists t : nat,
   t1 <= t < t2 /\
   P t /\
   (forall t' : nat, t1 <= t' -> P t' -> t <= t'))
  {
P: pred nat
t1, t2: nat
x: Datatypes_nat__canonical__eqtype_Equality
IN: t1 <= x < t2
Px: P x
(forall t : nat, t1 <= t < t2 -> ~~ P t) \/
(exists t : nat,
   t1 <= t < t2 /\
   P t /\
   (forall t' : nat, t1 <= t' -> P t' -> t <= t')) right.
P: pred nat
t1, t2: nat
x: Datatypes_nat__canonical__eqtype_Equality
IN: t1 <= x < t2
Px: P x
exists t : nat,
  t1 <= t < t2 /\
  P t /\
  (forall t' : nat, t1 <= t' -> P t' -> t <= t')
    have EX : exists n : nat, (t1 <= n < t2) && P n
        by exists x; apply/andP; split.
P: pred nat
t1, t2: nat
x: Datatypes_nat__canonical__eqtype_Equality
IN: t1 <= x < t2
Px: P x
EX: exists n : nat, (t1 <= n < t2) && P n
exists t : nat,
  t1 <= t < t2 /\
  P t /\
  (forall t' : nat, t1 <= t' -> P t' -> t <= t')
    have [x' /andP [IN' Px'] MIN] := (ex_minnP EX).
P: pred nat
t1, t2: nat
x: Datatypes_nat__canonical__eqtype_Equality
IN: t1 <= x < t2
Px: P x
EX: exists n : nat, (t1 <= n < t2) && P n
x': nat
IN': t1 <= x' < t2
Px': P x'
MIN: forall n : nat, (t1 <= n < t2) && P n -> x' <= n
exists t : nat,
  t1 <= t < t2 /\
  P t /\
  (forall t' : nat, t1 <= t' -> P t' -> t <= t')
    exists x'; (repeat split) => // t' LT Pt'.
P: pred nat
t1, t2: nat
x: Datatypes_nat__canonical__eqtype_Equality
IN: t1 <= x < t2
Px: P x
EX: exists n : nat, (t1 <= n < t2) && P n
x': nat
IN': t1 <= x' < t2
Px': P x'
MIN: forall n : nat, (t1 <= n < t2) && P n -> x' <= n
t': nat
LT: t1 <= t'
Pt': P t'
x' <= t'
    have [NEQ1|NEQ2] := leqP t2 t'; first by lia.
P: pred nat
t1, t2: nat
x: Datatypes_nat__canonical__eqtype_Equality
IN: t1 <= x < t2
Px: P x
EX: exists n : nat, (t1 <= n < t2) && P n
x': nat
IN': t1 <= x' < t2
Px': P x'
MIN: forall n : nat, (t1 <= n < t2) && P n -> x' <= n
t': nat
LT: t1 <= t'
Pt': P t'
NEQ2: t' < t2
x' <= t'
    by apply: MIN; repeat(apply/andP; split => //). }
Qed.

(** Next, we proceed to the function [search_arg]. *)
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
                | None => if P (f b') then Some b' else None
                | Some x => if 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:
    forall a b,
      search_arg a b = None <-> forall x, a <= x < b -> ~~ P (f x).
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.
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))
    move=> a b; split.
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)
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
    { (* if *)
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)
      elim: b => [ _ | b' HYP]; first by move=> _ /andP [_ FALSE] //.
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.
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].
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)
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)
      -
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) move: HYP.
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) case: (search_arg a b') => [y | HYP NIL x].
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)
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)
        +
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) case: (P (f b') && R (f b') (f y)) => //.
        +
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) move=> /andP[a_le_x x_lt_b'].
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)
          move: x_lt_b'.
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)
          rewrite ltnS leq_eqVlt => /orP [/eqP EQ|LT].
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)
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)
          *
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) rewrite EQ.
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')
            move: NIL.
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') case: (P (f b')) => //.
          *
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) feed HYP => //.
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)
            apply: (HYP x).
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'
            by apply /andP; split.
      -
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) move=> x /andP [a_le_x b_lt_b'].
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.
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'.
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.
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').
    }
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 *)
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
      rewrite /search_arg.
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 (a b : nat) {struct b} : option nat :=
   if a < b
   then
    match b with
    | 0 => None
    | 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
    end
   else None) a b = None
      elim: b  => [//|b'].
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 (a b : nat) {struct b} :
      option nat :=
    if a < b
    then
     match b with
     | 0 => None
     | 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
     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 (a b : nat) {struct b} :
         option nat :=
       if a < b
       then
        match b with
        | 0 => None
        | 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
        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_arg => IND  NOT_SAT.
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.
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
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
      {
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 IND => x /andP [a_le_x x_lt_n].
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).
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
        by apply /andP; split.
      }
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 | //].
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.
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.
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').
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.
    }
  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:
    forall a b,
      (exists x, (a <= x < b) /\ P (f x)) ->
      exists y, search_arg a b = Some y.
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.
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
    move=> a b H_exists.
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) as [n|] eqn:SEARCH; first by exists n.
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.
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_none => NOT_exists.
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.
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]].
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.
  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:
    forall a b x,
      search_arg a b = Some x -> P (f x).
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.
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)
    move=> a b x.
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.
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.
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 x =>
      if P (f n) && R (f n) (f x)
      then Some n
      else Some x
  | 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.
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 x =>
    if P (f n) && R (f n) (f x)
    then Some n
    else Some x
| None => if P (f n) then Some n else None
end = Some x -> P (f x)
    move: a_lt_Sn.
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 x =>
    if P (f n) && R (f n) (f x)
    then Some n
    else Some x
| None => if P (f n) then Some n else None
end = Some x -> P (f x) rewrite ltnS => a_lt_Sn.
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 x =>
    if P (f n) && R (f n) (f x)
    then Some n
    else Some x
| 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 move=> x_is; injection x_is => <-.
  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:
    forall a b x,
      search_arg a b = Some x -> a <= x < b.
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.
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
    move=> a b x.
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.
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.
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 x =>
      if P (f n) && R (f n) (f x)
      then Some n
      else Some x
  | 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.
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 x =>
    if P (f n) && R (f n) (f x)
    then Some n
    else Some x
| None => if P (f n) then Some n else None
end = Some x -> a <= x < n.+1
    move: a_lt_Sn.
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 x =>
    if P (f n) && R (f n) (f x)
    then Some n
    else Some x
| None => if P (f n) then Some n else None
end = Some x -> a <= x < n.+1 rewrite ltnS => a_lt_Sn.
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 x =>
    if P (f n) && R (f n) (f x)
    then Some n
    else Some x
| 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)) => //=.
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
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
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
    -
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 elim: (R (f n) (f q)) => //= x_is;
        first by injection x_is => <-; apply /andP; split.
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
      move: (IND x_is) => /andP [a_le_x x_lt_n].
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
      by apply /andP; split.
    -
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 move => x_is.
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
      move: (IND x_is) => /andP [a_le_x x_lt_n].
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
      by apply /andP; split.
    -
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 move => x_is.
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.
  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:
    forall a b x,
      search_arg a b = Some x ->
      forall y,
        a <= y < b ->
        P (f y) ->
        R (f x) (f y).
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.
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)
    move=> a b x SEARCH.
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 SEARCH => n IND x; first by rewrite /search_arg.
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.
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 x =>
      if P (f n) && R (f n) (f x)
      then Some n
      else Some x
  | 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.
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 x =>
    if P (f n) && R (f n) (f x)
    then Some n
    else Some x
| 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.
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 x =>
    if P (f n) && R (f n) (f x)
    then Some n
    else Some x
| 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 ltnS => a_lt_Sn.
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 x =>
    if P (f n) && R (f n) (f x)
    then Some n
    else Some x
| 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 => //=.
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)
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)
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)
    -
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) rewrite <- REC in IND.
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)
      destruct (R (f n) (f q)) eqn:REL => some_x_is;
        move=> y /andP [a_le_y y_lt_Sn] Pfy;
        injection some_x_is => x_is; rewrite -{}x_is //;
        move: y_lt_Sn; rewrite ltnS;
        rewrite leq_eqVlt => /orP [/eqP EQ | y_lt_n].
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)
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)
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)
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)
      +
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) by rewrite EQ; apply (R_reflexive (f n)).
      +
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) apply (R_transitive (f q)) => //.
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)
        move: (IND q REC y) => HOLDS.
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)
        apply HOLDS => //.
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
        by apply /andP; split.
      +
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) rewrite EQ.
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)
        move: (R_total (f q) (f n)) => /orP [R_qn | R_nq] //.
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)
        by move: REL => /negP.
      +
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) move: (IND q REC y) => HOLDS.
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)
        apply HOLDS => //.
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
        by apply /andP; split.
    -
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) move=> some_q_is y /andP [a_le_y y_lt_Sn] Pfy.
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)
      move: y_lt_Sn.
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) rewrite ltnS.
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)
      rewrite leq_eqVlt => /orP [/eqP EQ | y_lt_n].
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)
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)
      +
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) exfalso.
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 move: Pfn => /negP Pfn.
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 by subst.
      +
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) apply IND => //.
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 by apply /andP; split.
    -
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) move=> some_n_is.
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_is => n_is.
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)
      move=> y /andP [a_le_y y_lt_Sn] Pfy.
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.
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.
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].
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)
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)
      +
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) by rewrite -n_is EQ; apply (R_reflexive (f n)).
      +
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.
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.
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_none => NONE.
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.
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.
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.
  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:
    forall (P : nat -> Prop) (pred : nat -> bool) (ex : exists n, pred n),
      P (ex_minn ex) ->
      exists n, P n /\ pred n /\ (forall n', pred n' -> n <= n').
forall (P : nat -> Prop) (pred : nat -> bool)
  (ex0 : exists n : nat, pred n),
P (ex_minn (P:=pred) ex0) ->
exists n : nat,
  P n /\
  pred n /\ (forall n' : nat, pred n' -> n <= n')
  Proof.
forall (P : nat -> Prop) (pred : nat -> bool)
  (ex0 : exists n : nat, pred n),
P (ex_minn (P:=pred) ex0) ->
exists n : nat,
  P n /\
  pred n /\ (forall n' : nat, pred n' -> n <= n')
    move=> P pred ex.
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')
    exists (ex_minn ex); repeat split; auto.
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)
P: nat -> Prop
pred: nat -> bool
ex: exists n : nat, pred n
H: P (ex_minn (P:=pred) ex)
forall n' : nat, pred n' -> ex_minn (P:=pred) ex <= n'
    all: have MIN := ex_minnP ex; move: MIN => [n Pn MIN]; auto.
  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:
    forall (P : nat -> bool) (exP : exists n, P n) (c : nat),
      P c -> 
      ex_minn exP <= c.
forall (P : nat -> bool) (exP : exists n : nat, P n)
  (c : nat), P c -> ex_minn (P:=P) exP <= c
  Proof.
forall (P : nat -> bool) (exP : exists n : nat, P n)
  (c : nat), P c -> ex_minn (P:=P) exP <= c
    move=> P exP c EX.
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.
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]]].
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).
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.
  Qed.
  
End ExMinn.