Idris2Doc : Data.Prim.Integer.Extra

Data.Prim.Integer.Extra

(source)
Additional utilites for solving and deriving
(in)equalities in `Integer` arithmetics.

Reexports

import public Data.Prim.Integer

Definitions

0 pairPlusCommutative : (w + x = x + w, y + z = z + y)
  Allows us to commute addition on both sides of an inequality.

Totality: total
Visibility: export
0 pairMultCommutative : (w * x = x * w, y * z = z * y)
  Allows us to commute multiplication on both sides of an inequality.

Totality: total
Visibility: export
data Rel : (Integer -> Integer -> Type) -> Integer -> Integer -> Type
  Type describing a relation between two integers.
  
  This is used to solve integer (in)equalities with
  a syntax that is similar to the one used for preorder
  reasoning.

Totality: total
Visibility: public export
Constructors:
(<) : (x : Integer) -> (y : Integer) -> Rel (<) x y
(<=) : (x : Integer) -> (y : Integer) -> Rel (<=) x y
(===) : (x : Integer) -> (y : Integer) -> Rel (===) x y
(>=) : (x : Integer) -> (y : Integer) -> Rel (>=) x y
(>) : (x : Integer) -> (y : Integer) -> Rel (>) x y
0 rel : Rel r x y -> (u : Integer) -> (v : Integer) -> Rel r u v
Totality: total
Visibility: public export
App : a -> (a -> b) -> b
  Reversed function application.

Totality: total
Visibility: export
0 (|>) : Rel r x y -> r x y -> r x y
  The identity function for relations.

Totality: total
Visibility: export
Fixity Declarations:
infixl operator, level 0
prefix operator, level 1
0 (<>) : (a -> b) -> (b -> c) -> a -> c
  Reversed function composition.

Totality: total
Visibility: export
Fixity Declaration: infixl operator, level 0
0 (...) : Rel r x y -> (Rel r x y -> a -> r x y) -> a -> r x y
  Thought bubble similar to the one used in
  `Syntax.PreorderReasoning`.

Totality: total
Visibility: export
Fixity Declarations:
infix operator, level 1
infix operator, level 1
0 (..=) : Rel r x z -> y = z -> r x y -> r x z
  Replace the right hand side of an (in)equality.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1
0 (..~) : Rel r x z -> z = y -> r x y -> r x z
  Replace the right hand side of an (in)equality.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1
0 (=..) : Rel r x z -> y = x -> r y z -> r x z
  Replace the left hand side of an (in)equality.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1
0 (~..) : Rel r x z -> x = y -> r y z -> r x z
  Replace the left hand side of an (in)equality.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1
0 (=.=) : Rel r w z -> (x = w, y = z) -> r x y -> r w z
  Replace both sides of an (in)equality.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1
0 (~.~) : Rel r w z -> (w = x, z = y) -> r x y -> r w z
  Replace both sides of an (in)equality.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 1
0 plusLeft : Rel r (z + x) (z + y) -> r x y -> r (z + x) (z + y)
  Adding a value on the left does not affect an inequality.
  
  ```idris example
  |> x     < y
  <> z + x < z + y ... plusLeft
  ```

Totality: total
Visibility: export
0 plusRight : Rel r (x + z) (y + z) -> r x y -> r (x + z) (y + z)
  Adding a value on the right does not affect an inequality.
  
  ```idris example
  |> x     < y
  <> x + z < y + z ... plusRight
  ```

Totality: total
Visibility: export
0 plusPosRight : 0 < y -> x < (x + y)
  The result of adding a positive value is greater than
  the original.

Totality: total
Visibility: export
0 plusPosLeft : 0 < y -> x < (y + x)
  The result of adding a positive value is greater than
  the original.

Totality: total
Visibility: export
0 plusNonNegRight : 0 <= y -> x <= (x + y)
  The result of adding a positive value is not less than
  the original.

Totality: total
Visibility: export
0 plusNonNegLeft : 0 <= y -> x <= (y + x)
  The result of adding a positive value is not less than
  the original.

Totality: total
Visibility: export
0 plusNegRight : y < 0 -> (x + y) < x
  The result of adding a negative value is greater than
  the original.

Totality: total
Visibility: export
0 plusNegLeft : y < 0 -> (y + x) < x
  The result of adding a negative value is greater than
  the original.

Totality: total
Visibility: export
0 plusNonPosRight : y <= 0 -> (x + y) <= x
  The result of adding a positive value is not less than
  the original.

Totality: total
Visibility: export
0 plusNonPosLeft : y <= 0 -> (y + x) <= x
  The result of adding a positive value is not less than
  the original.

Totality: total
Visibility: export
0 minus : Rel r (x - z) (y - z) -> r x y -> r (x - z) (y - z)
  Subtracting a value does not affect an inequality.
  
  ```idris example
  |> x     < y
  <> x - z < y - z ... minus
  ```

Totality: total
Visibility: export
0 minusLT : x < y -> 0 < (y - x)
  Subtracting a value from a larger one
  yields a positive result.

Totality: total
Visibility: export
0 minusLTE : x <= y -> 0 <= (y - x)
  Subtracting a value from a non-smaller one
  yields a non-negative result.

Totality: total
Visibility: export
0 minusGT : x < y -> (x - y) < 0
  Subtracting a value from a smaller one
  yields a negative result.

Totality: total
Visibility: export
0 minusGTE : x <= y -> (x - y) <= 0
  Subtracting a value from a non-greater one
  yields a non-positive result.

Totality: total
Visibility: export
0 solvePlusRight : Rel r x y -> r (x + z) (y + z) -> r x y
  We can solve (in)equalities, where the same value has
  been added on both sides.
  
  ```idris example
  |> x + z < y + z
  <> x     < y     ... solvePlusRight
  ```

Totality: total
Visibility: export
0 solvePlusLeft : Rel r x y -> r (z + x) (z + y) -> r x y
  We can solve (in)equalities, where the same value has
  been added on both sides.
  
  ```idris example
  |> z + x < z + x
  <> x     < y     ... solvePlusLeft
  ```

Totality: total
Visibility: export
0 solveMinus : Rel r x y -> r (x - z) (y - z) -> r x y
  We can solve (in)equalities, where the same value has
  been subtracted from both sides.
  
  ```idris example
  |> x - z < y - z
  <> x     < y     ... solveMinus
  ```

Totality: total
Visibility: export
0 solvePlusRightZero : Rel r (neg y) x -> r 0 (x + y) -> r (neg y) x
  We can solve (in)equalities, with one side an addition
  and the other equalling zero.
  
  ```idris example
  |> 0     < x + y
  <> neg y < x     ... solvePlusRightZero
  ```

Totality: total
Visibility: export
0 solvePlusRightSelf : Rel r 0 x -> r y (x + y) -> r 0 x
  We can solve (in)equalities, with one side an addition
  and the other equalling the added value.
  
  ```idris example
  |> y  < x + y
  <> 0  < x     ... solvePlusRightSelf
  ```

Totality: total
Visibility: export
0 solvePlusLeftZero : Rel r (neg x) y -> r 0 (x + y) -> r (neg x) y
  We can solve (in)equalities, with one side an addition
  and the other equalling zero.
  
  ```idris example
  |> 0     < x + y
  <> neg x < y     ... solvePlusLeftZero
  ```

Totality: total
Visibility: export
0 solvePlusLeftSelf : Rel r 0 y -> r x (x + y) -> r 0 y
  We can solve (in)equalities, with one side an addition
  and the other equalling the added value.
  
  ```idris example
  |> x  < x + y
  <> 0  < y     ... solvePlusLeftSelf
  ```

Totality: total
Visibility: export
0 solveMinusZero : Rel r y x -> r 0 (x - y) -> r y x
  We can solve (in)equalities, with one side a subtraction
  and the other equalling zero.
  
  ```idris example
  |> 0 < x - y
  <> y < x     ... solveMinusZero
  ```

Totality: total
Visibility: export
0 plusOneLTE : x < y -> (x + 1) <= y
Totality: total
Visibility: export
0 negate : Rel r (neg y) (neg x) -> r x y -> r (neg y) (neg x)
  Negating both sides inverts an inequality.
  
  ```idris example
  |> x     <= y
  <> neg y <= neg x ... negate
  ```

Totality: total
Visibility: export
Fixity Declaration: prefix operator, level 10
0 negateNeg : Rel r y x -> r (neg x) (neg y) -> r y x
  Negating both sides inverts an inequality.
  
  ```idris example
  |> neg x <= neg y
  <> y     <= x     ... negateNeg
  ```

Totality: total
Visibility: export
0 negateZero : Rel r (neg x) 0 -> r 0 x -> r (neg x) 0
  `negate` specialized to where one side equals zero.
  
  ```idris example
  |> x < 0
  <> 0 < neg x ... negateZero
  ```
  
  ```idris example
  |> x <= 0
  <> 0 <= neg x ... negateZero
  ```

Totality: total
Visibility: export
0 negateNegZero : Rel r x 0 -> r 0 (neg x) -> r x 0
  `negate` specialized to where one side equals zero and the other
  a negated value.
  
  ```idris example
  |> neg x < 0
  <> 0     < x ... negateNegZero
  ```
  
  ```idris example
  |> neg x <= 0
  <> 0     <= x ... negateNegZero
  ```

Totality: total
Visibility: export
0 multPosLeft : 0 < z -> Rel r (z * x) (z * y) -> r x y -> r (z * x) (z * y)
  Multiplication with a positive number preserves an inequality.
  
  ```idris example
  |> x     < y
  <> z * x < z * y ... multPosLeft zgt0
  ```
  
  ```idris example
  |> x     <= y
  <> z * x <= z * y ... multPosLeft zgt0
  ```

Totality: total
Visibility: export
0 multPosRight : 0 < z -> Rel r (x * z) (y * z) -> r x y -> r (x * z) (y * z)
  Multiplication with a positive number preserves an inequality.
  
  ```idris example
  |> x     < y
  <> x * z < y * z ... multPosRight zgt0
  ```
  
  ```idris example
  |> x     <= y
  <> x * z <= y * z ... multPosRight zgt0
  ```

Totality: total
Visibility: export
0 multNegLeft : z < 0 -> Rel r (z * y) (z * x) -> r x y -> r (z * y) (z * x)
  Multiplication with a negative number reverses an inequality.
  
  ```idris example
  |> x     < y
  <> z * y < z * x ... multNegLeft zgt0
  ```
  
  ```idris example
  |> x     <= y
  <> z * y <= z * x ... multNegLeft zgt0
  ```

Totality: total
Visibility: export
0 multNegRight : z < 0 -> Rel r (y * z) (x * z) -> r x y -> r (y * z) (x * z)
  Multiplication with a negative number reverses an inequality.
  
  ```idris example
  |> x     < y
  <> y * z < x * z ... multNegRight zgt0
  ```
  
  ```idris example
  |> x     <= y
  <> y * z <= x * z ... multNegRight zgt0
  ```

Totality: total
Visibility: export
0 multNonNegRight : 0 <= z -> Rel (<=) (x * z) (y * z) -> x < y -> (x * z) <= (y * z)
  Multiplication with a non-negative number weakens an inequality.
  
  ```idris example
  |> x     <  y
  <> x * z <= y * z ... multNonNegRight zgte0
  ```

Totality: total
Visibility: export
0 multNonNegLeft : 0 <= z -> Rel (<=) (z * x) (z * y) -> x < y -> (z * x) <= (z * y)
  Multiplication with a non-negative number weakens an inequality.
  
  ```idris example
  |> x     <  y
  <> z * x <= z * y ... multNonNegLeft zgte0
  ```

Totality: total
Visibility: export
0 multNonPosRight : z <= 0 -> Rel (<=) (y * z) (x * z) -> x < y -> (y * z) <= (x * z)
  Multiplication with a non-positive number weakens and
  reverses an inequality.
  
  ```idris example
  |> x     <  y
  <> y * z <= x * z ... multNonPosRight zgte0
  ```

Totality: total
Visibility: export
0 multNonPosLeft : z <= 0 -> Rel (<=) (z * y) (z * x) -> x < y -> (z * y) <= (z * x)
  Multiplication with a non-positive number weakens and
  reverses an inequality.
  
  ```idris example
  |> x     <  y
  <> z * y <= z * x ... multNonPosLeft zlte0
  ```

Totality: total
Visibility: export
0 solveMultPosLeft : 0 < d -> Rel r x y -> r (d * x) (d * y) -> r x y
  We can solve (in)equalities, where both sides have
  been multiplied with the same positive value.
  
  ```idris example
  |> z * x < z * y
  <> x     < y     ... solveMultPosLeft zgt0
  ```

Totality: total
Visibility: export
0 solveMultPosRight : 0 < d -> Rel r x y -> r (x * d) (y * d) -> r x y
  We can solve (in)equalities, where both sides have
  been multiplied with the same positive value.
  
  ```idris example
  |> x * z < y * z
  <> x     < y     ... solveMultPosRight zgt0
  ```

Totality: total
Visibility: export
0 solveMultNegLeft : d < 0 -> Rel r y x -> r (d * x) (d * y) -> r y x
  We can solve (in)equalities, where both sides have
  been multiplied with the same negative value.
  
  ```idris example
  |> z * x < z * y
  <> y     < x     ... solveMultNegLeft zlt0
  ```

Totality: total
Visibility: export
0 solveMultNegRight : d < 0 -> Rel r y x -> r (x * d) (y * d) -> r y x
  We can solve (in)equalities, where both sides have
  been multiplied with the same negative value.
  
  ```idris example
  |> x * z < y * z
  <> y     < y     ... solveMultNegLeft zlt0
  ```

Totality: total
Visibility: export
0 solveMultPosRightZero : 0 < y -> Rel r 0 x -> r 0 (x * y) -> r 0 x
  We can solve (in)equalities, with one side a multiplication
  with a positive number and the other equalling zero.
  
  ```idris example
  |> 0 < x * y
  <> 0 < x     ... solveMultPosRightZero ygt0
  ```

Totality: total
Visibility: export
0 solveMultNegRightZero : y < 0 -> Rel r x 0 -> r 0 (x * y) -> r x 0
  We can solve (in)equalities, with one side a multiplication
  with a negative number and the other equalling zero.
  
  ```idris example
  |> 0 < x * y
  <> x < 0     ... solveMultNegRightZero ylt0
  ```

Totality: total
Visibility: export
0 solveMultPosLeftZero : 0 < x -> Rel r 0 y -> r 0 (x * y) -> r 0 y
  We can solve (in)equalities, with one side a multiplication
  with a positive number and the other equalling zero.
  
  ```idris example
  |> 0 < x * y
  <> 0 < y     ... solveMultPosLeftZero xgt0
  ```

Totality: total
Visibility: export
0 solveMultNegLeftZero : x < 0 -> Rel r y 0 -> r 0 (x * y) -> r y 0
  We can solve (in)equalities, with one side a multiplication
  with a negative number and the other equalling zero.
  
  ```idris example
  |> 0 < x * y
  <> y < 0     ... solveMultNegLeftZero xlt0
  ```

Totality: total
Visibility: export
0 solveMultPosRightSelf : 0 < y -> Rel r 1 x -> r y (x * y) -> r 1 x
  We can solve (in)equalities, with one side a multiplication
  with a positive number and the other equalling the positive
  number.
  
  ```idris example
  |> y < x * y
  <> 1 < x     ... solveMultPosRightSelf ygt0
  ```

Totality: total
Visibility: export
0 solveMultPosLeftSelf : 0 < x -> Rel r 1 y -> r x (x * y) -> r 1 y
  We can solve (in)equalities, with one side a multiplication
  with a positive number and the other equalling the positive
  number.
  
  ```idris example
  |> x < x * y
  <> 1 < y     ... solveMultPosLeftSelf xgt0
  ```

Totality: total
Visibility: export
0 solveMultNegRightSelf : y < 0 -> Rel r x 1 -> r y (x * y) -> r x 1
  We can solve (in)equalities, with one side a multiplication
  with a negative number and the other equalling the negative
  number.
  
  ```idris example
  |> y < x * y
  <> x < 1     ... solveMultNegRightSelf ylt0
  ```

Totality: total
Visibility: export
0 solveMultNegLeftSelf : x < 0 -> Rel r y 1 -> r x (x * y) -> r y 1
  We can solve (in)equalities, with one side a multiplication
  with a negative number and the other equalling the negative
  number.
  
  ```idris example
  |> x < x * y
  <> y < 1     ... solveMultNegLeftSelf xlt0
  ```

Totality: total
Visibility: export
0 multDivP1 : 0 < d -> (d * ((n `div` d) + 1)) > n
Totality: total
Visibility: export
0 multDiv : 0 < d -> (d * (n `div` d)) <= n
Totality: total
Visibility: export
0 divNonNeg : 0 <= n -> 0 < d -> 0 <= (n `div` d)
Totality: total
Visibility: export
0 modLTE : 0 <= n -> 0 < d -> (n `mod` d) <= n
Totality: total
Visibility: export
0 modOneIsZero : n `mod` 1 = 0
Totality: total
Visibility: export
0 divOneSame : n `div` 1 = n
Totality: total
Visibility: export
0 divGreaterOneLT : 0 < n -> 1 < d -> (n `div` d) < n
Totality: total
Visibility: export
0 divPos : d <= n -> 0 < d -> 0 < (n `div` d)
Totality: total
Visibility: export