Data.Nat


   0 | module Data.Nat
   1 | 
   2 | import Data.So
   3 | import public Control.Relation
   4 | import public Control.Ord
   5 | import public Control.Order
   6 | import public Control.Function
   7 | import Syntax.PreorderReasoning
   8 | import Syntax.PreorderReasoning.Generic
   9 | 
  10 | %default total
  11 | 
  12 | export
  13 | Uninhabited (Z = S n) where
  14 |   uninhabited Refl impossible
  15 | 
  16 | export
  17 | Uninhabited (S n = Z) where
  18 |   uninhabited Refl impossible
  19 | 
  20 | export
  21 | Uninhabited (a = b) => Uninhabited (S a = S b) where
  22 |   uninhabited Refl @{ab} = uninhabited @{ab} Refl
  23 | 
  24 | public export
  25 | isZero : Nat -> Bool
  26 | isZero Z     = True
  27 | isZero (S n) = False
  28 | 
  29 | public export
  30 | isSucc : Nat -> Bool
  31 | isSucc Z     = False
  32 | isSucc (S n) = True
  33 | 
  34 | ||| A definition of non-zero with a better behaviour than `Not (x = Z)`
  35 | ||| This is amenable to proof search and `NonZero Z` is more readily
  36 | ||| detected as impossible by Idris
  37 | public export
  38 | data IsSucc : (n : Nat) -> Type where
  39 |   ItIsSucc : IsSucc (S n)
  40 | 
  41 | export
  42 | Uninhabited (IsSucc Z) where
  43 |   uninhabited ItIsSucc impossible
  44 | 
  45 | public export
  46 | isItSucc : (n : Nat) -> Dec (IsSucc n)
  47 | isItSucc Z = No absurd
  48 | isItSucc (S n) = Yes ItIsSucc
  49 | 
  50 | ||| A historical synonym for `IsSucc`
  51 | public export
  52 | 0 NonZero : Nat -> Type
  53 | NonZero = IsSucc
  54 | 
  55 | -- Remove as soon as 0.8.0 (or greater) is released
  56 | ||| Use `ItIsSucc` instead
  57 | public export %inline
  58 | %deprecate
  59 | SIsNonZero : NonZero (S n)
  60 | SIsNonZero = ItIsSucc
  61 | 
  62 | public export
  63 | power : Nat -> Nat -> Nat
  64 | power base Z       = S Z
  65 | power base (S exp) = base * (power base exp)
  66 | 
  67 | public export
  68 | hyper : Nat -> Nat -> Nat -> Nat
  69 | hyper Z        a b      = S b
  70 | hyper (S Z)    a Z      = a
  71 | hyper (S(S Z)) a Z      = Z
  72 | hyper n        a Z      = S Z
  73 | hyper (S pn)   a (S pb) = hyper pn a (hyper (S pn) a pb)
  74 | 
  75 | public export
  76 | pred : Nat -> Nat
  77 | pred Z     = Z
  78 | pred (S n) = n
  79 | 
  80 | -- Comparisons
  81 | 
  82 | export
  83 | compareNatDiag : (k : Nat) -> compareNat k k === EQ
  84 | compareNatDiag Z = Refl
  85 | compareNatDiag (S k) = compareNatDiag k
  86 | 
  87 | export
  88 | compareNatFlip : (m, n : Nat) ->
  89 |   flip Prelude.compareNat m n === contra (compareNat m n)
  90 | compareNatFlip 0      0    = Refl
  91 | compareNatFlip 0     (S n) = Refl
  92 | compareNatFlip (S m) 0     = Refl
  93 | compareNatFlip (S m) (S n) = compareNatFlip m n
  94 | 
  95 | public export
  96 | data NotBothZero : (n, m : Nat) -> Type where
  97 |   LeftIsNotZero  : NotBothZero (S n) m
  98 |   RightIsNotZero : NotBothZero n     (S m)
  99 | 
 100 | export
 101 | Uninhabited (NotBothZero 0 0) where
 102 |   uninhabited LeftIsNotZero impossible
 103 |   uninhabited RightIsNotZero impossible
 104 | 
 105 | public export
 106 | data LTE  : (n, m : Nat) -> Type where
 107 |   LTEZero : LTE Z    right
 108 |   LTESucc : LTE left right -> LTE (S left) (S right)
 109 | 
 110 | export
 111 | Uninhabited (LTE (S n) Z) where
 112 |   uninhabited LTEZero impossible
 113 | 
 114 | export
 115 | Uninhabited (LTE m n) => Uninhabited (LTE (S m) (S n)) where
 116 |   uninhabited (LTESucc lte) = uninhabited lte
 117 | 
 118 | public export
 119 | Reflexive Nat LTE where
 120 |   reflexive {x = Z} = LTEZero
 121 |   reflexive {x = S _} = LTESucc $ reflexive
 122 | 
 123 | public export
 124 | Transitive Nat LTE where
 125 |   transitive LTEZero _ = LTEZero
 126 |   transitive (LTESucc xy) (LTESucc yz) =
 127 |     LTESucc $ transitive xy yz
 128 | 
 129 | public export
 130 | Antisymmetric Nat LTE where
 131 |   antisymmetric LTEZero LTEZero = Refl
 132 |   antisymmetric (LTESucc xy) (LTESucc yx) =
 133 |     cong S $ antisymmetric xy yx
 134 | 
 135 | public export
 136 | Connex Nat LTE where
 137 |   connex {x = Z} _ = Left LTEZero
 138 |   connex {y = Z} _ = Right LTEZero
 139 |   connex {x = S _} {y = S _} prf =
 140 |     case connex $ \xy => prf $ cong S xy of
 141 |       Left jk => Left $ LTESucc jk
 142 |       Right kj => Right $ LTESucc kj
 143 | 
 144 | public export
 145 | Preorder Nat LTE where
 146 | 
 147 | public export
 148 | PartialOrder Nat LTE where
 149 | 
 150 | public export
 151 | LinearOrder Nat LTE where
 152 | 
 153 | public export
 154 | GTE : Nat -> Nat -> Type
 155 | GTE left right = LTE right left
 156 | 
 157 | public export
 158 | LT : Nat -> Nat -> Type
 159 | LT left right = LTE (S left) right
 160 | 
 161 | namespace LT
 162 | 
 163 |   ||| LT is defined in terms of LTE which makes it annoying to use.
 164 |   ||| This convenient view of allows us to avoid having to constantly
 165 |   ||| perform nested matches to obtain another LT subproof instead of
 166 |   ||| an LTE one.
 167 |   public export
 168 |   data View : LT m n -> Type where
 169 |     LTZero : View (LTESucc LTEZero)
 170 |     LTSucc : (lt : m `LT` n) -> View (LTESucc lt)
 171 | 
 172 |   ||| Deconstruct an LT proof into either a base case or a further *LT*
 173 |   export
 174 |   view : (lt : LT m n) -> View lt
 175 |   view (LTESucc LTEZero) = LTZero
 176 |   view (LTESucc lt@(LTESucc _)) = LTSucc lt
 177 | 
 178 |   ||| A convenient alias for trivial LT proofs
 179 |   export
 180 |   ltZero : Z `LT` S m
 181 |   ltZero = LTESucc LTEZero
 182 | 
 183 | public export
 184 | GT : Nat -> Nat -> Type
 185 | GT left right = LT right left
 186 | 
 187 | export
 188 | succNotLTEzero : Not (LTE (S m) Z)
 189 | succNotLTEzero LTEZero impossible
 190 | 
 191 | export
 192 | fromLteSucc : LTE (S m) (S n) -> LTE m n
 193 | fromLteSucc (LTESucc x) = x
 194 | 
 195 | export
 196 | succNotLTEpred : Not $ LTE (S x) x
 197 | succNotLTEpred {x = (S right)} (LTESucc y) = succNotLTEpred y
 198 | 
 199 | public export
 200 | isLTE : (m, n : Nat) -> Dec (LTE m n)
 201 | isLTE Z n = Yes LTEZero
 202 | isLTE (S k) Z = No succNotLTEzero
 203 | isLTE (S k) (S j)
 204 |     = case isLTE k j of
 205 |            No contra => No (contra . fromLteSucc)
 206 |            Yes prf => Yes (LTESucc prf)
 207 | 
 208 | public export
 209 | isGTE : (m, n : Nat) -> Dec (GTE m n)
 210 | isGTE m n = isLTE n m
 211 | 
 212 | public export
 213 | isLT : (m, n : Nat) -> Dec (LT m n)
 214 | isLT m n = isLTE (S m) n
 215 | 
 216 | public export
 217 | isGT : (m, n : Nat) -> Dec (GT m n)
 218 | isGT m n = isLT n m
 219 | 
 220 | lteRecallLeft : LTE m n -> (m' : Nat ** m = m')
 221 | lteRecallLeft LTEZero = (0 ** Refl)
 222 | lteRecallLeft (LTESucc x) with (lteRecallLeft x)
 223 |   lteRecallLeft (LTESucc x) | (left ** Refl) = (S left ** Refl)
 224 | 
 225 | irrelevantLte : {m : Nat} -> (0 prf : LTE m n) -> LTE m n
 226 | irrelevantLte {m = 0} LTEZero = LTEZero
 227 | irrelevantLte {m = (S k)} (LTESucc x) = LTESucc (irrelevantLte x)
 228 | 
 229 | lteRecall : LTE m n -> {p : Nat -> Nat} -> (0 prf : LTE (p m) q) -> LTE (p m) q
 230 | lteRecall {m} x prf with (lteRecallLeft x)
 231 |   lteRecall {m = m} x prf | (m ** Refl) = irrelevantLte prf
 232 | 
 233 | ltRecall : LT m n -> {p : Nat -> Nat} -> (0 prf : LT (p m) q) -> LT (p m) q
 234 | ltRecall {m} x prf with (lteRecallLeft x)
 235 |   ltRecall {m = m} x prf | (S m ** Refl) = irrelevantLte prf
 236 | 
 237 | export
 238 | lteSuccRight : LTE n m -> LTE n (S m)
 239 | lteSuccRight LTEZero     = LTEZero
 240 | lteSuccRight (LTESucc x) = LTESucc (lteSuccRight x)
 241 | 
 242 | export
 243 | lteSuccLeft : LTE (S n) m -> LTE n m
 244 | lteSuccLeft (LTESucc x) = lteSuccRight x
 245 | 
 246 | export
 247 | lteAddRight : (n : Nat) -> LTE n (n + m)
 248 | lteAddRight Z = LTEZero
 249 | lteAddRight (S k) {m} = LTESucc (lteAddRight {m} k)
 250 | 
 251 | export
 252 | notLTEImpliesGT : {a, b : Nat} -> Not (a `LTE` b) -> a `GT` b
 253 | notLTEImpliesGT {a = 0  }           not_z_lte_b    = absurd $ not_z_lte_b LTEZero
 254 | notLTEImpliesGT {a = S a} {b = 0  } notLTE = LTESucc LTEZero
 255 | notLTEImpliesGT {a = S a} {b = S k} notLTE = LTESucc (notLTEImpliesGT (notLTE . LTESucc))
 256 | 
 257 | export
 258 | LTEImpliesNotGT : a `LTE` b -> Not (a `GT` b)
 259 | LTEImpliesNotGT LTEZero q = absurd q
 260 | LTEImpliesNotGT (LTESucc p) (LTESucc q) = LTEImpliesNotGT p q
 261 | 
 262 | export
 263 | notLTImpliesGTE : {a, b : _} -> Not (LT a b) -> GTE a b
 264 | notLTImpliesGTE notLT = fromLteSucc $ notLTEImpliesGT notLT
 265 | 
 266 | export
 267 | LTImpliesNotGTE : a `LT` b -> Not (a `GTE` b)
 268 | LTImpliesNotGTE p q = LTEImpliesNotGT q p
 269 | 
 270 | public export
 271 | lte : Nat -> Nat -> Bool
 272 | lte Z        right     = True
 273 | lte left     Z         = False
 274 | lte (S left) (S right) = lte left right
 275 | 
 276 | public export
 277 | gte : Nat -> Nat -> Bool
 278 | gte left right = lte right left
 279 | 
 280 | public export
 281 | lt : Nat -> Nat -> Bool
 282 | lt left right = lte (S left) right
 283 | 
 284 | public export
 285 | gt : Nat -> Nat -> Bool
 286 | gt left right = lt right left
 287 | 
 288 | export
 289 | lteReflectsLTE : (k : Nat) -> (n : Nat) -> lte k n === True -> k `LTE` n
 290 | lteReflectsLTE (S k)  0    _ impossible
 291 | lteReflectsLTE 0      0    _   = LTEZero
 292 | lteReflectsLTE 0     (S k) _   = LTEZero
 293 | lteReflectsLTE (S k) (S j) prf = LTESucc (lteReflectsLTE k j prf)
 294 | 
 295 | export
 296 | gteReflectsGTE : (k : Nat) -> (n : Nat) -> gte k n === True -> k `GTE` n
 297 | gteReflectsGTE k n prf = lteReflectsLTE n k prf
 298 | 
 299 | export
 300 | ltReflectsLT : (k : Nat) -> (n : Nat) -> lt k n === True -> k `LT` n
 301 | ltReflectsLT k n prf = lteReflectsLTE (S k) n prf
 302 | 
 303 | public export
 304 | ltOpReflectsLT : (m,n : Nat) -> So (m < n) -> LT m n
 305 | ltOpReflectsLT 0     (S k) prf = LTESucc LTEZero
 306 | ltOpReflectsLT (S k) (S j) prf = LTESucc (ltOpReflectsLT k j prf)
 307 | ltOpReflectsLT (S k) 0     prf impossible
 308 | ltOpReflectsLT 0 0         prf impossible
 309 | 
 310 | export
 311 | gtReflectsGT : (k : Nat) -> (n : Nat) -> gt k n === True -> k `GT` n
 312 | gtReflectsGT k n prf = ltReflectsLT n k prf
 313 | 
 314 | public export
 315 | minimum : Nat -> Nat -> Nat
 316 | minimum Z m = Z
 317 | minimum (S n) Z = Z
 318 | minimum (S n) (S m) = S (minimum n m)
 319 | 
 320 | public export
 321 | maximum : Nat -> Nat -> Nat
 322 | maximum Z m = m
 323 | maximum (S n) Z = S n
 324 | maximum (S n) (S m) = S (maximum n m)
 325 | 
 326 | -- Proofs on S
 327 | 
 328 | export
 329 | eqSucc : (0 left, right : Nat) -> left = right -> S left = S right
 330 | eqSucc _ _ Refl = Refl
 331 | 
 332 | export
 333 | Injective S where
 334 |   injective Refl = Refl
 335 | 
 336 | export
 337 | SIsNotZ : Not (S x = Z)
 338 | SIsNotZ = absurd
 339 | 
 340 | ||| Auxiliary function:
 341 | ||| mod' fuel a b = a `mod` (S b)
 342 | ||| assuming we have enough fuel
 343 | public export
 344 | mod' : Nat -> Nat -> Nat -> Nat
 345 | mod' Z        centre right = centre
 346 | mod' (S fuel) centre right =
 347 |       if lte centre right then
 348 |         centre
 349 |       else
 350 |         mod' fuel (minus centre (S right)) right
 351 | 
 352 | public export
 353 | modNatNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
 354 | modNatNZ left Z         p = void (absurd p)
 355 | modNatNZ left (S right) _ = mod' left left right
 356 | 
 357 | export partial
 358 | modNat : Nat -> Nat -> Nat
 359 | modNat left (S right) = modNatNZ left (S right) ItIsSucc
 360 | 
 361 | ||| Auxiliary function:
 362 | ||| div' fuel a b = a `div` (S b)
 363 | ||| assuming we have enough fuel
 364 | public export
 365 | div' : Nat -> Nat -> Nat -> Nat
 366 | div' Z        centre right = Z
 367 | div' (S fuel) centre right =
 368 |   if lte centre right then
 369 |     Z
 370 |   else
 371 |     S (div' fuel (minus centre (S right)) right)
 372 | 
 373 | -- 'public' to allow type-level division
 374 | public export
 375 | divNatNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
 376 | divNatNZ left (S right) _ = div' left left right
 377 | 
 378 | export partial
 379 | divNat : Nat -> Nat -> Nat
 380 | divNat left (S right) = divNatNZ left (S right) ItIsSucc
 381 | 
 382 | export
 383 | covering
 384 | divCeilNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
 385 | divCeilNZ x y p = case (modNatNZ x y p) of
 386 |   Z   => divNatNZ x y p
 387 |   S _ => S (divNatNZ x y p)
 388 | 
 389 | export partial
 390 | divCeil : Nat -> Nat -> Nat
 391 | divCeil x (S y) = divCeilNZ x (S y) ItIsSucc
 392 | 
 393 | 
 394 | public export
 395 | divmod' : Nat -> Nat -> Nat -> (Nat, Nat)
 396 | divmod' Z        centre right = (Z, centre)
 397 | divmod' (S fuel) centre right =
 398 |   if lte centre right then
 399 |     (Z, centre)
 400 |   else
 401 |     let qr = divmod' fuel (minus centre (S right)) right
 402 |     in (S (fst qr), snd qr)
 403 | 
 404 | public export
 405 | divmodNatNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> (Nat, Nat)
 406 | divmodNatNZ left (S right) _ = divmod' left left right
 407 | 
 408 | 
 409 | public export
 410 | Integral Nat where
 411 |   div = divNat
 412 |   mod = modNat
 413 | 
 414 | export
 415 | covering
 416 | gcd : (a: Nat) -> (b: Nat) -> {auto 0 ok: NotBothZero a b} -> Nat
 417 | gcd a Z     = a
 418 | gcd Z b     = b
 419 | gcd a (S b) = gcd (S b) (modNatNZ a (S b) ItIsSucc)
 420 | 
 421 | export partial
 422 | lcm : Nat -> Nat -> Nat
 423 | lcm _ Z     = Z
 424 | lcm Z _     = Z
 425 | lcm a (S b) = divNat (a * (S b)) (gcd a (S b))
 426 | 
 427 | --------------------------------------------------------------------------------
 428 | -- An informative comparison view
 429 | --------------------------------------------------------------------------------
 430 | public export
 431 | data CmpNat : Nat -> Nat -> Type where
 432 |      CmpLT : (y : _) -> CmpNat x (x + S y)
 433 |      CmpEQ : CmpNat x x
 434 |      CmpGT : (x : _) -> CmpNat (y + S x) y
 435 | 
 436 | export
 437 | cmp : (x, y : Nat) -> CmpNat x y
 438 | cmp Z Z     = CmpEQ
 439 | cmp Z (S k) = CmpLT _
 440 | cmp (S k) Z = CmpGT _
 441 | cmp (S x) (S y) with (cmp x y)
 442 |   cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k
 443 |   cmp (S x) (S x)           | CmpEQ   = CmpEQ
 444 |   cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k
 445 | 
 446 | -- Proofs on +
 447 | 
 448 | export
 449 | plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
 450 | plusZeroLeftNeutral _ = Refl
 451 | 
 452 | export
 453 | plusZeroRightNeutral : (left : Nat) -> left + 0 = left
 454 | plusZeroRightNeutral Z     = Refl
 455 | plusZeroRightNeutral (S n) = Calc $
 456 |   |~ 1 + (n + 0)
 457 |   ~~ 1 + n ...(cong (1+) $ plusZeroRightNeutral n)
 458 | 
 459 | export
 460 | plusSuccRightSucc : (left, right : Nat) -> S (left + right) = left + (S right)
 461 | plusSuccRightSucc Z _ = Refl
 462 | plusSuccRightSucc (S left) right = Calc $
 463 |   |~ 1 + (1 + (left + right))
 464 |   ~~ 1 + (left + (1 + right)) ...(cong (1+) $ plusSuccRightSucc left right)
 465 | 
 466 | export
 467 | plusCommutative : (left, right : Nat) -> left + right = right + left
 468 | plusCommutative Z right = Calc $
 469 |   |~ right
 470 |   ~~ right + 0 ..<(plusZeroRightNeutral right)
 471 | plusCommutative (S left) right = Calc $
 472 |   |~ 1 + (left + right)
 473 |   ~~ 1 + (right + left) ...(cong (1+) $ plusCommutative left right)
 474 |   ~~ right + (1 + left) ...(plusSuccRightSucc right left)
 475 | 
 476 | export
 477 | plusAssociative : (left, centre, right : Nat) ->
 478 |   left + (centre + right) = (left + centre) + right
 479 | plusAssociative Z _ _ = Refl
 480 | plusAssociative (S left) centre right = Calc $
 481 |   |~ 1 + (left + (centre + right))
 482 |   ~~ 1 + ((left + centre) + right) ...(cong (1+) $ plusAssociative left centre right)
 483 | 
 484 | export
 485 | plusConstantRight : (left, right, c : Nat) -> left = right ->
 486 |   left + c = right + c
 487 | plusConstantRight _ _ _ Refl = Refl
 488 | 
 489 | export
 490 | plusConstantLeft : (left, right, c : Nat) -> left = right ->
 491 |   c + left = c + right
 492 | plusConstantLeft _ _ _ Refl = Refl
 493 | 
 494 | export
 495 | plusOneSucc : (right : Nat) -> 1 + right = S right
 496 | plusOneSucc _ = Refl
 497 | 
 498 | export
 499 | plusLeftCancel : (left, right, right' : Nat) ->
 500 |   left + right = left + right' -> right = right'
 501 | plusLeftCancel Z _ _ p = p
 502 | plusLeftCancel (S left) right right' p =
 503 |     plusLeftCancel left right right' $ injective p
 504 | 
 505 | export
 506 | plusRightCancel : (left, left', right : Nat) ->
 507 |   left + right = left' + right -> left = left'
 508 | plusRightCancel left left' right p =
 509 |   plusLeftCancel right left left' $ Calc $
 510 |   |~ right + left
 511 |   ~~ left  + right ...(plusCommutative right left)
 512 |   ~~ left' + right ...(p)
 513 |   ~~ right + left' ...(plusCommutative left' right)
 514 | 
 515 | export
 516 | plusLeftLeftRightZero : (left, right : Nat) ->
 517 |   left + right = left -> right = Z
 518 | plusLeftLeftRightZero left right p =
 519 |   plusLeftCancel left right Z $ Calc $
 520 |   |~ left + right
 521 |   ~~ left     ...(p)
 522 |   ~~ left + 0 ..<(plusZeroRightNeutral left)
 523 | 
 524 | export
 525 | plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q+p) `LTE` (r+p)
 526 | plusLteMonotoneRight p  Z     r     LTEZero    = CalcSmart {leq = LTE} $
 527 |   |~ 0 + p
 528 |   <~ p + r ...(lteAddRight p)
 529 |   <~ r + p .=.(plusCommutative p r)
 530 | plusLteMonotoneRight p (S q) (S r) (LTESucc q_lte_r) =
 531 |   LTESucc $ CalcSmart {leq = LTE} $
 532 |   |~ q + p
 533 |   <~ r + p ...(plusLteMonotoneRight p q r q_lte_r)
 534 | 
 535 | export
 536 | plusLteMonotoneLeft : (p, q, r : Nat) -> q `LTE` r -> (p + q) `LTE` (p + r)
 537 | plusLteMonotoneLeft p q r q_lt_r = CalcSmart {leq = LTE} $
 538 |   |~ p + q
 539 |   <~ q + p .=.(plusCommutative p q)
 540 |   <~ r + p ...(plusLteMonotoneRight p q r q_lt_r)
 541 |   <~ p + r .=.(plusCommutative r p)
 542 | 
 543 | 
 544 | export
 545 | plusLteMonotone : {m, n, p, q : Nat} -> m `LTE` n -> p `LTE` q ->
 546 |                   (m + p) `LTE` (n + q)
 547 | plusLteMonotone left right = CalcSmart {leq = LTE} $
 548 |   |~ m + p
 549 |   <~ m + q ...(plusLteMonotoneLeft m p q right)
 550 |   <~ n + q ...(plusLteMonotoneRight q m n left)
 551 | 
 552 | zeroPlusLeftZero : (a,b : Nat) -> (0 = a + b) -> a = 0
 553 | zeroPlusLeftZero 0 0 Refl = Refl
 554 | zeroPlusLeftZero (S k) b _ impossible
 555 | 
 556 | zeroPlusRightZero : (a,b : Nat) -> (0 = a + b) -> b = 0
 557 | zeroPlusRightZero 0 0 Refl = Refl
 558 | zeroPlusRightZero (S k) b _ impossible
 559 | 
 560 | -- Proofs on *
 561 | 
 562 | export
 563 | multZeroLeftZero : (right : Nat) -> Z * right = Z
 564 | multZeroLeftZero _ = Refl
 565 | 
 566 | export
 567 | multZeroRightZero : (left : Nat) -> left * Z = Z
 568 | multZeroRightZero Z        = Refl
 569 | multZeroRightZero (S left) = multZeroRightZero left
 570 | 
 571 | export
 572 | multRightSuccPlus : (left, right : Nat) ->
 573 |   left * (S right) = left + (left * right)
 574 | multRightSuccPlus Z _ = Refl
 575 | multRightSuccPlus (S left) right = cong (1+) $ Calc $
 576 |   |~ right + (left * (1 + right))
 577 |   ~~ right + (left + (left * right))
 578 |          ...(cong (right +) $ multRightSuccPlus left right)
 579 |   ~~ (right + left) + (left * right)
 580 |          ...(plusAssociative right left (left*right))
 581 |   ~~ (left + right) + (left * right)
 582 |          ...(cong (+ (left * right)) $ plusCommutative right left)
 583 |   ~~ left + (right + (left * right))
 584 |          ..<(plusAssociative left right (left * right))
 585 |   ~~ left + ((1 + left) * right)
 586 |          ...(Refl)
 587 | 
 588 | export
 589 | multLeftSuccPlus : (left, right : Nat) ->
 590 |   (S left) * right = right + (left * right)
 591 | multLeftSuccPlus _ _ = Refl
 592 | 
 593 | export
 594 | multCommutative : (left, right : Nat) -> left * right = right * left
 595 | multCommutative Z right = Calc $
 596 |   |~ 0
 597 |   ~~ right * 0 ..<(multZeroRightZero right)
 598 | multCommutative (S left) right = Calc $
 599 |   |~ right + (left * right)
 600 |   ~~ right + (right * left)
 601 |        ...(cong (right +) $ multCommutative left right)
 602 |   ~~ right * (1 + left)
 603 |        ..<(multRightSuccPlus right left)
 604 | 
 605 | export
 606 | multDistributesOverPlusLeft : (left, centre, right : Nat) ->
 607 |   (left + centre) * right = (left * right) + (centre * right)
 608 | multDistributesOverPlusLeft Z _ _ = Refl
 609 | multDistributesOverPlusLeft (S left) centre right = Calc $
 610 |   |~ right + ((left + centre) * right)
 611 |   ~~ right + ((left * right) + (centre * right))
 612 |         ...(cong (right +) $
 613 |             multDistributesOverPlusLeft left centre right)
 614 |   ~~ (right + (left * right)) + (centre * right)
 615 |         ...(plusAssociative right (left*right) (centre*right))
 616 | export
 617 | multDistributesOverPlusRight : (left, centre, right : Nat) ->
 618 |   left * (centre + right) = (left * centre) + (left * right)
 619 | multDistributesOverPlusRight left centre right = Calc $
 620 |   |~ left * (centre + right)
 621 |   ~~ (centre + right) * left ...(multCommutative left (centre + right))
 622 |   ~~ (centre * left) + (right * left)
 623 |                              ...(multDistributesOverPlusLeft centre right left)
 624 |   ~~ (left * centre) + (left * right)
 625 |                              ...(cong2 (+)
 626 |                                  (multCommutative centre left)
 627 |                                  (multCommutative right left))
 628 | 
 629 | export
 630 | multAssociative : (left, centre, right : Nat) ->
 631 |   left * (centre * right) = (left * centre) * right
 632 | multAssociative Z _ _ = Refl
 633 | multAssociative (S left) centre right = Calc $
 634 |   |~ (centre * right) + (left * (centre * right))
 635 |   ~~ (centre * right) + ((left * centre) * right)
 636 |         ...(cong ((centre * right) +) $
 637 |             multAssociative left centre right)
 638 |   ~~ ((1 + left) * centre) * right ..<(multDistributesOverPlusLeft centre (left * centre) right)
 639 | 
 640 | export
 641 | multOneLeftNeutral : (right : Nat) -> 1 * right = right
 642 | multOneLeftNeutral right = plusZeroRightNeutral right
 643 | 
 644 | export
 645 | multOneRightNeutral : (left : Nat) -> left * 1 = left
 646 | multOneRightNeutral left = Calc $
 647 |   |~ left * 1
 648 |   ~~ 1 * left ...(multCommutative left 1)
 649 |   ~~ left     ...(multOneLeftNeutral left)
 650 | 
 651 | -- Proofs on minus
 652 | 
 653 | export
 654 | minusSuccSucc : (left, right : Nat) ->
 655 |   minus (S left) (S right) = minus left right
 656 | minusSuccSucc _ _ = Refl
 657 | 
 658 | export
 659 | minusZeroLeft : (right : Nat) -> minus 0 right = Z
 660 | minusZeroLeft _ = Refl
 661 | 
 662 | export
 663 | minusZeroRight : (left : Nat) -> minus left 0 = left
 664 | minusZeroRight Z     = Refl
 665 | minusZeroRight (S _) = Refl
 666 | 
 667 | export
 668 | minusZeroN : (n : Nat) -> Z = minus n n
 669 | minusZeroN Z     = Refl
 670 | minusZeroN (S n) = minusZeroN n
 671 | 
 672 | export
 673 | minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
 674 | minusOneSuccN Z     = Refl
 675 | minusOneSuccN (S n) = minusOneSuccN n
 676 | 
 677 | export
 678 | minusSuccOne : (n : Nat) -> minus (S n) 1 = n
 679 | minusSuccOne Z     = Refl
 680 | minusSuccOne (S _) = Refl
 681 | 
 682 | export
 683 | minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
 684 | minusPlusZero Z     _ = Refl
 685 | minusPlusZero (S n) m = minusPlusZero n m
 686 | 
 687 | export
 688 | minusPos : m `LT` n -> Z `LT` minus n m
 689 | minusPos lt = case view lt of
 690 |   LTZero    => ltZero
 691 |   LTSucc lt => minusPos lt
 692 | 
 693 | export
 694 | minusLteMonotone : {p : Nat} -> m `LTE` n -> minus m p `LTE` minus n p
 695 | minusLteMonotone LTEZero = LTEZero
 696 | minusLteMonotone {p = Z} prf@(LTESucc _) = prf
 697 | minusLteMonotone {p = S p} (LTESucc lte) = minusLteMonotone lte
 698 | 
 699 | export
 700 | minusLtMonotone : m `LT` n -> p `LT` n -> minus m p `LT` minus n p
 701 | minusLtMonotone {m} {p} mltn pltn = case view pltn of
 702 |     LTZero => ltRecall {p = (`minus` 0)} mltn $ CalcSmart {leq = LT} $
 703 |       |~ minus m Z
 704 |       ~~ m ...(minusZeroRight m)
 705 |       <~ minus n Z ...(mltn)
 706 |     LTSucc pltn => case view mltn of
 707 |       LTZero => minusPos pltn
 708 |       LTSucc mltn => minusLtMonotone mltn pltn
 709 | 
 710 | public export
 711 | minusPlus : (m : Nat) -> minus (plus m n) m === n
 712 | minusPlus Z = irrelevantEq (minusZeroRight n)
 713 | minusPlus (S m) = minusPlus m
 714 | 
 715 | export
 716 | plusMinusLte : (n, m : Nat) -> LTE n m -> (m `minus` n) + n = m
 717 | plusMinusLte  Z     m    _   = Calc $
 718 |   |~ (m `minus` 0) + 0
 719 |   ~~ m + 0 ...(cong (+0) $ minusZeroRight m)
 720 |   ~~ m     ...(plusZeroRightNeutral m)
 721 | plusMinusLte (S _)  Z    lte = absurd lte
 722 | plusMinusLte (S n) (S m) lte = Calc $
 723 |   |~ ((1+m) `minus` (1+n)) + (1+n)
 724 |   ~~ (m `minus` n) + (1 + n) ...(Refl)
 725 |   ~~ 1+((m `minus` n) + n)   ..<(plusSuccRightSucc (m `minus` n) n)
 726 |   ~~ 1+m                     ...(cong (1+) $ plusMinusLte n m
 727 |                                            $ fromLteSucc lte)
 728 | 
 729 | export
 730 | minusMinusMinusPlus : (left, centre, right : Nat) ->
 731 |   minus (minus left centre) right = minus left (centre + right)
 732 | minusMinusMinusPlus Z Z _ = Refl
 733 | minusMinusMinusPlus (S _) Z _ = Refl
 734 | minusMinusMinusPlus Z (S _) _ = Refl
 735 | minusMinusMinusPlus (S left) (S centre) right = Calc $
 736 |   |~ (((1+left) `minus` (1+centre)) `minus` right)
 737 |   ~~ ((left `minus` centre) `minus` right) ...(Refl)
 738 |   ~~ (left `minus` (centre + right))       ...(minusMinusMinusPlus left centre right)
 739 | 
 740 | export
 741 | plusMinusLeftCancel : (left, right : Nat) -> (right' : Nat) ->
 742 |   minus (left + right) (left + right') = minus right right'
 743 | plusMinusLeftCancel Z _ _ = Refl
 744 | plusMinusLeftCancel (S left) right right' = Calc $
 745 |   |~ ((left + right) `minus` (left + right'))
 746 |   ~~ (right `minus` right') ...(plusMinusLeftCancel left right right')
 747 | 
 748 | export
 749 | multDistributesOverMinusLeft : (left, centre, right : Nat) ->
 750 |   (minus left centre) * right = minus (left * right) (centre * right)
 751 | multDistributesOverMinusLeft Z Z _ = Refl
 752 | multDistributesOverMinusLeft (S left) Z right = Calc $
 753 |   |~ right + (left * right)
 754 |   ~~ ((right + (left * right)) `minus` 0)
 755 |          ..<(minusZeroRight (right + (left*right)))
 756 |   ~~ (((1+left) * right) `minus` (0 * right))
 757 |          ...(Refl)
 758 | multDistributesOverMinusLeft Z (S _) _ = Refl
 759 | multDistributesOverMinusLeft (S left) (S centre) right = Calc $
 760 |   |~ ((1 + left) `minus` (1 + centre)) * right
 761 |   ~~ (left `minus` centre) * right
 762 |        ...(Refl)
 763 |   ~~ ((left*right) `minus` (centre*right))
 764 |        ...(multDistributesOverMinusLeft left centre right)
 765 |   ~~ ((right + (left * right)) `minus` (right + (centre * right)))
 766 |       ..<(plusMinusLeftCancel right (left*right) (centre*right))
 767 |   ~~ (((1+ left) * right) `minus` ((1+centre) * right))
 768 |       ...(Refl)
 769 | export
 770 | multDistributesOverMinusRight : (left, centre, right : Nat) ->
 771 |   left * (minus centre right) = minus (left * centre) (left * right)
 772 | multDistributesOverMinusRight left centre right = Calc $
 773 |   |~ left * (centre `minus` right)
 774 |   ~~ (centre `minus` right) * left
 775 |          ...(multCommutative left (centre `minus` right))
 776 |   ~~ ((centre*left) `minus` (right*left))
 777 |          ...(multDistributesOverMinusLeft centre right left)
 778 |   ~~ ((left * centre) `minus` (left * right))
 779 |          ...(cong2 minus
 780 |              (multCommutative centre left)
 781 |              (multCommutative right left))
 782 | export
 783 | zeroMultEitherZero : (a,b : Nat) -> a*b = 0 -> Either (a = 0) (b = 0)
 784 | zeroMultEitherZero 0 b prf = Left Refl
 785 | zeroMultEitherZero (S a) b prf = Right $ zeroPlusLeftZero b (a * b) (sym prf)
 786 | 
 787 | -- power proofs
 788 | 
 789 | -- multPowerPowerPlus : (base, exp, exp' : Nat) ->
 790 | --   power base (exp + exp') = (power base exp) * (power base exp')
 791 | -- multPowerPowerPlus base Z       exp' =
 792 | --     rewrite sym $ plusZeroRightNeutral (power base exp') in Refl
 793 | -- multPowerPowerPlus base (S exp) exp' =
 794 | --   rewrite multPowerPowerPlus base exp exp' in
 795 | --     rewrite sym $ multAssociative base (power base exp) (power base exp') in
 796 | --       Refl
 797 | 
 798 | --powerOneNeutral : (base : Nat) -> power base 1 = base
 799 | --powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
 800 | --
 801 | --powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
 802 | --powerOneSuccOne Z       = Refl
 803 | --powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
 804 | --
 805 | --powerPowerMultPower : (base, exp, exp' : Nat) ->
 806 | --  power (power base exp) exp' = power base (exp * exp')
 807 | --powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
 808 | --powerPowerMultPower base exp (S exp') =
 809 | --  rewrite powerPowerMultPower base exp exp' in
 810 | --  rewrite multRightSuccPlus exp exp' in
 811 | --  rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
 812 | --          Refl
 813 | 
 814 | -- minimum / maximum proofs
 815 | 
 816 | export
 817 | maximumAssociative : (l, c, r : Nat) ->
 818 |   maximum l (maximum c r) = maximum (maximum l c) r
 819 | maximumAssociative Z _ _ = Refl
 820 | maximumAssociative (S _) Z _ = Refl
 821 | maximumAssociative (S _) (S _) Z = Refl
 822 | maximumAssociative (S k) (S j) (S i) = cong S $ Calc $
 823 |   |~ maximum k (maximum j i)
 824 |   ~~ maximum (maximum k j) i ...(maximumAssociative k j i)
 825 | 
 826 | export
 827 | maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l
 828 | maximumCommutative Z Z = Refl
 829 | maximumCommutative Z (S _) = Refl
 830 | maximumCommutative (S _) Z = Refl
 831 | maximumCommutative (S k) (S j) = cong S $ maximumCommutative k j
 832 | 
 833 | export
 834 | maximumIdempotent : (n : Nat) -> maximum n n = n
 835 | maximumIdempotent Z = Refl
 836 | maximumIdempotent (S k) = cong S $ maximumIdempotent k
 837 | 
 838 | export
 839 | maximumLeftUpperBound : (m, n : Nat) -> m `LTE` maximum m n
 840 | maximumLeftUpperBound 0 n = LTEZero
 841 | maximumLeftUpperBound (S m) 0 = reflexive
 842 | maximumLeftUpperBound (S m) (S n) = LTESucc (maximumLeftUpperBound m n)
 843 | 
 844 | export
 845 | maximumRightUpperBound : (m, n : Nat) -> n `LTE` maximum m n
 846 | maximumRightUpperBound 0 n = reflexive
 847 | maximumRightUpperBound (S m) 0 = LTEZero
 848 | maximumRightUpperBound (S m) (S n) = LTESucc (maximumRightUpperBound m n)
 849 | 
 850 | export
 851 | minimumAssociative : (l, c, r : Nat) ->
 852 |   minimum l (minimum c r) = minimum (minimum l c) r
 853 | minimumAssociative Z _ _ = Refl
 854 | minimumAssociative (S _) Z _ = Refl
 855 | minimumAssociative (S _) (S _) Z = Refl
 856 | minimumAssociative (S k) (S j) (S i) = cong S $ minimumAssociative k j i
 857 | 
 858 | export
 859 | minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l
 860 | minimumCommutative Z Z = Refl
 861 | minimumCommutative Z (S _) = Refl
 862 | minimumCommutative (S _) Z = Refl
 863 | minimumCommutative (S k) (S j) = cong S $ minimumCommutative k j
 864 | 
 865 | export
 866 | minimumIdempotent : (n : Nat) -> minimum n n = n
 867 | minimumIdempotent Z = Refl
 868 | minimumIdempotent (S k) = cong S $ minimumIdempotent k
 869 | 
 870 | export
 871 | minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
 872 | minimumZeroZeroLeft left = Calc $
 873 |   |~ minimum left 0
 874 |   ~~ minimum 0 left ...(minimumCommutative left 0)
 875 |   ~~ 0              ...(Refl)
 876 | 
 877 | export
 878 | minimumSuccSucc : (left, right : Nat) ->
 879 |   minimum (S left) (S right) = S (minimum left right)
 880 | minimumSuccSucc _ _ = Refl
 881 | 
 882 | export
 883 | maximumZeroNLeft : (left : Nat) -> maximum left Z = left
 884 | maximumZeroNLeft left = Calc $
 885 |   |~ maximum left 0
 886 |   ~~ maximum 0 left ...(maximumCommutative left Z)
 887 |   ~~ left           ...(Refl)
 888 | 
 889 | export
 890 | maximumSuccSucc : (left, right : Nat) ->
 891 |   S (maximum left right) = maximum (S left) (S right)
 892 | maximumSuccSucc _ _ = Refl
 893 | 
 894 | export
 895 | sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
 896 | sucMaxL Z = Refl
 897 | sucMaxL (S l) = cong S $ sucMaxL l
 898 | 
 899 | export
 900 | sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
 901 | sucMaxR Z = Refl
 902 | sucMaxR (S l) = cong S $ sucMaxR l
 903 | 
 904 | export
 905 | sucMinL : (l : Nat) -> minimum (S l) l = l
 906 | sucMinL Z = Refl
 907 | sucMinL (S l) = cong S $ sucMinL l
 908 | 
 909 | export
 910 | sucMinR : (l : Nat) -> minimum l (S l) = l
 911 | sucMinR Z = Refl
 912 | sucMinR (S l) = cong S $ sucMinR l
 913 | 
 914 | -- Algebra -----------------------------
 915 | 
 916 | namespace Monoid
 917 | 
 918 |   public export
 919 |   [Maximum] Monoid Nat using Semigroup.Maximum where
 920 |     neutral = 0
 921 |