# Library CoLoR.Util.Vector.VecFilterPerm

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2009-09-09
vector filtering with permutations

Set Implicit Arguments.

filtering function

Fixpoint Vfilter A n (l : list (N n)) (v : vector A n) : vector A (length l) :=
match l as l return vector A (length l) with
| nil => Vnil
| x :: l' => Vcons (Vnth v x) (Vfilter l' v)
end.

properties

Lemma Vfilter_eq_notin : forall A n (l : list (N n)) i (vi : vector A i) t u
j (vj : vector A j) (e : i+S j=n), (forall hi : i<n, ~In (N_ hi) l) ->
Vfilter l (Vcast (Vapp vi (Vcons t vj)) e)
= Vfilter l (Vcast (Vapp vi (Vcons u vj)) e).

Lemma Vfilter_app : forall A n (l1 l2 : list (N n)) (v : vector A n),
Vfilter (l1 ++ l2) v = Vcast (Vapp (Vfilter l1 v) (Vfilter l2 v))
(sym_eq (length_app l1 l2)).

Lemma Vfilter_app_eq : forall A n (l l1 l2 : list (N n)) (v : vector A n)
(e : length l1+length l2 = length l),
l=l1++l2 -> Vfilter l v = Vcast (Vapp (Vfilter l1 v) (Vfilter l2 v)) e.

Lemma Vfilter_eq_in : forall A n (v : vector A n) (l : list (N n))
(rf : nodup (map (@N_val n) l)) i, In i (map (@N_val n) l) ->
exists hi : i<n, exists l1, exists l2,
exists e : length l1+S(length l2)=length l,
Vfilter l v
= Vcast (Vapp (Vfilter l1 v) (Vcons (Vnth v hi) (Vfilter l2 v))) e.

Lemma Vfilter_map : forall A B (f : A -> B) n (v : vector A n) (l : list (N n)),
Vfilter l (Vmap f v) = Vmap f (Vfilter l v).

Lemma Vin_filter_elim_in : forall A n (l : list (N n)) (v : vector A n) x,
Vin x (Vfilter l v) -> Vin x v.

Lemma Vin_filter_elim_nth : forall A n (l : list (N n)) (v : vector A n) x,
Vin x (Vfilter l v) -> exists i (hi : i<n), In (N_ hi) l /\ Vnth v hi = x.

Lemma Vin_filter_intro : forall A n (l : list (N n)) (v : vector A n)
i (hi : i<n), In (N_ hi) l -> Vin (Vnth v hi) (Vfilter l v).