PlusNatAssoc.idr

-- Monoid
class Ding a where
    dong : a -> a -> a

-- Verified monoid
class Ding a => VDing a where
    law1 : (x,y,z : a) -> dong x (dong y z) = dong (dong x y) z

instance Ding Nat where
    dong = (+)

myCong : {f : t1 -> t2} -> a = b -> f a = f b
myCong Refl = Refl

p2 : {b : Nat} -> (b + Z) = b
p2 {b = Z} = Refl
p2 {b = S n} = myCong (p2 {b = n})

myReplace : {P : t -> Type} -> (a = b) -> P a -> P b
myReplace Refl x = x

r1 : {a,b,f : Nat} -> (a = b) -> f + a = f + b
r1 Refl = Refl

t1 : (a = b) -> (a = c) -> (b = c)
t1 Refl Refl = Refl

hnngg : {a,b : Nat} -> a + (b + Z) = a + b
hnngg = r1 p2

hnnggg2 : {a,b : Nat} -> (a + b) + Z = (a + b)
hnnggg2 = p2

derp : (a = q) -> (b = q) -> (a = b)
derp Refl Refl = Refl

dfvbdfjbv : {a,b : Nat} -> a + (b + Z) = (a + b) + Z
dfvbdfjbv = derp hnngg hnnggg2


total simpleL_1 : {a,b : Nat} -> S (a + b) = a + S b
simpleL_1 {a = Z} = simpleL_1_Z
    where
    simpleL_1_Z : {b : Nat} -> S (Z + b) = S b
    simpleL_1_Z = myCong simple_L_1_Z_S
        where
        simple_L_1_Z_S : {b : Nat} -> Z + b = b
        simple_L_1_Z_S = Refl
simpleL_1 {a = (S m)} = simpleL_1_S
    where
    total simpleL_1_S : {n,b : Nat} -> S ((S n) + b) = S n + S b
    simpleL_1_S = myCong simpleL_1_S_S
        where
        total simpleL_1_S_S : {n,b : Nat} -> (S n) + b = n + S b
        simpleL_1_S_S {n = Z} = Refl
        simpleL_1_S_S {n = (S m)} = myCong simpleL_1_S_S

simpleL_2 : S (a + (b + n)) = a + S (b + n)
simpleL_2 = simpleL_1

simpleL_4 : S (b + n) = b + S n
simpleL_4 = simpleL_1

simpleL_3 : a + S (b + n) = a + (b + S n)
simpleL_3 = myCong simpleL_4

total simpleL : {a,b,n : Nat} -> S (a + (b + n)) = (a + (b + S n))
simpleL = trans simpleL_2 simpleL_3

simpleR : S ((a + b) + n) = (a + b) + S n
simpleR = simpleL_1

simple : {a,b,n : Nat} -> (S (a + (b + n)) = S ((a + b) + n)) -> (a + (b + (S n)) = (a + b) + (S n))
simple prf = thing simpleL simpleR prf
    where
    thing : (a = a2) -> (b = b2) -> (a = b) -> (a2 = b2)
    thing Refl Refl Refl = Refl

symmS : (a = b) -> S a = S b
symmS = myCong

ind : {a,b,n : Nat} -> (a + (b + n) = (a + b) + n) -> (a + (b + (S n)) = (a + b) + (S n))
ind prf = simple (symmS prf)

p1 : {a,b,n : Nat} -> a + (b + n) = (a + b) + n
p1 {n = Z} = dfvbdfjbv
p1 {n = (S m)} = ind p1

prf : (a,b,n : Nat) -> a + (b + n) = (a + b) + n
prf a b n = p1

instance VDing Nat where
    law1 = prf