- 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
Constructor: - CommonFactorExists : (p : Nat) -> Factor p a -> Factor p b -> CommonFactor p a b
- 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
Constructors:
- ItIsFactor : Factor p n -> DecFactor p n
- ItIsNotFactor : NotFactor p n -> DecFactor p n
- 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
Constructor: - CofactorExists : (q : Nat) -> n = p * q -> Factor p n
- 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
Constructor: - MkGCD : NotBothZero a b => CommonFactor p a b -> ((q : Nat) -> CommonFactor q a b -> Factor q p) -> GCD p a b
- 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
Constructors:
- ZeroNotFactorS : (n : Nat) -> NotFactor 0 (S n)
- ProperRemExists : (q : Nat) -> (r : Fin (pred p)) -> n = (p * q) + S (finToNat r) -> NotFactor p n
- anythingFactorZero : (a : Nat) -> Factor a 0
Anything is a factor of 0.
Totality: total- cofactor : Factor p n -> DPair Nat (\q => Factor q n)
Given a statement that p is factor of n, return its cofactor.
Totality: total- 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- decFactor : (n : Nat) -> (d : Nat) -> DecFactor d n
A decision procedure for whether of not p is a factor of n.
Totality: total- 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- 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- 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- factorNotFactorAbsurd : Factor p n -> Not (NotFactor p n)
No number can simultaneously be and not be a factor of another number.
Totality: total- gcd : (a : Nat) -> (b : Nat) -> NotBothZero a b => DPair Nat (\f => 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. Unfortunately it's very slow, so improvements
in terms of efficiency would be welcome.
Totality: total- 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- 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- 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- 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- oneCommonFactor : (a : Nat) -> (b : Nat) -> CommonFactor 1 a b
1 is a common factor of any pair of natural numbers.
Totality: total- oneIsFactor : (n : Nat) -> Factor 1 n
1 is a factor of any natural number.
Totality: total- oneSoleFactorOfOne : (a : Nat) -> Factor a 1 -> a = 1
1 is the only factor of itself
Totality: total- 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- 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- 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- selfIsCommonFactor : (a : Nat) -> LTE 1 a => CommonFactor a a a
Any natural number is a common factor of itself and itself.
Totality: total