Proof of Euclid's Lemma in Idris - Number Theory Algorithms

Euclid.idr

module Euclid

import Syntax.PreorderReasoning

%default total

Divides : (divisor, dividend : Nat) -> Type
Divides d n = (q : Nat ** (n = q * d))

data Direction = LTR | RTL

diff : Direction -> Nat -> Nat -> Nat
diff LTR m n = minus m n
diff RTL m n = minus n m

||| ...
||| There is an action of (ℤ,+) on this type. We are actually
||| interested about the quotient of this type by that action.
data Coprime : (u,v : Nat) -> Type where
  MkCoprime : (dir : Direction) -> (s,t : Nat) -> (1 = diff dir (s * u) (t * v)) -> Coprime u v

coprimeCommutative : Coprime u v -> Coprime v u
coprimeCommutative (MkCoprime LTR s t tv'su) = (MkCoprime RTL t s tv'su)
coprimeCommutative (MkCoprime RTL s t tv'su) = (MkCoprime LTR t s tv'su)

multDistributesOverDiffLeft : (dir : Direction) -> (left, centre, right : Nat) ->
  (diff dir left centre) * right = diff dir (left * right) (centre * right)
multDistributesOverDiffLeft LTR left centre right = multDistributesOverMinusLeft left centre right
multDistributesOverDiffLeft RTL left centre right = multDistributesOverMinusLeft centre left right

pairingLemma : (dir : Direction) ->
  (ug_if : u * g = i * f) ->
  (vg_jf : v * g = j * f) ->
  (tv'su : 1 = diff dir (t * v) (s * u)) ->
           g = (diff dir (t * j) (s * i)) * f
pairingLemma {f}{g} {i}{j} {s}{t} {u}{v} dir ug_if vg_jf tv'su =
                                  (g)
={ sym $ multOneLeftNeutral g }=
                                (1 * g)
={ cong {f=(* g)} tv'su }=
                ((diff dir (t * v)      (s * u)) * g)
={ multDistributesOverDiffLeft dir (t * v) (s * u) g                                   }=
                (diff dir ((t * v) * g) ((s * u) * g))
={ cong {f=\m => diff dir ((t * v) * g)       m      } (sym $ multAssociative s u g)   }=
                (diff dir ((t * v) * g) (s * (u * g)))
={ cong {f=\m => diff dir ((t * v) * g) (s *    m   )} ug_if                           }=
                (diff dir ((t * v) * g) (s * (i * f)))
={ cong {f=\m => diff dir ((t * v) * g)       m      } (multAssociative s i f)         }=
                (diff dir ((t * v) * g) ((s * i) * f))
={ cong {f=\m => diff dir       m       ((s * i) * f)} (sym $ multAssociative t v g)   }=
                (diff dir (t * (v * g)) ((s * i) * f))
={ cong {f=\m => diff dir (t *    m   ) ((s * i) * f)} vg_jf                           }=
                (diff dir (t * (j * f)) ((s * i) * f))
={ cong {f=\m => diff dir       m       ((s * i) * f)} (multAssociative t j f)         }=
                (diff dir ((t * j) * f) ((s * i) * f))
={ sym $ multDistributesOverDiffLeft dir (t * j) (s * i) f                             }=
                ((diff dir (t * j)       (s * i)) * f)
QED

data IsGCD : (gcd,a,b : Nat) -> Type where
  MkGCD : (u,v : Nat) -> (a = u * g) -> (b = v * g) -> (Coprime u v) -> IsGCD g a b

gcdCommutative : IsGCD g a b -> IsGCD g b a
gcdCommutative (MkGCD u v ug_eq vg_eq cpm) = (MkGCD v u vg_eq ug_eq (coprimeCommutative cpm))

commuteGCD : (g ** IsGCD g a b) -> (g ** IsGCD g b a)
commuteGCD (g ** isGCD) = (g ** gcdCommutative isGCD)

egcd : (a,b : Nat) -> (g ** IsGCD g a b)

fst  : IsGCD g a b -> Divides g a
snd  : IsGCD g a b -> Divides g b
fst  (MkGCD u v a_ug b_vg _) = (u ** a_ug)
snd  (MkGCD u v a_ug b_vg _) = (v ** b_vg)

pair : IsGCD g a b -> (f : Nat) -> (f `Divides` a) -> (f `Divides` b) -> f `Divides` g
pair (MkGCD u v a_ug b_vg (MkCoprime LTR s t tv'su)) {g} f (i ** a_if) (j ** b_jf) 
  = (diff RTL (t * j) (s * i) ** pairingLemma RTL ug_if vg_jf tv'su)
where ug_if : u * g = i * f
      vg_jf : v * g = j * f
      ug_if = (sym a_ug) `trans` a_if
      vg_jf = (sym b_vg) `trans` b_jf
pair (MkGCD u v a_ug b_vg (MkCoprime RTL s t tv'su)) {g} f (i ** a_if) (j ** b_jf) 
  = (diff LTR (t * j) (s * i) ** pairingLemma LTR ug_if vg_jf tv'su)
where ug_if : u * g = i * f
      vg_jf : v * g = j * f
      ug_if = (sym a_ug) `trans` a_if
      vg_jf = (sym b_vg) `trans` b_jf

||| Corollary of Bezout's lemma
coprimeLemma : (Coprime f n) -> (f `Divides` n * g) -> (f `Divides` g)
coprimeLemma {f=v}{n=u}{g} (MkCoprime LTR s t tv'su) (b ** ug_bv) 
  = (diff RTL (t * b) (s * g) ** pairingLemma LTR ug_bv (multCommutative v g) tv'su)
coprimeLemma {f=v}{n=u}{g} (MkCoprime RTL s t tv'su) (b ** ug_bv) 
  = (diff LTR (t * b) (s * g) ** pairingLemma RTL ug_bv (multCommutative v g) tv'su)

Irreducible : (p : Nat) -> Type
Irreducible p = (a,b : Nat) -> (p = a * b) -> (1 + p = a + b)

%hint
irreducibleImpliesNotZero : Irreducible p -> Not (p = Z)
irreducibleImpliesNotZero {p} irdx p_z = void (SIsNotZ zSz)
where zSz : S Z = Z
      pSp : S p = p
      zSz = rewrite sym p_z in pSp
      pSp = irdx 0 p p_z

irreducibility : Irreducible p -> (a `Divides` p) -> (a = S (S a')) -> a = p
irreducibility {a}{p} irdx (Z       ** p_0a) _ = void $ irreducibleImpliesNotZero irdx p_0a
irreducibility {a}{p} irdx (S Z     ** p_1a) _ = rewrite sym (multOneLeftNeutral a) in sym p_1a
irreducibility {a}{p} irdx (S (S b) ** p_ba) {a'} a_SSa' = void (SIsNotZ (sym eq0))
where eq1 : S (S b) + a = S p
      eq2 :     S b + a = p
      eq3 :     S b + a = a + (S b * a)
      eq4 :     a + S b = a + (S b * a)
      eq5 :         S b = S b * a
      eq6 :         S b = S b * S (S a')
      eq7 :         S b = S (S a') * S b
      eq8 :         S b = S b + (S b + a' * S b)
      eq9 :     S b + Z = S b + (S b + a' * S b)
      eq0 :           Z = S b + a' * S b
      ------------------------------------------
      eq1 = sym $ irdx (S (S b)) a p_ba
      eq2 = succInjective (S b + a) p eq1
      eq3 = eq2 `trans` p_ba
      eq4 = rewrite plusCommutative a (S b) in eq3
      eq5 = plusLeftCancel a (S b) (S b * a) eq4
      eq6 = eq5 `trans` cong {f=((S b) *)} a_SSa'
      eq7 = rewrite multCommutative (S (S a')) (S b) in eq6
      eq8 = eq7
      eq9 = rewrite plusZeroRightNeutral (S b) in eq8
      eq0 = plusLeftCancel (S b) Z (S b + a' * S b) eq9

invert : Irreducible p -> (p `Divides` a -> Void) -> Coprime p a
invert {p}{a} irdx p_a with (egcd p a)
  | (S Z ** (MkGCD u v p_ug a_vg cpm)) = 
      rewrite a_vg `trans` multOneRightNeutral v in 
      rewrite p_ug `trans` multOneRightNeutral u in cpm
  | (S (S g) ** (MkGCD u v p_ug a_vg cpm)) = void (p_a p'a)
    where g2p : S (S g) = p
          g2p = irreducibility irdx (u ** p_ug) Refl
          p'a : p `Divides` a
          p'a = rewrite sym g2p in (v ** a_vg)
  | (Z ** (MkGCD u v p_ug a_vg cpm)) = void (p_a p'a)
    where p_z : p = Z
          p_z = rewrite sym $ multZeroRightZero u in p_ug
          a_z : a = Z
          a_z = rewrite sym $ multZeroRightZero v in a_vg
          p'a : p `Divides` a
          p'a = rewrite a_z in 
                rewrite p_z in (1 ** Refl)

euclidsLemma :
  Irreducible p ->
  (p `Divides` a -> Void) -> 
  (p `Divides` b -> Void) -> 
  (p `Divides` (a * b) -> Void)

euclidsLemma {p}{a}{b} irdx p_a p_b p'ab = p_b (coprimeLemma p_'_a p'ab)
where p_'_a : Coprime p a
      p_'_a = invert irdx p_a

--------------------------------------      

data LT' : (n,m : Nat) -> Type where
  Z' : LT' n (S n)
  S' : LT' n m -> LT' n (S m)

||| Lifted from IteratedSubtraction.idr
implementation WellFounded LT' where
  wellFounded x = Access (acc x)
  where acc : (x, y : Nat) -> LT' y x -> Accessible LT' y
        acc Z     y lt      impossible
        acc (S y) y Z'      = Access (acc y)
        acc (S x) y (S' lt) = acc x y lt

eqToLT : (j = S (i + d)) -> (i `LT'` j)
eqToLT {i} {d=Z}   eq = rewrite eq in rewrite sym $ plusZeroRightNeutral i in Z'
eqToLT {i} {d=S d} eq = rewrite eq in S' (eqToLT (sym $ plusSuccRightSucc i d))

data Subtraction : (i, j : Nat) -> Type where
  Pos  : (d : Nat) -> {auto eq : i = j + d}   -> Subtraction i j
  NegS : (d : Nat) -> {auto eq : j = S i + d} -> Subtraction i j

subtract : (i,j : Nat) -> Subtraction i j
subtract i     Z     = Pos i
subtract Z     (S j) = NegS j
subtract (S i) (S j) with (subtract i j)
  | Pos d  {eq} = Pos d  {eq = cong eq}
  | NegS d {eq} = NegS d {eq = cong eq}

data Fin : Nat -> Type where
  MkFin : (k : Nat) -> (k `LT'` n) -> Fin n

data NotZero : Nat -> Type where
  SIsNotZero : NotZero (S n)

QuotRem : (divisor, dividend : Nat) -> Fin divisor -> Type
QuotRem d n (MkFin r lt) = (q : Nat ** (n = r + q * d))

Division : (divisor, dividend : Nat) -> Type
Division d n = (r : Fin d ** QuotRem d n r)

DZ : (n : Nat) -> {auto lt : n `LT'` (S d)} -> Division (S d) n
DS : Division (S d) n -> Division (S d) ((S d) + n)

divide : (n,d : Nat) -> .{auto nz : NotZero d} -> Division d n
divide n d' {nz} = wfInd {P=P} divStep n d' nz
where P : (dividend : Nat) -> Type
      P dividend = (divisor : Nat) -> (nz : NotZero divisor) -> Division divisor dividend
      divStep : (dividend : Nat) -> (rec : (n' : Nat) -> LT' n' dividend -> P n') -> P dividend
      divStep n rec Z      nz impossible
      divStep n rec (S pd) nz with (subtract n (S pd))
        | NegS d {eq} = DZ n {lt = eqToLT eq}
        | Pos n' {eq} = 
            let ltn : LT' n' n = eqToLT (eq `trans` cong (plusCommutative pd n'))
            in rewrite eq in DS (rec n' ltn (S pd) nz)

multRotates : (x,y,z : Nat) -> (z * x) * y = x * (y * z)
multRotates x y z =
  ((z * x) * y)
={ multCommutative (z * x) y }=
  (y * (z * x))
={ multAssociative y z x }=
  ((y * z) * x)
={ multCommutative (y * z) x }=
  (x * (y * z))
QED

plusDiffLeftCancel : (dir : Direction) -> (left, right1, right2 : Nat) -> 
  diff dir (left + right1) (left + right2) = diff dir right1 right2
plusDiffLeftCancel LTR left right1 right2 = plusMinusLeftCancel left right1 right2
plusDiffLeftCancel RTL left right1 right2 = plusMinusLeftCancel left right2 right1

twistCoprime' : (dir : Direction) -> (q : Nat) -> diff dir (t * (v + u * q)) ((q * t + s) * u) = diff dir (t * v) (s * u)
twistCoprime' {s}{t}{u}{v} dir q = 
  rewrite multDistributesOverPlusLeft  (q * t) s u in 
  rewrite multDistributesOverPlusRight t v (u * q) in 
  rewrite multRotates t u q in
  rewrite plusCommutative (t * v) (t * (u * q)) in
    plusDiffLeftCancel dir (t * (u * q)) (t * v) (s * u)

twistCoprime : (q : Nat) -> (Coprime u v) -> (Coprime (v + u * q) u)
twistCoprime {u}{v} q (MkCoprime LTR s t su_1_tv) = 
  (MkCoprime RTL t (q * t + s) (su_1_tv `trans` sym (twistCoprime' RTL q)))
twistCoprime {u}{v} q (MkCoprime RTL s t su_1_tv) =
  (MkCoprime LTR t (q * t + s) (su_1_tv `trans` sym (twistCoprime' LTR q)))

gcd_lemma : Divides d a -> (g ** IsGCD g d r) -> (g ** IsGCD g (r + a) d)
gcd_lemma {d=ug}{r=vg}{a=qug} (q ** qug_eq)
  (g ** MkGCD u v ug_eq vg_eq cpm)
= (g ** MkGCD (v + u * q) u vg_qug_eq ug_eq (twistCoprime q cpm))
where vg_qug_eq : vg + qug = (v + u * q) * g
      vg_qug_eq =
                        ( vg   +      qug   )
      ={ cong {f=\m =>  ( vg   +       m    ) } qug_eq                  }=
                        ( vg   + q *   ug   )
      ={ cong {f=\m =>  (  m   + q *   ug   ) } vg_eq                   }= 
                        (v * g + q *   ug   )
      ={ cong {f=\m =>  (v * g + q *   m    ) } ug_eq                   }=
                        (v * g + q * (u * g))
      ={ cong {f=\m =>  (v * g +       m    ) } (multAssociative q u g) }= 
                        (v * g + (q * u) * g)
      ={ sym $ multDistributesOverPlusLeft v (q * u) g                  }= 
                        ((v + q * u)     * g)
      ={ cong {f=\m =>  ((v +   m  )     * g) } (multCommutative q u)   }= 
                        ((v + u * q)     * g) 
      QED

gcdLT : (a,b : Nat) -> (b `LT'` a) -> (g ** IsGCD g a b)
gcdLT x y lx = wfInd {P=P} gcdStep x y lx
where P : (a : Nat) -> Type
      P a = (b : Nat) -> (b `LT'` a) -> (g ** IsGCD g a b)
      gcdStep : (a : Nat) -> (rec : (a' : Nat) -> LT' a' a -> P a') -> P a
      gcdStep a rec Z lt 
        = (a ** MkGCD 1 0 (sym $ multOneLeftNeutral a) Refl (MkCoprime LTR 1 0 Refl))
      gcdStep a rec (S b) lt with (a `divide` (S b))
        | ((MkFin r lt') ** q ** eq) = rewrite eq in gcd_lemma (q ** Refl) (rec (S b) lt r lt')

egcd a b with (subtract a b)
  | NegS d    {eq} = commuteGCD (gcdLT b a (eqToLT eq))
  | Pos (S d) {eq} = gcdLT a b (eqToLT eq')
    where eq' : a = S (plus b d)
          eq' = rewrite plusSuccRightSucc b d in eq
  | Pos Z     {eq} = (b ** isGCD)
    where isGCD : IsGCD b a b
          cpm11 : Coprime 1 1
          cpm11 = MkCoprime RTL 0 1 Refl
          isGCD = MkGCD 1 1 eq (sym (plusZeroRightNeutral b)) cpm11

DZ r {lt} = ((MkFin r lt) ** Z ** (sym $ plusZeroRightNeutral r))
DS {n}{d} ((MkFin r lt) ** q ** eq) = ((MkFin r lt) ** (S q) ** eq')
where eq' : (S (d + n)) = (r + (S q * S d))
      eq' = 
                              (S (d +          n    ))
      ={ cong {f=\m =>         S (d +          m    )} eq                         }=
                              (S (d + (r  + (q * S d))))
      ={ plusAssociative      (S  d)   r    (q * S d)                             }= 
                             ((S  d +  r) + (q * S d))
      ={ cong {f=\m =>             m      + (q * S d)} (plusCommutative (S d) r)  }= 
                             ((r +   S d) + (q * S d))
      ={ sym $ plusAssociative r    (S d)   (q * S d)                             }= 
                              (r +  (S d  + (q * S d)))
      QED