Library prosa.classic.util.find_seq

From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
Require Import prosa.classic.util.all.

Section find_seq.
  Context {T:eqType}.
  Variable P: T bool.
  Fixpoint findP l:=
    match l with
    | nilNone
    | x::sif 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 jj==x) l < find (fun jj==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': Tx'==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.