@@ -1,4 +1,4 @@
1−module Data.Z
1+module Data.ZZ
22
33import Decidable.Equality
44import Data.Sign
@@ -9,82 +9,82 @@ import Data.Sign
99
1010-- | An integer is either a positive nat or the negated successor of a nat.
1111-- Zero is chosen to be positive.
12−data Z = Pos Nat | NegS Nat
12+data ZZ = Pos Nat | NegS Nat
1313
14−instance Signed Z where
14+instance Signed ZZ where
1515 sign (Pos _) = Plus
1616 sign (NegS _) = Minus
1717
18−absZ : Z -> Nat
18+absZ : ZZ -> Nat
1919absZ (Pos n) = n
2020absZ (NegS n) = S n
2121
22−instance Show Z where
22+instance Show ZZ where
2323 show (Pos n) = show n
2424 show (NegS n) = "-" ++ show (S n)
2525
26−negZ : Z -> Z
26+negZ : ZZ -> ZZ
2727negZ (Pos O) = Pos O
2828negZ (Pos (S n)) = NegS n
2929negZ (NegS n) = Pos (S n)
3030
31−negNat : Nat -> Z
31+negNat : Nat -> ZZ
3232negNat O = Pos O
3333negNat (S n) = NegS n
3434
35−minusNatZ : Nat -> Nat -> Z
35+minusNatZ : Nat -> Nat -> ZZ
3636minusNatZ n O = Pos n
3737minusNatZ O (S m) = NegS m
3838minusNatZ (S n) (S m) = minusNatZ n m
3939
40−plusZ : Z -> Z -> Z
40+plusZ : ZZ -> ZZ -> ZZ
4141plusZ (Pos n) (Pos m) = Pos (n + m)
4242plusZ (NegS n) (NegS m) = NegS (S (n + m))
4343plusZ (Pos n) (NegS m) = minusNatZ n (S m)
4444plusZ (NegS n) (Pos m) = minusNatZ m (S n)
4545
46−subZ : Z -> Z -> Z
46+subZ : ZZ -> ZZ -> ZZ
4747subZ n m = plusZ n (negZ m)
4848
49−instance Eq Z where
49+instance Eq ZZ where
5050 (Pos n) == (Pos m) = n == m
5151 (NegS n) == (NegS m) = n == m
5252 _ == _ = False
5353
5454
55−instance Ord Z where
55+instance Ord ZZ where
5656 compare (Pos n) (Pos m) = compare n m
5757 compare (NegS n) (NegS m) = compare m n
5858 compare (Pos _) (NegS _) = GT
5959 compare (NegS _) (Pos _) = LT
6060
6161
62−multZ : Z -> Z -> Z
62+multZ : ZZ -> ZZ -> ZZ
6363multZ (Pos n) (Pos m) = Pos $ n * m
6464multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
6565multZ (NegS n) (Pos m) = negNat $ (S n) * m
6666multZ (Pos n) (NegS m) = negNat $ n * (S m)
6767
68−fromInt : Integer -> Z
68+fromInt : Integer -> ZZ
6969fromInt n = if n < 0
7070 then NegS $ fromInteger {a=Nat} (-n - 1)
7171 else Pos $ fromInteger {a=Nat} n
7272
73−instance Cast Nat Z where
73+instance Cast Nat ZZ where
7474 cast n = Pos n
7575
76−instance Num Z where
76+instance Num ZZ where
7777 (+) = plusZ
7878 (-) = subZ
7979 (*) = multZ
8080 abs = cast . absZ
8181 fromInteger = fromInt
8282
83−instance Cast Z Integer where
83+instance Cast ZZ Integer where
8484 cast (Pos n) = cast n
8585 cast (NegS n) = (-1) * (cast n + 1)
8686
87−instance Cast Integer Z where
87+instance Cast Integer ZZ where
8888 cast = fromInteger
8989
9090
@@ -100,7 +100,7 @@ natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
100100 -> n * m = x -> (Pos n) * (Pos m) = Pos x
101101natMultZMult n m x h = cong h
102102
103−doubleNegElim : (z : Z) -> negZ (negZ z) = z
103+doubleNegElim : (z : ZZ) -> negZ (negZ z) = z
104104doubleNegElim (Pos O) = refl
105105doubleNegElim (Pos (S n)) = refl
106106doubleNegElim (NegS O) = refl
@@ -117,7 +117,7 @@ posNotNeg : Pos n = NegS m -> _|_
117117posNotNeg refl impossible
118118
119119-- Decidable equality
120−instance DecEq Z where
120+instance DecEq ZZ where
121121 decEq (Pos n) (NegS m) = No posNotNeg
122122 decEq (NegS n) (Pos m) = No $ negEqSym posNotNeg
123123 decEq (Pos n) (Pos m) with (decEq n m)
@@ -128,15 +128,15 @@ instance DecEq Z where
128128 | No p = No $ \h => p $ negSInjective h
129129
130130-- Plus
131−plusZeroLeftNeutralZ : (right : Z) -> 0 + right = right
131+plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right
132132plusZeroLeftNeutralZ (Pos n) = refl
133133plusZeroLeftNeutralZ (NegS n) = refl
134134
135−plusZeroRightNeutralZ : (left : Z) -> left + 0 = left
135+plusZeroRightNeutralZ : (left : ZZ) -> left + 0 = left
136136plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n
137137plusZeroRightNeutralZ (NegS n) = refl
138138
139−plusCommutativeZ : (left : Z) -> (right : Z) -> (left + right = right + left)
139+plusCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left + right = right + left)
140140plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m
141141plusCommutativeZ (Pos n) (NegS m) = refl
142142plusCommutativeZ (NegS n) (Pos m) = refl