Error on zeroMatAddRight

Test.idr

module Test

%default total
%access public export

data Shape : Type where
  L : Shape 
  B : Shape -> Shape -> Shape

data M : (a : Type)     -> 
         (rows : Shape) ->
         (cols : Shape) -> 
         Type where
  One : a -> M a L L
  Row : M a L c  ->
        M a L c' ->
        M a L (B c c')
  Col : M a r  L ->
        M a r' L ->
        M a (B r r') L
  Q   : M a r1 c1 -> M a r1 c2 ->
        M a r2 c1 -> M a r2 c2 -> 
        M a (B r1 r2) (B c1 c2)

infix 1 :=:

interface Equality a where
  (:=:)  : a -> a -> Type
  
interface Equality a => VerifiedEquality a where  
  eqRefl : {x : a} -> x :=: x
  eqSym  : {x, y : a} -> x :=: y -> y :=: x
  eqTran : {x, y, z : a} -> x :=: y -> y :=: z -> x :=: z

interface Semiring a where
  Zeros  : a           -- sum identity
  Ones   : a           -- times identity
  (<+>) : a -> a -> a -- sum
  (<*>) : a -> a -> a -- times

interface (Semiring a, Equality a) => VerifiedSemiring a where
  zeroIdLeft : (x : a) -> Zeros <+> x :=: x
  zeroIdRight : (x : a) -> x <+> Zeros :=: x
  oneIdLeft : (x : a) -> Ones <*> x :=: x
  oneIdRight : (x : a) -> x <*> Ones :=: x
  sumComm : (x, y : a) -> x <+> y :=: y <+> x
  sumAssoc : (x, y, z : a) -> x <+> (y <+> z) :=: (x <+> y) <+> z
  multAssoc : (x, y, z : a) -> x <*> (y <*> z) :=: (x <*> y) <*> z
  zeroMultLeft : (x : a) -> Zeros <*> x :=: Zeros
  zeroMultRight : (x : a) -> x <*> Zeros :=: Zeros
  multDistRight : (x, y, z : a) -> (x <+> y) <*> z :=: (x <*> z) <+> (y <*> z)
  multDistLeft :  (x, y, z : a) -> x <*> (y <+> z) :=: (x <*> y) <+> (x <*> z)
  respectsSum : {x, y, z, w : a} -> x :=: y -> z :=: w -> (x <+> z) :=: (y <+> w)
  respectsMult : {x, y, z, w : a} -> x :=: y -> z :=: w -> (x <*> z) :=: (y <*> w)

meq : Equality a => M a r c -> M a r c -> Type
meq {r = L}{c = L} (One x) (One y) 
  = x :=: y
meq {r = L}{c = (B c1 c2)} (Row x y) (Row z w) 
  = ( meq x z
    , meq y w )
meq {r = (B x y)}{c = L} (Col z w) (Col s t) 
  = ( meq z s
    , meq w t )
meq {r = (B r1 c1)}{c = (B r2 c2)} (Q s t u v) (Q x1 y1 z1 w1) 
  = ( meq s x1
    , ( meq t y1
      , ( meq u z1
        , meq v w1)))
      
-- reflexivity

meqRefl : VerifiedEquality a => 
          (r, c : Shape)     -> 
          {m : M a r c}      -> 
          meq m m
meqRefl L L {m = (One x)} 
  = eqRefl {x = x}
meqRefl L (B c1 c2) {m = (Row r1 r2)} 
  = ( meqRefl L c1 {m = r1}
    , meqRefl L c2 {m = r2} )
meqRefl (B r1 r2) L {m = (Col c1 c2)} 
  = ( meqRefl r1 L {m = c1}
    , meqRefl r2 L {m = c2} )
meqRefl (B r1 r2) (B c1 c2) {m = (Q s t u v)} 
  = ( meqRefl r1 c1 {m = s}
    , (meqRefl r1 c2 {m = t}
      , (meqRefl r2 c1 {m = u}
        , meqRefl r2 c2 {m = v})))


meqSym : VerifiedEquality a => 
         (r, c : Shape)     -> 
         {m1, m2 : M a r c} -> 
         meq m1 m2          -> 
         meq m2 m1
meqSym L L {m1 = (One x)}{m2 = (One y)} prf 
  = eqSym {x = x} {y = y} prf
meqSym L (B x y) {m1 = (Row z w)}{m2 = (Row s t)} (p , q) 
  = ( meqSym L x {m1 = z}{m2 = s} p
    , meqSym L y {m1 = w}{m2 = t} q )
meqSym (B x y) L {m1 = (Col z w)}{m2 = (Col s t)} (p,q) 
  = ( meqSym x L {m1 = z} {m2 = s} p
    , meqSym y L {m1 = w} {m2 = t} q )
meqSym (B x y) (B z w) {m1 = (Q s t u v)}{m2 = (Q x1 y1 z1 w1)} (p,(q,(p',q'))) 
  = ( meqSym x z {m1 = s} {m2 = x1} p 
    , (meqSym x w {m1 = t} {m2 = y1} q
      , (meqSym y z {m1 = u} {m2 = z1} p'
        , meqSym y w {m1 = v} {m2 = w1} q')))


meqTran : VerifiedEquality a     => 
          (r, c : Shape)         -> 
          {m1, m2, m3 : M a r c} ->
          meq m1 m2              ->
          meq m2 m3              ->
          meq m1 m3
meqTran L L {m1 = (One x)}
            {m2 = (One y)}
            {m3 = (One z)} prf1 prf2 
  = eqTran {x = x}{y = y}{z = z} prf1 prf2
meqTran L (B c1 c2) {m1 = (Row z w)}
                    {m2 = (Row s t)}
                    {m3 = (Row u v)} (p,q) (p',q') 
  = ( meqTran L c1 {m1 = z}{m2 = s}{m3 = u} p p'
    , meqTran L c2 {m1 = w}{m2 = t}{m3 = v} q q' )
meqTran (B r1 r2) L {m1 = (Col x y)}
                    {m2 = (Col z w)}
                    {m3 = (Col s t)} (p,q) (p',q') 
  = ( meqTran r1 L {m1 = x}{m2 = z}{m3 = s} p p'
    , meqTran r2 L {m1 = y}{m2 = w}{m3 = t} q q' )
meqTran (B r1 r2) (B c1 c2) 
                  {m1 = (Q s t 
                           u v)}
                  {m2 = (Q x1 y1 
                           z1 w1)}
                  {m3 = (Q s1 t1 
                           u1 v1)} 
                  ( p1 
                  , (p2 
                    , ( p3
                      , p4))) 
                  ( q1
                  , (q2
                    , ( q3
                      , q4 ))) = ( meqTran r1 c1 {m1 = s}{m2 = x1}{m3 = s1} p1 q1
                                 , ( meqTran r1 c2 {m1 = t}{m2 = y1}{m3 = t1} p2 q2
                                   , (meqTran r2 c1 {m1 = u}{m2 = z1}{m3 = u1} p3 q3
                                     , meqTran r2 c2 {m1 = v}{m2 = w1}{m3 = v1} p4 q4)))




Equality a => Equality (M a r c) where
  (:=:) = meq

              
VerifiedEquality a => VerifiedEquality (M a r c) where
  eqRefl {x = m} = meqRefl _ _ {m = m}
  eqSym  {x = m1}{y = m2} = meqSym _ _ {m1 = m1} {m2 = m2}
  eqTran {x = m1}{y = m2}{z = m3} = meqTran _ _ {m1 = m1} {m2 = m2} {m3 = m3}


addM : Semiring a => M a r c -> M a r c -> M a r c
addM (One x) (One x') 
  = One (x <+> x')
addM (Row m1 m2) (Row m1' m2') 
  = Row (addM m1 m1') (addM m2 m2')
addM (Col m1 m2) (Col m1' m2') 
  = Col (addM m1 m1') (addM m2 m2')
addM (Q m11 m12
        m21 m22) (Q m11' m12'
                    m21' m22') = Q (addM m11 m11') (addM m12 m12')
                                   (addM m21 m21') (addM m22 m22')

infixl 10 :+:

(:+:) : Semiring a => M a r c -> M a r c -> M a r c
(:+:) = addM

congAddM : ( VerifiedEquality s
           , VerifiedSemiring s ) =>
           (r, c : Shape) -> 
           {x, y, u, v : M s r c} -> 
           x :=: y ->
           u :=: v ->
           (x :+: u) :=: (y :+: v)
congAddM L L {x = (One x)}{y = (One y)}{u = (One z)}{v = (One w)} p q 
  = respectsSum {x = x}{y = y}{z = z}{w = w} p q
congAddM L (B z w) {x = (Row x s)}
                   {y = (Row y t)}
                   {u = (Row u x1)}
                   {v = (Row v y1)} (p1, p2) 
                                    (q1,q2)
  = ( congAddM L z {x = x}{y = y}{u = u}{v = v} p1 q1
    , congAddM L w {x = s}{y = t}{u = x1}{v = y1} p2 q2 )
congAddM (B z w) L {x = (Col x s)}
                   {y = (Col y t)}
                   {u = (Col u x1)}
                   {v = (Col v y1)} (p1,p2) (q1,q2)
  = ( congAddM z L {x = x}{y = y}{u = u}{v = v} p1 q1 
    , congAddM w L {x = s}{y = t}{u = x1}{v = y1} p2 q2 )
congAddM (B z w) (B s t) {x = (Q x x1 y1 z1)}
                         {y = (Q y w1 s1 t1)}
                         {u = (Q u u1 v1 x2)}
                         {v = (Q v y2 z2 w2)} (p1,(p2,(p3,p4))) 
                                              (q1,(q2,(q3,q4))) 
  = ( congAddM z s {x = x}{y = y}{u = u}{v = v} p1 q1
    , (congAddM z t {x = x1}{y = w1}{u = u1}{v = y2} p2 q2
      , (congAddM w s {x = y1}{y = s1}{u = v1}{v = z2} p3 q3
        , congAddM w t {x = z1}{y = t1}{u = x2}{v = w2} p4 q4)))
        

zeroMat : Semiring a => (r : Shape) -> (c : Shape) -> M a r c
zeroMat L L 
  = One Zeros
zeroMat L (B m1 m2) 
  = Row (zeroMat L m1) (zeroMat L m2)
zeroMat (B m1 m2) L 
  = Col (zeroMat m1 L) (zeroMat m2 L)
zeroMat (B m1 m2) (B m3 m4) 
  = Q (zeroMat m1 m3) (zeroMat m1 m4)
      (zeroMat m2 m3) (zeroMat m2 m4)
                            

zeroMatAddLeft : ( VerifiedSemiring s
                 , VerifiedEquality s ) =>
                 {r, c : Shape} ->
                 (m : M s r c)  ->
                 ((zeroMat r c) :+: m) :=: m
zeroMatAddLeft {r = L}{c = L} (One x) 
  = zeroIdLeft x
zeroMatAddLeft {r = L}{c = (B c1 c2)} (Row x y) 
  = ( zeroMatAddLeft {r = L} {c = c1} x
    , zeroMatAddLeft {r = L} {c = c2} y )
zeroMatAddLeft {r = (B r1 r2)}{c = L} (Col z w) 
  = ( zeroMatAddLeft {r = r1}{c = L} z
    , zeroMatAddLeft {r = r2}{c = L} w )
zeroMatAddLeft {r = (B r1 r2)}{c = (B c1 c2)} (Q t u v x1) 
  = ( zeroMatAddLeft {r = r1}{c = c1} t
    , ( zeroMatAddLeft {r = r1}{c = c2} u
      , ( zeroMatAddLeft {r = r2}{c = c1} v
        , zeroMatAddLeft {r = r2}{c = c2} x1 )))


addMatComm : ( VerifiedSemiring s
             , VerifiedEquality s ) => 
             {r, c : Shape} ->
             (m, m' : M s r c) ->
             m :+: m' :=: m' :+: m
addMatComm {r = L}{c = L} (One x) (One x') 
  = sumComm x x'
addMatComm {r = L}{c = (B x y)} (Row z w) (Row z' w') 
  = ( addMatComm {r = L}{c = x} z z'
    , addMatComm {r = L}{c = y} w w' ) 
addMatComm {r = (B x y)}{c = L} (Col z w) (Col z' w') 
  = ( addMatComm {r = x}{c = L} z z'
    , addMatComm {r = y}{c = L} w w' )
addMatComm {r = (B x y)}{c = (B z w)} (Q t u 
                                         v x1) 
                                      (Q t' u' 
                                         v' x1') 
  = ( addMatComm {r = x}{c = z} t t'
    , ( addMatComm {r = x}{c = w} u u'
      , ( addMatComm {r = y}{c = z} v v'
        , addMatComm {r = y}{c = w} x1 x1')))



syntax [expr] "QED" = qed expr 
syntax [from] "={" [prf] "}=" [to] = step from prf to

namespace EqReasoning
  using (a : Type, x : a, y : a, z : a)
    qed : VerifiedEquality a => (x : a) -> x :=: x
    qed x = eqRefl {x = x}
    
    step : VerifiedEquality a => (x : a) -> x :=: y -> (y :=: z) -> x :=: z
    step x prf prf1 = eqTran {x = x} prf prf1

-- error HERE

zeroMatAddRight : ( VerifiedSemiring s
                  , VerifiedEquality s ) =>
                  {r, c : Shape} ->
                  (m : M s r c)  -> 
                  (m :+: (zeroMat r c)) :=: m
zeroMatAddRight {r = r}{c = c} m 
  = m :+: (zeroMat r c)
      ={ addMatComm {r = r}{c = c} m (zeroMat r c) }=
    (zeroMat r c) :+: m
      ={ zeroMatAddLeft {r = r}{c = c} m }=
    m
    QED