From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
Require Import rt.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:
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.
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:
forall (P : nat -> Prop) (pred : nat -> bool) (ex : exists n, pred n),
P (ex_minn ex) ->
exists n, P n /\ pred n /\ (forall n', pred n' -> n <= n').
Proof.
intros.
exists (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:
forall (P : nat -> bool) (exP : exists n, P n) (c : nat),
P c ->
ex_minn exP <= c.
Proof.
intros ? ? ? 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.