Library prosa.util.search_arg

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
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.

Section ArgSearch.

  Context {T : Type}.
  Variable f: nat → T.

  Variable P: pred T.

  Variable R: rel T.

  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.

  Lemma search_arg_none:
    ∀ a b,
      search_arg a b = None ↔ ∀ x, a ≤ x < b → ~~ P (f x).

  Lemma search_arg_not_none:
    ∀ a b,
      (∃ x , (a ≤ x < b ) ∧ P (f x)) →
      ∃ y , search_arg a b = Some y.

  Lemma search_arg_pred:
    ∀ a b x,
      search_arg a b = Some x → P (f x).

  Lemma search_arg_in_range:
    ∀ a b x,
      search_arg a b = Some x → a ≤ x < b.

  Hypothesis R_reflexive: reflexive R.
  Hypothesis R_transitive: transitive R.
  Hypothesis R_total: total R.

  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.

Section ExMinn.

  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').

  Corollary ex_minn_le_ex:
    ∀ (P : nat → bool) (exP : ∃ n , P n) (c : nat),
      P c →
      ex_minn exP ≤ c.

End ExMinn.