Data.Nat.Factor


   0 | module Data.Nat.Factor
   1 | 
   2 | import Syntax.PreorderReasoning
   3 | import Control.WellFounded
   4 | import Data.Fin
   5 | import Data.Fin.Extra
   6 | import Data.Nat
   7 | import Data.Nat.Order.Properties
   8 | import Data.Nat.Equational
   9 | import Data.Nat.Division
  10 | 
  11 | %default total
  12 | 
  13 | ||| Factor n p is a witness that p is indeed a factor of n,
  14 | ||| i.e. there exists a q such that p * q = n.
  15 | public export
  16 | data Factor : Nat -> Nat -> Type where
  17 |     CofactorExists : {p, n : Nat} -> (q : Nat) -> n = p * q -> Factor p n
  18 | 
  19 | ||| NotFactor n p is a witness that p is NOT a factor of n,
  20 | ||| i.e. there exist a q and an r, greater than 0 but smaller than p,
  21 | ||| such that p * q + r = n.
  22 | public export
  23 | data NotFactor : Nat -> Nat -> Type where
  24 |     ZeroNotFactorS : (n : Nat) -> NotFactor Z (S n)
  25 |     ProperRemExists : {p, n : Nat} -> (q : Nat) ->
  26 |         (r : Fin (pred p)) ->
  27 |         n = p * q + S (finToNat r) ->
  28 |         NotFactor p n
  29 | 
  30 | ||| DecFactor n p is a result of the process which decides
  31 | ||| whether or not p is a factor on n.
  32 | public export
  33 | data DecFactor : Nat -> Nat -> Type where
  34 |     ItIsFactor : Factor p n -> DecFactor p n
  35 |     ItIsNotFactor : NotFactor p n -> DecFactor p n
  36 | 
  37 | ||| CommonFactor n m p is a witness that p is a factor of both n and m.
  38 | public export
  39 | data CommonFactor : Nat -> Nat -> Nat -> Type where
  40 |     CommonFactorExists : {a, b : Nat} -> (p : Nat) -> Factor p a -> Factor p b -> CommonFactor p a b
  41 | 
  42 | ||| GCD n m p is a witness that p is THE greatest common factor of both n and m.
  43 | ||| The second argument to the constructor is a function which for all q being
  44 | ||| a factor of both n and m, proves that q is a factor of p.
  45 | |||
  46 | ||| This is equivalent to a more straightforward definition, stating that for
  47 | ||| all q being a factor of both n and m, q is less than or equal to p, but more
  48 | ||| powerful and therefore more useful for further proofs. See below for a proof
  49 | ||| that if q is a factor of p then q must be less than or equal to p.
  50 | public export
  51 | data GCD : Nat -> Nat -> Nat -> Type where
  52 |     MkGCD : {a, b, p : Nat} ->
  53 |         {auto notBothZero : NotBothZero a b} ->
  54 |         (Lazy (CommonFactor p a b)) ->
  55 |         ((q : Nat) -> CommonFactor q a b -> Factor q p) ->
  56 |         GCD p a b
  57 | 
  58 | 
  59 | Uninhabited (Factor Z (S n)) where
  60 |     uninhabited (CofactorExists q prf) = uninhabited prf
  61 | 
  62 | ||| Given a statement that p is factor of n, return its cofactor.
  63 | export
  64 | cofactor : Factor p n -> (q : Nat ** Factor q n)
  65 | cofactor (CofactorExists q prf) =
  66 |         (q ** CofactorExists p $ rewrite multCommutative q p in prf)
  67 | 
  68 | ||| 1 is a factor of any natural number.
  69 | export
  70 | oneIsFactor : (n : Nat) -> Factor 1 n
  71 | oneIsFactor Z = CofactorExists Z Refl
  72 | oneIsFactor (S k) = CofactorExists (S k) (rewrite plusZeroRightNeutral k in Refl)
  73 | 
  74 | ||| 1 is the only factor of itself
  75 | export
  76 | oneSoleFactorOfOne : (a : Nat) -> Factor a 1 -> a = 1
  77 | oneSoleFactorOfOne 0 (CofactorExists _ prf) = sym prf
  78 | oneSoleFactorOfOne 1 _ = Refl
  79 | oneSoleFactorOfOne (S (S k)) (CofactorExists Z prf) =
  80 |   absurd . uninhabited $ trans prf $ multCommutative k 0
  81 | oneSoleFactorOfOne (S (S k)) (CofactorExists (S j) prf) =
  82 |   absurd . uninhabited $
  83 |     trans
  84 |       (injective prf)
  85 |       (plusCommutative j (S (j + (k * S j))))
  86 | 
  87 | ||| Every natural number is factor of itself.
  88 | export
  89 | Reflexive Nat Factor where
  90 |   reflexive = CofactorExists 1 $ rewrite multOneRightNeutral x in Refl
  91 | 
  92 | ||| Factor relation is transitive. If b is factor of a and c is b factor of c
  93 | ||| is also a factor of a.
  94 | export
  95 | Transitive Nat Factor where
  96 |   transitive (CofactorExists qb prfAB) (CofactorExists qc prfBC) =
  97 |     CofactorExists (qb * qc) $
  98 |         rewrite prfBC in
  99 |         rewrite prfAB in
 100 |         rewrite multAssociative x qb qc in
 101 |         Refl
 102 | 
 103 | export
 104 | Preorder Nat Factor where
 105 | 
 106 | multOneSoleNeutral : (a, b : Nat) -> S a = S a * b -> b = 1
 107 | multOneSoleNeutral Z b prf =
 108 |         rewrite sym $ plusZeroRightNeutral b in
 109 |         sym prf
 110 | multOneSoleNeutral (S k) Z prf =
 111 |         absurd . uninhabited $ trans prf $ multCommutative k 0
 112 | multOneSoleNeutral (S k) (S Z) prf = Refl
 113 | multOneSoleNeutral (S k) (S (S j)) prf =
 114 |         absurd . uninhabited .
 115 |         subtractEqLeft k {c = S j + S (j + (k * S j))} $
 116 |         rewrite plusSuccRightSucc j (S (j + (k * S j))) in
 117 |         rewrite plusZeroRightNeutral k in
 118 |         rewrite plusAssociative k j (S (S (j + (k * S j)))) in
 119 |         rewrite sym $ plusCommutative j k in
 120 |         rewrite sym $ plusAssociative j k (S (S (j + (k * S j)))) in
 121 |         rewrite sym $ plusSuccRightSucc k (S (j + (k * S j))) in
 122 |         rewrite sym $ plusSuccRightSucc k (j + (k * S j)) in
 123 |         rewrite plusAssociative k j (k * S j) in
 124 |         rewrite plusCommutative k j in
 125 |         rewrite sym $ plusAssociative j k (k * S j) in
 126 |         rewrite sym $ multRightSuccPlus k (S j) in
 127 |         injective $ injective prf
 128 | 
 129 | ||| If a is a factor of b and b is a factor of a, then a = b.
 130 | public export
 131 | Antisymmetric Nat Factor where
 132 |   antisymmetric {x = Z} (CofactorExists _ prfAB) _ = sym prfAB
 133 |   antisymmetric {y = Z} _ (CofactorExists _ prfBA) = prfBA
 134 |   antisymmetric {x = S a} {y = S _} (CofactorExists qa prfAB) (CofactorExists qb prfBA) =
 135 |       let qIs1 = multOneSoleNeutral a (qa * qb) $
 136 |               rewrite multAssociative (S a) qa qb in
 137 |               rewrite sym prfAB in
 138 |               prfBA
 139 |       in
 140 |       rewrite prfAB in
 141 |       rewrite oneSoleFactorOfOne qa . CofactorExists qb $ sym qIs1 in
 142 |       rewrite multOneRightNeutral a in
 143 |       Refl
 144 | 
 145 | PartialOrder Nat Factor where
 146 | 
 147 | ||| No number can simultaneously be and not be a factor of another number.
 148 | export
 149 | factorNotFactorAbsurd : Factor p n -> Not (NotFactor p n)
 150 | factorNotFactorAbsurd (CofactorExists _ prf) (ZeroNotFactorS _) =
 151 |         uninhabited prf
 152 | factorNotFactorAbsurd (CofactorExists q prf) (ProperRemExists q' r contra) with (cmp q q')
 153 |     factorNotFactorAbsurd (CofactorExists q prf) (ProperRemExists (q + S d) r contra) | CmpLT d =
 154 |         SIsNotZ .
 155 |         subtractEqLeft (p * q) {b = S ((p * S d) + finToNat r)} $
 156 |         rewrite plusZeroRightNeutral (p * q) in
 157 |         rewrite plusSuccRightSucc (p * S d) (finToNat r) in
 158 |         rewrite plusAssociative (p * q) (p * S d) (S (finToNat r)) in
 159 |         rewrite sym $ multDistributesOverPlusRight p q (S d) in
 160 |         rewrite sym contra in
 161 |         rewrite sym prf in
 162 |         Refl
 163 |     factorNotFactorAbsurd (CofactorExists q prf) (ProperRemExists q r contra) | CmpEQ =
 164 |       SIsNotZ $ sym $
 165 |         plusLeftCancel (p * q) 0 (S (finToNat r)) $
 166 |           trans (plusZeroRightNeutral (p * q)) $
 167 |             trans (sym prf) contra
 168 |     factorNotFactorAbsurd (CofactorExists (q + S d) prf) (ProperRemExists q r contra) | CmpGT d =
 169 |         let srEQpPlusPD = the (p + (p * d) = S (finToNat r)) $
 170 |                 rewrite sym $ multRightSuccPlus p d in
 171 |                 subtractEqLeft (p * q) $
 172 |                     rewrite sym $ multDistributesOverPlusRight p q (S d) in
 173 |                     rewrite sym contra in
 174 |                     sym prf
 175 |         in
 176 |         case p of
 177 |             Z => uninhabited srEQpPlusPD
 178 |             (S k) =>
 179 |                 succNotLTEzero .
 180 |                 subtractLteLeft k {b = S (d + (k * d))} $
 181 |                 rewrite sym $ plusSuccRightSucc k (d + (k * d)) in
 182 |                 rewrite plusZeroRightNeutral k in
 183 |                 rewrite srEQpPlusPD in
 184 |                 elemSmallerThanBound r
 185 | 
 186 | ||| Anything is a factor of 0.
 187 | export
 188 | anythingFactorZero : (a : Nat) -> Factor a 0
 189 | anythingFactorZero a = CofactorExists 0 (sym $ multZeroRightZero a)
 190 | 
 191 | ||| For all natural numbers p and q, p is a factor of (p * q).
 192 | export
 193 | multFactor : (p, q : Nat) -> Factor p (p * q)
 194 | multFactor p q = CofactorExists q Refl
 195 | 
 196 | ||| If n > 0 then any factor of n must be less than or equal to n.
 197 | export
 198 | factorLteNumber : Factor p n -> {auto positN : LTE 1 n} -> LTE p n
 199 | factorLteNumber (CofactorExists Z prf) =
 200 |         let nIsZero = trans prf $ multCommutative p 0
 201 |             oneLteZero = replace {p = LTE 1} nIsZero positN
 202 |         in
 203 |         absurd $ succNotLTEzero oneLteZero
 204 | factorLteNumber (CofactorExists (S k) prf) =
 205 |         rewrite prf in
 206 |         leftFactorLteProduct p k
 207 | 
 208 | ||| If p is a factor of n, then it is also a factor of (n + p).
 209 | export
 210 | plusDivisorAlsoFactor : Factor p n -> Factor p (n + p)
 211 | plusDivisorAlsoFactor (CofactorExists q prf) =
 212 |         CofactorExists (S q) $
 213 |             rewrite plusCommutative n p in
 214 |             rewrite multRightSuccPlus p q in
 215 |             cong (plus p) prf
 216 | 
 217 | ||| If p is NOT a factor of n, then it also is NOT a factor of (n + p).
 218 | export
 219 | plusDivisorNeitherFactor : NotFactor p n -> NotFactor p (n + p)
 220 | plusDivisorNeitherFactor (ZeroNotFactorS k) =
 221 |         rewrite plusZeroRightNeutral k in
 222 |         ZeroNotFactorS k
 223 | plusDivisorNeitherFactor (ProperRemExists q r remPrf) =
 224 |         ProperRemExists (S q) r $
 225 |             rewrite multRightSuccPlus p q in
 226 |             rewrite sym $ plusAssociative p (p * q) (S $ finToNat r) in
 227 |             rewrite plusCommutative p ((p * q) + S (finToNat r)) in
 228 |             rewrite remPrf in
 229 |             Refl
 230 | 
 231 | ||| If p is a factor of n, then it is also a factor of any multiply of n.
 232 | export
 233 | multNAlsoFactor : Factor p n -> (a : Nat) -> {auto aok : LTE 1 a} -> Factor p (n * a)
 234 | multNAlsoFactor _ Z = absurd $ succNotLTEzero aok
 235 | multNAlsoFactor (CofactorExists q prf) (S a) =
 236 |         CofactorExists (q * S a) $
 237 |             rewrite prf in
 238 |             sym $ multAssociative p q (S a)
 239 | 
 240 | ||| If p is a factor of both n and m, then it is also a factor of their sum.
 241 | export
 242 | plusFactor : Factor p n -> Factor p m -> Factor p (n + m)
 243 | plusFactor (CofactorExists qn prfN) (CofactorExists qm prfM) =
 244 |         rewrite prfN in
 245 |         rewrite prfM in
 246 |         rewrite sym $ multDistributesOverPlusRight p qn qm in
 247 |         multFactor p (qn + qm)
 248 | 
 249 | ||| If p is a factor of a sum (n + m) and a factor of n, then it is also
 250 | ||| a factor of m. This could be expressed more naturally with minus, but
 251 | ||| it would be more difficult to prove, since minus lacks certain properties
 252 | ||| that one would expect from decent subtraction.
 253 | export
 254 | minusFactor : {b : Nat} -> Factor p (a + b) -> Factor p a -> Factor p b
 255 | minusFactor (CofactorExists qab prfAB) (CofactorExists qa prfA) =
 256 |         CofactorExists (minus qab qa) $
 257 |             rewrite multDistributesOverMinusRight p qab qa in
 258 |             rewrite sym prfA in
 259 |             rewrite sym prfAB in
 260 |             replace {p = \x => b = minus (a + b) x} (plusZeroRightNeutral a) $
 261 |             rewrite plusMinusLeftCancel a b 0 in
 262 |             rewrite minusZeroRight b in
 263 |             Refl
 264 | 
 265 | ||| If p is a common factor of n and mod m n, then it is also a factor of m.
 266 | export
 267 | modFactorAlsoFactorOfDivider : {m, n, p : Nat} -> {auto 0 nNotZ : NonZero n} -> Factor p n -> Factor p (modNatNZ m n nNotZ) -> Factor p m
 268 | modFactorAlsoFactorOfDivider (CofactorExists qn prfN) (CofactorExists qModMN prfModMN) =
 269 |   CofactorExists (qModMN + divNatNZ m n nNotZ * qn) $ Calc $
 270 |     |~ m
 271 |     ~~ modNatNZ m n nNotZ + divNatNZ m n nNotZ * n ...(DivisionTheorem m n nNotZ nNotZ)
 272 |     ~~ qModMN * p + divNatNZ m n nNotZ * (qn * p)
 273 |               ...(rewrite multCommutative qModMN p in
 274 |                   rewrite multCommutative qn p in
 275 |                   cong2 (+) prfModMN $ cong ((*) (divNatNZ m n nNotZ)) prfN)
 276 |     ~~ qModMN * p + (divNatNZ m n nNotZ * qn) * p
 277 |               ...(cong ((+) (qModMN * p)) $ multAssociative (divNatNZ m n nNotZ) qn p)
 278 |     ~~ (qModMN + divNatNZ m n nNotZ * qn) * p ...(sym $ multDistributesOverPlusLeft qModMN _ p)
 279 |     ~~ p * (qModMN + divNatNZ m n nNotZ * qn) ...(multCommutative _ p)
 280 | 
 281 | ||| If p is a common factor of m and n, then it is also a factor of their mod.
 282 | export
 283 | commonFactorAlsoFactorOfMod : {0 m, n, p : Nat} -> {auto 0 nNotZ : NonZero n} -> Factor p m -> Factor p n -> Factor p (modNatNZ m n nNotZ)
 284 | commonFactorAlsoFactorOfMod (CofactorExists qm prfM) (CofactorExists qn prfN) =
 285 |   CofactorExists (qm `minus` divNatNZ (qm * p) n nNotZ * qn) $
 286 |       rewrite prfM in
 287 |       rewrite multCommutative p qm
 288 |       in Calc $
 289 |     |~ (modNatNZ (qm * p) n nNotZ)
 290 |     ~~ (qm * p `minus` divNatNZ (qm * p) n nNotZ * n) ...(modDividendMinusDivMultDivider (qm * p) n)
 291 |     ~~ (qm * p `minus` divNatNZ (qm * p) n nNotZ * (qn * p))
 292 |               ...(rewrite multCommutative qn p in
 293 |                   cong (\v => qm * p `minus` divNatNZ (qm * p) n nNotZ * v) prfN)
 294 |     ~~ (qm * p `minus` divNatNZ (qm * p) n nNotZ * qn * p)
 295 |               ...(cong (minus (qm * p)) $ multAssociative (divNatNZ (qm * p) n nNotZ) qn p)
 296 |     ~~ (qm `minus` (divNatNZ (qm * p) n nNotZ * qn)) * p
 297 |               ...(sym $ multDistributesOverMinusLeft qm (divNatNZ (qm * p) n nNotZ * qn) p)
 298 |     ~~ p * (qm `minus` (divNatNZ (qm * p) n nNotZ * qn)) ...(multCommutative _ p)
 299 | 
 300 | ||| A decision procedure for whether of not p is a factor of n.
 301 | export
 302 | decFactor : (n, d : Nat) -> DecFactor d n
 303 | decFactor Z Z = ItIsFactor $ reflexive
 304 | decFactor (S k) Z = ItIsNotFactor $ ZeroNotFactorS k
 305 | decFactor n (S d) =
 306 |         let Fraction n (S d) q r prf = Data.Fin.Extra.divMod n (S d) in
 307 |         case r of
 308 |             FZ =>
 309 |               ItIsFactor $ CofactorExists q $
 310 |                 rewrite sym prf in
 311 |                   rewrite plusCommutative (q * (S d)) 0 in
 312 |                     multCommutative q (S d)
 313 | 
 314 |             (FS pr) =>
 315 |                 ItIsNotFactor $ ProperRemExists q pr (
 316 |                         rewrite multCommutative d q in
 317 |                         rewrite sym $ multRightSuccPlus q d in
 318 |                         sym prf
 319 |                     )
 320 | 
 321 | ||| For all p greater than 1, if p is a factor of n, then it is NOT a factor
 322 | ||| of (n + 1).
 323 | export
 324 | factNotSuccFact : {p : Nat} -> GT p 1 -> Factor p n -> NotFactor p (S n)
 325 | factNotSuccFact {p = Z} pGt1 (CofactorExists q prf) =
 326 |         absurd $ succNotLTEzero pGt1
 327 | factNotSuccFact {p = S Z} pGt1 (CofactorExists q prf) =
 328 |         absurd . succNotLTEzero $ fromLteSucc pGt1
 329 | factNotSuccFact {p = S (S k)} pGt1 (CofactorExists q prf) =
 330 |         ProperRemExists q FZ (
 331 |             rewrite sym prf in
 332 |             rewrite plusCommutative n 1 in
 333 |             Refl
 334 |         )
 335 | 
 336 | using (p : Nat)
 337 |   ||| The relation of common factor is symmetric, that is if p is a
 338 |   ||| common factor of n and m, then it is also a common factor of
 339 |   ||| m and n.
 340 |   public export
 341 |   Symmetric Nat (CommonFactor p) where
 342 |     symmetric (CommonFactorExists p pfx pfy) = CommonFactorExists p pfy pfx
 343 | 
 344 |   ||| The relation of greatest common divisor is symmetric.
 345 |   public export
 346 |   Symmetric Nat (GCD p) where
 347 |     symmetric {x = Z} {y = Z} (MkGCD _ _) impossible
 348 |     symmetric {x = S _} (MkGCD cf greatest) =
 349 |       MkGCD (symmetric cf) $ \q, cf => greatest q $ symmetric cf
 350 |     symmetric {y = S _} (MkGCD cf greatest) =
 351 |       MkGCD (symmetric cf) $ \q, cf => greatest q $ symmetric cf
 352 | 
 353 | ||| If p is a common factor of a and b, then it is also a factor of their GCD.
 354 | ||| This actually follows directly from the definition of GCD.
 355 | export
 356 | commonFactorAlsoFactorOfGCD : {p : Nat} -> Factor p a -> Factor p b -> GCD q a b -> Factor p q
 357 | commonFactorAlsoFactorOfGCD pfa pfb (MkGCD _ greatest) =
 358 |         greatest p (CommonFactorExists p pfa pfb)
 359 | 
 360 | ||| 1 is a common factor of any pair of natural numbers.
 361 | export
 362 | oneCommonFactor : (a, b : Nat) -> CommonFactor 1 a b
 363 | oneCommonFactor a b = CommonFactorExists 1
 364 |         (CofactorExists a (rewrite plusZeroRightNeutral a in Refl))
 365 |         (CofactorExists b (rewrite plusZeroRightNeutral b in Refl))
 366 | 
 367 | ||| Any natural number is a common factor of itself and itself.
 368 | export
 369 | selfIsCommonFactor : (a : Nat) -> {auto ok : LTE 1 a} -> CommonFactor a a a
 370 | selfIsCommonFactor a = CommonFactorExists a reflexive reflexive
 371 | 
 372 | gcdUnproven' : (m, n : Nat) -> (0 sizeM : SizeAccessible m) -> (0 n_lt_m : LT n m) -> Nat
 373 | gcdUnproven' m Z _ _ = m
 374 | gcdUnproven' m (S n) (Access rec) n_lt_m =
 375 |   let mod_lt_n = boundModNatNZ m (S n) ItIsSucc in
 376 |   gcdUnproven' (S n) (modNatNZ m (S n) ItIsSucc) (rec _ n_lt_m) mod_lt_n
 377 | 
 378 | ||| Total definition of the gcd function. Does not return GСD evidence, but is faster.
 379 | gcdUnproven : Nat -> Nat -> Nat
 380 | gcdUnproven m n with (isLT n m)
 381 |   gcdUnproven m n | Yes n_lt_m = gcdUnproven' m n (wellFounded m) n_lt_m
 382 |   gcdUnproven m n | No not_n_lt_m with (decomposeLte m n $ notLTImpliesGTE not_n_lt_m)
 383 |     gcdUnproven m n | No not_n_lt_m | Left m_lt_n = gcdUnproven' n m (wellFounded n) m_lt_n
 384 |     gcdUnproven m n | No not_n_lt_m | Right m_eq_n = m
 385 | 
 386 | gcdUnproven'Greatest : {m, n, c : Nat} -> (0 sizeM : SizeAccessible m) -> (0 n_lt_m : LT n m)
 387 |   -> Factor c m -> Factor c n -> Factor c (gcdUnproven' m n sizeM n_lt_m)
 388 | gcdUnproven'Greatest {n = Z} _ _ cFactM _ = cFactM
 389 | gcdUnproven'Greatest {n = S n} (Access rec) n_lt_m cFactM cFactN =
 390 |   gcdUnproven'Greatest (rec _ n_lt_m) (boundModNatNZ m (S n) ItIsSucc) cFactN (commonFactorAlsoFactorOfMod cFactM cFactN)
 391 | 
 392 | gcdUnprovenGreatest : (m, n : Nat) -> {auto 0 ok : NotBothZero m n} -> (q : Nat) -> CommonFactor q m n -> Factor q (gcdUnproven m n)
 393 | gcdUnprovenGreatest m n q (CommonFactorExists q qFactM qFactN) with (isLT n m)
 394 |   gcdUnprovenGreatest m n q (CommonFactorExists q qFactM qFactN) | Yes n_lt_m
 395 |     = gcdUnproven'Greatest (sizeAccessible m) n_lt_m qFactM qFactN
 396 |   gcdUnprovenGreatest m n q (CommonFactorExists q qFactM qFactN) | No not_n_lt_m with (decomposeLte m n $ notLTImpliesGTE not_n_lt_m)
 397 |     gcdUnprovenGreatest m n q (CommonFactorExists q qFactM qFactN) | No not_n_lt_m | Left m_lt_n
 398 |       = gcdUnproven'Greatest (sizeAccessible n) m_lt_n qFactN qFactM
 399 |     gcdUnprovenGreatest Z Z q (CommonFactorExists q qFactM qFactN) | No not_n_lt_m | Right m_eq_n impossible
 400 |     gcdUnprovenGreatest (S m) (S n) q (CommonFactorExists q qFactM qFactN) | No not_n_lt_m | Right m_eq_n = qFactM
 401 | 
 402 | gcdUnproven'CommonFactor : {m, n : Nat} -> (0 sizeM : SizeAccessible m) -> (0 n_lt_m : LT n m) -> CommonFactor (gcdUnproven' m n sizeM n_lt_m) m n
 403 | gcdUnproven'CommonFactor {n = Z} _ _ = CommonFactorExists _ reflexive (anythingFactorZero m)
 404 | gcdUnproven'CommonFactor {n = S n} (Access rec) n_lt_m with (gcdUnproven'CommonFactor (rec _ n_lt_m) (boundModNatNZ m (S n) ItIsSucc))
 405 |   gcdUnproven'CommonFactor (Access rec) n_lt_m | (CommonFactorExists _ factM factN)
 406 |     = CommonFactorExists _ (modFactorAlsoFactorOfDivider factM factN) factM
 407 | 
 408 | gcdUnprovenCommonFactor : (m, n : Nat) -> {auto 0 ok : NotBothZero m n} -> CommonFactor (gcdUnproven m n) m n
 409 | gcdUnprovenCommonFactor m n with (isLT n m)
 410 |   gcdUnprovenCommonFactor m n | Yes n_lt_m = gcdUnproven'CommonFactor (sizeAccessible m) n_lt_m
 411 |   gcdUnprovenCommonFactor m n | No not_n_lt_m with (decomposeLte m n $ notLTImpliesGTE not_n_lt_m)
 412 |     gcdUnprovenCommonFactor m n | No not_n_lt_m | Left m_lt_n = symmetric $ gcdUnproven'CommonFactor (sizeAccessible n) m_lt_n
 413 |     gcdUnprovenCommonFactor Z Z | No not_n_lt_m | Right m_eq_n impossible
 414 |     gcdUnprovenCommonFactor (S m) (S n) | No not_n_lt_m | Right m_eq_n = rewrite m_eq_n in selfIsCommonFactor (S n)
 415 | 
 416 | ||| An implementation of Euclidean Algorithm for computing greatest common
 417 | ||| divisors. It is proven correct and total; returns a proof that computed
 418 | ||| number actually IS the GCD.
 419 | export
 420 | gcd : (a, b : Nat) -> {auto ok : NotBothZero a b} -> (f : Nat ** GCD f a b)
 421 | gcd a b = (_ ** MkGCD (gcdUnprovenCommonFactor a b) (gcdUnprovenGreatest a b))
 422 | 
 423 | ||| For every two natural numbers there is a unique greatest common divisor.
 424 | export
 425 | gcdUnique : GCD p a b -> GCD q a b -> p = q
 426 | gcdUnique (MkGCD pCFab greatestP) (MkGCD qCFab greatestQ) =
 427 |     antisymmetric (greatestQ p pCFab) (greatestP q qCFab)
 428 | 
 429 | divByGcdHelper : (a, b, c : Nat) -> GCD (S a) (S a * S b) (S a * c) -> GCD 1 (S b) c
 430 | divByGcdHelper a b c (MkGCD _ greatest) =
 431 |     MkGCD (CommonFactorExists 1 (oneIsFactor (S b)) (oneIsFactor c)) $
 432 |     \q, (CommonFactorExists q (CofactorExists qb prfQB) (CofactorExists qc prfQC)) =>
 433 |         let qFab = CofactorExists qb $
 434 |                 rewrite multCommutative q (S a) in
 435 |                 rewrite sym $ multAssociative (S a) q qb in
 436 |                 rewrite sym $ prfQB in
 437 |                 Refl
 438 |             qFac = CofactorExists qc $
 439 |                 rewrite multCommutative q (S a) in
 440 |                 rewrite sym $ multAssociative (S a) q qc in
 441 |                 rewrite sym $ prfQC in
 442 |                 Refl
 443 |             CofactorExists f prfQAfA =
 444 |                 greatest (q * S a) (CommonFactorExists (q * S a) qFab qFac)
 445 |             qf1 = multOneSoleNeutral a (f * q) $
 446 |                 rewrite multCommutative f q in
 447 |                 rewrite multAssociative (S a) q f in
 448 |                 rewrite sym $ multCommutative q (S a) in
 449 |                 prfQAfA
 450 |         in
 451 |         CofactorExists f $
 452 |             rewrite multCommutative q f in
 453 |             sym qf1
 454 | 
 455 | ||| For every two natural numbers, if we divide both of them by their GCD,
 456 | ||| the GCD of resulting numbers will always be 1.
 457 | export
 458 | divByGcdGcdOne : {a, b, c : Nat} -> GCD a (a * b) (a * c) -> GCD 1 b c
 459 | divByGcdGcdOne {a = Z} (MkGCD _ _) impossible
 460 | divByGcdGcdOne {a = S a} {b = Z} {c = Z} (MkGCD {notBothZero} _ _) =
 461 |         case replace {p = \x => NotBothZero x x} (multZeroRightZero (S a)) notBothZero of
 462 |             LeftIsNotZero impossible
 463 |             RightIsNotZero impossible
 464 | divByGcdGcdOne {a = S a} {b = Z} {c = S c} gcdPrf@(MkGCD {notBothZero} _ _) =
 465 |         case replace {p = \x => NotBothZero x (S a * S c)} (multZeroRightZero (S a)) notBothZero of
 466 |             LeftIsNotZero impossible
 467 |             RightIsNotZero => symmetric $ divByGcdHelper a c Z $ symmetric gcdPrf
 468 | divByGcdGcdOne {a = S a} {b = S b} {c = Z} gcdPrf@(MkGCD {notBothZero} _ _) =
 469 |         case replace {p = \x => NotBothZero (S a * S b) x} (multZeroRightZero (S a)) notBothZero of
 470 |             RightIsNotZero impossible
 471 |             LeftIsNotZero => divByGcdHelper a b Z gcdPrf
 472 | divByGcdGcdOne {a = S a} {b = S b} {c = S c} gcdPrf =
 473 |         divByGcdHelper a b (S c) gcdPrf
 474 |