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).