Library squarematrices
Require Export matrices.
Module Type TSquareMatrices.
Parameter A : Set.
Parameter Aopp : A -> A.
Parameters (Aplus : A -> A -> A) (Amult : A -> A -> A).
Parameters (A0 : A) (A1 : A).
Parameter Aeq : A -> A -> bool.
Parameter A_ring : Ring_Theory Aplus Amult A1 A0 Aopp Aeq.
Parameter smatrix : nat -> Set.
Parameter addmatrix : forall n : nat, smatrix n -> smatrix n -> smatrix n.
Parameter prodmat : forall n : nat, smatrix n -> smatrix n -> smatrix n.
Parameter oppmatrix : forall n : nat, smatrix n -> smatrix n.
Parameter o : forall n : nat, smatrix n.
Parameter I : forall n : nat, smatrix n.
Axiom addmatrix_sym :
forall (n : nat) (w w' : smatrix n), addmatrix n w w' = addmatrix n w' w.
Axiom addmatrix_assoc : forall (n : nat) (w w' w'' : smatrix n),
addmatrix n (addmatrix n w w') w'' = addmatrix n w (addmatrix n w' w'').
Axiom addmatrix_oppmatrix :
forall (n : nat) (w : smatrix n), addmatrix n w (oppmatrix n w) = o n.
Axiom addmatrix_zero_l :
forall (n : nat) (w : smatrix n), addmatrix n (o n) w = w.
Axiom I_mat : forall (n : nat) (w : smatrix n), prodmat n (I n) w = w.
Axiom mat_I : forall (n : nat) (w : smatrix n), prodmat n w (I n) = w.
Axiom prodmat_distr_l :
forall (n : nat) (a b w : smatrix n),
prodmat n (addmatrix n a b) w = addmatrix n (prodmat n a w) (prodmat n b w).
Axiom prodmat_distr_r :
forall (n : nat) (a b w : smatrix n),
prodmat n w (addmatrix n a b) = addmatrix n (prodmat n w a) (prodmat n w b).
Axiom prodmat_assoc :
forall (n : nat) (a b c : smatrix n),
prodmat n (prodmat n a b) c = prodmat n a (prodmat n b c).
End TSquareMatrices.
Module SquareMatrices (C: Carrier) <: TSquareMatrices with Definition A := C.A with
Definition Aopp := C.Aopp with Definition Aplus := C.Aplus with Definition
Amult := C.Amult with Definition A0 := C.A0 with Definition A1 := C.A1 with
Definition Aeq := C.Aeq with Definition A_ring := C.A_ring.
Definition A := C.A.
Definition Aopp := C.Aopp.
Definition Aplus := C.Aplus.
Definition Amult := C.Amult.
Definition A0 := C.A0.
Definition A1 := C.A1.
Definition Aeq := C.Aeq.
Definition A_ring := C.A_ring.
Module MyMatrices := Matrices C.
Import MyMatrices.
Import C.
Definition smatrix (n : nat) := vect (vect A n) n.
Definition eq_add_S_tr (n m : nat) (H : S n = S m) : n = m := f_equal pred H.
Definition addmatrix (n : nat) (v w : smatrix n) := MyMatrices.addmatrix n n v w.
Definition prodmat (n : nat) ( w1 w2 : smatrix n) : (smatrix n) :=
MyMatrices.prodmat n n n w1 w2.
Definition oppmatrix (n : nat) (w: smatrix n) : (smatrix n) :=
MyMatrices.oppmatrix n n w.
Definition o (n : nat) : smatrix n := MyMatrices.o n n.
Definition I ( n : nat) := MyMatrices.I n.
Lemma addmatrix_sym :
forall (n : nat) (w w' : smatrix n),
addmatrix n w w' = addmatrix n w' w.
intros n w w'.
unfold addmatrix.
apply MyMatrices.addmatrix_sym.
Qed.
Lemma addmatrix_assoc :
forall (n : nat) (w w' w'' : smatrix n),
addmatrix n (addmatrix n w w') w'' =
addmatrix n w (addmatrix n w' w'').
intros n w w' w''.
unfold addmatrix.
apply MyMatrices.addmatrix_assoc.
Qed.
Lemma addmatrix_oppmatrix :
forall (n : nat) (w : smatrix n),
addmatrix n w (oppmatrix n w) = o n.
intros n w.
unfold addmatrix, oppmatrix, o.
apply MyMatrices.addmatrix_oppmatrix.
Qed.
Lemma addmatrix_zero_l :
forall (n : nat) (w : smatrix n), addmatrix n (o n) w = w.
intros n w.
unfold addmatrix, o.
apply MyMatrices.addmatrix_zero_l.
Qed.
Lemma I_mat : forall (n : nat) (w : smatrix n), prodmat n (I n) w = w.
intros n w.
unfold I, prodmat.
apply (MyMatrices.I_mat n n w).
Qed.
Lemma mat_I : forall (n : nat) (w : smatrix n), prodmat n w (I n) = w.
intros n w.
unfold I, prodmat.
apply (MyMatrices.mat_I n n w).
Qed.
Lemma prodmat_distr_l :
forall (n : nat) (a b w : smatrix n),
prodmat n (addmatrix n a b) w =
addmatrix n (prodmat n a w) (prodmat n b w).
intros n a b w.
unfold prodmat, addmatrix.
apply (MyMatrices.prodmat_distr_l n n n a b w).
Qed.
Lemma prodmat_distr_r :
forall (n : nat) (a b w : smatrix n),
prodmat n w (addmatrix n a b) =
addmatrix n (prodmat n w a) (prodmat n w b).
intros n a b w.
unfold prodmat, addmatrix.
apply (MyMatrices.prodmat_distr_r n n n a b w).
Qed.
Lemma prodmat_assoc :
forall (n : nat) (a b c : smatrix n),
prodmat n (prodmat n a b) c = prodmat n a (prodmat n b c).
intros n a b c.
unfold prodmat.
apply (MyMatrices.prodmat_assoc n n n n a b c).
Qed.
End SquareMatrices.
Module squarematrixZ := SquareMatrices Zc.
Index
This page has been generated by coqdoc