Library rt.util.search_arg
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).
(* 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.
(* 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).
(* 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.
(* 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).
End ArgSearch.