Inductive nat : Type := | O : nat | S : V (x: nat). nat. Recursive plus (a: nat) (b: nat) [0] : nat := match a with | b | \ (a: nat). S (plus a b). Recursive mult (a: nat) (b: nat) [0] : nat := match a with | O | \ (a: nat). plus b (mult a b). Inductive vector (A: Type) : V (n0: nat). Type := | epsi: V (e: A). vector A O | suiv: V (n: nat). V (e: A). V (s: vector A n). vector A (S n). Definition vectorfstelt (A: Type) (n: nat) (v: vector A n) : A := match v with | \ (A: Type). \ (e: A). e | \ (A: Type). \ (n: nat). \ (e: A). \ (v: vector A n). e. Definition vectorsnd (A: Type) (n: nat) (v: vector A (S n)) : vector A n := match v with | \ (A: Type). \ (n: nat). \ (e: A). \ (v: vector A n). v. Recursive buildvector (A: Type) (a: A) (n: nat) [2] : vector A n := match n with | epsi A a | \ (n: nat). suiv A n a (buildvector A a n). Recursive applyvector (A: Type) (B: Type) (n: nat) (v1: vector (V (a: A). B) n) (v2: vector A n) [3] : vector B n := match v1 with | \ (C: Type). \ (f: (V (a: A). B)). ( match v2 with | \ (A: Type). \ (a: A). epsi B (f a) ) | \ (C: Type). \ (n: nat). \ (f: (V (a: A). B)). \ (v1: vector (V (a: A). B) n). ( match v2 with | \ (A: Type). \ (n: nat). \ (a: A). \ (v2: vector A n). suiv B n (f a) (applyvector A B n v1 v2) ). Definition mapvector (A: Type) (B: Type) (f: V (a: A). B) (n: nat) (v: vector A n) : vector B n := applyvector A B n (buildvector (V (a: A). B) f n) v. Definition apply2vector (A: Type) (B: Type) (C: Type) (f: V (a: A). V (b: B). C) (n: nat) (va: vector A n) (vb: vector B n) : vector C n := applyvector B C n (applyvector A (V (b: B). C) n (buildvector (V (a: A). V (b: B). C) f n) va) vb. Recursive foldvector (A: Type) (n: nat) (v: vector A n) (f: V (x: A). V (y: A). A) [2] : A := match v with | \ (A: Type). \ (e: A). e | \ (A: Type). \ (n: nat). \ (e: A). \ (v: vector A n). f e (foldvector A n v f). Definition innerproduct (A: Type) (plus: V (x: A). V (y: A). A) (mult: V (x: A). V (y: A). A) (n: nat) (va: vector A n) (vb: vector A n) : A := foldvector A n ( apply2vector A A A mult n va vb ) plus. Definition matrix (A: Type) (n: nat) (m: nat) : Type := vector (vector A n) m. Recursive buildmatrix (A: Type) (a: A) (n: nat) (m: nat) [3] : matrix A n m := match m with | epsi (vector A n) (buildvector A a n) | \ (m: nat). suiv (vector A n) m (buildvector A a n) (buildmatrix A a n m). Recursive applymatrix (A: Type) (B: Type) (n: nat) (m: nat) (m1: matrix (V (a: A). B) n m) (m2: matrix A n m) [4] : matrix B n m := match m1 with | \ (C: Type). \ (c: vector (V (a: A). B) n). ( match m2 with | \ (D: Type). \ (d: vector A n). epsi (vector B n) (applyvector A B n c d) ) | \ (C: Type). \ (m: nat). \ (c: vector (V (a: A). B) n). \ (m1: matrix (V (a: A). B) n m). ( match m2 with | \ (D: Type). \ (m: nat). \ (d: vector A n). \ (m2: matrix A n m). suiv (vector B n) m (applyvector A B n c d) (applymatrix A B n m m1 m2) ). Definition mapmatrix (A: Type) (B: Type) (f: V (a: A). B) (n: nat) (m: nat) (v: matrix A n m) : matrix B n m := applymatrix A B n m (buildmatrix (V (a: A). B) f n m) v. Definition apply2matrix (A: Type) (B: Type) (C: Type) (f: V (a: A). V (b: B). C) (n: nat) (m: nat) (ma: matrix A n m) (mb: matrix B n m) : matrix C n m := applymatrix B C n m (applymatrix A (V (b: B). C) n m (buildmatrix (V (a: A). V (b: B). C) f n m) ma) mb. Definition plusnatmatrix (n: nat) (m: nat) (ma: matrix nat n m) (mb: matrix nat n m) : matrix nat n m := apply2matrix nat nat nat plus n m ma mb. Recursive matrixfstrow (A: Type) (n: nat) (m: nat) (mat: matrix A n m) [3] : vector A m := match mat with | \ (B: Type). \ (e: vector A n). epsi A (vectorfstelt A n e) | \ (B: Type). \ (m: nat). \ (e: vector A n). \ (mat: matrix A n m). suiv A m (vectorfstelt A n e) (matrixfstrow A n m mat). Recursive matrixsnd (A: Type) (n: nat) (m: nat) (mat: matrix A (S n) m) [3] : matrix A n m := match mat with | \ (B: Type). \ (e: vector A (S n)). epsi (vector A n) (vectorsnd A n e) | \ (B: Type). \ (m: nat). \ (e: vector A (S n)). \ (mat: matrix A (S n) m). suiv (vector A n) m (vectorsnd A n e) (matrixsnd A n m mat). Recursive transpose (A: Type) (n: nat) (m: nat) (mat: matrix A n m) [1] : matrix A m n := match n with | epsi (vector A m) (matrixfstrow A n m mat) | \ (n0: nat). suiv (vector A m) n0 (matrixfstrow A (S n0) m mat) (transpose A n0 m (matrixsnd A n0 m mat)). Recursive innervectormatrix (A: Type) (plus: V (x: A). V (y: A). A) (mult: V (x: A). V (y: A). A) (p: nat) (m : nat) (vec: vector A p) (mat: matrix A p m) [6] : vector A m := match mat with | \ (B: Type). \ (e: vector A p). epsi A (innerproduct A plus mult p vec e) | \ (B: Type). \ (m: nat). \ (e: vector A p). \ (mat: matrix A p m). suiv A m (innerproduct A plus mult p vec e) (innervectormatrix A plus mult p m vec mat ). Recursive innermatrix (A: Type) (plus: V (x: A). V (y: A). A) (mult: V (x: A). V (y: A). A) (n: nat) (p: nat) (m : nat) (m1: matrix A p n) (m2: matrix A p m) [6] : matrix A m n := match m1 with | \ (B: Type). \ (e: vector A p). epsi (vector A m) (innervectormatrix A plus mult p m e m2 ) | \ (B: Type). \ (n: nat). \ (e: vector A p). \ (m1: matrix A p n). suiv (vector A m) n (innervectormatrix A plus mult p m e m2 ) (innermatrix A plus mult n p m m1 m2 ). Definition matrixprod (A: Type) (plus: V (x: A). V (y: A). A) (mult: V (x: A). V (y: A). A) (n: nat) (p: nat) (m : nat) (m1: matrix A n p) (m2: matrix A p m) : matrix A n m := transpose A m n ( innermatrix A plus mult n p m (transpose A n p m1) m2 ). Compute (plus (S (S O)) (S (S (S O)))). Compute (mult (S (S (S (S O)))) (S (S (S (S O))))). Check transpose.