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 0      0    _   = LTEZero
 291 | lteReflectsLTE 0     (S k) _   = LTEZero
 292 | lteReflectsLTE (S k) (S j) prf = LTESucc (lteReflectsLTE k j prf)
 293 | 
 294 | export
 295 | gteReflectsGTE : (k : Nat) -> (n : Nat) -> gte k n === True -> k `GTE` n
 296 | gteReflectsGTE k n prf = lteReflectsLTE n k prf
 297 | 
 298 | export
 299 | ltReflectsLT : (k : Nat) -> (n : Nat) -> lt k n === True -> k `LT` n
 300 | ltReflectsLT k n prf = lteReflectsLTE (S k) n prf
 301 | 
 302 | public export
 303 | ltOpReflectsLT : (m,n : Nat) -> So (m < n) -> LT m n
 304 | ltOpReflectsLT 0     (S k) prf = LTESucc LTEZero
 305 | ltOpReflectsLT (S k) (S j) prf = LTESucc (ltOpReflectsLT k j prf)
 306 | 
 307 | export
 308 | gtReflectsGT : (k : Nat) -> (n : Nat) -> gt k n === True -> k `GT` n
 309 | gtReflectsGT k n prf = ltReflectsLT n k prf
 310 | 
 311 | public export
 312 | minimum : Nat -> Nat -> Nat
 313 | minimum Z m = Z
 314 | minimum (S n) Z = Z
 315 | minimum (S n) (S m) = S (minimum n m)
 316 | 
 317 | public export
 318 | maximum : Nat -> Nat -> Nat
 319 | maximum Z m = m
 320 | maximum (S n) Z = S n
 321 | maximum (S n) (S m) = S (maximum n m)
 322 | 
 323 | -- Proofs on S
 324 | 
 325 | export
 326 | eqSucc : (0 left, right : Nat) -> left = right -> S left = S right
 327 | eqSucc _ _ Refl = Refl
 328 | 
 329 | export
 330 | Injective S where
 331 |   injective Refl = Refl
 332 | 
 333 | export
 334 | SIsNotZ : Not (S x = Z)
 335 | SIsNotZ = absurd
 336 | 
 337 | ||| Auxiliary function:
 338 | ||| mod' fuel a b = a `mod` (S b)
 339 | ||| assuming we have enough fuel
 340 | public export
 341 | mod' : Nat -> Nat -> Nat -> Nat
 342 | mod' Z        centre right = centre
 343 | mod' (S fuel) centre right =
 344 |       if lte centre right then
 345 |         centre
 346 |       else
 347 |         mod' fuel (minus centre (S right)) right
 348 | 
 349 | public export
 350 | modNatNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
 351 | modNatNZ left Z         p = void (absurd p)
 352 | modNatNZ left (S right) _ = mod' left left right
 353 | 
 354 | export partial
 355 | modNat : Nat -> Nat -> Nat
 356 | modNat left (S right) = modNatNZ left (S right) ItIsSucc
 357 | 
 358 | ||| Auxiliary function:
 359 | ||| div' fuel a b = a `div` (S b)
 360 | ||| assuming we have enough fuel
 361 | public export
 362 | div' : Nat -> Nat -> Nat -> Nat
 363 | div' Z        centre right = Z
 364 | div' (S fuel) centre right =
 365 |   if lte centre right then
 366 |     Z
 367 |   else
 368 |     S (div' fuel (minus centre (S right)) right)
 369 | 
 370 | -- 'public' to allow type-level division
 371 | public export
 372 | divNatNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
 373 | divNatNZ left (S right) _ = div' left left right
 374 | 
 375 | export partial
 376 | divNat : Nat -> Nat -> Nat
 377 | divNat left (S right) = divNatNZ left (S right) ItIsSucc
 378 | 
 379 | export
 380 | covering
 381 | divCeilNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> Nat
 382 | divCeilNZ x y p = case (modNatNZ x y p) of
 383 |   Z   => divNatNZ x y p
 384 |   S _ => S (divNatNZ x y p)
 385 | 
 386 | export partial
 387 | divCeil : Nat -> Nat -> Nat
 388 | divCeil x (S y) = divCeilNZ x (S y) ItIsSucc
 389 | 
 390 | 
 391 | public export
 392 | divmod' : Nat -> Nat -> Nat -> (Nat, Nat)
 393 | divmod' Z        centre right = (Z, centre)
 394 | divmod' (S fuel) centre right =
 395 |   if lte centre right then
 396 |     (Z, centre)
 397 |   else
 398 |     let qr = divmod' fuel (minus centre (S right)) right
 399 |     in (S (fst qr), snd qr)
 400 | 
 401 | public export
 402 | divmodNatNZ : Nat -> (y: Nat) -> (0 _ : NonZero y) -> (Nat, Nat)
 403 | divmodNatNZ left (S right) _ = divmod' left left right
 404 | 
 405 | 
 406 | public export
 407 | Integral Nat where
 408 |   div = divNat
 409 |   mod = modNat
 410 | 
 411 | export
 412 | covering
 413 | gcd : (a: Nat) -> (b: Nat) -> {auto 0 ok: NotBothZero a b} -> Nat
 414 | gcd a Z     = a
 415 | gcd Z b     = b
 416 | gcd a (S b) = gcd (S b) (modNatNZ a (S b) ItIsSucc)
 417 | 
 418 | export partial
 419 | lcm : Nat -> Nat -> Nat
 420 | lcm _ Z     = Z
 421 | lcm Z _     = Z
 422 | lcm a (S b) = divNat (a * (S b)) (gcd a (S b))
 423 | 
 424 | --------------------------------------------------------------------------------
 425 | -- An informative comparison view
 426 | --------------------------------------------------------------------------------
 427 | public export
 428 | data CmpNat : Nat -> Nat -> Type where
 429 |      CmpLT : (y : _) -> CmpNat x (x + S y)
 430 |      CmpEQ : CmpNat x x
 431 |      CmpGT : (x : _) -> CmpNat (y + S x) y
 432 | 
 433 | export
 434 | cmp : (x, y : Nat) -> CmpNat x y
 435 | cmp Z Z     = CmpEQ
 436 | cmp Z (S k) = CmpLT _
 437 | cmp (S k) Z = CmpGT _
 438 | cmp (S x) (S y) with (cmp x y)
 439 |   cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k
 440 |   cmp (S x) (S x)           | CmpEQ   = CmpEQ
 441 |   cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k
 442 | 
 443 | -- Proofs on +
 444 | 
 445 | export
 446 | plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
 447 | plusZeroLeftNeutral _ = Refl
 448 | 
 449 | export
 450 | plusZeroRightNeutral : (left : Nat) -> left + 0 = left
 451 | plusZeroRightNeutral Z     = Refl
 452 | plusZeroRightNeutral (S n) = Calc $
 453 |   |~ 1 + (n + 0)
 454 |   ~~ 1 + n ...(cong (1+) $ plusZeroRightNeutral n)
 455 | 
 456 | export
 457 | plusSuccRightSucc : (left, right : Nat) -> S (left + right) = left + (S right)
 458 | plusSuccRightSucc Z _ = Refl
 459 | plusSuccRightSucc (S left) right = Calc $
 460 |   |~ 1 + (1 + (left + right))
 461 |   ~~ 1 + (left + (1 + right)) ...(cong (1+) $ plusSuccRightSucc left right)
 462 | 
 463 | export
 464 | plusCommutative : (left, right : Nat) -> left + right = right + left
 465 | plusCommutative Z right = Calc $
 466 |   |~ right
 467 |   ~~ right + 0 ..<(plusZeroRightNeutral right)
 468 | plusCommutative (S left) right = Calc $
 469 |   |~ 1 + (left + right)
 470 |   ~~ 1 + (right + left) ...(cong (1+) $ plusCommutative left right)
 471 |   ~~ right + (1 + left) ...(plusSuccRightSucc right left)
 472 | 
 473 | export
 474 | plusAssociative : (left, centre, right : Nat) ->
 475 |   left + (centre + right) = (left + centre) + right
 476 | plusAssociative Z _ _ = Refl
 477 | plusAssociative (S left) centre right = Calc $
 478 |   |~ 1 + (left + (centre + right))
 479 |   ~~ 1 + ((left + centre) + right) ...(cong (1+) $ plusAssociative left centre right)
 480 | 
 481 | export
 482 | plusConstantRight : (left, right, c : Nat) -> left = right ->
 483 |   left + c = right + c
 484 | plusConstantRight _ _ _ Refl = Refl
 485 | 
 486 | export
 487 | plusConstantLeft : (left, right, c : Nat) -> left = right ->
 488 |   c + left = c + right
 489 | plusConstantLeft _ _ _ Refl = Refl
 490 | 
 491 | export
 492 | plusOneSucc : (right : Nat) -> 1 + right = S right
 493 | plusOneSucc _ = Refl
 494 | 
 495 | export
 496 | plusLeftCancel : (left, right, right' : Nat) ->
 497 |   left + right = left + right' -> right = right'
 498 | plusLeftCancel Z _ _ p = p
 499 | plusLeftCancel (S left) right right' p =
 500 |     plusLeftCancel left right right' $ injective p
 501 | 
 502 | export
 503 | plusRightCancel : (left, left', right : Nat) ->
 504 |   left + right = left' + right -> left = left'
 505 | plusRightCancel left left' right p =
 506 |   plusLeftCancel right left left' $ Calc $
 507 |   |~ right + left
 508 |   ~~ left  + right ...(plusCommutative right left)
 509 |   ~~ left' + right ...(p)
 510 |   ~~ right + left' ...(plusCommutative left' right)
 511 | 
 512 | export
 513 | plusLeftLeftRightZero : (left, right : Nat) ->
 514 |   left + right = left -> right = Z
 515 | plusLeftLeftRightZero left right p =
 516 |   plusLeftCancel left right Z $ Calc $
 517 |   |~ left + right
 518 |   ~~ left     ...(p)
 519 |   ~~ left + 0 ..<(plusZeroRightNeutral left)
 520 | 
 521 | export
 522 | plusLteMonotoneRight : (p, q, r : Nat) -> q `LTE` r -> (q+p) `LTE` (r+p)
 523 | plusLteMonotoneRight p  Z     r     LTEZero    = CalcSmart {leq = LTE} $
 524 |   |~ 0 + p
 525 |   <~ p + r ...(lteAddRight p)
 526 |   <~ r + p .=.(plusCommutative p r)
 527 | plusLteMonotoneRight p (S q) (S r) (LTESucc q_lte_r) =
 528 |   LTESucc $ CalcSmart {leq = LTE} $
 529 |   |~ q + p
 530 |   <~ r + p ...(plusLteMonotoneRight p q r q_lte_r)
 531 | 
 532 | export
 533 | plusLteMonotoneLeft : (p, q, r : Nat) -> q `LTE` r -> (p + q) `LTE` (p + r)
 534 | plusLteMonotoneLeft p q r q_lt_r = CalcSmart {leq = LTE} $
 535 |   |~ p + q
 536 |   <~ q + p .=.(plusCommutative p q)
 537 |   <~ r + p ...(plusLteMonotoneRight p q r q_lt_r)
 538 |   <~ p + r .=.(plusCommutative r p)
 539 | 
 540 | 
 541 | export
 542 | plusLteMonotone : {m, n, p, q : Nat} -> m `LTE` n -> p `LTE` q ->
 543 |                   (m + p) `LTE` (n + q)
 544 | plusLteMonotone left right = CalcSmart {leq = LTE} $
 545 |   |~ m + p
 546 |   <~ m + q ...(plusLteMonotoneLeft m p q right)
 547 |   <~ n + q ...(plusLteMonotoneRight q m n left)
 548 | 
 549 | zeroPlusLeftZero : (a,b : Nat) -> (0 = a + b) -> a = 0
 550 | zeroPlusLeftZero 0 0 Refl = Refl
 551 | zeroPlusLeftZero (S k) b _ impossible
 552 | 
 553 | zeroPlusRightZero : (a,b : Nat) -> (0 = a + b) -> b = 0
 554 | zeroPlusRightZero 0 0 Refl = Refl
 555 | zeroPlusRightZero (S k) b _ impossible
 556 | 
 557 | -- Proofs on *
 558 | 
 559 | export
 560 | multZeroLeftZero : (right : Nat) -> Z * right = Z
 561 | multZeroLeftZero _ = Refl
 562 | 
 563 | export
 564 | multZeroRightZero : (left : Nat) -> left * Z = Z
 565 | multZeroRightZero Z        = Refl
 566 | multZeroRightZero (S left) = multZeroRightZero left
 567 | 
 568 | export
 569 | multRightSuccPlus : (left, right : Nat) ->
 570 |   left * (S right) = left + (left * right)
 571 | multRightSuccPlus Z _ = Refl
 572 | multRightSuccPlus (S left) right = cong (1+) $ Calc $
 573 |   |~ right + (left * (1 + right))
 574 |   ~~ right + (left + (left * right))
 575 |          ...(cong (right +) $ multRightSuccPlus left right)
 576 |   ~~ (right + left) + (left * right)
 577 |          ...(plusAssociative right left (left*right))
 578 |   ~~ (left + right) + (left * right)
 579 |          ...(cong (+ (left * right)) $ plusCommutative right left)
 580 |   ~~ left + (right + (left * right))
 581 |          ..<(plusAssociative left right (left * right))
 582 |   ~~ left + ((1 + left) * right)
 583 |          ...(Refl)
 584 | 
 585 | export
 586 | multLeftSuccPlus : (left, right : Nat) ->
 587 |   (S left) * right = right + (left * right)
 588 | multLeftSuccPlus _ _ = Refl
 589 | 
 590 | export
 591 | multCommutative : (left, right : Nat) -> left * right = right * left
 592 | multCommutative Z right = Calc $
 593 |   |~ 0
 594 |   ~~ right * 0 ..<(multZeroRightZero right)
 595 | multCommutative (S left) right = Calc $
 596 |   |~ right + (left * right)
 597 |   ~~ right + (right * left)
 598 |        ...(cong (right +) $ multCommutative left right)
 599 |   ~~ right * (1 + left)
 600 |        ..<(multRightSuccPlus right left)
 601 | 
 602 | export
 603 | multDistributesOverPlusLeft : (left, centre, right : Nat) ->
 604 |   (left + centre) * right = (left * right) + (centre * right)
 605 | multDistributesOverPlusLeft Z _ _ = Refl
 606 | multDistributesOverPlusLeft (S left) centre right = Calc $
 607 |   |~ right + ((left + centre) * right)
 608 |   ~~ right + ((left * right) + (centre * right))
 609 |         ...(cong (right +) $
 610 |             multDistributesOverPlusLeft left centre right)
 611 |   ~~ (right + (left * right)) + (centre * right)
 612 |         ...(plusAssociative right (left*right) (centre*right))
 613 | export
 614 | multDistributesOverPlusRight : (left, centre, right : Nat) ->
 615 |   left * (centre + right) = (left * centre) + (left * right)
 616 | multDistributesOverPlusRight left centre right = Calc $
 617 |   |~ left * (centre + right)
 618 |   ~~ (centre + right) * left ...(multCommutative left (centre + right))
 619 |   ~~ (centre * left) + (right * left)
 620 |                              ...(multDistributesOverPlusLeft centre right left)
 621 |   ~~ (left * centre) + (left * right)
 622 |                              ...(cong2 (+)
 623 |                                  (multCommutative centre left)
 624 |                                  (multCommutative right left))
 625 | 
 626 | export
 627 | multAssociative : (left, centre, right : Nat) ->
 628 |   left * (centre * right) = (left * centre) * right
 629 | multAssociative Z _ _ = Refl
 630 | multAssociative (S left) centre right = Calc $
 631 |   |~ (centre * right) + (left * (centre * right))
 632 |   ~~ (centre * right) + ((left * centre) * right)
 633 |         ...(cong ((centre * right) +) $
 634 |             multAssociative left centre right)
 635 |   ~~ ((1 + left) * centre) * right ..<(multDistributesOverPlusLeft centre (left * centre) right)
 636 | 
 637 | export
 638 | multOneLeftNeutral : (right : Nat) -> 1 * right = right
 639 | multOneLeftNeutral right = plusZeroRightNeutral right
 640 | 
 641 | export
 642 | multOneRightNeutral : (left : Nat) -> left * 1 = left
 643 | multOneRightNeutral left = Calc $
 644 |   |~ left * 1
 645 |   ~~ 1 * left ...(multCommutative left 1)
 646 |   ~~ left     ...(multOneLeftNeutral left)
 647 | 
 648 | -- Proofs on minus
 649 | 
 650 | export
 651 | minusSuccSucc : (left, right : Nat) ->
 652 |   minus (S left) (S right) = minus left right
 653 | minusSuccSucc _ _ = Refl
 654 | 
 655 | export
 656 | minusZeroLeft : (right : Nat) -> minus 0 right = Z
 657 | minusZeroLeft _ = Refl
 658 | 
 659 | export
 660 | minusZeroRight : (left : Nat) -> minus left 0 = left
 661 | minusZeroRight Z     = Refl
 662 | minusZeroRight (S _) = Refl
 663 | 
 664 | export
 665 | minusZeroN : (n : Nat) -> Z = minus n n
 666 | minusZeroN Z     = Refl
 667 | minusZeroN (S n) = minusZeroN n
 668 | 
 669 | export
 670 | minusOneSuccN : (n : Nat) -> S Z = minus (S n) n
 671 | minusOneSuccN Z     = Refl
 672 | minusOneSuccN (S n) = minusOneSuccN n
 673 | 
 674 | export
 675 | minusSuccOne : (n : Nat) -> minus (S n) 1 = n
 676 | minusSuccOne Z     = Refl
 677 | minusSuccOne (S _) = Refl
 678 | 
 679 | export
 680 | minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
 681 | minusPlusZero Z     _ = Refl
 682 | minusPlusZero (S n) m = minusPlusZero n m
 683 | 
 684 | export
 685 | minusPos : m `LT` n -> Z `LT` minus n m
 686 | minusPos lt = case view lt of
 687 |   LTZero    => ltZero
 688 |   LTSucc lt => minusPos lt
 689 | 
 690 | export
 691 | minusLteMonotone : {p : Nat} -> m `LTE` n -> minus m p `LTE` minus n p
 692 | minusLteMonotone LTEZero = LTEZero
 693 | minusLteMonotone {p = Z} prf@(LTESucc _) = prf
 694 | minusLteMonotone {p = S p} (LTESucc lte) = minusLteMonotone lte
 695 | 
 696 | export
 697 | minusLtMonotone : m `LT` n -> p `LT` n -> minus m p `LT` minus n p
 698 | minusLtMonotone {m} {p} mltn pltn = case view pltn of
 699 |     LTZero => ltRecall {p = (`minus` 0)} mltn $ CalcSmart {leq = LT} $
 700 |       |~ minus m Z
 701 |       ~~ m ...(minusZeroRight m)
 702 |       <~ minus n Z ...(mltn)
 703 |     LTSucc pltn => case view mltn of
 704 |       LTZero => minusPos pltn
 705 |       LTSucc mltn => minusLtMonotone mltn pltn
 706 | 
 707 | public export
 708 | minusPlus : (m : Nat) -> minus (plus m n) m === n
 709 | minusPlus Z = irrelevantEq (minusZeroRight n)
 710 | minusPlus (S m) = minusPlus m
 711 | 
 712 | export
 713 | plusMinusLte : (n, m : Nat) -> LTE n m -> (m `minus` n) + n = m
 714 | plusMinusLte  Z     m    _   = Calc $
 715 |   |~ (m `minus` 0) + 0
 716 |   ~~ m + 0 ...(cong (+0) $ minusZeroRight m)
 717 |   ~~ m     ...(plusZeroRightNeutral m)
 718 | plusMinusLte (S _)  Z    lte = absurd lte
 719 | plusMinusLte (S n) (S m) lte = Calc $
 720 |   |~ ((1+m) `minus` (1+n)) + (1+n)
 721 |   ~~ (m `minus` n) + (1 + n) ...(Refl)
 722 |   ~~ 1+((m `minus` n) + n)   ..<(plusSuccRightSucc (m `minus` n) n)
 723 |   ~~ 1+m                     ...(cong (1+) $ plusMinusLte n m
 724 |                                            $ fromLteSucc lte)
 725 | 
 726 | export
 727 | minusMinusMinusPlus : (left, centre, right : Nat) ->
 728 |   minus (minus left centre) right = minus left (centre + right)
 729 | minusMinusMinusPlus Z Z _ = Refl
 730 | minusMinusMinusPlus (S _) Z _ = Refl
 731 | minusMinusMinusPlus Z (S _) _ = Refl
 732 | minusMinusMinusPlus (S left) (S centre) right = Calc $
 733 |   |~ (((1+left) `minus` (1+centre)) `minus` right)
 734 |   ~~ ((left `minus` centre) `minus` right) ...(Refl)
 735 |   ~~ (left `minus` (centre + right))       ...(minusMinusMinusPlus left centre right)
 736 | 
 737 | export
 738 | plusMinusLeftCancel : (left, right : Nat) -> (right' : Nat) ->
 739 |   minus (left + right) (left + right') = minus right right'
 740 | plusMinusLeftCancel Z _ _ = Refl
 741 | plusMinusLeftCancel (S left) right right' = Calc $
 742 |   |~ ((left + right) `minus` (left + right'))
 743 |   ~~ (right `minus` right') ...(plusMinusLeftCancel left right right')
 744 | 
 745 | export
 746 | multDistributesOverMinusLeft : (left, centre, right : Nat) ->
 747 |   (minus left centre) * right = minus (left * right) (centre * right)
 748 | multDistributesOverMinusLeft Z Z _ = Refl
 749 | multDistributesOverMinusLeft (S left) Z right = Calc $
 750 |   |~ right + (left * right)
 751 |   ~~ ((right + (left * right)) `minus` 0)
 752 |          ..<(minusZeroRight (right + (left*right)))
 753 |   ~~ (((1+left) * right) `minus` (0 * right))
 754 |          ...(Refl)
 755 | multDistributesOverMinusLeft Z (S _) _ = Refl
 756 | multDistributesOverMinusLeft (S left) (S centre) right = Calc $
 757 |   |~ ((1 + left) `minus` (1 + centre)) * right
 758 |   ~~ (left `minus` centre) * right
 759 |        ...(Refl)
 760 |   ~~ ((left*right) `minus` (centre*right))
 761 |        ...(multDistributesOverMinusLeft left centre right)
 762 |   ~~ ((right + (left * right)) `minus` (right + (centre * right)))
 763 |       ..<(plusMinusLeftCancel right (left*right) (centre*right))
 764 |   ~~ (((1+ left) * right) `minus` ((1+centre) * right))
 765 |       ...(Refl)
 766 | export
 767 | multDistributesOverMinusRight : (left, centre, right : Nat) ->
 768 |   left * (minus centre right) = minus (left * centre) (left * right)
 769 | multDistributesOverMinusRight left centre right = Calc $
 770 |   |~ left * (centre `minus` right)
 771 |   ~~ (centre `minus` right) * left
 772 |          ...(multCommutative left (centre `minus` right))
 773 |   ~~ ((centre*left) `minus` (right*left))
 774 |          ...(multDistributesOverMinusLeft centre right left)
 775 |   ~~ ((left * centre) `minus` (left * right))
 776 |          ...(cong2 minus
 777 |              (multCommutative centre left)
 778 |              (multCommutative right left))
 779 | export
 780 | zeroMultEitherZero : (a,b : Nat) -> a*b = 0 -> Either (a = 0) (b = 0)
 781 | zeroMultEitherZero 0 b prf = Left Refl
 782 | zeroMultEitherZero (S a) b prf = Right $ zeroPlusLeftZero b (a * b) (sym prf)
 783 | 
 784 | -- power proofs
 785 | 
 786 | -- multPowerPowerPlus : (base, exp, exp' : Nat) ->
 787 | --   power base (exp + exp') = (power base exp) * (power base exp')
 788 | -- multPowerPowerPlus base Z       exp' =
 789 | --     rewrite sym $ plusZeroRightNeutral (power base exp') in Refl
 790 | -- multPowerPowerPlus base (S exp) exp' =
 791 | --   rewrite multPowerPowerPlus base exp exp' in
 792 | --     rewrite sym $ multAssociative base (power base exp) (power base exp') in
 793 | --       Refl
 794 | 
 795 | --powerOneNeutral : (base : Nat) -> power base 1 = base
 796 | --powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
 797 | --
 798 | --powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
 799 | --powerOneSuccOne Z       = Refl
 800 | --powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
 801 | --
 802 | --powerPowerMultPower : (base, exp, exp' : Nat) ->
 803 | --  power (power base exp) exp' = power base (exp * exp')
 804 | --powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
 805 | --powerPowerMultPower base exp (S exp') =
 806 | --  rewrite powerPowerMultPower base exp exp' in
 807 | --  rewrite multRightSuccPlus exp exp' in
 808 | --  rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
 809 | --          Refl
 810 | 
 811 | -- minimum / maximum proofs
 812 | 
 813 | export
 814 | maximumAssociative : (l, c, r : Nat) ->
 815 |   maximum l (maximum c r) = maximum (maximum l c) r
 816 | maximumAssociative Z _ _ = Refl
 817 | maximumAssociative (S _) Z _ = Refl
 818 | maximumAssociative (S _) (S _) Z = Refl
 819 | maximumAssociative (S k) (S j) (S i) = cong S $ Calc $
 820 |   |~ maximum k (maximum j i)
 821 |   ~~ maximum (maximum k j) i ...(maximumAssociative k j i)
 822 | 
 823 | export
 824 | maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l
 825 | maximumCommutative Z Z = Refl
 826 | maximumCommutative Z (S _) = Refl
 827 | maximumCommutative (S _) Z = Refl
 828 | maximumCommutative (S k) (S j) = cong S $ maximumCommutative k j
 829 | 
 830 | export
 831 | maximumIdempotent : (n : Nat) -> maximum n n = n
 832 | maximumIdempotent Z = Refl
 833 | maximumIdempotent (S k) = cong S $ maximumIdempotent k
 834 | 
 835 | export
 836 | maximumLeftUpperBound : (m, n : Nat) -> m `LTE` maximum m n
 837 | maximumLeftUpperBound 0 n = LTEZero
 838 | maximumLeftUpperBound (S m) 0 = reflexive
 839 | maximumLeftUpperBound (S m) (S n) = LTESucc (maximumLeftUpperBound m n)
 840 | 
 841 | export
 842 | maximumRightUpperBound : (m, n : Nat) -> n `LTE` maximum m n
 843 | maximumRightUpperBound 0 n = reflexive
 844 | maximumRightUpperBound (S m) 0 = LTEZero
 845 | maximumRightUpperBound (S m) (S n) = LTESucc (maximumRightUpperBound m n)
 846 | 
 847 | export
 848 | minimumAssociative : (l, c, r : Nat) ->
 849 |   minimum l (minimum c r) = minimum (minimum l c) r
 850 | minimumAssociative Z _ _ = Refl
 851 | minimumAssociative (S _) Z _ = Refl
 852 | minimumAssociative (S _) (S _) Z = Refl
 853 | minimumAssociative (S k) (S j) (S i) = cong S $ minimumAssociative k j i
 854 | 
 855 | export
 856 | minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l
 857 | minimumCommutative Z Z = Refl
 858 | minimumCommutative Z (S _) = Refl
 859 | minimumCommutative (S _) Z = Refl
 860 | minimumCommutative (S k) (S j) = cong S $ minimumCommutative k j
 861 | 
 862 | export
 863 | minimumIdempotent : (n : Nat) -> minimum n n = n
 864 | minimumIdempotent Z = Refl
 865 | minimumIdempotent (S k) = cong S $ minimumIdempotent k
 866 | 
 867 | export
 868 | minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
 869 | minimumZeroZeroLeft left = Calc $
 870 |   |~ minimum left 0
 871 |   ~~ minimum 0 left ...(minimumCommutative left 0)
 872 |   ~~ 0              ...(Refl)
 873 | 
 874 | export
 875 | minimumSuccSucc : (left, right : Nat) ->
 876 |   minimum (S left) (S right) = S (minimum left right)
 877 | minimumSuccSucc _ _ = Refl
 878 | 
 879 | export
 880 | maximumZeroNLeft : (left : Nat) -> maximum left Z = left
 881 | maximumZeroNLeft left = Calc $
 882 |   |~ maximum left 0
 883 |   ~~ maximum 0 left ...(maximumCommutative left Z)
 884 |   ~~ left           ...(Refl)
 885 | 
 886 | export
 887 | maximumSuccSucc : (left, right : Nat) ->
 888 |   S (maximum left right) = maximum (S left) (S right)
 889 | maximumSuccSucc _ _ = Refl
 890 | 
 891 | export
 892 | sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
 893 | sucMaxL Z = Refl
 894 | sucMaxL (S l) = cong S $ sucMaxL l
 895 | 
 896 | export
 897 | sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
 898 | sucMaxR Z = Refl
 899 | sucMaxR (S l) = cong S $ sucMaxR l
 900 | 
 901 | export
 902 | sucMinL : (l : Nat) -> minimum (S l) l = l
 903 | sucMinL Z = Refl
 904 | sucMinL (S l) = cong S $ sucMinL l
 905 | 
 906 | export
 907 | sucMinR : (l : Nat) -> minimum l (S l) = l
 908 | sucMinR Z = Refl
 909 | sucMinR (S l) = cong S $ sucMinR l
 910 | 
 911 | -- Algebra -----------------------------
 912 | 
 913 | namespace Monoid
 914 | 
 915 |   public export
 916 |   [Maximum] Monoid Nat using Semigroup.Maximum where
 917 |     neutral = 0
 918 |