IntegralDomain.idr

import ZZ

%default total

integralDomainN : Not (m = Z) -> Not (n = Z) -> Not (m * n = Z)
integralDomainN mNotZ nNotZ mnEqZ {m = Z} = mNotZ Refl
integralDomainN mNotZ nNotZ mnEqZ {n = Z} = nNotZ Refl
integralDomainN mNotZ nNotZ mnEqZ {m = S a} {n = S b} = uninhabited mnEqZ

infixl 9 |>
(|>) : a -> (a -> b) -> b
(|>) a f = f a

intergalDomainZBaseCase : {a, c, i, j : Nat} -> a * c + (a + S i) * (c + S j) = a * (c + S j) + (a + S i) * c -> Void
intergalDomainZBaseCase {a} {c} {i} {j} prf =
  let
    rhs1 = a * (c + S j) + (a + S i) * c
    lhs1 = a * c + ((a + S i) * c + (a * S j + S i * S j))
    lhs2 = (a + S i) * c + (a * S j + S i * S j)
  in
    prf
    |> replace {P = \z => a * c + z = rhs1} (multDistributesOverPlusRight (a + S i) c (S j))
    |> replace {P = \z => a * c + ((a + S i) * c + z) = rhs1} (multDistributesOverPlusLeft a (S i) (S j))
    |> replace {P = \z => lhs1 = z + (a + S i) * c} (multDistributesOverPlusRight a c (S j))
    |> replace {P = \z => lhs1 = z} (sym $ plusAssociative (a * c) (a * S j) ((a + S i) * c))
    |> plusLeftCancel (a * c) lhs2 (a * S j + (a + S i) * c)
    |> replace {P = \z => lhs2 = z} (plusCommutative (a * S j) ((a + S i) * c))
    |> plusLeftCancel ((a + S i) * c) (a * S j + S i * S j) (a * S j)
    |> replace {P = \z => a * S j + S i * S j = z} (sym $ plusZeroRightNeutral (a * S j))
    |> plusLeftCancel (a * S j) (S i * S j) Z
    |> uninhabited

integralDomainZ : Not (ZZEquiv x 0) -> Not (ZZEquiv y 0) -> Not (ZZEquiv (x * y) 0)
integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus a b} {y = Minus c d} with (diff a b)
  integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus b b} {y = Minus c d} | DiffZ = xNeq0 (IsZZEquiv Refl)
  integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus a (a + S i)} {y = Minus c d} | (LTByS i) with (diff c d)
    integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus a (a + S i)} {y = Minus d d} | (LTByS i) | DiffZ = yNeq0 (IsZZEquiv Refl)
    integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus a (a + S i)} {y = Minus c (c + S j)} | (LTByS i) | (LTByS j) =
      prf
      |> replace {P = \z => z = a * (c + S j) + (a + S i) * c + 0} (plusZeroRightNeutral (a * c + (a + S i) * (c + S j)))
      |> replace {P = \z => a * c + (a + S i) * (c + S j) = z} (plusZeroRightNeutral (a * (c + S j) + (a + S i) * c))
      |> intergalDomainZBaseCase
    integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus a (a + S i)} {y = Minus (d + S j) d} | (LTByS i) | (GTByS j) =
      prf
      |> replace {P = \z => z = a * d + (a + S i) * (d + S j) + 0} (plusZeroRightNeutral (a * (d + S j) + (a + S i) * d))
      |> replace {P = \z => a * (d + S j) + (a + S i) * d = z} (plusZeroRightNeutral (a * d + (a + S i) * (d + S j)))
      |> sym
      |> intergalDomainZBaseCase
  integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus (b + S i) b} {y = Minus c d} | (GTByS i) with (diff c d)
    integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus (b + S i) b} {y = Minus d d} | (GTByS i) | DiffZ = yNeq0 (IsZZEquiv Refl)
    integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus (b + S i) b} {y = Minus c (c + S j)} | (GTByS i) | (LTByS j) =
      prf
      |> replace {P = \z => z = (b + S i) * (c + S j) + b * c + 0} (plusZeroRightNeutral ((b + S i) * c + b * (c + S j)))
      |> replace {P = \z => (b + S i) * c + b * (c + S j) = z} (plusZeroRightNeutral ((b + S i) * (c + S j) + b * c))
      |> sym
      |> replace {P = \z => z = (b + S i) * c + b * (c + S j)} (plusCommutative ((b + S i) * (c + S j)) (b * c))
      |> replace {P = \z => b * c + (b + S i) * (c + S j) = z} (plusCommutative ((b + S i) * c) (b * (c + S j)))
      |> intergalDomainZBaseCase
    integralDomainZ xNeq0 yNeq0 (IsZZEquiv prf) {x = Minus (b + S i) b} {y = Minus (d + S j) d} | (GTByS i) | (GTByS j) =
      prf
      |> replace {P = \z => z = (b + S i) * d + b * (d + S j) + 0} (plusZeroRightNeutral ((b + S i) * (d + S j) + b * d))
      |> replace {P = \z => (b + S i) * (d + S j) + b * d = z} (plusZeroRightNeutral ((b + S i) * d + b * (d + S j)))
      |> replace {P = \z => z = (b + S i) * d + b * (d + S j)} (plusCommutative ((b + S i) * (d + S j)) (b * d))
      |> replace {P = \z => b * d + (b + S i) * (d + S j) = z} (plusCommutative ((b + S i) * d) (b * (d + S j)))
      |> intergalDomainZBaseCase

factorZeroN : {m, n : Nat} -> m * n = 0 -> Either (m = 0) (n = 0)
factorZeroN prf {m = Z}   {n = n}   = Left Refl
factorZeroN prf {m = S k} {n = Z}   = Right Refl
factorZeroN prf {m = S k} {n = S j} = absurd (uninhabited prf)

factorZeroZ : {m, n : ZZ} -> ZZEquiv (m * n) 0 -> Either (ZZEquiv m 0) (ZZEquiv n 0)
factorZeroZ prf {m} {n} = case ((decEquiv m 0, decEquiv n 0)) of
  (Yes p, _    ) => Left p
  (No c1, Yes p) => Right p
  (No c1, No c2) => absurd $ integralDomainZ c1 c2 prf