Library prosa.util.search_arg
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Export mathcomp.zify.zify.
Require Import prosa.util.tactics.
Require Export mathcomp.zify.zify.
Require Import prosa.util.tactics.
This file introduces a function called search_arg that allows finding the
argument within a given range for which a function is minimal w.r.t. to a
given order while satisfying a given predicate, along with lemmas
establishing the basic properties of search_arg.
Note that while this is quite similar to arg min ... / arg max ... in
ssreflect (fintype), this function is subtly different in that it possibly
returns None and that it does not require the last element in the given
range to satisfy the predicate. In contrast, ssreflect's notion of
extremum in fintype uses the upper bound of the search space as the
default value, which is rather unnatural when searching through a schedule.
First, we show that, given an interval
[t1, t2) and a
predicate P, either no element in the interval satisfy P or
there is an element that satisfies P.
Lemma earliest_pred_element_exists_case :
∀ (P : pred nat) (t1 t2 : nat),
(∀ t, t1 ≤ t < t2 → ~~ P t)
∨ (∃ t,
t1 ≤ t < t2
∧ P t
∧ ∀ t', t1 ≤ t' → P t' → t ≤ t').
Proof.
move⇒ P t1 t2.
have [/allP ALL|/allPn [x /[!mem_index_iota] IN /negPn Px]]:=
boolP(all (fun x ⇒ ~~ P x) (index_iota t1 t2)).
{ by left ⇒ t IN; apply: ALL; rewrite mem_index_iota. }
{ right.
have EX : ∃ n : nat, (t1 ≤ n < t2) && P n
by ∃ x; apply/andP; split.
have [x' /andP [IN' Px'] MIN] := (ex_minnP EX).
∃ x'; (repeat split) ⇒ // t' LT Pt'.
have [NEQ1|NEQ2] := leqP t2 t'; first by lia.
by apply: MIN; repeat(apply/andP; split ⇒ //). }
Qed.
∀ (P : pred nat) (t1 t2 : nat),
(∀ t, t1 ≤ t < t2 → ~~ P t)
∨ (∃ t,
t1 ≤ t < t2
∧ P t
∧ ∀ t', t1 ≤ t' → P t' → t ≤ t').
Proof.
move⇒ P t1 t2.
have [/allP ALL|/allPn [x /[!mem_index_iota] IN /negPn Px]]:=
boolP(all (fun x ⇒ ~~ P x) (index_iota t1 t2)).
{ by left ⇒ t IN; apply: ALL; rewrite mem_index_iota. }
{ right.
have EX : ∃ n : nat, (t1 ≤ n < t2) && P n
by ∃ x; apply/andP; split.
have [x' /andP [IN' Px'] MIN] := (ex_minnP EX).
∃ x'; (repeat split) ⇒ // t' LT Pt'.
have [NEQ1|NEQ2] := leqP t2 t'; first by lia.
by apply: MIN; repeat(apply/andP; split ⇒ //). }
Qed.
Next, we proceed to the function search_arg.
Section ArgSearch.
(* Given a function f that maps the naturals to elements of type T... *)
Context {T : Type}.
Variable f: nat → T.
(* ... a predicate P on T ... *)
Variable P: pred T.
(* ... and an order R on T ... *)
Variable R: rel T.
(* ... we define the procedure search_arg to iterate a given search space
a, b), while checking each element whether [f] satisfies [P] at that point and returning the extremum as defined by [R]. *)
Fixpoint search_arg (a b : nat) : option nat :=
if a < b then
match b with
| 0 ⇒ None
| S b' ⇒ match search_arg a b' with
| None ⇒ if P (f b') then Some b' else None
| Some x ⇒ if P (f b') && R (f b') (f x) then Some b' else Some x
end
end
else None.
(* 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).
Proof.
move⇒ a b; 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).
by apply /andP; split.
}
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:
∀ a b,
(∃ x, (a ≤ x < b) ∧ P (f x)) →
∃ y, search_arg a b = Some y.
Proof.
move⇒ a b H_exists.
destruct (search_arg a b) as [n|] eqn:SEARCH; first by ∃ 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:
∀ 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:
∀ 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].
by apply /andP; split.
- move ⇒ x_is.
move: (IND x_is) ⇒ /andP [a_le_x x_lt_n].
by apply /andP; split.
- 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:
∀ a b x,
search_arg a b = Some x →
∀ 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.
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').
Proof.
move⇒ P pred ex.
∃ (ex_minn ex); repeat split; auto.
all: have MIN := ex_minnP ex; move: MIN ⇒ [n Pn MIN]; auto.
Qed.
(* As a corollary, we show that if there is a constant c such
that P c, then the minimal satisfying argument ex_minn ex
of a predicate P is less than or equal to c. *)
Corollary ex_minn_le_ex:
∀ (P : nat → bool) (exP : ∃ n, P n) (c : nat),
P c →
ex_minn exP ≤ c.
Proof.
move⇒ P exP c EX.
rewrite leqNgt; apply/negP; intros GT.
pattern (ex_minn (P:=P) exP) in GT;
apply prop_on_ex_minn in GT; move: GT ⇒ [n [LT [Pn MIN]]].
specialize (MIN c EX).
by move: MIN; rewrite leqNgt; move ⇒ /negP MIN; apply: MIN.
Qed.
End ExMinn.