Data.Nat.Factor

Definitions

data Factor : 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
Visibility: public export
Constructor: 

CofactorExists : (q : Nat) -> n = p * q -> Factor p n

Hints:

Antisymmetric Nat Factor

PartialOrder Nat Factor

Preorder Nat Factor

Reflexive Nat Factor

Transitive Nat Factor

Uninhabited (Factor 0 (S n))

data NotFactor : 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
Visibility: public export
Constructors:

ZeroNotFactorS : (n : Nat) -> NotFactor 0 (S n)

ProperRemExists : (q : Nat) -> (r : Fin (pred p)) -> n = (p * q) + S (finToNat r) -> NotFactor p n

data DecFactor : 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
Visibility: public export
Constructors:

ItIsFactor : Factor p n -> DecFactor p n

ItIsNotFactor : NotFactor p n -> DecFactor p n

data CommonFactor : Nat -> Nat -> Nat -> Type

  CommonFactor n m p is a witness that p is a factor of both n and m.

Totality: total
Visibility: public export
Constructor: 

CommonFactorExists : (p : Nat) -> Factor p a -> Factor p b -> CommonFactor p a b

Hint: 

Symmetric Nat (CommonFactor p)

data GCD : 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
Visibility: public export
Constructor: 

MkGCD : NotBothZero a b => Lazy (CommonFactor p a b) -> ((q : Nat) -> CommonFactor q a b -> Factor q p) -> GCD p a b

Hint: 

Symmetric Nat (GCD p)

cofactor : Factor p n -> (q : Nat ** Factor q n)

  Given a statement that p is factor of n, return its cofactor.

Totality: total
Visibility: export

oneIsFactor : (n : Nat) -> Factor 1 n

  1 is a factor of any natural number.

Totality: total
Visibility: export

oneSoleFactorOfOne : (a : Nat) -> Factor a 1 -> a = 1

  1 is the only factor of itself

Totality: total
Visibility: export

factorNotFactorAbsurd : Factor p n -> Not (NotFactor p n)

  No number can simultaneously be and not be a factor of another number.

Totality: total
Visibility: export

anythingFactorZero : (a : Nat) -> Factor a 0

  Anything is a factor of 0.

Totality: total
Visibility: export

multFactor : (p : Nat) -> (q : Nat) -> Factor p (p * q)

  For all natural numbers p and q, p is a factor of (p * q).

Totality: total
Visibility: export

factorLteNumber : Factor p n -> LTE 1 n => LTE p n

  If n > 0 then any factor of n must be less than or equal to n.

Totality: total
Visibility: export

plusDivisorAlsoFactor : Factor p n -> Factor p (n + p)

  If p is a factor of n, then it is also a factor of (n + p).

Totality: total
Visibility: export

plusDivisorNeitherFactor : NotFactor p n -> NotFactor p (n + p)

  If p is NOT a factor of n, then it also is NOT a factor of (n + p).

Totality: total
Visibility: export

multNAlsoFactor : Factor p n -> (a : Nat) -> LTE 1 a => Factor p (n * a)

  If p is a factor of n, then it is also a factor of any multiply of n.

Totality: total
Visibility: export

plusFactor : Factor p n -> Factor p m -> Factor p (n + m)

  If p is a factor of both n and m, then it is also a factor of their sum.

Totality: total
Visibility: export

minusFactor : Factor p (a + b) -> Factor p a -> Factor p b

  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
Visibility: export

modFactorAlsoFactorOfDivider : {auto 0 nNotZ : NonZero n} -> Factor p n -> Factor p (modNatNZ m n nNotZ) -> Factor p m

  If p is a common factor of n and mod m n, then it is also a factor of m.

Totality: total
Visibility: export

commonFactorAlsoFactorOfMod : {auto 0 nNotZ : NonZero n} -> Factor p m -> Factor p n -> Factor p (modNatNZ m n nNotZ)

  If p is a common factor of m and n, then it is also a factor of their mod.

Totality: total
Visibility: export

decFactor : (n : Nat) -> (d : Nat) -> DecFactor d n

  A decision procedure for whether of not p is a factor of n.

Totality: total
Visibility: export

factNotSuccFact : GT p 1 -> Factor p n -> NotFactor p (S n)

  For all p greater than 1, if p is a factor of n, then it is NOT a factor
  of (n + 1).

Totality: total
Visibility: export

commonFactorAlsoFactorOfGCD : Factor p a -> Factor p b -> GCD q a b -> Factor p q

  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
Visibility: export

oneCommonFactor : (a : Nat) -> (b : Nat) -> CommonFactor 1 a b

  1 is a common factor of any pair of natural numbers.

Totality: total
Visibility: export

selfIsCommonFactor : (a : Nat) -> LTE 1 a => CommonFactor a a a

  Any natural number is a common factor of itself and itself.

Totality: total
Visibility: export

gcd : (a : Nat) -> (b : Nat) -> NotBothZero a b => (f : Nat ** GCD f a b)

  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.

Totality: total
Visibility: export

gcdUnique : GCD p a b -> GCD q a b -> p = q

  For every two natural numbers there is a unique greatest common divisor.

Totality: total
Visibility: export

divByGcdGcdOne : GCD a (a * b) (a * c) -> GCD 1 b c

  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
Visibility: export