Library rt.util.search_arg
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
From rt.util Require Import 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
| 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:
∀ 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)
----------------------------------------------------------------------------- *)
- move⇒ x /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_arg ⇒ IND 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 IND ⇒ x /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.
move⇒ a 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_none ⇒ NOT_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.
move⇒ a 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 ltnS ⇒ a_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 move⇒ x_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.
move⇒ a 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 ltnS ⇒ a_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
----------------------------------------------------------------------------- *)
- move ⇒ x_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
----------------------------------------------------------------------------- *)
- move ⇒ x_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.
move⇒ a 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 SEARCH ⇒ n 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 ltnS ⇒ a_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: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].
(* ----------------------------------[ coqtop ]---------------------------------
6 subgoals (ID 619)
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 620) is:
R (f n) (f y)
subgoal 3 (ID 699) is:
R (f q) (f y)
subgoal 4 (ID 700) 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 620)
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 699) is:
R (f q) (f y)
subgoal 3 (ID 700) 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 704)
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 699) is:
R (f q) (f y)
subgoal 3 (ID 700) 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 728)
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 699) is:
R (f q) (f y)
subgoal 3 (ID 700) 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 729)
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 699) is:
R (f q) (f y)
subgoal 3 (ID 700) 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 699)
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 700) 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 781)
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 700) 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 847)
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 700) 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 700)
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 912)
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 913)
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)
----------------------------------------------------------------------------- *)
- move⇒ some_q_is y [/andP [a_le_y y_lt_Sn] Pfy].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1010)
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 1012)
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 1016)
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 1095)
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 1096) 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 1097)
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 1096) 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 1139)
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 1096) 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 1096)
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 1174)
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)
----------------------------------------------------------------------------- *)
- move⇒ some_n_is.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1225)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1228)
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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1274)
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 1276)
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 1280)
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 1359)
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 1360) is:
R (f x) (f y)
----------------------------------------------------------------------------- *)
+ by rewrite -n_is EQ; apply (R_reflexive (f n)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1360)
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 1365)
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 1367)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1392)
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 1394)
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 1400)
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.