ZZ.idr

module ZZ

import Data.Sign

%default total
%access public export

data Diff : Nat -> Nat -> Type where
  LTByS : (d : Nat) -> Diff n (n + S d)
  GTByS : (d : Nat) -> Diff (n + S d) n
  DiffZ : Diff n n

diff : (a, b : Nat) -> Diff a b
diff Z     Z     = DiffZ
diff Z     (S b) = LTByS b
diff (S a) Z     = GTByS a
diff (S a) (S b) = case diff a b of
  LTByS d => LTByS d
  GTByS d => GTByS d
  DiffZ   => DiffZ

data ZZ : Type where
  Minus : Nat -> Nat -> ZZ

Eq ZZ where
  (Minus a b) == (Minus c d) = a + d == b + c

data ZZEquiv : ZZ -> ZZ -> Type where
  IsZZEquiv : (a + d = b + c) -> ZZEquiv (Minus a b) (Minus c d)

decEquiv : (x : ZZ) -> (y : ZZ) -> Dec (ZZEquiv x y)
decEquiv (Minus a b) (Minus c d) = case decEq (a + d) (b + c) of
  Yes prf   => Yes $ IsZZEquiv prf
  No contra => No $ \(IsZZEquiv p) => absurd (contra p)

eqEquiv : (x = y) -> ZZEquiv x y
eqEquiv p {y = Minus a b} = rewrite p in IsZZEquiv (plusCommutative a b)

plus : ZZ -> ZZ -> ZZ
plus (Minus a b) (Minus c d) = Minus (a + c) (b + d)

minus : ZZ -> ZZ -> ZZ
minus (Minus a b) (Minus c d) = Minus (a + d) (b + c)

mult : ZZ -> ZZ -> ZZ
mult (Minus a b) (Minus c d) = Minus (a * c + b * d) (a * d + b * c)

Num ZZ where
  (+) = plus
  (*) = mult
  fromInteger n =
    if n < 0
      then Minus Z (cast (-n))
      else Minus (cast n) Z

Signed ZZ where
  sign (Minus a b) = case compare a b of
    LT => Minus
    GT => Plus
    EQ => Zero

Neg ZZ where
  negate (Minus a b) = Minus b a
  (-) = minus

Abs ZZ where
  abs (Minus a b) = case diff a b of
    LTByS d => Minus (S d) Z
    GTByS d => Minus (S d) Z
    DiffZ   => Minus Z Z

Cast Nat ZZ where
  cast n = Minus n Z

Cast ZZ Integer where
  cast (Minus a b) = (cast a) - (cast b)

Cast Integer ZZ where
  cast = fromInteger

natPlusZPlus : a + b = c -> ZZEquiv ((Minus a Z) + (Minus b Z)) (Minus c Z)
natPlusZPlus p {c} = rewrite p in IsZZEquiv (plusZeroRightNeutral c)

natMultZMult : a * b = c -> ZZEquiv ((Minus a Z) * (Minus b Z)) (Minus c Z)
natMultZMult p {a} {c} =
  rewrite p in IsZZEquiv $
    rewrite multZeroRightZero a in
    rewrite plusZeroRightNeutral c in
    plusZeroRightNeutral c

doubleNegElim : (z : ZZ) -> negate (negate z) = z
doubleNegElim (Minus a b) = Refl

posNotNeg : ZZEquiv (Minus (S a) Z) (Minus Z (S b)) -> Void
posNotNeg (IsZZEquiv prf) =
  succNotLTEzero $ replace {P = \z => LTE z 0} (sym prf) LTEZero

plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right
plusZeroLeftNeutralZ (Minus a b) = Refl

plusZeroRightNeutralZ : (left : ZZ) -> left + 0 = left
plusZeroRightNeutralZ (Minus a b) =
  rewrite plusZeroRightNeutral a in
  rewrite plusZeroRightNeutral b in Refl

plusCommutativeZ : (left : ZZ) -> (right : ZZ) -> left + right = right + left
plusCommutativeZ (Minus a b) (Minus c d) =
  rewrite plusCommutative a c in
  rewrite plusCommutative b d in Refl

negateDistributesPlus : (x, y : ZZ) -> negate (x + y) = (negate x) + (negate y)
negateDistributesPlus (Minus a b) (Minus c d) = Refl

plusAssociativeZ : (x, y, z : ZZ) -> x + (y + z) = (x + y) + z
plusAssociativeZ (Minus a1 b1) (Minus a2 b2) (Minus a3 b3) =
  rewrite plusAssociative a1 a2 a3 in
  rewrite plusAssociative b1 b2 b3 in Refl

plusNegateInverseLZ : (x : ZZ) -> ZZEquiv (x + negate x) 0
plusNegateInverseLZ (Minus a b) = IsZZEquiv $ rewrite plusCommutative a b in Refl

plusNegateInverseRZ : (x : ZZ) -> ZZEquiv (negate x + x) 0
plusNegateInverseRZ (Minus a b) = IsZZEquiv $ rewrite plusCommutative a b in Refl

multZeroLeftZeroZ : (right : ZZ) -> 0 * right = 0
multZeroLeftZeroZ (Minus a b) = Refl

multZeroRightZeroZ : (left : ZZ) -> left * 0 = 0
multZeroRightZeroZ (Minus a b) =
  rewrite multZeroRightZero a in
  rewrite multZeroRightZero b in Refl

multOneLeftNeutralZ : (right : ZZ) -> 1 * right = right
multOneLeftNeutralZ (Minus a b) =
  rewrite plusZeroRightNeutral a in
  rewrite plusZeroRightNeutral a in
  rewrite plusZeroRightNeutral b in
  rewrite plusZeroRightNeutral b in Refl

multOneRightNeutralZ : (left : ZZ) -> left * 1 = left
multOneRightNeutralZ (Minus a b) =
  rewrite multOneRightNeutral a in
  rewrite multZeroRightZero b in
  rewrite plusZeroRightNeutral a in
  rewrite multZeroRightZero a in
  rewrite multOneRightNeutral b in Refl

multCommutativeZ : (left : ZZ) -> (right : ZZ) -> left * right = right * left
multCommutativeZ (Minus a b) (Minus c d) =
  rewrite multCommutative a c in
  rewrite multCommutative b d in
  rewrite multCommutative a d in
  rewrite multCommutative b c in
  rewrite plusCommutative (c * b) (d * a) in Refl

multNegLeftZ : (k : Nat) -> (j : ZZ) -> (Minus Z (S k)) * j = negate ((Minus (S k) Z) * j)
multNegLeftZ k (Minus a b) =
  rewrite plusZeroRightNeutral (b + k * b) in
  rewrite plusZeroRightNeutral (a + k * a) in Refl

multNegateLeftZ : (k, j : ZZ) -> (negate k) * j = negate (k * j)
multNegateLeftZ (Minus a b) (Minus c d) =
  rewrite plusCommutative (b * c) (a * d) in
  rewrite plusCommutative (b * d) (a * c) in Refl

multAssociativeZ : (x, y, z : ZZ) -> x * (y * z) = (x * y) * z
multAssociativeZ (Minus a b) (Minus c d) (Minus e f) =
  rewrite multDistributesOverPlusRight a (c * e) (d * f) in
  rewrite multDistributesOverPlusRight b (c * f) (d * e) in
  rewrite multDistributesOverPlusRight a (c * f) (d * e) in
  rewrite multDistributesOverPlusRight b (c * e) (d * f) in
  rewrite multDistributesOverPlusLeft (a * c) (b * d) e in
  rewrite multDistributesOverPlusLeft (a * d) (b * c) f in
  rewrite multDistributesOverPlusLeft (a * c) (b * d) f in
  rewrite multDistributesOverPlusLeft (a * d) (b * c) e in
  rewrite multAssociative a c e in
  rewrite multAssociative a d f in
  rewrite multAssociative b c f in
  rewrite multAssociative b d e in
  rewrite multAssociative a c f in
  rewrite multAssociative a d e in
  rewrite multAssociative b c e in
  rewrite multAssociative b d f in
  rewrite plusCommutative (b * c * f) (b * d * e) in
  rewrite plusAssociative (a * c * e + a * d * f) (b * d * e) (b * c * f) in
  rewrite sym $ plusAssociative (a * c * e) (a * d * f) (b * d * e) in
  rewrite plusCommutative (a * d * f) (b * d * e) in
  rewrite plusAssociative (a * c * e) (b * d * e) (a * d * f) in
  rewrite sym $ plusAssociative (a * c * e + b * d * e) (a * d * f) (b * c * f) in
  rewrite plusAssociative (a * c * f + b * d * f) (a * d * e) (b * c * e) in
  rewrite plusCommutative (a * c * f) (b * d * f) in
  rewrite sym $ plusAssociative (b * d * f) (a * c * f) (a * d * e) in
  rewrite plusCommutative (b * d * f) (a * c * f + a * d * e) in
  rewrite sym $ plusAssociative (a * c * f + a * d * e) (b * d * f) (b * c * e) in
  rewrite plusCommutative (b * d * f) (b * c * e) in Refl

multDistributesOverPlusRightZ : (x, y, z : ZZ) -> x * (y + z) = (x * y) + (x * z)
multDistributesOverPlusRightZ (Minus a b) (Minus c d) (Minus e f) =
  rewrite multDistributesOverPlusRight a c e in
  rewrite multDistributesOverPlusRight b d f in
  rewrite multDistributesOverPlusRight a d f in
  rewrite multDistributesOverPlusRight b c e in
  rewrite plusAssociative (a * c + a * e) (b * d) (b * f) in
  rewrite sym $ plusAssociative (a * c) (a * e) (b * d) in
  rewrite plusCommutative (a * e) (b * d) in
  rewrite plusAssociative (a * c) (b * d) (a * e) in
  rewrite sym $ plusAssociative (a * c + b * d) (a * e) (b * f) in
  rewrite plusAssociative (a * d + a * f) (b * c) (b * e) in
  rewrite sym $ plusAssociative (a * d) (a * f) (b * c) in
  rewrite plusCommutative (a * f) (b * c) in
  rewrite plusAssociative (a * d) (b * c) (a * f) in
  rewrite sym $ plusAssociative (a * d + b * c) (a * f) (b * e) in Refl

multDistributesOverPlusLeftZ : (x, y, z : ZZ) -> (x + y) * z = (x * z) + (y * z)
multDistributesOverPlusLeftZ x y z =
  rewrite multCommutativeZ (x + y) z in
  rewrite multDistributesOverPlusRightZ z x y in
  rewrite multCommutativeZ z x in
  rewrite multCommutativeZ z y in Refl