Module Extra

Require Export Util.
Import Utf8 Coqlib.

Definition list_exists {A} (f: A → bool) : list A → bool :=
  fix list_exists m :=
    match m with
    | nil => false
    | a :: m' => if f a then true else list_exists m'
    end.

Lemma list_exists_forall {A} f m :
  list_exists f m = false →
  ∀ a : A, In a m → f a = false.

Lemma list_norepet_cons {A} (a: A) (m: list A) :
  list_norepet (a :: m) →
  ¬ In a m ∧ list_norepet m.

Definition map_o {X Y} (f: X → option Y) : list X → option (list Y) :=
  fix map_o xs :=
    match xs with
    | nil => Some nil
    | x :: xs' => do y <- f x; do ys <- map_o xs'; Some (y :: ys)
    end.