git.iko.soy/Idris-dev
on fa29447 help sign in
Idris-dev/lib/Data/Z.idr
144 lines 3.6 kB history raw
1module Data.Z
3import Decidable.Equality
4import Data.Sign
6%default total
7%access public
10-- | An integer is either a positive nat or the negated successor of a nat.
11-- Zero is chosen to be positive.
12data Z = Pos Nat | NegS Nat
14instance Signed Z where
15 sign (Pos _) = Plus
16 sign (NegS _) = Minus
18absZ : Z -> Nat
19absZ (Pos n) = n
20absZ (NegS n) = S n
22instance Show Z where
23 show (Pos n) = show n
24 show (NegS n) = "-" ++ show (S n)
26negZ : Z -> Z
27negZ (Pos O) = Pos O
28negZ (Pos (S n)) = NegS n
29negZ (NegS n) = Pos (S n)
31negNat : Nat -> Z
32negNat O = Pos O
33negNat (S n) = NegS n
35minusNatZ : Nat -> Nat -> Z
36minusNatZ n O = Pos n
37minusNatZ O (S m) = NegS m
38minusNatZ (S n) (S m) = minusNatZ n m
40plusZ : Z -> Z -> Z
41plusZ (Pos n) (Pos m) = Pos (n + m)
42plusZ (NegS n) (NegS m) = NegS (S (n + m))
43plusZ (Pos n) (NegS m) = minusNatZ n (S m)
44plusZ (NegS n) (Pos m) = minusNatZ m (S n)
46subZ : Z -> Z -> Z
47subZ n m = plusZ n (negZ m)
49instance Eq Z where
50 (Pos n) == (Pos m) = n == m
51 (NegS n) == (NegS m) = n == m
52 _ == _ = False
55instance Ord Z where
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
62multZ : Z -> Z -> Z
63multZ (Pos n) (Pos m) = Pos $ n * m
64multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
65multZ (NegS n) (Pos m) = negNat $ (S n) * m
66multZ (Pos n) (NegS m) = negNat $ n * (S m)
68fromInt : Int -> Z
69fromInt n = if n < 0
70 then NegS $ fromInteger {a=Nat} (-n - 1)
71 else Pos $ fromInteger {a=Nat} n
73instance Cast Nat Z where
74 cast n = Pos n
76instance Num Z where
77 (+) = plusZ
78 (-) = subZ
79 (*) = multZ
80 abs = cast . absZ
81 fromInteger = fromInt
83instance Cast Z Int where
84 cast (Pos n) = cast n
85 cast (NegS n) = (-1) * (cast n + 1)
87instance Cast Int Z where
88 cast = fromInteger
91--------------------------------------------------------------------------------
92-- Properties
93--------------------------------------------------------------------------------
95natPlusZPlus : (n : Nat) -> (m : Nat) -> (x : Nat)
96 -> n + m = x -> (Pos n) + (Pos m) = Pos x
97natPlusZPlus n m x h = cong h
99natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
100 -> n * m = x -> (Pos n) * (Pos m) = Pos x
101natMultZMult n m x h = cong h
103doubleNegElim : (z : Z) -> negZ (negZ z) = z
104doubleNegElim (Pos O) = refl
105doubleNegElim (Pos (S n)) = refl
106doubleNegElim (NegS O) = refl
107doubleNegElim (NegS (S n)) = refl
109-- Injectivity
110posInjective : Pos n = Pos m -> n = m
111posInjective refl = refl
113negSInjective : NegS n = NegS m -> n = m
114negSInjective refl = refl
116posNotNeg : Pos n = NegS m -> _|_
117posNotNeg refl impossible
119-- Decidable equality
120instance 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
130-- Plus
131plusZeroLeftNeutralZ : (right : Z) -> 0 + right = right
132plusZeroLeftNeutralZ (Pos n) = refl
133plusZeroLeftNeutralZ (NegS n) = refl
135plusZeroRightNeutralZ : (left : Z) -> left + 0 = left
136plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n
137plusZeroRightNeutralZ (NegS n) = refl
139plusCommutativeZ : (left : Z) -> (right : Z) -> (left + right = right + left)
140plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m
141plusCommutativeZ (Pos n) (NegS m) = refl
142plusCommutativeZ (NegS n) (Pos m) = refl
143plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m