Lvc.Infra.Filter

Require Import Util List OptionMap LengthEq Map Get Take MoreList.

Set Implicit Arguments.

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.

Fixpoint countTrue (L:list bool) :=
  match L with
  | nil ⇒ 0
  | true :: xs ⇒ 1 + countTrue xs
  | false :: xscountTrue xs
  end.

Lemma countTrue_exists (L:list bool) n
  : get L n true
     countTrue L 0.
Proof.
  intros. general induction H; simpl; eauto.
  - cases; eauto.
Qed.

Lemma countTrue_app (L L':list bool)
  : countTrue (L ++ L') = countTrue L + countTrue L'.
Proof.
  intros. induction L; simpl; eauto.
  destruct a; eauto. omega.
Qed.

Arguments filter_by [A B] f L L'.

Lemma filter_by_ext A B (f f':A bool) L1 L1' (L2:list B)
  : length L1 = length L1'
     ( n a a', get L1 n a get L1' n a' f a = f' a')
     filter_by f L1 L2 = filter_by f' L1' L2.
Proof.
  intros. length_equify.
  general induction H; destruct L2; simpl; eauto.
  - erewrite H0; eauto using get.
    cases; eauto using get.
    f_equal. eauto using get.
Qed.

Lemma map_filter_by A B C (f:A bool) (g:B C) L L'
  : g filter_by f L L' = filter_by f L (g L').
Proof.
  general induction L; destruct L'; simpl; repeat cases; simpl; f_equal; eauto.
Qed.

Lemma filter_by_app A B (f:A bool) L1 (L1':list B) L2 L2' (LEN: L1 = L1')
  : filter_by f (L1 ++ L2) (L1' ++ L2') = filter_by f L1 L1' ++ filter_by f L2 L2'.
Proof.
  length_equify.
  general induction LEN; simpl; repeat cases; simpl; f_equal; eauto.
Qed.

Lemma filter_by_nil A B (f:A bool) L (L':list B)
  : ( n b, get L n b f b = false)
     filter_by f L L' = nil.
Proof.
  intros.
  general induction L; destruct L'; simpl; repeat cases; simpl; f_equal; eauto using get.
  - exfalso. exploit H; eauto using get. congruence.
Qed.

Lemma filter_by_not_nil A B (f:A bool) L (L':list B) n b
  : L = L'
     get L n b
     f b = true
     filter_by f L L' nil.
Proof.
  intros LEN Get Tru. length_equify.
  general induction LEN; simpl; repeat cases; simpl; f_equal; eauto using get; isabsurd.
  - inv Get; isabsurd; eauto.
Qed.

Lemma get_filter_by A B (p:Abool) (Z:list A) (Y:list B) y n z
  : get Z n z
     get Y n y
     p z
     get (filter_by p Z Y) (countTrue (p (take n Z))) y.
Proof.
  intros GetZ GetY Pz.
  eapply get_getT in GetZ.
  eapply get_getT in GetY.
  general induction GetZ; inv GetY; simpl in × |- *; isabsurd.
  - cases. eauto using get.
  - exploit IHGetZ; eauto.
    cases; eauto using get.
Qed.

Lemma filter_by_length A B (p: A bool) L (L':list B)
  : L = L'
     filter_by p L L' = countTrue (p L).
Proof.
  intros LEN; length_equify.
  general induction LEN; simpl; eauto.
  cases; simpl; f_equal; eauto.
Qed.

Fixpoint posOfTrue (n:nat) (L:list bool) :=
  match L, n with
  | nil, _ ⇒ 0
  | true :: xs, S nS (posOfTrue n xs)
  | true :: xs, 0 ⇒ 0
  | false :: xs, nS (posOfTrue n xs)
  end.

Lemma filter_by_get A B p (Z:list A) (Y:list B) y n
: get (filter_by p Z Y) n y
   { z : A | get Y (posOfTrue n (p Z)) y get Z (posOfTrue n (p Z)) z p z }.
Proof.
  intros.
  general induction Z; destruct Y; simpl in × |- *; isabsurd.
  cases in H.
  - eapply get_getT in H.
    inv H.
    + do 2 eexists; repeat split; eauto using get.
    + eapply getT_get in X.
      edestruct IHZ as [? [? []]]; eauto; dcr.
      do 2 eexists; eauto using get.
  - edestruct IHZ as [? [? []]]; eauto; dcr; eauto.
    do 2 eexists; eauto using get.
Qed.

Lemma posOfTrue_countTrue L (n:nat)
: get L n true
   posOfTrue (countTrue (take n L)) L = n.
Proof.
  intros. general induction L; [ isabsurd |].
  - invc H; simpl; eauto.
    cases; f_equal; eauto.
Qed.

Lemma filter_get A p (Y:list A) y n
: get (List.filter p Y) n y
   get Y (posOfTrue n (p Y)) y p y.
Proof.
  intros.
  general induction Y; simpl in × |- *; isabsurd.
  cases in H.
  - eapply get_getT in H.
    inv H; eauto using get.
    + eapply getT_get in X.
      edestruct IHY as [? ?]; dcr; eauto using get.
  - edestruct IHY; dcr; eauto using get.
Qed.

Ltac inv_get_step_filter dummy :=
  first [inv_get_step |
         repeat (match goal with
         | [ H : get (filter_by ?p ?L ?L') ?n ?x |- _ ] ⇒
           eapply filter_by_get in H; try rewrite map_id in H; destruct H as [? [? [? ?]]]
| [ H : get (filter ?p ?L) ?n ?x |- _ ] ⇒
           eapply filter_get in H; try rewrite map_id in H; destruct H as [H ?]
         | [ H : get _ (posOfTrue (countTrue (?f take ?n ?L)) (?f ?L)) _,
                 H' : get ?L ?n ?x, H'' : ?f ?x = true |- _ ] ⇒
           rewrite (@map_take _ _ f L) in H;
           rewrite (@posOfTrue_countTrue (f L) n) in H;[| eauto using map_get_eq]
         end)
        ].

Tactic Notation "inv_get_step" := inv_get_step_filter idtac.
Tactic Notation "inv_get" := inv_get' inv_get_step_filter.

Lemma lookup_list_filter_by_commute A B C (V:AB) (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).
Proof.
  intros. eapply length_length_eq in H.
  general induction H; simpl; eauto.
  + cases; simpl; rewrite IHlength_eq; eauto.
Qed.

Lemma of_list_filter X `{OrderedType X} lv Y
  : of_list (List.filter (fun y : XB[y lv]) Y) [=] lv of_list Y.
Proof.
  general induction Y; simpl.
  - cset_tac; intuition.
  - decide (a lv); simpl.
    rewrite IHY; eauto. cset_tac; intuition.
    rewrite IHY; eauto. cset_tac; intuition.
Qed.

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).
Proof.
  intros. eapply length_length_eq in H0.
  general induction H0; simpl in × |- *; eauto.
  monad_inv H. cases; simpl; eauto.
  - rewrite EQ. erewrite IHlength_eq; simpl; eauto.
Qed.

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).
Proof.
  intros. eapply length_length_eq in H.
  general induction H; simpl; eauto.
  cases; simpl. rewrite IHlength_eq; eauto. eauto.
Qed.

Hint Resolve filter_filter_by_length : len.

Lemma filter_incl2 X `{OrderedType X} (p:Xbool) Z
: of_list (List.filter p Z) of_list Z.
Proof.
  general induction Z; simpl.
  - reflexivity.
  - cases; simpl. rewrite IHZ; reflexivity.
    rewrite IHZ. cset_tac; intuition.
Qed.

Lemma filter_p X p (Z:list X)
: n x, get (List.filter p Z) n x p x.
Proof.
  intros.
  general induction Z; simpl.
  - isabsurd.
  - simpl in H. cases in H. inv H. rewrite <- Heq. eapply I.
    eapply IHZ; eauto.
    eapply IHZ; eauto.
Qed.

Lemma filter_in X `{OrderedType X} (p:Xbool) `{Proper _ (_eq ==> eq) p} a Z
 : p a
     a \In of_list Z
     a \In of_list (List.filter p Z).
Proof.
  general induction Z; simpl in × |- *; eauto.
  - cset_tac. rewrite <- H3 in H1.
    cases; isabsurd. rewrite <- H3. simpl. cset_tac; intuition.
    cases; eauto. simpl. exploit IHZ; eauto. cset_tac; intuition.
Qed.

Lemma agree_on_update_filter X `{OrderedType X} Y `{Equivalence (option Y)}
      (lv:set X) (V: X option Y) Z VL
: length Z = length VL
   agree_on R lv
             (V [Z <-- List.map Some VL])
             (V [List.filter (fun xB[x lv]) Z <--
                             List.map Some (filter_by (fun xB[x lv]) Z VL)]).
Proof.
  intros. eapply length_length_eq in H1.
  general induction H1.
  - eapply agree_on_refl. eapply H0.
  - simpl. cases. simpl. eapply agree_on_update_same. reflexivity.
    eapply agree_on_incl. eapply IHlength_eq. eauto. cset_tac; intuition.
    eapply agree_on_update_dead; eauto.
Qed.

Lemma agree_on_update_filter' X `{OrderedType X} Y `{Equivalence (option Y)} (lv:set X) (V V':X option Y) Z VL
: length Z = length VL
   agree_on R (lv \ of_list Z) V V'
   agree_on R lv
             (V [Z <-- List.map Some VL])
             (V' [(List.filter (fun xB[x lv]) Z) <-- (List.map Some
                             (filter_by (fun xB[x lv]) Z VL))]).
Proof.
  intros.
  eapply agree_on_trans. eapply H0.
  eapply update_with_list_agree; eauto. rewrite map_length; eauto.
  eapply agree_on_update_filter; eauto.
Qed.