Library CoLoR.Util.Vector.VecArith

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-03-19 (setoid)
  • Adam Koprowski, 2007-04-02
Arithmetic over vectors on some semiring.

Set Implicit Arguments.


Module VectorArith (SRT : SemiRingType).

  Module Export SR := SemiRing SRT.

  Notation vec := (vector A).

  Definition zero_vec := Vconst A0.

  Definition id_vec n i (ip : i < n) := Vreplace (zero_vec n) ip A1.

  Notation "v1 =v v2" := (Vforall2 eqA v1 v2) (at level 70).

addition

  Definition vector_plus n (v1 v2 : vec n) := Vmap2 Aplus v1 v2.

  Infix "[+]" := vector_plus (at level 50).

  Instance vector_plus_mor n :
    Proper (Vforall2 eqA ==> Vforall2 eqA ==> Vforall2 eqA) (@vector_plus n).


  Lemma vector_plus_nth n (vl vr : vec n) i (ip : i < n) :
    Vnth (vl [+] vr) ip =A= Vnth vl ip + Vnth vr ip.

  Lemma vector_plus_comm n (v1 v2 : vec n) : v1 [+] v2 =v v2 [+] v1.

  Lemma vector_plus_assoc n (v1 v2 v3 : vec n) :
    v1 [+] (v2 [+] v3) =v v1 [+] v2 [+] v3.

  Lemma vector_plus_zero_r n (v : vec n) : v [+] zero_vec n =v v.

  Lemma vector_plus_zero_l n (v : vec n) : zero_vec n [+] v =v v.

sum of a vector of vectors

  Definition add_vectors n k (v : vector (vec n) k) :=
    Vfold_left_rev (@vector_plus n) (zero_vec n) v.

  Instance add_vectors_mor n k :
    Proper (Vforall2 (Vforall2 eqA) ==> Vforall2 eqA) (@add_vectors n k).


  Lemma add_vectors_cons n i (a : vec n) (v : vector (vec n) i) :
    add_vectors (Vcons a v) =v a [+] add_vectors v.

  Lemma add_vectors_zero n k : forall v : vector (vec n) k,
    Vforall (fun v => v =v zero_vec n) v -> add_vectors v =v zero_vec n.

  Lemma add_vectors_perm n i v v' (vs : vector (vec n) i) :
    add_vectors (Vcons v (Vcons v' vs)) =v add_vectors (Vcons v' (Vcons v vs)).

  Lemma add_vectors_nth n k : forall (vs : vector (vec n) k) i (ip : i < n),
    Vnth (add_vectors vs) ip
    =A= Vfold_left_rev Aplus A0 (Vmap (fun v => Vnth v ip) vs).

  Lemma add_vectors_split n : forall k (v vl vr : vector (vec n) k),
    (forall i (ip : i < k), Vnth v ip =v Vnth vl ip [+] Vnth vr ip) ->
    add_vectors v =v add_vectors vl [+] add_vectors vr.

point-wise product

  Definition dot_product n (l r : vec n) :=
    Vfold_left_rev Aplus A0 (Vmap2 Amult l r).

  Instance dot_product_mor n :
    Proper (Vforall2 eqA ==> Vforall2 eqA ==> eqA) (@dot_product n).


  Lemma dot_product_zero : forall n (v v' : vec n),
    Vforall (fun el => el =A= A0) v -> dot_product v v' =A= A0.

  Lemma dot_product_id : forall i n (ip : i < n) v,
    dot_product (id_vec ip) v =A= Vnth v ip.

  Lemma dot_product_comm : forall n (u v : vec n),
    dot_product u v =A= dot_product v u.

  Lemma dot_product_distr_r : forall n (v vl vr : vec n),
    dot_product v (vl [+] vr) =A= dot_product v vl + dot_product v vr.

  Lemma dot_product_distr_l n (v vl vr : vec n) :
    dot_product (vl [+] vr) v =A= dot_product vl v + dot_product vr v.

  Lemma dot_product_cons : forall n al ar (vl vr : vec n),
    dot_product (Vcons al vl) (Vcons ar vr) =A= al * ar + dot_product vl vr.

  Lemma dot_product_distr_mult : forall n a (v v' : vec n),
    a * dot_product v v'
    =A= dot_product (Vbuild (fun i ip => a * Vnth v ip)) v'.

hints
product ordering on vectors

Module OrdVectorArith (OSRT : OrdSemiRingType).

  Module Export VA := VectorArith OSRT.SR.
  Module Export OSR := OrdSemiRing OSRT.

ge on vectors

  Infix ">=v" := (Vforall2 ge) (at level 70).

  Instance vec_ge_mor n :
    Proper (Vforall2 eqA ==> Vforall2 eqA ==> iff) (Vforall2 ge (n:=n)).



  Lemma vec_plus_ge_compat : forall n (vl vl' vr vr' : vec n),
    vl >=v vl' -> vr >=v vr' -> vl [+] vr >=v vl' [+] vr'.

  Lemma vec_plus_ge_compat_r : forall n (vl vl' vr : vec n),
    vl >=v vl' -> vl [+] vr >=v vl' [+] vr.

  Lemma vec_plus_ge_compat_l : forall n (vl vr vr' : vec n),
    vr >=v vr' -> vl [+] vr >=v vl [+] vr'.

End OrdVectorArith.