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) :=
           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 n 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

              ).

Typecheck (matrixprod).
Typecheck (transpose).