Library prosa.util.search_arg
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
Require Import prosa.util.tactics.
This file introduces a function called [search_arg] that allows finding the
argument within a given range for which a function is minimal w.r.t. to a
given order while satisfying a given predicate, along with lemmas
establishing the basic properties of [search_arg].
Note that while this is quite similar to [arg min ...] / [arg max ...] in
[ssreflect] ([fintype]), this function is subtly different in that it possibly
returns None and that it does not require the last element in the given
range to satisfy the predicate. In contrast, [ssreflect]'s notion of
extremum in [fintype] uses the upper bound of the search space as the
default value, which is rather unnatural when searching through a schedule.
Section ArgSearch.
(* Given a function [f] that maps the naturals to elements of type [T]... *)
Context {T : Type}.
Variable f: nat → T.
(* ... a predicate [P] on [T] ... *)
Variable P: pred T.
(* ... and an order [R] on [T] ... *)
Variable R: rel T.
(* ... we define the procedure [search_arg] to iterate a given search space
[a, b), while checking each element whether [f] satisfies [P] at that
point and returning the extremum as defined by [R]. *)
Fixpoint search_arg (a b : nat) : option nat :=
if a < b then
match b with
| 0 ⇒ None
| S b' ⇒ match search_arg a b' with
| 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 611)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = true
some_x_is : Some n = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
EQ : y = n
============================
R (f n) (f y)
subgoal 2 (ID 612) is:
R (f n) (f y)
subgoal 3 (ID 691) is:
R (f q) (f y)
subgoal 4 (ID 692) is:
R (f q) (f y)
subgoal 5 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 6 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
+ by rewrite EQ; apply (R_reflexive (f n)).
(* ----------------------------------[ coqtop ]---------------------------------
5 subgoals (ID 612)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = true
some_x_is : Some n = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
============================
R (f n) (f y)
subgoal 2 (ID 691) is:
R (f q) (f y)
subgoal 3 (ID 692) is:
R (f q) (f y)
subgoal 4 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 5 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
+ apply (R_transitive (f q)) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
5 subgoals (ID 696)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = true
some_x_is : Some n = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
============================
R (f q) (f y)
subgoal 2 (ID 691) is:
R (f q) (f y)
subgoal 3 (ID 692) is:
R (f q) (f y)
subgoal 4 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 5 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
move: (IND q REC y) ⇒ HOLDS.
(* ----------------------------------[ coqtop ]---------------------------------
5 subgoals (ID 720)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = true
some_x_is : Some n = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
HOLDS : a <= y < n -> P (f y) -> R (f q) (f y)
============================
R (f q) (f y)
subgoal 2 (ID 691) is:
R (f q) (f y)
subgoal 3 (ID 692) is:
R (f q) (f y)
subgoal 4 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 5 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
apply HOLDS ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
5 subgoals (ID 721)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = true
some_x_is : Some n = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
HOLDS : a <= y < n -> P (f y) -> R (f q) (f y)
============================
a <= y < n
subgoal 2 (ID 691) is:
R (f q) (f y)
subgoal 3 (ID 692) is:
R (f q) (f y)
subgoal 4 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 5 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
by apply /andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 691)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = false
some_x_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
EQ : y = n
============================
R (f q) (f y)
subgoal 2 (ID 692) is:
R (f q) (f y)
subgoal 3 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 4 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
+ rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 773)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = false
some_x_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
EQ : y = n
============================
R (f q) (f n)
subgoal 2 (ID 692) is:
R (f q) (f y)
subgoal 3 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 4 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
move: (R_total (f q) (f n)) ⇒ /orP [R_qn | R_nq] //.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 839)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = false
some_x_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
EQ : y = n
R_nq : R (f n) (f q)
============================
R (f q) (f n)
subgoal 2 (ID 692) is:
R (f q) (f y)
subgoal 3 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 4 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
by move: REL ⇒ /negP.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 692)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = false
some_x_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
============================
R (f q) (f y)
subgoal 2 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 3 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
+ move: (IND q REC y) ⇒ HOLDS.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 904)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = false
some_x_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
HOLDS : a <= y < n -> P (f y) -> R (f q) (f y)
============================
R (f q) (f y)
subgoal 2 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 3 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
apply HOLDS ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 905)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
search_arg a n = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
REL : R (f n) (f q) = false
some_x_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
HOLDS : a <= y < n -> P (f y) -> R (f q) (f y)
============================
a <= y < n
subgoal 2 (ID 258) is:
Some q = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 3 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
by apply /andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 258)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
Some q = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = false
============================
Some q = Some x ->
forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
subgoal 2 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
- move⇒ some_q_is y /andP [a_le_y y_lt_Sn] Pfy.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 998)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
Some q = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = false
some_q_is : Some q = Some x
y : nat
a_le_y : a <= y
y_lt_Sn : y < n.+1
Pfy : P (f y)
============================
R (f x) (f y)
subgoal 2 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
move: y_lt_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1000)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
Some q = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = false
some_q_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
============================
y < n.+1 -> R (f x) (f y)
subgoal 2 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
rewrite ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1004)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
Some q = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = false
some_q_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
============================
y <= n -> R (f x) (f y)
subgoal 2 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
rewrite leq_eqVlt ⇒ /orP [/eqP EQ | y_lt_n].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1083)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
Some q = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = false
some_q_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
EQ : y = n
============================
R (f x) (f y)
subgoal 2 (ID 1084) is:
R (f x) (f y)
subgoal 3 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
+ exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1085)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
Some q = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = false
some_q_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
EQ : y = n
============================
False
subgoal 2 (ID 1084) is:
R (f x) (f y)
subgoal 3 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
move: Pfn ⇒ /negP Pfn.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1127)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
Some q = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
some_q_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
EQ : y = n
Pfn : ~ P (f n)
============================
False
subgoal 2 (ID 1084) is:
R (f x) (f y)
subgoal 3 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
by subst.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1084)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
Some q = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = false
some_q_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
============================
R (f x) (f y)
subgoal 2 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
+ apply IND ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1162)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n, q : nat
REC : search_arg a n = Some q
IND : forall x : nat,
Some q = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = false
some_q_is : Some q = Some x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
============================
a <= y < n
subgoal 2 (ID 302) is:
Some n = Some x -> forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
by apply /andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 302)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
REC : search_arg a n = None
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
============================
Some n = Some x ->
forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
- move⇒ some_n_is.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1213)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
REC : search_arg a n = None
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
============================
forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
injection some_n_is ⇒ n_is.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1216)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
REC : search_arg a n = None
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
============================
forall y : nat, a <= y < n.+1 -> P (f y) -> R (f x) (f y)
----------------------------------------------------------------------------- *)
move⇒ y /andP [a_le_y y_lt_Sn] Pfy.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1258)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
REC : search_arg a n = None
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
y_lt_Sn : y < n.+1
Pfy : P (f y)
============================
R (f x) (f y)
----------------------------------------------------------------------------- *)
move: y_lt_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1260)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
REC : search_arg a n = None
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
Pfy : P (f y)
============================
y < n.+1 -> R (f x) (f y)
----------------------------------------------------------------------------- *)
rewrite ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1264)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
REC : search_arg a n = None
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
Pfy : P (f y)
============================
y <= n -> R (f x) (f y)
----------------------------------------------------------------------------- *)
rewrite leq_eqVlt ⇒ /orP [/eqP EQ | y_lt_n].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1343)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
REC : search_arg a n = None
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
Pfy : P (f y)
EQ : y = n
============================
R (f x) (f y)
subgoal 2 (ID 1344) is:
R (f x) (f y)
----------------------------------------------------------------------------- *)
+ by rewrite -n_is EQ; apply (R_reflexive (f n)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1344)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
REC : search_arg a n = None
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
============================
R (f x) (f y)
----------------------------------------------------------------------------- *)
+ exfalso.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1349)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
REC : search_arg a n = None
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
============================
False
----------------------------------------------------------------------------- *)
move: REC.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1351)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
============================
search_arg a n = None -> False
----------------------------------------------------------------------------- *)
rewrite search_arg_none ⇒ NONE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1376)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
NONE : forall x : nat, a <= x < n -> ~~ P (f x)
============================
False
----------------------------------------------------------------------------- *)
move: (NONE y) ⇒ not_Pfy.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1378)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
NONE : forall x : nat, a <= x < n -> ~~ P (f x)
not_Pfy : a <= y < n -> ~~ P (f y)
============================
False
----------------------------------------------------------------------------- *)
feed not_Pfy; first by apply /andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1384)
T : Type
f : nat -> T
P : pred T
R : rel T
R_reflexive : reflexive (T:=T) R
R_transitive : transitive (T:=T) R
R_total : total (T:=T) R
a, n : nat
IND : forall x : nat,
None = Some x ->
forall y : nat, a <= y < n -> P (f y) -> R (f x) (f y)
x : nat
a_lt_Sn : (a <= n) = true
Pfn : P (f n) = true
some_n_is : Some n = Some x
n_is : n = x
y : nat
a_le_y : a <= y
Pfy : P (f y)
y_lt_n : y < n
NONE : forall x : nat, a <= x < n -> ~~ P (f x)
not_Pfy : ~~ P (f y)
============================
False
----------------------------------------------------------------------------- *)
by move: not_Pfy ⇒ /negP.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ArgSearch.
Section ExMinn.
(* We show that the fact that the minimal satisfying argument [ex_minn ex] of
a predicate [pred] satisfies another predicate [P] implies the existence
of a minimal element that satisfies both [pred] and [P]. *)
Lemma prop_on_ex_minn:
∀ (P : nat → Prop) (pred : nat → bool) (ex : ∃ n, pred n),
P (ex_minn ex) →
∃ n, P n ∧ pred n ∧ (∀ n', pred n' → n ≤ n').
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 24)
============================
forall (P : nat -> Prop) (pred : nat -> bool) (ex : exists n : nat, pred n),
P (ex_minn (P:=pred) ex) ->
exists n : nat, P n /\ pred n /\ (forall n' : nat, pred n' -> n <= n')
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
P : nat -> Prop
pred : nat -> bool
ex : exists n : nat, pred n
H : P (ex_minn (P:=pred) ex)
============================
exists n : nat, P n /\ pred n /\ (forall n' : nat, pred n' -> n <= n')
----------------------------------------------------------------------------- *)
∃ (ex_minn ex); repeat split; auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 36)
P : nat -> Prop
pred : nat -> bool
ex : exists n : nat, pred n
H : P (ex_minn (P:=pred) ex)
============================
pred (ex_minn (P:=pred) ex)
subgoal 2 (ID 37) is:
forall n' : nat, pred n' -> ex_minn (P:=pred) ex <= n'
----------------------------------------------------------------------------- *)
all: have MIN := ex_minnP ex; move: MIN ⇒ [n Pn MIN]; auto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* As a corollary, we show that if there is a constant [c] such
that [P c], then the minimal satisfying argument [ex_minn ex]
of a predicate [P] is less than or equal to [c]. *)
Corollary ex_minn_le_ex:
∀ (P : nat → bool) (exP : ∃ n, P n) (c : nat),
P c →
ex_minn exP ≤ c.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
============================
forall (P : nat -> bool) (exP : exists n : nat, P n) (c : nat),
P c -> ex_minn (P:=P) exP <= c
----------------------------------------------------------------------------- *)
Proof.
intros ? ? ? EX.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 32)
P : nat -> bool
exP : exists n : nat, P n
c : nat
EX : P c
============================
ex_minn (P:=P) exP <= c
----------------------------------------------------------------------------- *)
rewrite leqNgt; apply/negP; intros GT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
P : nat -> bool
exP : exists n : nat, P n
c : nat
EX : P c
GT : c < ex_minn (P:=P) exP
============================
False
----------------------------------------------------------------------------- *)
pattern (ex_minn (P:=P) exP) in GT;
apply prop_on_ex_minn in GT; move: GT ⇒ [n [LT [Pn MIN]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 94)
P : nat -> bool
exP : exists n : nat, P n
c : nat
EX : P c
n : nat
LT : c < n
Pn : P n
MIN : forall n' : nat, P n' -> n <= n'
============================
False
----------------------------------------------------------------------------- *)
specialize (MIN c EX).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 96)
P : nat -> bool
exP : exists n : nat, P n
c : nat
EX : P c
n : nat
LT : c < n
Pn : P n
MIN : n <= c
============================
False
----------------------------------------------------------------------------- *)
by move: MIN; rewrite leqNgt; move ⇒ /negP MIN; apply: MIN.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ExMinn.