Last active
February 23, 2021 03:25
-
-
Save SekiT/bcaaffe3d7a2759f6a3a47ee29758ae2 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment