Library CoLoR.Util.Matrix.Matrix

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-03-23 (setoid)
  • Adam Koprowski and Hans Zantema, 2007-03
    Matrices as a functor.


Set Implicit Arguments.

functor building matrices over a given carrier

Module Matrix (OSRT : OrdSemiRingType).

  Module Export OSR := OrdSemiRing OSRT.
  Module Export VA := OrdVectorArith OSRT.

basic definitions

  Notation vec := (vector A).

  Definition matrix m n := vector (vec n) m.

accessors

  Definition get_row m n (M : matrix m n) i (ip : i < m) := Vnth M ip.

  Definition get_col m n (M : matrix m n) i (ip : i < n) :=
    Vmap (fun v => Vnth v ip) M.

  Definition get_elem m n (M : matrix m n) i j (ip : i < m) (jp : j < n) :=
    Vnth (get_row M ip) jp.

  Lemma get_elem_swap : forall m n (M : matrix m n) i j (ip : i < m)
    (jp : j < n), Vnth (get_row M ip) jp = Vnth (get_col M jp) ip.

  Definition mat_eqA m n (M N : matrix m n) :=
    forall i j (ip : i < m) (jp : j < n),
      get_elem M ip jp =A= get_elem N ip jp.

  Notation "M =m N" := (mat_eqA M N) (at level 70).

  Instance mat_eqA_refl m n : Reflexive (@mat_eqA m n).


  Instance mat_eqA_sym m n : Symmetric (@mat_eqA m n).


  Instance mat_eqA_trans m n : Transitive (@mat_eqA m n).


  Instance mat_eqA_equiv m n : Equivalence (@mat_eqA m n).


  Lemma mat_eq : forall m n (M N : matrix m n),
    (forall i j (ip : i < m) (jp : j < n),
      get_elem M ip jp = get_elem N ip jp) -> M = N.

  Instance get_row_mor m n i (h:i<m) :
    Proper (@mat_eqA m n ==> Vforall2 eqA) (fun M => @get_row m n M i h).


  Instance get_col_mor m n i (h:i<n) :
    Proper (@mat_eqA m n ==> Vforall2 eqA) (fun M => @get_col m n M i h).


  Instance get_elem_mor m n i j (ip:i<m) (jp:j<n) :
    Proper (@mat_eqA m n ==> eqA) (fun M => @get_elem m n M i j ip jp).


matrix construction

  Definition mat_build_spec : forall m n
    (gen : forall i j, i < m -> j < n -> A),
    { M : matrix m n | forall i j (ip : i < m) (jp : j < n),
      get_elem M ip jp = gen i j ip jp }.


  Definition mat_build m n gen : matrix m n := proj1_sig (mat_build_spec gen).

  Lemma mat_build_elem : forall m n gen i j (ip : i < m) (jp : j < n),
    get_elem (mat_build gen) ip jp = gen i j ip jp.

  Lemma mat_build_nth : forall m n gen i j (ip : i < m) (jp : j < n),
    Vnth (Vnth (mat_build gen) ip) jp = gen i j ip jp.

Some elementary matrices

  Definition zero_matrix m n : matrix m n := mat_build (fun i j ip jp => A0).

  Definition id_matrix n : matrix n n := Vbuild (fun i ip => id_vec ip).

  Definition inverse_matrix inv m n (M : matrix m n) : matrix m n :=
    mat_build (fun i j ip jp => inv (get_elem M ip jp)).

1-row and 1-column matrices

  Definition row_mat n := matrix 1 n.
  Definition col_mat n := matrix n 1.

  Definition vec_to_row_mat n (v : vec n) : row_mat n := Vcons v Vnil.

  Definition vec_to_col_mat n (v : vec n) : col_mat n :=
    Vmap (fun i => Vcons i Vnil) v.

  Instance vec_to_col_mat_mor n :
    Proper (Vforall2 eqA ==> @mat_eqA n 1) (@vec_to_col_mat n).


  Definition access_0 : 0 < 1 := le_n 1.

  Definition row_mat_to_vec n (m : row_mat n) := get_row m access_0.
  Definition col_mat_to_vec n (m : col_mat n) := get_col m access_0.

  Ltac mat_get_simpl :=
    repeat progress unfold get_elem, get_col, get_row,
      vec_to_col_mat, vec_to_row_mat, col_mat_to_vec, row_mat_to_vec;
      repeat progress (try rewrite Vnth_map; try rewrite Vnth_map2);
        ring_simplify; try refl.

  Lemma get_col_col_mat : forall n (v : vec n) (p : 0 < 1),
    get_col (vec_to_col_mat v) p = v.

  Lemma vec_to_col_mat_spec : forall n (v : vec n) i (ip : i < n) j
    (jp : j < 1), get_elem (vec_to_col_mat v) ip jp = Vnth v ip.

  Lemma vec_to_row_mat_spec : forall n (v : vec n) i (ip : i < 1) j
    (jp : j < n), get_elem (vec_to_row_mat v) ip jp = Vnth v jp.

  Lemma Vnth_col_mat : forall n (m : col_mat n) i (ip : i < n),
    Vnth (col_mat_to_vec m) ip = get_elem m ip access_0.

  Lemma Vnth_row_mat : forall n (m : row_mat n) i (ip : i < n),
    Vnth (row_mat_to_vec m) ip = get_elem m access_0 ip.

  Lemma col_mat_to_vec_idem : forall n (v : vec n),
    col_mat_to_vec (vec_to_col_mat v) = v.

  Lemma vec_to_col_mat_idem : forall n (M : col_mat n),
    vec_to_col_mat (col_mat_to_vec M) = M.

  Lemma row_mat_to_vec_idem : forall n (v : vec n),
    row_mat_to_vec (vec_to_row_mat v) = v.

  Lemma vec_to_row_mat_idem : forall n (M : row_mat n),
    vec_to_row_mat (row_mat_to_vec M) = M.

matrix transposition

  Definition mat_transpose m n (M : matrix m n) :=
    mat_build (fun _ _ i j => get_elem M j i).

  Lemma mat_transpose_row_col : forall m n (M : matrix m n) i (ip : i < m),
    get_col (mat_transpose M) ip = get_row M ip.

  Lemma mat_transpose_col_row : forall m n (M : matrix m n) i (ip : i < n),
    get_row (mat_transpose M) ip = get_col M ip.

  Lemma mat_transpose_idem : forall m n (M : matrix m n),
    mat_transpose (mat_transpose M) = M.

matrix addition

  Definition vec_plus n (L R : vec n) := Vmap2 Aplus L R.

  Definition mat_plus m n (L R : matrix m n) := Vmap2 (@vec_plus n) L R.

  Infix "<+>" := mat_plus (at level 50).

  Lemma mat_plus_comm : forall m n (L R : matrix m n), L <+> R =m R <+> L.

matrix multiplication

  Definition mat_mult m n p (L : matrix m n) (R : matrix n p) :=
    mat_build (fun i j ip jp => dot_product (get_row L ip) (get_col R jp)).

  Infix "<*>" := mat_mult (at level 40).

  Instance mat_mult_mor m n p :
    Proper (@mat_eqA m n ==> @mat_eqA n p ==> @mat_eqA m p) (@mat_mult m n p).


  Lemma mat_mult_elem : forall m n p (M : matrix m n) (N : matrix n p)
    i (ip : i < m) j (jp : j < p),
    Vnth (Vnth (M <*> N) ip) jp = dot_product (get_row M ip) (get_col N jp).

  Lemma mat_mult_spec : forall m n p (M : matrix m n) (N : matrix n p)
    i (ip : i < m) j (jp : j < p),
    get_elem (M <*> N) ip jp = dot_product (get_row M ip) (get_col N jp).

  Lemma mat_mult_row : forall m n p (M : matrix m n) (N : matrix n p)
    i (ip : i < m),
    get_row (M <*> N) ip =
    Vbuild (fun j jp => dot_product (get_row M ip) (get_col N jp)).

  Lemma mat_mult_col : forall m n p (M : matrix m n) (N : matrix n p)
    j (jp : j < p),
    get_col (M <*> N) jp =
    Vbuild (fun i ip => dot_product (get_row M ip) (get_col N jp)).

  Lemma mat_mult_id_l : forall n p (np : n >= p) (M : matrix n p),
    id_matrix n <*> M =m M.

  Lemma zero_matrix_mult_l : forall m n p (M : matrix n p),
    zero_matrix m n <*> M =m zero_matrix m p.

  Lemma dot_product_assoc : forall m n v v' (M : matrix m n),
    dot_product v (Vbuild (fun i (ip : i < m ) =>
      dot_product (get_row M ip) v')) =A=
    dot_product (Vbuild (fun j (jp : j < n) =>
      dot_product v (get_col M jp))) v'.

  Lemma mat_mult_assoc : forall m n p l
    (M : matrix m n) (N : matrix n p) (P : matrix p l),
    M <*> (N <*> P) =m M <*> N <*> P.

matrix-col vector product

  Definition mat_vec_prod m n (m : matrix m n) (v : vec n) :=
    col_mat_to_vec (m <*> (vec_to_col_mat v)).

  Instance mat_vec_prod_mor m n :
    Proper (@mat_eqA m n ==> Vforall2 eqA ==> Vforall2 eqA) (@mat_vec_prod m n).


  Lemma mat_vec_prod_distr_vec : forall m n (M : matrix m n) v1 v2,
    mat_vec_prod M (v1 [+] v2) =v
    mat_vec_prod M v1 [+] mat_vec_prod M v2.

  Lemma mat_vec_prod_distr_mat : forall m n (Ml Mr : matrix m n) v,
    mat_vec_prod (Ml <+> Mr) v =v
    mat_vec_prod Ml v [+] mat_vec_prod Mr v.

  Lemma mat_vec_prod_distr_add_vectors : forall m n (M : matrix m n) k v1 v2,
    (forall i (ip : i < k), mat_vec_prod M (Vnth v1 ip) =v Vnth v2 ip) ->
    mat_vec_prod M (add_vectors v1) =v add_vectors v2.

forall

  Section Forall.

    Variables (P : A -> Prop) (m n : nat) (M : matrix m n).

    Definition mat_forall := forall i j (ip : i < m) (jp : j < n),
      P (get_elem M ip jp).

    Definition mat_forall' := Vforall (@Vforall A P n) M.

  End Forall.

forall2

  Section Forall2.

    Variables (P : relation A) (m n : nat).

    Definition mat_forall2 (M N : matrix m n):= forall i j (ip : i < m)
      (jp : j < n), P (get_elem M ip jp) (get_elem N ip jp).

    Definition mat_forall2_intro : forall M N,
      (forall i j (ip : i < m) (jp : j < n),
        P (get_elem M ip jp) (get_elem N ip jp)) ->
      mat_forall2 M N := fun M N H => H.

    Definition mat_forall2' (M N : matrix m n) :=
      Vforall2 (@Vforall2 A A P n) M N.

    Variable P_dec : rel_dec P.

    Lemma mat_forall2'_dec : rel_dec mat_forall2'.

    Lemma mat_forall2_equiv1 : forall M N,
      mat_forall2 M N -> mat_forall2' M N.

    Lemma mat_forall2_equiv2 : forall M N,
      mat_forall2' M N -> mat_forall2 M N.

    Lemma mat_forall2_dec : rel_dec mat_forall2.

  End Forall2.

  Hint Rewrite mat_mult_id_l zero_matrix_mult_l using simpl : arith.

'monotonicity' of matrix multiplication over naturals

  Section MatMultMonotonicity.

    Variables (m n p : nat) (M M' : matrix m n) (N N' : matrix n p).

    Definition mat_ge := mat_forall2 ge.

    Infix ">=m" := mat_ge (at level 70).

    Lemma mat_ge_refl : M >=m M.

    Lemma mat_ge_dec : forall m n, rel_dec (@mat_ge m n).

    Lemma dot_product_mon : forall i (v v' w w' : vec i), v >=v v' ->
      w >=v w' -> dot_product v w >>= dot_product v' w'.

    Lemma mat_mult_mon : M >=m M' -> N >=m N' -> M <*> N >=m M' <*> N'.

  End MatMultMonotonicity.

  Lemma mat_vec_prod_ge_compat : forall i j (M M' : matrix i j) m m',
    mat_ge M M' -> m >=v m' -> mat_vec_prod M m >=v mat_vec_prod M' m'.

  Infix ">=m" := mat_ge (at level 70).

End Matrix.

matrix construction functions

Section MatrixConstruction.

  Variable A : Set.

  Definition mkMatrix1 (v1 : A) := Vcons (vec_of_list (v1 :: nil)) Vnil.
  Definition mkMatrix2 (v1 v2 v3 v4 : A) :=
    Vcons (vec_of_list (v1 :: v2 :: nil))
    (Vcons (vec_of_list (v3 :: v4 :: nil)) Vnil).
  Definition mkMatrix3 (v1 v2 v3 v4 v5 v6 v7 v8 v9 : A) :=
    Vcons (vec_of_list (v1 :: v2 :: v3 :: nil))
    (Vcons (vec_of_list (v4 :: v5 :: v6 :: nil))
      (Vcons (vec_of_list (v7 :: v8 :: v9 :: nil)) Vnil)).
  Definition mkMatrix4 (v1 v2 v3 v4 v5 v6 v7 v8 v9 v10
    v11 v12 v13 v14 v15 v16 : A) :=
  Vcons (vec_of_list ( v1 :: v2 :: v3 :: v4 :: nil))
  (Vcons (vec_of_list ( v5 :: v6 :: v7 :: v8 :: nil))
    (Vcons (vec_of_list ( v9 :: v10 :: v11 :: v12 :: nil))
      (Vcons (vec_of_list (v13 :: v14 :: v15 :: v16 :: nil)) Vnil))).

End MatrixConstruction.

matrices over different domains