2 | module Data.Prim.Integer.Extra

   4 | import public Data.Prim.Integer

   5 | import Syntax.PreorderReasoning

   7 | %default total

   9 | export infixl 0  <>

  10 | export prefix 1  |>

  11 | export infix  1  ..., ..=, =.., =.=

  12 | export infix  1  ~.., ..~, ~.~

  20 | 0 pairPlusCommutative :  {w,x,y,z : Integer}

  21 |                       -> (w + x === x + w, y + z === z + y)

  22 | pairPlusCommutative = (plusCommutative, plusCommutative)

  26 | 0 pairMultCommutative :  {w,x,y,z : Integer}

  27 |                       -> (w * x === x * w, y * z === z * y)

  28 | pairMultCommutative = (multCommutative, multCommutative)

  39 | public export

  40 | data Rel :

  41 |      (rel : Integer -> Integer -> Type)

  42 |   -> (x,y : Integer)

  43 |   -> Type where

  45 |   (<)   : (x,y : Integer) -> Rel (<)   x y

  46 |   (<=)  : (x,y : Integer) -> Rel (<=)  x y

  47 |   (===) : (x,y : Integer) -> Rel (===) x y

  48 |   (>=)  : (x,y : Integer) -> Rel (>=)  x y

  49 |   (>)   : (x,y : Integer) -> Rel (>)   x y

  51 | public export

  52 | 0 rel : Rel r x y -> (u,v : Integer) -> Rel r u v

  53 | rel (_ < _)   u v = u < v

  54 | rel (_ <= _)  u v = u <= v

  55 | rel (_ === _) u v = u === v

  56 | rel (_ >= _)  u v = u >= v

  57 | rel (_ > _)   u v = u > v

  61 | App : a -> (a -> b) -> b

  62 | App x f = f x

  66 | 0 (|>) : Rel r x y -> r x y -> r x y

  67 | (|>) _ v = v

  71 | 0 (<>) : (a -> b) -> (b -> c) -> a -> c

  72 | (<>) f g = g . f

  77 | 0 (...) : Rel r x y -> (Rel r x y -> a -> r x y) -> a -> r x y

  78 | (...) r f = f r

  82 | 0 (..=) : Rel r x z -> (y === z) -> r x y -> r x z

  83 | (..=) _ prf v = replace {p = r x} prf v

  87 | 0 (..~) : Rel r x z -> (z === y) -> r x y -> r x z

  88 | (..~) r prf = r ..= sym prf

  92 | 0 (=..) : Rel r x z -> (y === x) -> r y z -> r x z

  93 | (=..) _ prf v = replace {p = \a => r a z} prf v

  97 | 0 (~..) : Rel r x z -> (x === y) -> r y z -> r x z

  98 | (~..) r prf = r =.. sym prf

 102 | 0 (=.=) : Rel r w z -> (x === w, y === z) -> r x y -> r w z

 103 | (=.=) _ (p1,p2) v = replace {p = r w} p2

 104 |                   $ replace {p = \a => r a y} p1 v

 108 | 0 (~.~) : Rel r w z -> (w === x, z === y) -> r x y -> r w z

 109 | (~.~) r (p1,p2) = r =.= (sym p1, sym p2)

 122 | 0 plusLeft :

 123 |      {x,y,z : Integer}

 124 |   -> Rel r (z + x) (z + y)

 125 |   -> r x y

 126 |   -> r (z + x) (z + y)

 127 | plusLeft (_ < _)   v         = plusGT x y z v

 128 | plusLeft (_ <= _)  (Left v)  = Left $ plusGT x y z v

 129 | plusLeft (_ <= _)  (Right v) = Right $ cong (z +) v

 130 | plusLeft (_ === _) v         = cong (z +) v

 131 | plusLeft (_ >= _)  (Left v)  = Left $ plusGT y x z v

 132 | plusLeft (_ >= _)  (Right v) = Right $ cong (z +) v

 133 | plusLeft (_ > _)   v         = plusGT y x z v

 142 | 0 plusRight :

 143 |      {x,y,z : Integer}

 144 |   -> Rel r (x + z) (y + z)

 145 |   -> r x y

 146 |   -> r (x + z) (y + z)

 147 | plusRight w =

 148 |   |> rel w x y

 149 |   <> rel w (z + x) (z + y) ... plusLeft

 150 |   <> rel w (x + z) (y + z) =.= pairPlusCommutative

 155 | 0 plusPosRight :  {x,y : Integer} -> 0 < y -> x < x + y

 156 | plusPosRight =

 157 |   |> 0 < y

 158 |   <> x + 0 < x + y ... plusLeft

 159 |   <> x     < x + y =.. plusZeroRightNeutral

 164 | 0 plusPosLeft :  {x,y : Integer} -> 0 < y -> x < y + x

 165 | plusPosLeft =

 166 |   |> 0 < y

 167 |   <> 0 + x < y + x ... plusRight

 168 |   <> x     < y + x =.. plusZeroLeftNeutral

 173 | 0 plusNonNegRight :  {x,y : Integer} -> 0 <= y -> x <= x + y

 174 | plusNonNegRight (Left lt)  = Left (plusPosRight lt)

 175 | plusNonNegRight (Right eq) =

 176 |   Right $ rewrite sym eq in (sym $ plusZeroRightNeutral {n = x})

 181 | 0 plusNonNegLeft :  {x,y : Integer} -> 0 <= y -> x <= y + x

 182 | plusNonNegLeft (Left lt)  = Left (plusPosLeft lt)

 183 | plusNonNegLeft (Right eq) =

 184 |   Right $ rewrite sym eq in (sym $ plusZeroLeftNeutral {n = x})

 189 | 0 plusNegRight :  {x,y : Integer} -> y < 0 -> x + y < x

 190 | plusNegRight =

 191 |   |> y < 0

 192 |   <> x + y < x + 0 ... plusLeft

 193 |   <> x + y < x     ..= plusZeroRightNeutral

 198 | 0 plusNegLeft :  {x,y : Integer} -> y < 0 -> y + x < x

 199 | plusNegLeft =

 200 |   |> y < 0

 201 |   <> y + x < 0 + x ... plusRight

 202 |   <> y + x < x     ..= plusZeroLeftNeutral

 207 | 0 plusNonPosRight :  {x,y : Integer} -> y <= 0 -> x + y <= x

 208 | plusNonPosRight (Left lt)  = Left (plusNegRight lt)

 209 | plusNonPosRight (Right eq) =

 210 |   Right $ rewrite eq in (plusZeroRightNeutral {n = x})

 215 | 0 plusNonPosLeft :  {x,y : Integer} -> y <= 0 -> y + x <= x

 216 | plusNonPosLeft (Left lt)  = Left (plusNegLeft lt)

 217 | plusNonPosLeft (Right eq) =

 218 |   Right $ rewrite eq in (plusZeroLeftNeutral {n = x})

 227 | 0 minus :

 228 |      {x,y,z : Integer}

 229 |   -> Rel r (x - z) (y - z)

 230 |   -> r x y

 231 |   -> r (x - z) (y - z)

 232 | minus r =

 233 |   |> rel r x y

 234 |   <> rel r (x + neg z) (y + neg z) ... plusRight

 235 |   <> rel r (x - z) (y - z)         ~.~ (minusIsPlusNeg, minusIsPlusNeg)

 240 | 0 minusLT :  {x,y : Integer} -> x < y -> 0 < y - x

 241 | minusLT =

 242 |   |> x     < y

 243 |   <> x - x < y - x ... minus

 244 |   <> 0     < y - x =.. minusSelfZero

 249 | 0 minusLTE :  {x,y : Integer} -> x <= y -> 0 <= y - x

 250 | minusLTE (Left lt)  = Left (minusLT lt)

 251 | minusLTE (Right eq) = Right $ Calc $

 252 |   |~ 0

 253 |   ~~ x - x ..< minusSelfZero

 254 |   ~~ y - x ... cong (\v => v - x) eq

 259 | 0 minusGT :  {x,y : Integer} -> x < y -> x - y < 0

 260 | minusGT =

 261 |   |> x     < y

 262 |   <> x - y < y - y ... minus

 263 |   <> x - y < 0     ..= minusSelfZero

 268 | 0 minusGTE :  {x,y : Integer} -> x <= y -> x - y <= 0

 269 | minusGTE (Left lt)  = Left (minusGT lt)

 270 | minusGTE (Right eq) = Right $ Calc $

 271 |   |~ x - y

 272 |   ~~ x - x ..< cong (\v => x - v) eq

 273 |   ~~ 0     ... minusSelfZero

 283 | 0 solvePlusRight :

 284 |      {x,y,z : Integer}

 285 |   -> Rel r x y

 286 |   -> r (x + z) (y + z)

 287 |   -> r x y

 288 | solvePlusRight r =

 289 |   |> rel r (x + z) (y + z)

 290 |   <> rel r ((x + z) - z) ((y + z - z)) ... minus

 291 |   <> rel r x y                         =.= (

 292 |        solve [x,z] ((x .+. z) -. z) (var x)

 293 |      , solve [y,z] ((y .+. z) -. z) (var y)

 294 |      )

 304 | 0 solvePlusLeft :

 305 |      {x,y,z : Integer}

 306 |   -> Rel r x y

 307 |   -> r (z + x) (z + y)

 308 |   -> r x y

 309 | solvePlusLeft r =

 310 |   |> rel r (z + x) (z + y)

 311 |   <> rel r (x + z) (y + z) =.= pairPlusCommutative

 312 |   <> rel r x y             ... solvePlusRight

 322 | 0 solveMinus :

 323 |      {x,y,z : Integer}

 324 |   -> Rel r x y

 325 |   -> r (x - z) (y - z)

 326 |   -> r x y

 327 | solveMinus r =

 328 |   |> rel r (x - z) (y - z)

 329 |   <> rel r ((x - z) + z) ((y - z) + z) ... plusRight

 330 |   <> rel r x y                         =.= (

 331 |        solve [x,z] ((x .-. z) +. z) (var x)

 332 |      , solve [y,z] ((y .-. z) +. z) (var y)

 333 |      )

 343 | 0 solvePlusRightZero :

 344 |      {x,y : Integer}

 345 |   -> Rel r (neg y) x

 346 |   -> r 0 (x + y)

 347 |   -> r (neg y) x

 348 | solvePlusRightZero r =

 349 |   |> rel r 0 (x + y)

 350 |   <> rel r (0 - y) ((x + y) - y) ... minus

 351 |   <> rel r (neg y) x             =.= (

 352 |        solve [y]   (0 -. y) (neg (var y))

 353 |      , solve [x,y] ((x .+. y) -. y) (var x)

 354 |      )

 364 | 0 solvePlusRightSelf :

 365 |      {x,y : Integer}

 366 |   -> Rel r 0 x

 367 |   -> r y (x + y)

 368 |   -> r 0 x

 369 | solvePlusRightSelf r =

 370 |   |> rel r y (x + y)

 371 |   <> rel r (0 + y) (x + y) ~.. plusZeroLeftNeutral

 372 |   <> rel r 0 x             ... solvePlusRight

 382 | 0 solvePlusLeftZero :

 383 |      {x,y : Integer}

 384 |   -> Rel r (neg x) y

 385 |   -> r 0 (x + y)

 386 |   -> r (neg x) y

 387 | solvePlusLeftZero r =

 388 |   |> rel r 0 (x + y)

 389 |   <> rel r 0 (y + x)  ..= plusCommutative

 390 |   <> rel r (neg x) y  ... solvePlusRightZero

 400 | 0 solvePlusLeftSelf :

 401 |      {x,y : Integer}

 402 |   -> Rel r 0 y

 403 |   -> r x (x + y)

 404 |   -> r 0 y

 405 | solvePlusLeftSelf r =

 406 |   |> rel r x (x + y)

 407 |   <> rel r (x + 0) (x + y) ~.. plusZeroRightNeutral

 408 |   <> rel r 0 y             ... solvePlusLeft

 418 | 0 solveMinusZero : {x,y : Integer} -> Rel r y x -> r 0 (x - y) -> r y x

 419 | solveMinusZero r =

 420 |   |> rel r 0 (x - y)

 421 |   <> rel r (0 + y) ((x - y) + y) ... plusRight

 422 |   <> rel r y x                   =.= (

 423 |        solve [y]   (0 +. y) (var y)

 424 |      , solve [x,y] ((x .-. y) +. y) (var x)

 425 |      )

 428 | 0 plusOneLTE : {x,y : Integer} -> x < y -> x + 1 <= y

 429 | plusOneLTE lt = App (oneAfterZero (y - x) (minusLT lt)) $

 430 |   |> 1     <= y - x

 431 |   <> x + 1 <= x + (y - x) ... plusLeft

 432 |   <> x + 1 <= y           ..= solve [x,y] (x .+ (y .-. x)) (var y)

 445 | 0 negate :

 446 |      {x,y : Integer}

 447 |   -> Rel r (neg y) (neg x)

 448 |   -> r x y

 449 |   -> r (neg y) (neg x)

 450 | negate r =

 451 |   |> rel r x y

 452 |   <> rel r (x - (x + y)) (y - (x + y)) ... minus

 453 |   <> rel r (neg y) (neg x)             =.= (

 454 |        solve [x,y] (x .- (x .+. y)) (negate $ var y)

 455 |      , solve [x,y] (y .- (x .+. y)) (negate $ var x)

 456 |      )

 465 | 0 negateNeg : {x,y : Integer} -> Rel r y x -> r (neg x) (neg y) -> r y x

 466 | negateNeg r =

 467 |   |> rel r (neg x) (neg y)

 468 |   <> rel r (neg $ neg y) (neg $ neg x) ... negate

 469 |   <> rel r y x                         =.= (negInvolutory, negInvolutory)

 483 | 0 negateZero : {x : Integer} -> Rel r (neg x) 0 -> r 0 x -> r (neg x) 0

 484 | negateZero r =

 485 |   |> rel r 0 x

 486 |   <> rel r (neg x) (neg 0) ... negate

 487 |   <> rel r (neg x) 0       ..= negZero

 502 | 0 negateNegZero : {x : Integer} -> Rel r x 0 -> r 0 (neg x) -> r x 0

 503 | negateNegZero r =

 504 |   |> rel r 0             (neg x)

 505 |   <> rel r (neg (neg x)) (neg 0) ... negate

 506 |   <> rel r x 0                   =.= (negInvolutory, negZero)

 512 | 0 mplLemma :

 513 |      {x,y,z : Integer}

 514 |   -> 0 < z

 515 |   -> x < y

 516 |   -> z * x < z * y

 517 | mplLemma p =

 518 |   |> x         < y

 519 |   <> x - x     < y - x               ... minus

 520 |   <> 0         < y - x               =.. minusSelfZero

 521 |   <> 0         < z * (y - x)         ... (\_ => multPosPosGT0 _ _ p)

 522 |   <> 0 + z * x < z * (y - x) + z * x ... plusRight

 523 |   <> z * x     < z * y               =.= (

 524 |        solve [x,z]   (0 + z .*. x) (z .*. x)

 525 |      , solve [x,y,z] (z .* (y .-. x) + z .*. x) (z .*. y)

 526 |      )

 540 | 0 multPosLeft :

 541 |      {x,y,z : Integer}

 542 |   -> 0 < z

 543 |   -> Rel r (z * x) (z * y)

 544 |   -> r x y

 545 |   -> r (z * x) (z * y)

 546 | multPosLeft p (_ < _)   rxy       = mplLemma p rxy

 547 | multPosLeft p (_ <= _)  (Left w)  = Left $ mplLemma p w

 548 | multPosLeft p (_ <= _)  (Right w) = Right $ cong (z *) w

 549 | multPosLeft p (_ === _) rxy       = cong (z *) rxy

 550 | multPosLeft p (_ >= _)  (Left w)  = Left $ mplLemma p w

 551 | multPosLeft p (_ >= _)  (Right w) = Right $ cong (z *) w

 552 | multPosLeft p (_ > _)   rxy       = mplLemma p rxy

 566 | 0 multPosRight :

 567 |      {x,y,z : Integer}

 568 |   -> 0 < z

 569 |   -> Rel r (x * z) (y * z)

 570 |   -> r x y

 571 |   -> r (x * z) (y * z)

 572 | multPosRight p r =

 573 |   |> rel r x y

 574 |   <> rel r (z * x) (z * y) ... multPosLeft p

 575 |   <> rel r (x * z) (y * z) =.= pairMultCommutative

 589 | 0 multNegLeft :

 590 |      {x,y,z : Integer}

 591 |   -> z < 0

 592 |   -> Rel r (z * y) (z * x)

 593 |   -> r x y

 594 |   -> r (z * y) (z * x)

 595 | multNegLeft p r =

 596 |   let negp = negateZero (neg z > 0) p

 597 |    in |> rel r x y

 598 |       <> rel r (neg y) (neg x)                 ... negate

 599 |       <> rel r (neg z * neg y) (neg z * neg x) ... multPosLeft negp

 600 |       <> rel r (z * y) (z * x)                 =.= (

 601 |            solve [z,y] (neg (var z) * neg (var y)) (z .*. y)

 602 |          , solve [z,x] (neg (var z) * neg (var x)) (z .*. x)

 603 |          )

 617 | 0 multNegRight :

 618 |      {x,y,z : Integer}

 619 |   -> z < 0

 620 |   -> Rel r (y * z) (x * z)

 621 |   -> r x y

 622 |   -> r (y * z) (x * z)

 623 | multNegRight p r =

 624 |   |> rel r x y

 625 |   <> rel r (z * y) (z * x) ... multNegLeft p

 626 |   <> rel r (y * z) (x * z) =.= pairMultCommutative

 628 | 0 lemmaMult0 : {x,y,z : Integer} -> 0 === z -> x * z === y * z

 629 | lemmaMult0 prf = Calc $

 630 |   |~ x * z

 631 |   ~~ x * 0 ..< cong (x *) prf

 632 |   ~~ 0     ... multZeroRightAbsorbs

 633 |   ~~ y * 0 ..< multZeroRightAbsorbs

 634 |   ~~ y * z ... cong (y *) prf

 643 | 0 multNonNegRight :

 644 |      {x,y,z : Integer}

 645 |   -> 0 <= z

 646 |   -> Rel (<=) (x * z) (y * z)

 647 |   -> x < y

 648 |   -> x * z <= y * z

 649 | multNonNegRight (Left p) r xy = Left $ multPosRight p (x * z < y * z) xy

 650 | multNonNegRight (Right p) r xy = Right $ lemmaMult0 p

 659 | 0 multNonNegLeft :

 660 |      {x,y,z : Integer}

 661 |   -> 0 <= z

 662 |   -> Rel (<=) (z * x) (z * y)

 663 |   -> x < y

 664 |   -> z * x <= z * y

 665 | multNonNegLeft p r =

 666 |   |> x < y

 667 |   <> x * z <= y * z ... multNonNegRight p

 668 |   <> z * x <= z * y =.= pairMultCommutative

 678 | 0 multNonPosRight :

 679 |      {x,y,z : Integer}

 680 |   -> z <= 0

 681 |   -> Rel (<=) (y * z) (x * z)

 682 |   -> x < y

 683 |   -> y * z <= x * z

 684 | multNonPosRight (Left p) r xy = Left $ multNegRight p (y * z < x * z) xy

 685 | multNonPosRight (Right p) r xy = Right $ lemmaMult0 (sym p)

 695 | 0 multNonPosLeft :

 696 |      {x,y,z : Integer}

 697 |   -> z <= 0

 698 |   -> Rel (<=) (z * y) (z * x)

 699 |   -> x < y

 700 |   -> z * y <= z * x

 701 | multNonPosLeft p r =

 702 |   |> x < y

 703 |   <> y * z <= x * z ... multNonPosRight p

 704 |   <> z * y <= z * x =.= pairMultCommutative

 706 | 0 smpLemma1 : {d,x,y : Integer} -> 0 < d -> d * x < d * y -> x < y

 707 | smpLemma1 dpos lt = case comp x y of

 708 |   LT p _ _ => p

 709 |   EQ _ p _ => void (EQ_not_LT (cong (d *) p) lt)

 710 |   GT _ _ p => void (GT_not_LT (multPosLeft dpos (d * x > d * y) p) lt)

 712 | 0 smpLemma2 : {d,x,y : Integer} -> 0 < d -> d * x === d * y -> x === y

 713 | smpLemma2 dpos lt = case comp x y of

 714 |   LT p _ _ => void (LT_not_EQ (multPosLeft dpos (d * x < d * y) p) lt)

 715 |   EQ _ p _ => p

 716 |   GT _ _ p => void (GT_not_EQ (multPosLeft dpos (d * x > d * y) p) lt)

 726 | 0 solveMultPosLeft :

 727 |      {d,x,y : Integer}

 728 |   -> 0 < d

 729 |   -> Rel r x y

 730 |   -> r (d * x) (d * y)

 731 |   -> r x y

 732 | solveMultPosLeft dpos (x < y)   lt         = smpLemma1 dpos lt

 733 | solveMultPosLeft dpos (x <= y)  (Left lt)  = Left $ smpLemma1 dpos lt

 734 | solveMultPosLeft dpos (x <= y)  (Right eq) = Right $ smpLemma2 dpos eq

 735 | solveMultPosLeft dpos (x === y) eq         = smpLemma2 dpos eq

 736 | solveMultPosLeft dpos (x >= y)  (Left lt)  = Left $ smpLemma1 dpos lt

 737 | solveMultPosLeft dpos (x >= y)  (Right eq) = Right $ smpLemma2 dpos eq

 738 | solveMultPosLeft dpos (x > y)   lt         = smpLemma1 dpos lt

 748 | 0 solveMultPosRight :

 749 |      {x,y,d : Integer}

 750 |   -> 0 < d

 751 |   -> Rel r x y

 752 |   -> r (x * d) (y * d)

 753 |   -> r x y

 754 | solveMultPosRight dpos r =

 755 |   |> rel r (x * d) (y * d)

 756 |   <> rel r (d * x) (d * y) =.= pairMultCommutative

 757 |   <> rel r x       y       ... solveMultPosLeft dpos

 767 | 0 solveMultNegLeft :

 768 |      {d,x,y : Integer}

 769 |   -> d < 0

 770 |   -> Rel r y x

 771 |   -> r (d * x) (d * y)

 772 |   -> r y x

 773 | solveMultNegLeft dneg r =

 774 |   let negdPos = negateZero (neg d > 0) dneg

 775 |    in |> rel r (d * x) (d * y)

 776 |       <> rel r (neg (d * y)) (neg (d * x)) ... negate

 777 |       <> rel r (neg d * y) (neg d * x)     =.= (

 778 |            solve [d,y] (neg (d .*. y)) (neg (var d) *. y)

 779 |          , solve [d,x] (neg (d .*. x)) (neg (var d) *. x)

 780 |          )

 781 |       <> rel r y x ... solveMultPosLeft negdPos

 791 | 0 solveMultNegRight :

 792 |      {x,y,d : Integer}

 793 |   -> d < 0

 794 |   -> Rel r y x

 795 |   -> r (x * d) (y * d)

 796 |   -> r y x

 797 | solveMultNegRight dneg r =

 798 |   |> rel r (x * d) (y * d)

 799 |   <> rel r (d * x) (d * y) =.= pairMultCommutative

 800 |   <> rel r y       x       ... solveMultNegLeft dneg

 810 | 0 solveMultPosRightZero :

 811 |      {x,y : Integer}

 812 |   -> 0 < y

 813 |   -> Rel r 0 x

 814 |   -> r 0 (x * y)

 815 |   -> r 0 x

 816 | solveMultPosRightZero pos r =

 817 |   |> rel r 0 (x * y)

 818 |   <> rel r (0 * y) (x * y) ~.. multZeroLeftAbsorbs

 819 |   <> rel r 0 x             ... solveMultPosRight pos

 829 | 0 solveMultNegRightZero :

 830 |      {x,y : Integer}

 831 |   -> y < 0

 832 |   -> Rel r x 0

 833 |   -> r 0 (x * y)

 834 |   -> r x 0

 835 | solveMultNegRightZero neg r =

 836 |   |> rel r 0 (x * y)

 837 |   <> rel r (0 * y) (x * y) ~.. multZeroLeftAbsorbs

 838 |   <> rel r x 0             ... solveMultNegRight neg

 848 | 0 solveMultPosLeftZero :

 849 |      {x,y : Integer}

 850 |   -> 0 < x

 851 |   -> Rel r 0 y

 852 |   -> r 0 (x * y)

 853 |   -> r 0 y

 854 | solveMultPosLeftZero pos r =

 855 |   |> rel r 0 (x * y)

 856 |   <> rel r (x * 0) (x * y) ~.. multZeroRightAbsorbs

 857 |   <> rel r 0 y             ... solveMultPosLeft pos

 867 | 0 solveMultNegLeftZero :

 868 |      {x,y : Integer}

 869 |   -> x < 0

 870 |   -> Rel r y 0

 871 |   -> r 0 (x * y)

 872 |   -> r y 0

 873 | solveMultNegLeftZero neg r =

 874 |   |> rel r 0 (x * y)

 875 |   <> rel r (x * 0) (x * y) ~.. multZeroRightAbsorbs

 876 |   <> rel r y 0             ... solveMultNegLeft neg

 887 | 0 solveMultPosRightSelf :

 888 |      {x,y : Integer}

 889 |   -> 0 < y

 890 |   -> Rel r 1 x

 891 |   -> r y (x * y)

 892 |   -> r 1 x

 893 | solveMultPosRightSelf pos r =

 894 |   |> rel r y (x * y)

 895 |   <> rel r (1 * y) (x * y) ~.. multOneLeftNeutral

 896 |   <> rel r 1 x             ... solveMultPosRight pos

 907 | 0 solveMultPosLeftSelf :

 908 |      {x,y : Integer}

 909 |   -> 0 < x

 910 |   -> Rel r 1 y

 911 |   -> r x (x * y)

 912 |   -> r 1 y

 913 | solveMultPosLeftSelf pos r =

 914 |   |> rel r x (x * y)

 915 |   <> rel r (x * 1) (x * y) ~.. multOneRightNeutral

 916 |   <> rel r 1 y             ... solveMultPosLeft pos

 927 | 0 solveMultNegRightSelf :

 928 |      {x,y : Integer}

 929 |   -> y < 0

 930 |   -> Rel r x 1

 931 |   -> r y (x * y)

 932 |   -> r x 1

 933 | solveMultNegRightSelf neg r =

 934 |   |> rel r y (x * y)

 935 |   <> rel r (1 * y) (x * y) ~.. multOneLeftNeutral

 936 |   <> rel r x 1             ... solveMultNegRight neg

 947 | 0 solveMultNegLeftSelf :

 948 |      {x,y : Integer}

 949 |   -> x < 0

 950 |   -> Rel r y 1

 951 |   -> r x (x * y)

 952 |   -> r y 1

 953 | solveMultNegLeftSelf neg r =

 954 |   |> rel r x (x * y)

 955 |   <> rel r (x * 1) (x * y) ~.. multOneRightNeutral

 956 |   <> rel r y 1             ... solveMultNegLeft neg

 963 | 0 multDivP1 : {n,d : Integer} -> (0 < d) -> d * (div n d + 1) > n

 964 | multDivP1 dpos = App (snd $ modLT n d dpos) $

 965 |   |> mod n d               < d

 966 |   <> d * div n d + mod n d < d * div n d + d ... plusLeft

 967 |   <> n < d * (div n d + 1)                   =.= (

 968 |        lawDivMod n d %search

 969 |      , solve [n,d,div n d] (d .*. div n d +. d)

 970 |                            (d .* (div n d .+ 1))

 971 |      )

 974 | 0 multDiv : {n,d : Integer} -> (0 < d) -> d * div n d <= n

 975 | multDiv dpos = App (fst $ modLT n d dpos) $

 976 |   |> 0 <= mod n d

 977 |   <> d * div n d + 0 <= d * div n d + mod n d ... plusLeft

 978 |   <> d * div n d     <= n                     =.= (

 979 |        plusZeroRightNeutral

 980 |      , lawDivMod n d %search

 981 |      )

 984 | 0 divNonNeg : {n,d : Integer} -> (0 <= n) -> (0 < d) -> 0 <= div n d

 985 | divNonNeg ngte0 dpos = App (trans_GT_GTE (multDivP1 dpos) ngte0) $

 986 |   |> 0     <  d * (div n d + 1)

 987 |   <> 0     <  div n d + 1       ... solveMultPosLeftZero dpos

 988 |   <> 1     <= div n d + 1       ... (\_ => oneAfterZero _)

 989 |   <> 0     <= div n d           ... solvePlusRightSelf

 992 | 0 modLTE : {n,d : Integer} -> (0 <= n) -> (0 < d) -> mod n d <= n

 993 | modLTE ngte0 dpos = App (divNonNeg ngte0 dpos) $

 994 |   |> 0               <= div n d

 995 |   <> d * 0           <= d * div n d           ... multPosLeft dpos

 996 |   <> d * 0 + mod n d <= d * div n d + mod n d ... plusRight

 997 |   <> mod n d         <= n                     =.= (

 998 |        solve [d, mod n d] (d .* 0 +. mod n d) (var (mod n d))

 999 |      , lawDivMod n d %search

1000 |      )

1003 | 0 modOneIsZero : {n : Integer} -> mod n 1 === 0

1004 | modOneIsZero = assert_total $ case comp (mod n 1) 0 of

1005 |   EQ _ p _ => p

1006 |   LT p _ _ => void (LT_not_GTE p $ fst $ modLT n 1 %search)

1007 |   GT _ _ p => void (LT_not_GTE (snd $ modLT n 1 %search) (oneAfterZero _ p))

1010 | 0 divOneSame : {n : Integer} -> div n 1 === n

1011 | divOneSame = assert_total $ Calc $

1012 |   |~ div n 1

1013 |   ~~ 1 * div n 1           ..< multOneLeftNeutral

1014 |   ~~ 1 * div n 1 + 0       ..< plusZeroRightNeutral

1015 |   ~~ 1 * div n 1 + mod n 1 ..< cong (1 * div n 1 +) modOneIsZero

1016 |   ~~ n                     ... lawDivMod n 1 %search

1019 | 0 divGreaterOneLT : {n,d : Integer} -> 0 < n -> 1 < d -> div n d < n

1020 | divGreaterOneLT npos dgt1 =

1021 |   let dpos = the (0 < d) $ trans %search dgt1

1022 |    in assert_total $ case comp 0 (div n d) of

1023 |        EQ _ p _ => replace {p = (< n)} p npos

1024 |        LT p _ _ => App dgt1 $

1025 |          |> 1 < d

1026 |          <> 1 * div n d < d * div n d ... multPosRight p

1027 |          <> div n d     < d * div n d =.. multOneLeftNeutral

1028 |          <> div n d     < n           ... (\_ => trans_GTE_GT $ multDiv dpos)

1029 |        GT _ _ p => void (LT_not_GTE p $ divNonNeg %search dpos)

1032 | 0 divPos : {n,d : Integer} -> (d <= n) -> (0 < d) -> 0 < div n d

1033 | divPos dn dp = assert_total $ case comp 0 (div n d) of

1034 |   LT p _ _ => p

1035 |   EQ _ p _ =>

1036 |     let modIsN = Calc $

1037 |           |~ mod n d

1038 |           ~~ 0 + mod n d             ..< plusZeroLeftNeutral

1039 |           ~~ (d * 0) + mod n d       ..< cong (+ mod n d) multZeroRightAbsorbs

1040 |           ~~ (d * div n d) + mod n d ... cong (\x => (d * x) + mod n d) p

1041 |           ~~ n                       ... lawDivMod n d (Right dp)

1042 |      in void (LTE_not_GT dn $ rewrite sym modIsN in snd (modLT n d dp))

1043 |   GT _ _ p => void (GT_not_LTE p (divNonNeg (Left $ trans_LT_LTE dp dn) dp))