Idris2Doc : Data.Nat.Factor

# Data.Nat.Factor

dataCommonFactor : Nat -> Nat -> Nat -> Type
`  CommonFactor n m p is a witness that p is a factor of both n and m.`

Totality: total
Constructor:
CommonFactorExists : (p : Nat) -> Factorpa -> Factorpb -> CommonFactorpab
dataDecFactor : Nat -> Nat -> Type
`  DecFactor n p is a result of the process which decides  whether or not p is a factor on n.`

Totality: total
Constructors:
ItIsFactor : Factorpn -> DecFactorpn
ItIsNotFactor : NotFactorpn -> DecFactorpn
dataFactor : Nat -> Nat -> Type
`  Factor n p is a witness that p is indeed a factor of n,  i.e. there exists a q such that p * q = n.`

Totality: total
Constructor:
CofactorExists : (q : Nat) -> n = p*q -> Factorpn
dataGCD : Nat -> Nat -> Nat -> Type
`  GCD n m p is a witness that p is THE greatest common factor of both n and m.  The second argument to the constructor is a function which for all q being  a factor of both n and m, proves that q is a factor of p.    This is equivalent to a more straightforward definition, stating that for  all q being a factor of both n and m, q is less than or equal to p, but more  powerful and therefore more useful for further proofs. See below for a proof  that if q is a factor of p then q must be less than or equal to p.`

Totality: total
Constructor:
MkGCD : NotBothZeroab => CommonFactorpab -> ((q : Nat) -> CommonFactorqab -> Factorqp) -> GCDpab
dataNotFactor : Nat -> Nat -> Type
`  NotFactor n p is a witness that p is NOT a factor of n,  i.e. there exist a q and an r, greater than 0 but smaller than p,  such that p * q + r = n.`

Totality: total
Constructors:
ZeroNotFactorS : (n : Nat) -> NotFactor0 (Sn)
ProperRemExists : (q : Nat) -> (r : Fin (predp)) -> n = (p*q) +S (finToNatr) -> NotFactorpn
anythingFactorZero : (a : Nat) -> Factora0
`  Anything is a factor of 0.`

Totality: total
cofactor : Factorpn -> DPairNat (\q => Factorqn)
`  Given a statement that p is factor of n, return its cofactor.`

Totality: total
commonFactorAlsoFactorOfGCD : Factorpa -> Factorpb -> GCDqab -> Factorpq
`  If p is a common factor of a and b, then it is also a factor of their GCD.  This actually follows directly from the definition of GCD.`

Totality: total
decFactor : (n : Nat) -> (d : Nat) -> DecFactordn
`  A decision procedure for whether of not p is a factor of n.`

Totality: total
divByGcdGcdOne : GCDa (a*b) (a*c) -> GCD1bc
`  For every two natural numbers, if we divide both of them by their GCD,  the GCD of resulting numbers will always be 1.`

Totality: total
factNotSuccFact : GTp1 -> Factorpn -> NotFactorp (Sn)
`  For all p greater than 1, if p is a factor of n, then it is NOT a factor  of (n + 1).`

Totality: total
factorLteNumber : Factorpn -> LTE1n => LTEpn
`  If n > 0 then any factor of n must be less than or equal to n.`

Totality: total
factorNotFactorAbsurd : Factorpn -> Not (NotFactorpn)
`  No number can simultaneously be and not be a factor of another number.`

Totality: total
gcd : (a : Nat) -> (b : Nat) -> NotBothZeroab => DPairNat (\f => GCDfab)
`  An implementation of Euclidean Algorithm for computing greatest common  divisors. It is proven correct and total; returns a proof that computed  number actually IS the GCD. Unfortunately it's very slow, so improvements  in terms of efficiency would be welcome.`

Totality: total
gcdUnique : GCDpab -> GCDqab -> p = q
`  For every two natural numbers there is a unique greatest common divisor.`

Totality: total
minusFactor : Factorp (a+b) -> Factorpa -> Factorpb
`  If p is a factor of a sum (n + m) and a factor of n, then it is also  a factor of m. This could be expressed more naturally with minus, but  it would be more difficult to prove, since minus lacks certain properties  that one would expect from decent subtraction.`

Totality: total
multFactor : (p : Nat) -> (q : Nat) -> Factorp (p*q)
`  For all natural numbers p and q, p is a factor of (p * q).`

Totality: total
multNAlsoFactor : Factorpn -> (a : Nat) -> LTE1a => Factorp (n*a)
`  If p is a factor of n, then it is also a factor of any multiply of n.`

Totality: total
oneCommonFactor : (a : Nat) -> (b : Nat) -> CommonFactor1ab
`  1 is a common factor of any pair of natural numbers.`

Totality: total
oneIsFactor : (n : Nat) -> Factor1n
`  1 is a factor of any natural number.`

Totality: total
oneSoleFactorOfOne : (a : Nat) -> Factora1 -> a = 1
`  1 is the only factor of itself`

Totality: total
plusDivisorAlsoFactor : Factorpn -> Factorp (n+p)
`  If p is a factor of n, then it is also a factor of (n + p).`

Totality: total
plusDivisorNeitherFactor : NotFactorpn -> NotFactorp (n+p)
`  If p is NOT a factor of n, then it also is NOT a factor of (n + p).`

Totality: total
plusFactor : Factorpn -> Factorpm -> Factorp (n+m)
`  If p is a factor of both n and m, then it is also a factor of their sum.`

Totality: total
selfIsCommonFactor : (a : Nat) -> LTE1a => CommonFactoraaa
`  Any natural number is a common factor of itself and itself.`

Totality: total