Data.INTEGER


   0 | module Data.INTEGER
   1 | 
   2 | import Data.Nat
   3 | import Syntax.PreorderReasoning
   4 | 
   5 | %default total
   6 | 
   7 | public export
   8 | data INTEGER : Type where
   9 |   Z : INTEGER
  10 |   PS : Nat -> INTEGER
  11 |   NS : Nat -> INTEGER
  12 | 
  13 | public export
  14 | Cast Nat INTEGER where
  15 |   cast Z = Z
  16 |   cast (S n) = PS n
  17 | 
  18 | public export
  19 | Cast Integer INTEGER where
  20 |   cast i = case compare 0 i of
  21 |     LT => PS (cast (i - 1))
  22 |     EQ => Z
  23 |     GT => NS (cast (negate i - 1))
  24 | 
  25 | public export
  26 | Cast INTEGER Integer where
  27 |   cast Z = 0
  28 |   cast (PS n) = 1 + cast n
  29 |   cast (NS n) = negate (1 + cast n)
  30 | 
  31 | public export
  32 | Show INTEGER where
  33 |   show = show . cast {to = Integer}
  34 | 
  35 | public export
  36 | add : INTEGER -> INTEGER -> INTEGER
  37 | add Z n = n
  38 | add m Z = m
  39 | add (PS m) (PS n) = PS (S (m + n))
  40 | add (NS m) (NS n) = NS (S (m + n))
  41 | add (PS m) (NS n) = case compare m n of
  42 |   LT => NS (minus n (S m)) -- 1+m-1-n = 1+(m-n-1)
  43 |   EQ => Z
  44 |   GT => PS (minus m (S n))
  45 | add (NS n) (PS m) = case compare m n of
  46 |   LT => NS (minus n (S m))
  47 |   EQ => Z
  48 |   GT => PS (minus m (S n))
  49 | 
  50 | public export
  51 | mult : INTEGER -> INTEGER -> INTEGER
  52 | mult Z n = Z
  53 | mult m Z = Z
  54 | mult (PS m) (PS n) = PS (m * n + m + n)
  55 | mult (NS m) (NS n) = PS (m * n + m + n)
  56 | mult (PS m) (NS n) = NS (m * n + m + n)
  57 | mult (NS m) (PS n) = NS (m * n + m + n)
  58 | 
  59 | public export
  60 | Num INTEGER where
  61 |   fromInteger = cast
  62 |   (+) = add
  63 |   (*) = mult
  64 | 
  65 | export
  66 | plusZeroRightNeutral : (m : INTEGER) -> m + 0 === m
  67 | plusZeroRightNeutral Z = Refl
  68 | plusZeroRightNeutral (PS k) = Refl
  69 | plusZeroRightNeutral (NS k) = Refl
  70 | 
  71 | export
  72 | plusCommutative : (m, n : INTEGER) -> m + n === n + m
  73 | plusCommutative Z n = sym $ plusZeroRightNeutral n
  74 | plusCommutative m Z = plusZeroRightNeutral m
  75 | plusCommutative (PS k) (PS j) = cong (PS . S) (plusCommutative k j)
  76 | plusCommutative (NS k) (NS j) = cong (NS . S) (plusCommutative k j)
  77 | plusCommutative (PS k) (NS j) with (compare k j)
  78 |   _ | LT = Refl
  79 |   _ | EQ = Refl
  80 |   _ | GT = Refl
  81 | plusCommutative (NS k) (PS j) with (compare j k)
  82 |   _ | LT = Refl
  83 |   _ | EQ = Refl
  84 |   _ | GT = Refl
  85 | 
  86 | export
  87 | castPlus : (m, n : Nat) -> the INTEGER (cast (m + n)) = cast m + cast n
  88 | castPlus 0     n     = Refl
  89 | castPlus (S m) 0     = cong PS (plusZeroRightNeutral m)
  90 | castPlus (S m) (S n) = cong PS (sym $ plusSuccRightSucc m n)
  91 | 
  92 | public export
  93 | Neg INTEGER where
  94 |   negate Z = Z
  95 |   negate (PS n) = NS n
  96 |   negate (NS n) = PS n
  97 | 
  98 |   m - n = add m (negate n)
  99 | 
 100 | export
 101 | unfoldPS : (m : Nat) -> PS m === 1 + cast m
 102 | unfoldPS Z = Refl
 103 | unfoldPS (S m) = Refl
 104 | 
 105 | export
 106 | unfoldNS : (m : Nat) -> NS m === - 1 - cast m
 107 | unfoldNS Z = Refl
 108 | unfoldNS (S m) = Refl
 109 | 
 110 | export
 111 | difference : (m, n : Nat) -> INTEGER
 112 | difference 0 n = - cast n
 113 | difference m 0 = cast m
 114 | difference (S m) (S n) = difference m n
 115 | 
 116 | export
 117 | differenceZeroRight : (n : Nat) -> difference n 0 === cast n
 118 | differenceZeroRight 0 = Refl
 119 | differenceZeroRight (S k) = Refl
 120 | 
 121 | export
 122 | minusSuccSucc : (m, n : Nat) ->
 123 |   the INTEGER (cast (S m) - cast (S n)) === cast m - cast n
 124 | minusSuccSucc 0 0 = Refl
 125 | minusSuccSucc 0 (S n) = cong NS (minusZeroRight n)
 126 | minusSuccSucc (S m) 0 = cong PS (minusZeroRight m)
 127 | minusSuccSucc (S m) (S n) with (compare m n)
 128 |   _ | LT = Refl
 129 |   _ | EQ = Refl
 130 |   _ | GT = Refl
 131 | 
 132 | export
 133 | unfoldDifference : (m, n : Nat) -> difference m n === cast m - cast n
 134 | unfoldDifference 0 n = Refl
 135 | unfoldDifference m 0 = Calc $
 136 |   |~ difference m 0
 137 |   ~~ cast m     ...( differenceZeroRight m )
 138 |   ~~ cast m + 0 ...( sym (plusZeroRightNeutral $ cast m) )
 139 | unfoldDifference (S m) (S n) = Calc $
 140 |   |~ difference m n
 141 |   ~~ cast m - cast n         ...( unfoldDifference m n )
 142 |   ~~ cast (S m) - cast (S n) ...( sym (minusSuccSucc m n) )
 143 | 
 144 | export
 145 | negateInvolutive : (m : INTEGER) -> - - m === m
 146 | negateInvolutive Z = Refl
 147 | negateInvolutive (PS k) = Refl
 148 | negateInvolutive (NS k) = Refl
 149 | 
 150 | export
 151 | negatePlus : (m, n : INTEGER) -> - (m + n) === - m + - n
 152 | negatePlus Z n = Refl
 153 | negatePlus (PS k) Z = Refl
 154 | negatePlus (NS k) Z = Refl
 155 | negatePlus (PS k) (PS j) = Refl
 156 | negatePlus (PS k) (NS j) with (compare k j) proof eq
 157 |   _ | LT = rewrite compareNatFlip k j in rewrite eq in Refl
 158 |   _ | EQ = rewrite compareNatFlip k j in rewrite eq in Refl
 159 |   _ | GT = rewrite compareNatFlip k j in rewrite eq in Refl
 160 | negatePlus (NS k) (PS j) with (compare k j) proof eq
 161 |   _ | LT = rewrite compareNatFlip k j in rewrite eq in Refl
 162 |   _ | EQ = rewrite compareNatFlip k j in rewrite eq in Refl
 163 |   _ | GT = rewrite compareNatFlip k j in rewrite eq in Refl
 164 | negatePlus (NS k) (NS j) = Refl
 165 | 
 166 | export
 167 | negateDifference : (m, n : Nat) -> - difference m n === difference n m
 168 | negateDifference 0 n = Calc $
 169 |   |~ - - cast n
 170 |   ~~ cast n         ...( negateInvolutive (cast n) )
 171 |   ~~ difference n 0 ...( sym (differenceZeroRight n) )
 172 | negateDifference m 0 = cong negate (differenceZeroRight m)
 173 | negateDifference (S m) (S n) = negateDifference m n
 174 | 
 175 | plusNatDifferenceLeft : (m, n, p : Nat) ->
 176 |   cast m + difference n p === difference (m + n) p
 177 | plusNatDifferenceLeft m 0 p = Calc $
 178 |   |~ cast m - cast p
 179 |   ~~ difference m p
 180 |     ...( sym (unfoldDifference m p) )
 181 |   ~~ difference (m + 0) p
 182 |     ...( cong (flip difference p) (sym $ plusZeroRightNeutral m) )
 183 | plusNatDifferenceLeft m (S n) p = Calc $
 184 |   |~ cast m + difference (S n) p
 185 |   ~~ PS m + difference n p
 186 |      ...( sym (aux n p m) )
 187 |   ~~ difference (S m + n) p
 188 |      ...( plusNatDifferenceLeft (S m) n p )
 189 |   ~~ difference (m + S n) p
 190 |      ...( cong (flip difference p) (plusSuccRightSucc m n) )
 191 | 
 192 |  where
 193 | 
 194 |   aux : (m, n, p : Nat) -> PS p + difference m n === cast p + difference (S m) n
 195 |   aux 0 0 p = Calc $
 196 |     |~ PS p
 197 |     ~~ 1 + cast p ...( unfoldPS p )
 198 |     ~~ cast p + 1 ...( plusCommutative 1 (cast p) )
 199 |   aux 0 (S k) p = Calc $
 200 |     |~ PS p + NS k
 201 |     ~~ difference (S p) (S k) ...( sym (unfoldDifference (S p) (S k)) )
 202 |     ~~ difference p k         ...( Refl )
 203 |     ~~ cast p - cast k        ...( unfoldDifference p k )
 204 |   aux (S k) 0 p = sym $ Calc $
 205 |     |~ cast p + PS (S k)
 206 |     ~~ cast (p + S (S k)) ...( sym (castPlus p (S (S k))) )
 207 |     ~~ cast (S (p + S k)) ...( cong cast (sym $ plusSuccRightSucc p (S k)) )
 208 |     ~~ cast (S (S p + k)) ...( cong PS (sym $ plusSuccRightSucc p k) )
 209 |   aux (S k) (S j) p = aux k j p
 210 | 
 211 | minusNatDifferenceRight : (m, n, p : Nat) ->
 212 |   - cast m + difference n p === difference n (m + p)
 213 | minusNatDifferenceRight m n p = Calc $
 214 |   |~ - cast m + difference n p
 215 |   ~~ - cast m - - difference n p
 216 |      ...( cong (- cast m +) (sym $ negateInvolutive ?) )
 217 |   ~~ - (cast m - difference n p)
 218 |      ...( sym (negatePlus (cast m) (- difference n p)) )
 219 |   ~~ - (cast m + difference p n)
 220 |      ...( cong (negate . (cast m +)) (negateDifference n p) )
 221 |   ~~ - (difference (m + p) n)
 222 |      ...( cong negate (plusNatDifferenceLeft m p n) )
 223 |   ~~ - - difference n (m + p)
 224 |      ...( cong negate (sym $ negateDifference n (m + p)) )
 225 |   ~~ difference n (m + p)
 226 |      ...( negateInvolutive ? )
 227 | 
 228 | 
 229 | export
 230 | minusZeroRight : (m : INTEGER) -> m - 0 === m
 231 | minusZeroRight = plusZeroRightNeutral
 232 | 
 233 | 
 234 | export
 235 | plusInverse : (m : INTEGER) -> m - m === Z
 236 | plusInverse Z      = Refl
 237 | plusInverse (PS k) = rewrite compareNatDiag k in Refl
 238 | plusInverse (NS k) = rewrite compareNatDiag k in Refl
 239 | 
 240 | export
 241 | plusAssociative : (m, n, p : INTEGER) -> m + (n + p) === (m + n) + p
 242 | plusAssociative Z n p = Refl
 243 | plusAssociative m Z p = cong (+ p) (sym $ plusZeroRightNeutral m)
 244 | plusAssociative m n Z = Calc $
 245 |   |~ m + (n + Z)
 246 |   ~~ m + n     ...( cong (m +) (plusZeroRightNeutral n) )
 247 |   ~~ m + n + Z ...( sym $ plusZeroRightNeutral (m + n) )
 248 | plusAssociative (PS k) (PS j) (PS i) = cong (PS . S) $ Calc $
 249 |   |~ k + S (j + i)
 250 |   ~~ S (k + (j + i)) ...( sym (plusSuccRightSucc k (j + i)) )
 251 |   ~~ S ((k + j) + i) ...( cong S (plusAssociative k j i) )
 252 | plusAssociative (PS k) (PS j) (NS i) = Calc $
 253 |   |~ PS k + (PS j - PS i)
 254 |   ~~ PS k + difference (S j) (S i)
 255 |      ...( cong (PS k +) (sym $ unfoldDifference (S j) (S i)) )
 256 |   ~~ difference (S k + S j) (S i)
 257 |      ...( plusNatDifferenceLeft (S k) (S j) (S i) )
 258 |   ~~ difference (S (S (k + j))) (S i)
 259 |      ...( cong (flip difference (S i)) (sym $ plusSuccRightSucc (S k) j) )
 260 |   ~~ PS k + PS j - PS i
 261 |      ...( unfoldDifference (S (S (k + j))) (S i) )
 262 | plusAssociative (PS k) (NS j) (PS i) = Calc $
 263 |   |~ PS k + (NS j + PS i)
 264 |   ~~ PS k + (PS i + NS j)
 265 |      ...( cong (PS k +) (plusCommutative (NS j) (PS i)) )
 266 |   ~~ PS k + difference (S i) (S j)
 267 |      ...( cong (PS k +) (sym $ unfoldDifference (S i) (S j)) )
 268 |   ~~ difference (S k + S i) (S j)
 269 |      ...( plusNatDifferenceLeft (S k) (S i) (S j) )
 270 |   ~~ difference (S i + S k) (S j)
 271 |      ...( cong (flip difference (S j)) (plusCommutative (S k) (S i)) )
 272 |   ~~ PS i + difference (S k) (S j)
 273 |      ...( sym (plusNatDifferenceLeft (S i) (S k) (S j)) )
 274 |   ~~ difference (S k) (S j) + PS i
 275 |      ...( plusCommutative (PS i) (difference (S k) (S j)) )
 276 |   ~~ PS k + NS j + PS i
 277 |      ...( cong (+ PS i) (unfoldDifference (S k) (S j)) )
 278 | plusAssociative (PS k) (NS j) (NS i) = Calc $
 279 |   |~ PS k + NS (S j + i)
 280 |   ~~ difference (S k) (S (S j + i))
 281 |      ...( sym (unfoldDifference (S k) (S (S j + i))) )
 282 |   ~~ difference (S k) (S i + S j)
 283 |      ...( cong (difference k) (plusCommutative (S j) i) )
 284 |   ~~ NS i + difference (S k) (S j)
 285 |      ...( sym (minusNatDifferenceRight (S i) (S k) (S j)) )
 286 |   ~~ difference (S k) (S j) + NS i
 287 |      ...( plusCommutative (NS i) (difference (S k) (S j)) )
 288 |   ~~ (PS k + NS j) + NS i
 289 |      ...( cong (+ NS i) (unfoldDifference (S k) (S j)) )
 290 | plusAssociative (NS k) (PS j) (PS i) = Calc $
 291 |   |~ NS k + (PS j + PS i)
 292 |   ~~ (PS j + PS i) + NS k
 293 |      ...( plusCommutative (NS k) (PS j + PS i) )
 294 |   ~~ difference (S (S (j + i))) (S k)
 295 |      ...( sym (unfoldDifference (S (S (j + i))) (S k)) )
 296 |   ~~ difference (S i + S j) (S k)
 297 |      ...( cong (flip difference k) (plusCommutative (S j) i) )
 298 |   ~~ PS i + difference (S j) (S k)
 299 |      ...( sym (plusNatDifferenceLeft (S i) (S j) (S k)) )
 300 |   ~~ difference (S j) (S k) + PS i
 301 |      ...( plusCommutative (PS i) (difference (S j) (S k)) )
 302 |   ~~ (PS j + NS k) + PS i
 303 |      ...( cong (+ PS i) (unfoldDifference (S j) (S k)) )
 304 |   ~~ (NS k + PS j) + PS i
 305 |      ...( cong (+ PS i) (plusCommutative (PS j) (NS k)) )
 306 | plusAssociative (NS k) (PS j) (NS i) = Calc $
 307 |   |~ NS k + (PS j + NS i)
 308 |   ~~ NS k + difference (S j) (S i)
 309 |      ...( cong (NS k +) (sym $ unfoldDifference (S j) (S i)) )
 310 |   ~~ difference (S j) (S k + S i)
 311 |      ...( minusNatDifferenceRight (S k) (S j) (S i) )
 312 |   ~~ difference (S j) (S i + S k)
 313 |      ...( cong (difference (S j)) (plusCommutative (S k) (S i)) )
 314 |   ~~ NS i + difference (S j) (S k)
 315 |      ...( sym (minusNatDifferenceRight (S i) (S j) (S k)) )
 316 |   ~~ difference (S j) (S k) + NS i
 317 |      ...( plusCommutative (NS i) (difference (S j) (S k)) )
 318 |   ~~ (PS j + NS k) + NS i
 319 |      ...( cong (+ NS i) (unfoldDifference (S j) (S k)) )
 320 |   ~~ (NS k + PS j) + NS i
 321 |      ...( cong (+ NS i) (plusCommutative (PS j) (NS k)) )
 322 | plusAssociative (NS k) (NS j) (PS i) = Calc $
 323 |   |~ NS k + (NS j + PS i)
 324 |   ~~ NS k + (PS i + NS j)
 325 |      ...( cong (NS k +) (plusCommutative (NS j) (PS i)) )
 326 |   ~~ NS k + difference (S i) (S j)
 327 |      ...( cong (NS k +) (sym $ unfoldDifference (S i) (S j)) )
 328 |   ~~ difference (S i) (S k + S j)
 329 |      ...( minusNatDifferenceRight (S k) (S i) (S j) )
 330 |   ~~ difference (S i) (S (S (k + j)))
 331 |      ...( cong (difference i) (sym $ plusSuccRightSucc k j) )
 332 |   ~~ PS i + (NS k + NS j)
 333 |      ...( unfoldDifference (S i) (S (S (k + j))) )
 334 |   ~~ (NS k + NS j) + PS i
 335 |      ...( plusCommutative (PS i) (NS k + NS j) )
 336 | plusAssociative (NS k) (NS j) (NS i) = cong (NS . S) $ Calc $
 337 |   |~ k + S (j + i)
 338 |   ~~ S (k + (j + i)) ...( sym (plusSuccRightSucc k (j + i)) )
 339 |   ~~ S ((k + j) + i) ...( cong S (plusAssociative k j i) )
 340 |