From bf4412d00991184cab2d8be1d9c8674b5c9b48b0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 27 Jun 2019 23:11:42 +0200
Subject: [PATCH] add utility function search_arg for searching across
schedules
Given an interval [a, b), a function f: nat -> T, a predicate P, and a
total, reflexive, transitive relation R, [search_arg f P R a b] will
find the x in [a, b) that is an extremum w.r.t. R among all elements x
in [a, b) for which (f x) satisfies P.
For example, this can be used to search in a schedule for a scheduled
job released before some reference time with the earliest deadline.
---
util/all.v | 1 +
util/search_arg.v | 204 ++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 205 insertions(+)
create mode 100644 util/search_arg.v
diff --git a/util/all.v b/util/all.v
index 892aad02c..987a28eec 100644
--- a/util/all.v
+++ b/util/all.v
@@ -18,3 +18,4 @@ Require Export rt.util.minmax.
Require Export rt.util.seqset.
Require Export rt.util.step_function.
Require Export rt.util.epsilon.
+Require Export rt.util.search_arg.
diff --git a/util/search_arg.v b/util/search_arg.v
new file mode 100644
index 000000000..0761e4a93
--- /dev/null
+++ b/util/search_arg.v
@@ -0,0 +1,204 @@
+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:
+ forall a b,
+ search_arg a b = None <-> forall x, a <= x < b -> ~~ P (f x).
+ Proof.
+ split.
+ { (* if *)
+ elim: b => [ _ | b' HYP]; first by move=> _ /andP [_ FALSE] //.
+ rewrite /search_arg -/search_arg.
+ case: (boolP (a < b'.+1)) => [a_lt_b | not_a_lt_b' TRIV].
+ - move: HYP. case: (search_arg a b') => [y | HYP NIL x].
+ + case: (P (f b') && R (f b') (f y)) => //.
+ + move=> /andP[a_le_x x_lt_b'].
+ move: x_lt_b'.
+ rewrite ltnS leq_eqVlt => /orP [/eqP EQ|LT].
+ * rewrite EQ.
+ move: NIL. case: (P (f b')) => //.
+ * feed HYP => //.
+ apply: (HYP x).
+ by apply /andP; split.
+ - move=> x /andP [a_le_x b_lt_b'].
+ exfalso.
+ move: not_a_lt_b'. rewrite -leqNgt ltnNge => /negP b'_lt_a.
+ by move: (leq_ltn_trans a_le_x b_lt_b').
+ }
+ { (* only if *)
+ rewrite /search_arg.
+ elim: b => [//|b'].
+ rewrite -/search_arg => IND NOT_SAT.
+ have ->: search_arg a b' = None.
+ {
+ apply IND => x /andP [a_le_x x_lt_n].
+ apply: (NOT_SAT x).
+ apply /andP; split => //.
+ by rewrite ltnS; apply ltnW.
+ }
+ case: (boolP (a < b'.+1)) => [a_lt_b | //].
+ apply ifF.
+ apply negbTE.
+ apply (NOT_SAT b').
+ by apply /andP; split.
+ }
+ Qed.
+
+ (* Conversely, if we know that [f] satisfies [P] for at least one point in
+ the search space, then [search_arg] yields some point. *)
+ Lemma search_arg_not_none:
+ forall a b,
+ (exists x, (a <= x < b) /\ P (f x)) ->
+ exists y, search_arg a b = Some y.
+ Proof.
+ move=> a b H_exists.
+ destruct (search_arg a b) eqn:SEARCH; first by exists n.
+ move: SEARCH. rewrite search_arg_none => NOT_exists.
+ exfalso.
+ move: H_exists => [x [RANGE Pfx]].
+ by move: (NOT_exists x RANGE) => /negP not_Pfx.
+ Qed.
+
+ (* Since [search_arg] considers only points at which [f] satisfies [P], if it
+ returns a point, then that point satisfies [P]. *)
+ Lemma search_arg_pred:
+ forall a b x,
+ search_arg a b = Some x -> P (f x).
+ Proof.
+ move=> a b x.
+ elim: b => [| n IND]; first by rewrite /search_arg // ifN.
+ rewrite /search_arg -/search_arg.
+ destruct (a < n.+1) eqn:a_lt_Sn; last by trivial.
+ move: a_lt_Sn. rewrite ltnS => a_lt_Sn.
+ destruct (search_arg a n) as [q|] eqn:REC;
+ destruct (P (f n)) eqn:Pfn => //=;
+ [elim: (R (f n) (f q)) => // |];
+ by move=> x_is; injection x_is => <-.
+ Qed.
+
+ (* Since [search_arg] considers only points within a given range, if it
+ returns a point, then that point lies within the given range. *)
+ Lemma search_arg_in_range:
+ forall a b x,
+ search_arg a b = Some x -> a <= x < b.
+ Proof.
+ move=> a b x.
+ elim: b => [| n IND]; first by rewrite /search_arg // ifN.
+ rewrite /search_arg -/search_arg.
+ destruct (a < n.+1) eqn:a_lt_Sn; last by trivial.
+ move: a_lt_Sn. rewrite ltnS => a_lt_Sn.
+ destruct (search_arg a n) as [q|] eqn:REC;
+ elim: (P (f n)) => //=.
+ - elim: (R (f n) (f q)) => //= x_is;
+ first by injection x_is => <-; apply /andP; split.
+ move: (IND x_is) => /andP [a_le_x x_lt_n].
+ apply /andP; split => //.
+ by rewrite ltnS ltnW.
+ - move => x_is.
+ move: (IND x_is) => /andP [a_le_x x_lt_n].
+ apply /andP; split => //.
+ by rewrite ltnS ltnW.
+ - move => x_is.
+ by injection x_is => <-; apply /andP; split.
+ Qed.
+
+ (* Let us assume that [R] is a reflexive and transitive total order... *)
+ Hypothesis R_reflexive: reflexive R.
+ Hypothesis R_transitive: transitive R.
+ Hypothesis R_total: total R.
+
+ (* ...then [search_arg] yields an extremum w.r.t. to [a, b), that is, if
+ [search_arg] yields a point x, then [R (f x) (f y)] holds for any y in the
+ search range [a, b) that satisfies [P]. *)
+ Lemma search_arg_extremum:
+ forall a b x,
+ search_arg a b = Some x ->
+ forall y,
+ a <= y < b ->
+ P (f y) ->
+ R (f x) (f y).
+ Proof.
+ move=> a b x SEARCH.
+ elim: b x SEARCH => n IND x; first by rewrite /search_arg.
+ rewrite /search_arg -/search_arg.
+ destruct (a < n.+1) eqn:a_lt_Sn; last by trivial.
+ move: a_lt_Sn. rewrite ltnS => a_lt_Sn.
+ destruct (search_arg a n) as [q|] eqn:REC;
+ destruct (P (f n)) eqn:Pfn => //=.
+ - rewrite <- REC in IND.
+ 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].
+ + by rewrite EQ; apply (R_reflexive (f n)).
+ + apply (R_transitive (f q)) => //.
+ move: (IND q REC y) => HOLDS.
+ apply HOLDS => //.
+ by apply /andP; split.
+ + rewrite EQ.
+ move: (R_total (f q) (f n)) => /orP [R_qn | R_nq] //.
+ by move: REL => /negP.
+ + move: (IND q REC y) => HOLDS.
+ apply HOLDS => //.
+ by apply /andP; split.
+ - move=> some_q_is y [/andP [a_le_y y_lt_Sn] Pfy].
+ move: y_lt_Sn. rewrite ltnS.
+ rewrite leq_eqVlt => /orP [/eqP EQ | y_lt_n].
+ + exfalso. move: Pfn => /negP Pfn. by subst.
+ + apply IND => //. by apply /andP; split.
+ - move=> some_n_is. injection some_n_is => n_is.
+ move=> y [/andP [a_le_y y_lt_Sn] Pfy].
+ move: y_lt_Sn. rewrite ltnS.
+ rewrite leq_eqVlt => /orP [/eqP EQ | y_lt_n].
+ + by rewrite -n_is EQ; apply (R_reflexive (f n)).
+ + exfalso.
+ move: REC. rewrite search_arg_none => NONE.
+ move: (NONE y) => not_Pfy.
+ feed not_Pfy; first by apply /andP; split.
+ by move: not_Pfy => /negP.
+ Qed.
+
+End ArgSearch.
--
GitLab