@@ -0,0 +1,144 @@
3+import Decidable.Equality
10+-- | An integer is either a positive nat or the negated successor of a nat.
11+-- Zero is chosen to be positive.
12+data Z = Pos Nat | NegS Nat
14+instance Signed Z where
16+ sign (NegS _) = Minus
23+ show (Pos n) = show n
24+ show (NegS n) = "-" ++ show (S n)
28+negZ (Pos (S n)) = NegS n
29+negZ (NegS n) = Pos (S n)
35+minusNatZ : Nat -> Nat -> Z
37+minusNatZ O (S m) = NegS m
38+minusNatZ (S n) (S m) = minusNatZ n m
41+plusZ (Pos n) (Pos m) = Pos (n + m)
42+plusZ (NegS n) (NegS m) = NegS (S (n + m))
43+plusZ (Pos n) (NegS m) = minusNatZ n (S m)
44+plusZ (NegS n) (Pos m) = minusNatZ m (S n)
47+subZ n m = plusZ n (negZ m)
50+ (Pos n) == (Pos m) = n == m
51+ (NegS n) == (NegS m) = n == m
56+ compare (Pos n) (Pos m) = compare n m
57+ compare (NegS n) (NegS m) = compare m n
58+ compare (Pos _) (NegS _) = GT
59+ compare (NegS _) (Pos _) = LT
63+multZ (Pos n) (Pos m) = Pos $ n * m
64+multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
65+multZ (NegS n) (Pos m) = negNat $ (S n) * m
66+multZ (Pos n) (NegS m) = negNat $ n * (S m)
70+ then NegS $ fromInteger {a=Nat} (-n - 1)
71+ else Pos $ fromInteger {a=Nat} n
73+instance Cast Nat Z where
81+ fromInteger = fromInt
83+instance Cast Z Int where
84+ cast (Pos n) = cast n
85+ cast (NegS n) = (-1) * (cast n + 1)
87+instance Cast Int Z where
91+--------------------------------------------------------------------------------
93+--------------------------------------------------------------------------------
95+natPlusZPlus : (n : Nat) -> (m : Nat) -> (x : Nat)
96+ -> n + m = x -> (Pos n) + (Pos m) = Pos x
97+natPlusZPlus n m x h = cong h
99+natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
100+ -> n * m = x -> (Pos n) * (Pos m) = Pos x
101+natMultZMult n m x h = cong h
103+doubleNegElim : (z : Z) -> negZ (negZ z) = z
104+doubleNegElim (Pos O) = refl
105+doubleNegElim (Pos (S n)) = refl
106+doubleNegElim (NegS O) = refl
107+doubleNegElim (NegS (S n)) = refl
110+posInjective : Pos n = Pos m -> n = m
111+posInjective refl = refl
113+negSInjective : NegS n = NegS m -> n = m
114+negSInjective refl = refl
116+posNotNeg : Pos n = NegS m -> _|_
117+posNotNeg refl impossible
119+-- Decidable equality
120+instance DecEq Z where
121+ decEq (Pos n) (NegS m) = No posNotNeg
122+ decEq (NegS n) (Pos m) = No $ negEqSym posNotNeg
123+ decEq (Pos n) (Pos m) with (decEq n m)
124+ | Yes p = Yes $ cong p
125+ | No p = No $ \h => p $ posInjective h
126+ decEq (NegS n) (NegS m) with (decEq n m)
127+ | Yes p = Yes $ cong p
128+ | No p = No $ \h => p $ negSInjective h
131+plusZeroLeftNeutralZ : (right : Z) -> 0 + right = right
132+plusZeroLeftNeutralZ (Pos n) = refl
133+plusZeroLeftNeutralZ (NegS n) = refl
135+plusZeroRightNeutralZ : (left : Z) -> left + 0 = left
136+plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n
137+plusZeroRightNeutralZ (NegS n) = refl
139+plusCommutativeZ : (left : Z) -> (right : Z) -> (left + right = right + left)
140+plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m
141+plusCommutativeZ (Pos n) (NegS m) = refl
142+plusCommutativeZ (NegS n) (Pos m) = refl
143+plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m