Library rt.util.find_seq

Require Import rt.util.all.

Section find_seq.
  Context {T:eqType}.
  Variable P: T→ bool.
  Fixpoint findP l:=
    match l with
    | nil ⇒ None
    | x::s ⇒ if P x then Some x else findP s
    end.

  Lemma findP_FIFO:
    ∀ (l:seq T) x y,
    P y = true → y \in l → x ≠ y →
    findP l = Some x →
    find (fun j ⇒ j==x) l < find (fun j ⇒ j==y) l.

  Lemma find_uniql:
    ∀ (x:T) l1 l2,
    uniq(l1 ++ l2) →
    x \in l2 →
    ¬ x \in l1.

  Lemma find_uniq:
    ∀ (x:T) l1 l2,
    uniq(l1 ++ l2) →
    x \in l2 →
    has (fun x': T⇒ x'==x) l1 = false.

  Lemma findP_in_seq:
    ∀ (l:seq T) x,
    findP l = Some x →
    P x ∧ x \in l.

  Lemma findP_notSome_in_seq:
    ∀ (l:seq T) x,
    findP l != Some x →
    x \in l→
    ¬ P x ∨ ∃ y, findP l = Some y.

End find_seq.