Library CoLoR.Util.Vector.VecFilter

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-06-08
vector filtering

Set Implicit Arguments.


Section S.

Variable A : Type.

Notation vec := (vector A).

Fixpoint Vfilter n (bs : bools n) : vec n -> vec (Vtrue bs) :=
  match bs as bs in vector _ n return vec n -> vec (Vtrue bs) with
  | Vnil => fun _ => Vnil
  | Vcons true bs' => fun v => Vcons (Vhead v) (Vfilter bs' (Vtail v))
  | Vcons false bs' => fun v => Vfilter bs' (Vtail v)
  end.

Lemma Vfilter_in : forall n bs (v : vec n) x, Vin x (Vfilter bs v) -> Vin x v.

Lemma Vfilter_app_eq : forall n (bs : bools n) n1 (v1 : vec n1)
  n2 (v2 : vec n2) (h : n=n1+n2) (h' : Vtrue (fst (Vbreak (Vcast bs h)))
    + Vtrue (snd (Vbreak (Vcast bs h))) = Vtrue (Vcast bs h)),
  Vfilter (Vcast bs h) (Vapp v1 v2)
  = Vcast (Vapp (Vfilter (fst (Vbreak (Vcast bs h))) v1)
    (Vfilter (snd (Vbreak (Vcast bs h))) v2)) h'.

Lemma Vfilter_app : forall n (bs : bools n) n1 (v1 : vec n1) n2 (v2 : vec n2)
  (h : n=n1+n2), Vfilter (Vcast bs h) (Vapp v1 v2)
  = Vcast (Vapp (Vfilter (fst (Vbreak (Vcast bs h))) v1)
    (Vfilter (snd (Vbreak (Vcast bs h))) v2)) (Vtrue_break (Vcast bs h)).

Lemma Vfilter_cons_eq : forall n (bs : bools (S n)) x (v : vec n)
  (h' : Vtrue_cons bs = Vtrue bs),
  Vfilter bs (Vcons x v) = Vcast (
    if Vhead bs as b return vec (Vtrue_cons_if b bs)
    then Vcons x (Vfilter (Vtail bs) v)
    else Vfilter (Vtail bs) v) h'.

Lemma Vfilter_cons : forall n (bs : bools (S n)) x (v : vec n),
  Vfilter bs (Vcons x v) = Vcast (
    if Vhead bs as b return vec (Vtrue_cons_if b bs)
    then Vcons x (Vfilter (Vtail bs) v)
    else Vfilter (Vtail bs) v) (Vtrue_cons_eq bs).

Lemma Vfilter_cons_true_eq : forall n b (bs : bools n) x (v : vec n), b = true
  -> forall h : S (Vtrue bs) = Vtrue (Vcons b bs),
  Vfilter (Vcons b bs) (Vcons x v) = Vcast (Vcons x (Vfilter bs v)) h.

Lemma Vfilter_cons_true : forall n b (bs : bools n) x (v : vec n)
  (h : b = true), Vfilter (Vcons b bs) (Vcons x v)
  = Vcast (Vcons x (Vfilter bs v)) (Vtrue_cons_true bs h).

Lemma Vfilter_head_true_eq : forall n (bs : bools (S n)) x (v : vec n),
  Vhead bs = true -> forall h : S (Vtrue (Vtail bs)) = Vtrue bs,
  Vfilter bs (Vcons x v) = Vcast (Vcons x (Vfilter (Vtail bs) v)) h.

Lemma Vfilter_head_true : forall n (bs : bools (S n)) x (v : vec n)
  (h : Vhead bs = true), Vfilter bs (Vcons x v)
  = Vcast (Vcons x (Vfilter (Vtail bs) v)) (Vtrue_Sn_true bs h).

Lemma Vfilter_cons_false_eq : forall n b (bs : bools n) x (v : vec n),
  b = false -> forall h : Vtrue bs = Vtrue (Vcons b bs),
  Vfilter (Vcons b bs) (Vcons x v) = Vcast (Vfilter bs v) h.

Lemma Vfilter_cons_false : forall n b (bs : bools n) x (v : vec n)
  (h : b = false), Vfilter (Vcons b bs) (Vcons x v)
  = Vcast (Vfilter bs v) (Vtrue_cons_false bs h).

Lemma Vfilter_head_false_eq : forall n (bs : bools (S n)) x (v : vec n),
  Vhead bs = false -> forall h : Vtrue (Vtail bs) = Vtrue bs,
  Vfilter bs (Vcons x v) = Vcast (Vfilter (Vtail bs) v) h.

Lemma Vfilter_head_false : forall n (bs : bools (S n)) x (v : vec n)
  (h : Vhead bs = false), Vfilter bs (Vcons x v)
  = Vcast (Vfilter (Vtail bs) v) (Vtrue_Sn_false bs h).

Lemma Vfilter_app2_eq : forall n1 (bs1 : bools n1) (v1 : vec n1)
  n2 (bs2 : bools n2) (v2 : vec n2)
  (h : Vtrue bs1 + Vtrue bs2 = Vtrue (Vapp bs1 bs2)),
  Vfilter (Vapp bs1 bs2) (Vapp v1 v2)
  = Vcast (Vapp (Vfilter bs1 v1) (Vfilter bs2 v2)) h.

Lemma Vfilter_app2 : forall n1 (bs1 : bools n1) (v1 : vec n1)
  n2 (bs2 : bools n2) (v2 : vec n2),
  Vfilter (Vapp bs1 bs2) (Vapp v1 v2) =
  Vcast (Vapp (Vfilter bs1 v1) (Vfilter bs2 v2)) (sym_eq (Vtrue_app bs1 bs2)).

Lemma Vfilter_break_eq : forall n1 n2 (bs : bools (n1+n2)) (v : vec (n1+n2))
  (h : Vtrue (fst (Vbreak bs)) + Vtrue (snd (Vbreak bs)) = Vtrue bs),
  Vfilter bs v = Vcast (Vapp (Vfilter (fst (Vbreak bs)) (fst (Vbreak v)))
    (Vfilter (snd (Vbreak bs)) (snd (Vbreak v)))) h.

Lemma Vfilter_break : forall n1 n2 (bs : bools (n1+n2)) (v : vec (n1+n2)),
  Vfilter bs v = Vcast (Vapp (Vfilter (fst (Vbreak bs)) (fst (Vbreak v)))
    (Vfilter (snd (Vbreak bs)) (snd (Vbreak v)))) (Vtrue_break bs).

Lemma Vfilter_cast_eq : forall n (bs : bools n) p (v : vec p)
  (hpn : p=n) (hnp: n=p) (h' : Vtrue (Vcast bs hnp) = Vtrue bs),
  Vfilter bs (Vcast v hpn) = Vcast (Vfilter (Vcast bs hnp) v) h'.

Lemma Vfilter_cast : forall n (bs : bools n) p (v : vec p) (h : p=n),
  Vfilter bs (Vcast v h)
  = Vcast (Vfilter (Vcast bs (sym_eq h)) v) (Vtrue_cast bs (sym_eq h)).

End S.


Lemma Vmap_filter : forall (A B : Type) (f : A->B) n (bs : bools n)
  (v : vector A n), Vmap f (Vfilter bs v) = Vfilter bs (Vmap f v).