Idris2Doc : Data.Nat

Data.Nat

Reexports
import public Control.Relation
import public Control.Ord
import public Control.Order
import public Control.Function
Definitions
isZero : Nat -> Bool
  Totality: total
  Visibility: public export
isSucc : Nat -> Bool
  Totality: total
  Visibility: public export
data IsSucc : Nat -> Type
  Totality: total
  Visibility: public export
  Constructor: 
ItIsSucc : IsSucc (S n)

  Hint: 
Uninhabited (IsSucc 0)
isItSucc : (n : Nat) -> Dec (IsSucc n)
  Totality: total
  Visibility: public export
power : Nat -> Nat -> Nat
  Totality: total
  Visibility: public export
hyper : Nat -> Nat -> Nat -> Nat
  Totality: total
  Visibility: public export
pred : Nat -> Nat
  Totality: total
  Visibility: public export
compareNatDiag : (k : Nat) -> compareNat k k = EQ
  Totality: total
  Visibility: export
compareNatFlip : (m : Nat) -> (n : Nat) -> flip compareNat m n = contra (compareNat m n)
  Totality: total
  Visibility: export
data NotBothZero : Nat -> Nat -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
LeftIsNotZero : NotBothZero (S n) m
  
RightIsNotZero : NotBothZero n (S m)

  Hint: 
Uninhabited (NotBothZero 0 0)
data LTE : Nat -> Nat -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
LTEZero : LTE 0 right
  
LTESucc : LTE left right -> LTE (S left) (S right)

  Hints:
  
Antisymmetric Nat LTE
  
Connex Nat LTE
  
LinearOrder Nat LTE
  
PartialOrder Nat LTE
  
Preorder Nat LTE
  
Reflexive Nat LTE
  
Transitive Nat LTE
  
Uninhabited (LTE (S n) 0)
  
Uninhabited (LTE m n) => Uninhabited (LTE (S m) (S n))
GTE : Nat -> Nat -> Type
  Totality: total
  Visibility: public export
LT : Nat -> Nat -> Type
  Totality: total
  Visibility: public export
data View : LT m n -> Type
  LT is defined in terms of LTE which makes it annoying to use.
  This convenient view of allows us to avoid having to constantly
  perform nested matches to obtain another LT subproof instead of
  an LTE one.

  Totality: total
  Visibility: public export
  Constructors:
  
LTZero : View (LTESucc LTEZero)
  
LTSucc : (lt : LT m n) -> View (LTESucc lt)
view : (lt : LT m n) -> View lt
  Deconstruct an LT proof into either a base case or a further *LT*

  Totality: total
  Visibility: export
ltZero : LT 0 (S m)
  A convenient alias for trivial LT proofs

  Totality: total
  Visibility: export
GT : Nat -> Nat -> Type
  Totality: total
  Visibility: public export
succNotLTEzero : Not (LTE (S m) 0)
  Totality: total
  Visibility: export
fromLteSucc : LTE (S m) (S n) -> LTE m n
  Totality: total
  Visibility: export
succNotLTEpred : Not (LTE (S x) x)
  Totality: total
  Visibility: export
isLTE : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
  Totality: total
  Visibility: public export
isGTE : (m : Nat) -> (n : Nat) -> Dec (GTE m n)
  Totality: total
  Visibility: public export
isLT : (m : Nat) -> (n : Nat) -> Dec (LT m n)
  Totality: total
  Visibility: public export
isGT : (m : Nat) -> (n : Nat) -> Dec (GT m n)
  Totality: total
  Visibility: public export
lteSuccRight : LTE n m -> LTE n (S m)
  Totality: total
  Visibility: export
lteSuccLeft : LTE (S n) m -> LTE n m
  Totality: total
  Visibility: export
lteAddRight : (n : Nat) -> LTE n (n + m)
  Totality: total
  Visibility: export
notLTEImpliesGT : Not (LTE a b) -> GT a b
  Totality: total
  Visibility: export
LTEImpliesNotGT : LTE a b -> Not (GT a b)
  Totality: total
  Visibility: export
notLTImpliesGTE : Not (LT a b) -> GTE a b
  Totality: total
  Visibility: export
LTImpliesNotGTE : LT a b -> Not (GTE a b)
  Totality: total
  Visibility: export
lte : Nat -> Nat -> Bool
  Totality: total
  Visibility: public export
gte : Nat -> Nat -> Bool
  Totality: total
  Visibility: public export
lt : Nat -> Nat -> Bool
  Totality: total
  Visibility: public export
gt : Nat -> Nat -> Bool
  Totality: total
  Visibility: public export
lteReflectsLTE : (k : Nat) -> (n : Nat) -> lte k n = True -> LTE k n
  Totality: total
  Visibility: export
gteReflectsGTE : (k : Nat) -> (n : Nat) -> gte k n = True -> GTE k n
  Totality: total
  Visibility: export
ltReflectsLT : (k : Nat) -> (n : Nat) -> lt k n = True -> LT k n
  Totality: total
  Visibility: export
ltOpReflectsLT : (m : Nat) -> (n : Nat) -> So (m < n) -> LT m n
  Totality: total
  Visibility: public export
gtReflectsGT : (k : Nat) -> (n : Nat) -> gt k n = True -> GT k n
  Totality: total
  Visibility: export
minimum : Nat -> Nat -> Nat
  Totality: total
  Visibility: public export
maximum : Nat -> Nat -> Nat
  Totality: total
  Visibility: public export
eqSucc : (0 left : Nat) -> (0 right : Nat) -> left = right -> S left = S right
  Totality: total
  Visibility: export
data NonZero : Nat -> Type
  A definition of non-zero with a better behaviour than `Not (x = Z)`
  This is amenable to proof search and `NonZero Z` is more readily
  detected as impossible by Idris

  Totality: total
  Visibility: public export
  Constructor: 
SIsNonZero : NonZero (S x)

  Hint: 
Uninhabited (NonZero 0)
SIsNotZ : Not (S x = 0)
  Totality: total
  Visibility: export
mod' : Nat -> Nat -> Nat -> Nat
  Auxiliary function:
  mod' fuel a b = a `mod` (S b)
  assuming we have enough fuel

  Totality: total
  Visibility: public export
modNatNZ : Nat -> (y : Nat) -> (0 _ : NonZero y) -> Nat
  Totality: total
  Visibility: public export
modNat : Nat -> Nat -> Nat
  Visibility: export
div' : Nat -> Nat -> Nat -> Nat
  Auxiliary function:
  div' fuel a b = a `div` (S b)
  assuming we have enough fuel

  Totality: total
  Visibility: public export
divNatNZ : Nat -> (y : Nat) -> (0 _ : NonZero y) -> Nat
  Totality: total
  Visibility: public export
divNat : Nat -> Nat -> Nat
  Visibility: export
divCeilNZ : Nat -> (y : Nat) -> (0 _ : NonZero y) -> Nat
  Visibility: export
divCeil : Nat -> Nat -> Nat
  Visibility: export
divmod' : Nat -> Nat -> Nat -> (Nat, Nat)
  Totality: total
  Visibility: public export
divmodNatNZ : Nat -> (y : Nat) -> (0 _ : NonZero y) -> (Nat, Nat)
  Totality: total
  Visibility: public export
gcd : (a : Nat) -> (b : Nat) -> {auto 0 _ : NotBothZero a b} -> Nat
  Visibility: export
lcm : Nat -> Nat -> Nat
  Visibility: export
data CmpNat : Nat -> Nat -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
CmpLT : (y : Nat) -> CmpNat x (x + S y)
  
CmpEQ : CmpNat x x
  
CmpGT : (x : Nat) -> CmpNat (y + S x) y
cmp : (x : Nat) -> (y : Nat) -> CmpNat x y
  Totality: total
  Visibility: export
plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
  Totality: total
  Visibility: export
plusZeroRightNeutral : (left : Nat) -> left + 0 = left
  Totality: total
  Visibility: export
plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
  Totality: total
  Visibility: export
plusCommutative : (left : Nat) -> (right : Nat) -> left + right = right + left
  Totality: total
  Visibility: export
plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left + (centre + right) = (left + centre) + right
  Totality: total
  Visibility: export
plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) -> left = right -> left + c = right + c
  Totality: total
  Visibility: export
plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) -> left = right -> c + left = c + right
  Totality: total
  Visibility: export
plusOneSucc : (right : Nat) -> 1 + right = S right
  Totality: total
  Visibility: export
plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> left + right = left + right' -> right = right'
  Totality: total
  Visibility: export
plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) -> left + right = left' + right -> left = left'
  Totality: total
  Visibility: export
plusLeftLeftRightZero : (left : Nat) -> (right : Nat) -> left + right = left -> right = 0
  Totality: total
  Visibility: export
plusLteMonotoneRight : (p : Nat) -> (q : Nat) -> (r : Nat) -> LTE q r -> LTE (q + p) (r + p)
  Totality: total
  Visibility: export
plusLteMonotoneLeft : (p : Nat) -> (q : Nat) -> (r : Nat) -> LTE q r -> LTE (p + q) (p + r)
  Totality: total
  Visibility: export
plusLteMonotone : LTE m n -> LTE p q -> LTE (m + p) (n + q)
  Totality: total
  Visibility: export
multZeroLeftZero : (right : Nat) -> 0 * right = 0
  Totality: total
  Visibility: export
multZeroRightZero : (left : Nat) -> left * 0 = 0
  Totality: total
  Visibility: export
multRightSuccPlus : (left : Nat) -> (right : Nat) -> left * S right = left + (left * right)
  Totality: total
  Visibility: export
multLeftSuccPlus : (left : Nat) -> (right : Nat) -> S left * right = right + (left * right)
  Totality: total
  Visibility: export
multCommutative : (left : Nat) -> (right : Nat) -> left * right = right * left
  Totality: total
  Visibility: export
multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (left + centre) * right = (left * right) + (centre * right)
  Totality: total
  Visibility: export
multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre + right) = (left * centre) + (left * right)
  Totality: total
  Visibility: export
multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre * right) = (left * centre) * right
  Totality: total
  Visibility: export
multOneLeftNeutral : (right : Nat) -> 1 * right = right
  Totality: total
  Visibility: export
multOneRightNeutral : (left : Nat) -> left * 1 = left
  Totality: total
  Visibility: export
minusSuccSucc : (left : Nat) -> (right : Nat) -> minus (S left) (S right) = minus left right
  Totality: total
  Visibility: export
minusZeroLeft : (right : Nat) -> minus 0 right = 0
  Totality: total
  Visibility: export
minusZeroRight : (left : Nat) -> minus left 0 = left
  Totality: total
  Visibility: export
minusZeroN : (n : Nat) -> 0 = minus n n
  Totality: total
  Visibility: export
minusOneSuccN : (n : Nat) -> 1 = minus (S n) n
  Totality: total
  Visibility: export
minusSuccOne : (n : Nat) -> minus (S n) 1 = n
  Totality: total
  Visibility: export
minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = 0
  Totality: total
  Visibility: export
minusPos : LT m n -> LT 0 (minus n m)
  Totality: total
  Visibility: export
minusLteMonotone : LTE m n -> LTE (minus m p) (minus n p)
  Totality: total
  Visibility: export
minusLtMonotone : LT m n -> LT p n -> LT (minus m p) (minus n p)
  Totality: total
  Visibility: export
minusPlus : (m : Nat) -> minus (plus m n) m = n
  Totality: total
  Visibility: public export
plusMinusLte : (n : Nat) -> (m : Nat) -> LTE n m -> minus m n + n = m
  Totality: total
  Visibility: export
minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) -> minus (minus left centre) right = minus left (centre + right)
  Totality: total
  Visibility: export
plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> minus (left + right) (left + right') = minus right right'
  Totality: total
  Visibility: export
multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> minus left centre * right = minus (left * right) (centre * right)
  Totality: total
  Visibility: export
multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * minus centre right = minus (left * centre) (left * right)
  Totality: total
  Visibility: export
zeroMultEitherZero : (a : Nat) -> (b : Nat) -> a * b = 0 -> Either (a = 0) (b = 0)
  Totality: total
  Visibility: export
maximumAssociative : (l : Nat) -> (c : Nat) -> (r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r
  Totality: total
  Visibility: export
maximumCommutative : (l : Nat) -> (r : Nat) -> maximum l r = maximum r l
  Totality: total
  Visibility: export
maximumIdempotent : (n : Nat) -> maximum n n = n
  Totality: total
  Visibility: export
maximumLeftUpperBound : (m : Nat) -> (n : Nat) -> LTE m (maximum m n)
  Totality: total
  Visibility: export
maximumRightUpperBound : (m : Nat) -> (n : Nat) -> LTE n (maximum m n)
  Totality: total
  Visibility: export
minimumAssociative : (l : Nat) -> (c : Nat) -> (r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r
  Totality: total
  Visibility: export
minimumCommutative : (l : Nat) -> (r : Nat) -> minimum l r = minimum r l
  Totality: total
  Visibility: export
minimumIdempotent : (n : Nat) -> minimum n n = n
  Totality: total
  Visibility: export
minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = 0
  Totality: total
  Visibility: export
minimumSuccSucc : (left : Nat) -> (right : Nat) -> minimum (S left) (S right) = S (minimum left right)
  Totality: total
  Visibility: export
maximumZeroNLeft : (left : Nat) -> maximum left 0 = left
  Totality: total
  Visibility: export
maximumSuccSucc : (left : Nat) -> (right : Nat) -> S (maximum left right) = maximum (S left) (S right)
  Totality: total
  Visibility: export
sucMaxL : (l : Nat) -> maximum (S l) l = S l
  Totality: total
  Visibility: export
sucMaxR : (l : Nat) -> maximum l (S l) = S l
  Totality: total
  Visibility: export
sucMinL : (l : Nat) -> minimum (S l) l = l
  Totality: total
  Visibility: export
sucMinR : (l : Nat) -> minimum l (S l) = l
  Totality: total
  Visibility: export