Lvc.Filter

Require Import Util List OptionMap LengthEq Map Get.

Notation "B[ x ]" := (if [ x ] then true else false).

Fixpoint filter_by {A B} (f:A → bool) (L:list A) (L´:list B) : list B :=
  match L, L´ with
    | x :: L, y::L´ ⇒ if f x then y :: filter_by f L L´ else filter_by f L L´
    | _, _ ⇒ nil
  end.


Lemma lookup_list_filter_by_commute A B C (V:A→B) (Z:list C) Y p
: length Z = length Y
  → lookup_list V (filter_by p Z Y) =
    filter_by p Z (lookup_list V Y).

Lemma filter_incl X `{OrderedType X} lv Y
  : of_list (List.filter (fun y : X ⇒ B[y ∈ lv]) Y) ⊆ lv.

Lemma omap_filter_by A B C f p (Y:list A) (l:list B) (Z:list C)
: omap f Y = Some l
  → length Y = length Z
  → omap f (filter_by p Z Y) = Some (filter_by p Z l).

Lemma filter_filter_by_length {X} {Y} (Z:list X) (VL:list Y)
: length Z = length VL
  → ∀ p, length (List.filter p Z) =
    length (filter_by p Z VL).

Lemma filter_incl2 X `{OrderedType X} (p:X→bool) Z
: of_list (List.filter p Z) ⊆ of_list Z.

Lemma filter_by_get A B p (Z:list A) (Y:list B) y n
: get (filter_by p Z Y) n y
  → length Z = length Y
  → { n : nat & { z : A | get Y n y ∧ get Z n z ∧ p z } }.

Lemma filter_p X p (Z:list X)
: ∀ n x, get (List.filter p Z) n x → p x.

Lemma filter_in X `{OrderedType X} (p:X→bool) `{Proper _ (_eq ==> eq) p} a Z
 : p a
    → a \In of_list Z
    → a \In of_list (List.filter p Z).