search_arg.v 8.61 KB
Newer Older
1
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
2
Require Import rt.util.tactics.
3

4
(** This file introduces a function called [search_arg] that allows finding the
5 6
    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
7
    establishing the basic properties of [search_arg].
8 9

    Note that while this is quite similar to [arg min ...] / [arg max ...] in
10
    [ssreflect] ([fintype]), this function is subtly different in that it possibly
11
    returns None and that it does not require the last element in the given
12 13
    range to satisfy the predicate. In contrast, [ssreflect]'s notion of
    extremum in [fintype] uses the upper bound of the search space as the
14 15 16 17
    default value, which is rather unnatural when searching through a schedule.
*)

Section ArgSearch.
Sergey Bozhko's avatar
Sergey Bozhko committed
18
  
19
  (* Given a function [f] that maps the naturals to elements of type [T]... *)
Sergey Bozhko's avatar
Sergey Bozhko committed
20
  Context {T : Type}.
21 22 23 24 25 26 27 28 29 30 31
  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]. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
32
  Fixpoint search_arg (a b : nat) : option nat :=
33 34 35 36 37 38 39 40 41 42 43 44
    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]. *)

45
  (* To begin, we observe that the search yields [None] iff predicate [P] does
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
     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
154
     [search_arg] yields a point x, then [R (f x) (f y)] holds for any [y] in the
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
     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.
Sergey Bozhko's avatar
Sergey Bozhko committed
206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238

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.