@@ -1,4 +1,4 @@
1−module Data.Z
1+module Data.ZZ
3import Decidable.Equality
3import Decidable.Equality
4import Data.Sign
4import Data.Sign
@@ -9,82 +9,82 @@ import Data.Sign
10-- | An integer is either a positive nat or the negated successor of a nat.
10-- | An integer is either a positive nat or the negated successor of a nat.
11-- Zero is chosen to be positive.
11-- Zero is chosen to be positive.
12−data Z = Pos Nat | NegS Nat
12+data ZZ = Pos Nat | NegS Nat
14−instance Signed Z where
14+instance Signed ZZ where
15 sign (Pos _) = Plus
15 sign (Pos _) = Plus
16 sign (NegS _) = Minus
16 sign (NegS _) = Minus
18−absZ : Z -> Nat
18+absZ : ZZ -> Nat
19absZ (Pos n) = n
19absZ (Pos n) = n
20absZ (NegS n) = S n
20absZ (NegS n) = S n
22−instance Show Z where
22+instance Show ZZ where
23 show (Pos n) = show n
23 show (Pos n) = show n
24 show (NegS n) = "-" ++ show (S n)
24 show (NegS n) = "-" ++ show (S n)
26−negZ : Z -> Z
26+negZ : ZZ -> ZZ
27negZ (Pos O) = Pos O
27negZ (Pos O) = Pos O
28negZ (Pos (S n)) = NegS n
28negZ (Pos (S n)) = NegS n
29negZ (NegS n) = Pos (S n)
29negZ (NegS n) = Pos (S n)
31−negNat : Nat -> Z
31+negNat : Nat -> ZZ
32negNat O = Pos O
32negNat O = Pos O
33negNat (S n) = NegS n
33negNat (S n) = NegS n
35−minusNatZ : Nat -> Nat -> Z
35+minusNatZ : Nat -> Nat -> ZZ
36minusNatZ n O = Pos n
36minusNatZ n O = Pos n
37minusNatZ O (S m) = NegS m
37minusNatZ O (S m) = NegS m
38minusNatZ (S n) (S m) = minusNatZ n m
38minusNatZ (S n) (S m) = minusNatZ n m
40−plusZ : Z -> Z -> Z
40+plusZ : ZZ -> ZZ -> ZZ
41plusZ (Pos n) (Pos m) = Pos (n + m)
41plusZ (Pos n) (Pos m) = Pos (n + m)
42plusZ (NegS n) (NegS m) = NegS (S (n + m))
42plusZ (NegS n) (NegS m) = NegS (S (n + m))
43plusZ (Pos n) (NegS m) = minusNatZ n (S m)
43plusZ (Pos n) (NegS m) = minusNatZ n (S m)
44plusZ (NegS n) (Pos m) = minusNatZ m (S n)
44plusZ (NegS n) (Pos m) = minusNatZ m (S n)
46−subZ : Z -> Z -> Z
46+subZ : ZZ -> ZZ -> ZZ
47subZ n m = plusZ n (negZ m)
47subZ n m = plusZ n (negZ m)
49−instance Eq Z where
49+instance Eq ZZ where
50 (Pos n) == (Pos m) = n == m
50 (Pos n) == (Pos m) = n == m
51 (NegS n) == (NegS m) = n == m
51 (NegS n) == (NegS m) = n == m
52 _ == _ = False
52 _ == _ = False
55−instance Ord Z where
55+instance Ord ZZ where
56 compare (Pos n) (Pos m) = compare n m
56 compare (Pos n) (Pos m) = compare n m
57 compare (NegS n) (NegS m) = compare m n
57 compare (NegS n) (NegS m) = compare m n
58 compare (Pos _) (NegS _) = GT
58 compare (Pos _) (NegS _) = GT
59 compare (NegS _) (Pos _) = LT
59 compare (NegS _) (Pos _) = LT
62−multZ : Z -> Z -> Z
62+multZ : ZZ -> ZZ -> ZZ
63multZ (Pos n) (Pos m) = Pos $ n * m
63multZ (Pos n) (Pos m) = Pos $ n * m
64multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
64multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
65multZ (NegS n) (Pos m) = negNat $ (S n) * m
65multZ (NegS n) (Pos m) = negNat $ (S n) * m
66multZ (Pos n) (NegS m) = negNat $ n * (S m)
66multZ (Pos n) (NegS m) = negNat $ n * (S m)
68−fromInt : Integer -> Z
68+fromInt : Integer -> ZZ
69fromInt n = if n < 0
69fromInt n = if n < 0
70 then NegS $ fromInteger {a=Nat} (-n - 1)
70 then NegS $ fromInteger {a=Nat} (-n - 1)
71 else Pos $ fromInteger {a=Nat} n
71 else Pos $ fromInteger {a=Nat} n
73−instance Cast Nat Z where
73+instance Cast Nat ZZ where
74 cast n = Pos n
74 cast n = Pos n
76−instance Num Z where
76+instance Num ZZ where
77 (+) = plusZ
77 (+) = plusZ
78 (-) = subZ
78 (-) = subZ
79 (*) = multZ
79 (*) = multZ
80 abs = cast . absZ
80 abs = cast . absZ
81 fromInteger = fromInt
81 fromInteger = fromInt
83−instance Cast Z Integer where
83+instance Cast ZZ Integer where
84 cast (Pos n) = cast n
84 cast (Pos n) = cast n
85 cast (NegS n) = (-1) * (cast n + 1)
85 cast (NegS n) = (-1) * (cast n + 1)
87−instance Cast Integer Z where
87+instance Cast Integer ZZ where
88 cast = fromInteger
88 cast = fromInteger
@@ -100,7 +100,7 @@ natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
100 -> n * m = x -> (Pos n) * (Pos m) = Pos x
100 -> n * m = x -> (Pos n) * (Pos m) = Pos x
101natMultZMult n m x h = cong h
101natMultZMult n m x h = cong h
103−doubleNegElim : (z : Z) -> negZ (negZ z) = z
103+doubleNegElim : (z : ZZ) -> negZ (negZ z) = z
104doubleNegElim (Pos O) = refl
104doubleNegElim (Pos O) = refl
105doubleNegElim (Pos (S n)) = refl
105doubleNegElim (Pos (S n)) = refl
106doubleNegElim (NegS O) = refl
106doubleNegElim (NegS O) = refl
@@ -117,7 +117,7 @@ posNotNeg : Pos n = NegS m -> _|_
117posNotNeg refl impossible
117posNotNeg refl impossible
119-- Decidable equality
119-- Decidable equality
120−instance DecEq Z where
120+instance DecEq ZZ where
121 decEq (Pos n) (NegS m) = No posNotNeg
121 decEq (Pos n) (NegS m) = No posNotNeg
122 decEq (NegS n) (Pos m) = No $ negEqSym posNotNeg
122 decEq (NegS n) (Pos m) = No $ negEqSym posNotNeg
123 decEq (Pos n) (Pos m) with (decEq n m)
123 decEq (Pos n) (Pos m) with (decEq n m)
@@ -128,15 +128,15 @@ instance DecEq Z where
128 | No p = No $ \h => p $ negSInjective h
128 | No p = No $ \h => p $ negSInjective h
131−plusZeroLeftNeutralZ : (right : Z) -> 0 + right = right
131+plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right
132plusZeroLeftNeutralZ (Pos n) = refl
132plusZeroLeftNeutralZ (Pos n) = refl
133plusZeroLeftNeutralZ (NegS n) = refl
133plusZeroLeftNeutralZ (NegS n) = refl
135−plusZeroRightNeutralZ : (left : Z) -> left + 0 = left
135+plusZeroRightNeutralZ : (left : ZZ) -> left + 0 = left
136plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n
136plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n
137plusZeroRightNeutralZ (NegS n) = refl
137plusZeroRightNeutralZ (NegS n) = refl
139−plusCommutativeZ : (left : Z) -> (right : Z) -> (left + right = right + left)
139+plusCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left + right = right + left)
140plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m
140plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m
141plusCommutativeZ (Pos n) (NegS m) = refl
141plusCommutativeZ (Pos n) (NegS m) = refl
142plusCommutativeZ (NegS n) (Pos m) = refl
142plusCommutativeZ (NegS n) (Pos m) = refl