{-# OPTIONS --allow-unsolved-metas #-}
module gcd where

open import Data.Nat 
open import Data.Nat.Properties
open import Data.Empty
open import Data.Unit using (⊤ ; tt)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions
open import nat
open import logic

record Factor (n m : ℕ ) : Set where
   field 
      factor : ℕ
      remain : ℕ
      is-factor : factor * n + remain ≡ m

record Dividable (n m : ℕ ) : Set where
   field 
      factor : ℕ
      f>0 : factor > 0
      is-factor : factor * n + 0 ≡ m 

open Factor

DtoF : {n m : ℕ} → Dividable n m → Factor n m
DtoF {n} {m} record { factor = f ; f>0 = f>0 ; is-factor = fa } = record { factor = f ; remain = 0 ; is-factor = fa }

FtoD : {n m : ℕ} → (fc : Factor n m) → factor fc > 0 → remain fc ≡ 0 → Dividable n m 
FtoD {n} {m} record { factor = f ; remain = r ; is-factor = fa } f>0 refl = record { factor = f ; f>0 = f>0  ; is-factor = fa }

decf : { n k : ℕ } → ( x : Factor k (suc n) ) → Factor k n
decf {n} {k} record { factor = f ; remain = r ; is-factor = fa } = 
 decf1 {n} {k} f r fa where
  dr : ( n k : ℕ ) → (f r : ℕ) → ℕ
  dr n zero (suc f) zero = 0
  dr n (suc k) (suc f) zero = k
  dr n k f (suc r) = r
  dr n zero zero zero = r
  dr n (suc k) zero zero = r
  decf1 : { n k : ℕ } → (f r : ℕ) → (f * k + r ≡ suc n)  → Factor k n 
  decf1 {n} {k} f (suc r) fa  =  -- this case must be the first
     record { factor = f ; remain = r ; is-factor = ( begin -- fa : f * k + suc r ≡ suc n
        f * k + r ≡⟨ cong pred ( begin
          suc ( f * k + r ) ≡⟨ +-comm _ r ⟩
          r + suc (f * k)  ≡⟨ sym (+-assoc r 1 _) ⟩
          (r + 1) + f * k ≡⟨ cong (λ t → t + f * k ) (+-comm r 1) ⟩
          (suc r ) + f * k ≡⟨ +-comm (suc r) _ ⟩
          f * k + suc r  ≡⟨ fa ⟩
          suc n ∎ ) ⟩ 
        n ∎ ) }  where open ≡-Reasoning
  decf1 {n} {zero} (suc f) zero fa  = ⊥-elim ( nat-≡< fa (
        begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero)  ⟩
        suc (f * 0) ≡⟨ cong suc (*-comm f zero)  ⟩
        suc zero ≤⟨ s≤s z≤n ⟩
        suc n ∎ )) where open ≤-Reasoning
  decf1 {n} {suc k} (suc f) zero fa  = 
     record { factor = f ; remain = k ; is-factor = ( begin -- fa : suc (k + f * suc k + zero) ≡ suc n
        f * suc k + k ≡⟨ +-comm _ k ⟩
        k + f * suc k ≡⟨ +-comm zero _ ⟩
        (k + f * suc k) + zero  ≡⟨ cong pred fa ⟩
        n ∎ ) }  where open ≡-Reasoning

decf-step : {i k i0 : ℕ } → k > 1 → (if : Factor k (suc i)) → (i0f : Factor k i0)
     → Dividable k (suc i - remain if)  → Dividable k (i - remain (decf {i} {k} if))
decf-step {i} {suc k} {i0} k>1 if i0f div = decf-step1 {i} {suc k} {i0} (factor if) (remain if) (is-factor if) {!!} i0f div where
   if0 : suc (suc i) > remain if
   if0 = begin
        suc (remain if) ≤⟨ s≤s (m≤n+m _ (factor if * suc k)) ⟩
        suc (factor if * suc k + remain if) ≡⟨ cong suc ( is-factor if) ⟩
        suc (suc i) ∎  where open ≤-Reasoning
   if1 : factor if ≡ Dividable.factor div
   if1 = begin
        factor if  ≡⟨ *-cancelʳ-≡ _ _ {k} ( +-cancelʳ-≡ _ _ ( begin
        factor if * suc k + remain if ≡⟨ is-factor if ⟩
        suc i ≡⟨ sym (minus+n {suc i} {remain if} if0) ⟩
        (suc i - remain if) + remain if ≡⟨ cong (λ g → g + remain if) (sym (Dividable.is-factor div )) ⟩
        (Dividable.factor div * suc k + 0) + remain if  ≡⟨ cong (λ g → g + remain if) (+-comm _ 0) ⟩
        Dividable.factor div * suc k + remain if ∎  )) ⟩ Dividable.factor div ∎   where open ≡-Reasoning
   decf-step1 : {i k i0 : ℕ } →  (f r : ℕ) → (fa : f * k + r ≡ suc i) → f > 0  →  (i0f : Factor k i0)
        → Dividable k (suc i - r)  → Dividable k (i - remain (decf record {factor = f ; remain = r ; is-factor = fa}))
   decf-step1 {i} {k} {i0}  f (suc r) fa f>0 i0f div = 
      record { factor = f ;  f>0 = f>0 ; is-factor = ( --  f * k + suc r ≡ suc i → f * k + suc r ≡ suc i
        begin f * k + 0 ≡⟨ +-comm _ 0 ⟩
        f * k ≡⟨ sym ( x=y+z→x-z=y {suc i} {_} {suc r} (sym fa) ) ⟩
        suc i - suc r ≡⟨ refl ⟩
        i - r ≡⟨ refl ⟩
         (i - remain (decf (record { factor = f ; remain = suc r ; is-factor = fa }))) ∎ ) }  where
            open ≡-Reasoning
   decf-step1 {i} {zero} {i0} (suc f) zero fa f>0 i0f div = ⊥-elim (nat-≡< fa (
        begin suc (suc f * zero + zero) ≡⟨ cong suc (+-comm _ zero)  ⟩
        suc (f * 0) ≡⟨ cong suc (*-comm f zero)  ⟩
        suc zero ≤⟨ s≤s z≤n ⟩
        suc i ∎ )) where open ≤-Reasoning  -- suc (0 + i) ≡ i0
   decf-step1 {i} {suc k} {i0} (suc f)  zero fa f>0 i0f div = 
      record { factor = f ;  f>0 = {!!} ; is-factor = ( --  suc (k + f * suc k + zero) ≡ suc i →  f * suc k + 0 ≡ i - k 
        begin f * suc k + 0 ≡⟨ sym ( x=y+z→x-z=y {i} {_} {k} (begin
          i ≡⟨ sym (cong pred fa) ⟩
          pred (suc f * suc k + zero) ≡⟨ refl ⟩
          pred ((suc k + f * suc k) + zero) ≡⟨ cong pred ( +-assoc (suc k) _ zero) ⟩
          pred (suc k + (f * suc k + zero))  ≡⟨ refl ⟩
          k + (f * suc k + 0) ≡⟨ +-comm k _ ⟩
          f * suc k + 0 + k ∎ ))  ⟩ 
        i - k ∎ ) }  where open ≡-Reasoning

ifk0 : (  i0 k : ℕ ) → (i0f : Factor k i0 )  → ( i0=0 : remain i0f ≡ 0 )  → factor i0f * k + 0 ≡ i0
ifk0 i0 k i0f i0=0 = begin
   factor i0f * k + 0  ≡⟨ cong (λ m → factor i0f * k + m) (sym i0=0)  ⟩
   factor i0f * k + remain i0f  ≡⟨ is-factor i0f ⟩
   i0 ∎ 
         where open ≡-Reasoning

ifzero : {k : ℕ } → (jf :  Factor k zero ) →  remain jf ≡ 0
ifzero {k} record { factor = zero ; remain = zero ; is-factor = is-factor } = refl
ifzero {zero} record { factor = (suc factor₁) ; remain = zero ; is-factor = is-factor } = refl
ifzero {zero} record { factor = (suc f) ; remain = (suc r) ; is-factor = is-factor } =
      ⊥-elim (nat-≡< (sym is-factor) (subst (λ k → zero < k ) (+-comm (suc r)  _) if1 )) where
   if1 : zero < suc r + suc f * zero 
   if1 = s≤s z≤n

gcd1 : ( i i0 j j0 : ℕ ) → ℕ
gcd1 zero i0 zero j0 with <-cmp i0 j0
... | tri< a ¬b ¬c = i0
... | tri≈ ¬a refl ¬c = i0
... | tri> ¬a ¬b c = j0
gcd1 zero i0 (suc zero) j0 = 1
gcd1 zero zero (suc (suc j)) j0 = j0
gcd1 zero (suc i0) (suc (suc j)) j0 = gcd1 i0 (suc i0) (suc j) (suc (suc j))
gcd1 (suc zero) i0 zero j0 = 1
gcd1 (suc (suc i)) i0 zero zero = i0
gcd1 (suc (suc i)) i0 zero (suc j0) = gcd1 (suc i) (suc (suc i))  j0 (suc j0)
gcd1 (suc i) i0 (suc j) j0 = gcd1 i i0 j j0  

gcd : ( i j : ℕ ) → ℕ
gcd i j = gcd1 i i j j 

nfk : {k : ℕ } → k > 1 → ¬ (Dividable k 0)
nfk {k} k>1 fk1 = ⊥-elim ( nat-≡< (sym (Dividable.is-factor fk1)) ( begin 
        1 <⟨ k>1 ⟩
        k ≡⟨ +-comm 0 _ ⟩
        k + 0 * k ≡⟨ refl ⟩
        1 * k ≤⟨ *≤ (Dividable.f>0 fk1 ) ⟩
        Dividable.factor fk1 * k ≡⟨ sym (+-comm _ 0) ⟩
        Dividable.factor fk1 * k + 0 ∎  )) where open ≤-Reasoning

gcd-gt : ( i i0 j j0 k : ℕ ) → k > 1 → (if : Factor k i) (i0f : Dividable k i0 ) (jf : Factor k j ) (j0f : Dividable k j0)
   → Dividable k (i - remain if) → Dividable k (j - remain jf) 
   → Dividable k ( gcd1 i i0 j j0 ) 
gcd-gt zero i0 zero j0 k k>1 if i0f jf j0f ir=i0 jr=j0 with <-cmp i0 j0
... | tri< a ¬b ¬c = i0f 
... | tri≈ ¬a refl ¬c = i0f
... | tri> ¬a ¬b c = j0f
gcd-gt zero i0 (suc zero) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 =
     ⊥-elim ( nfk k>1 (subst (λ g → Dividable k g ) (minus<=0 {zero} {remain if} z≤n) ir=i0)) -- can't happen
gcd-gt zero zero (suc (suc j)) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = j0f
gcd-gt zero (suc i0) (suc (suc j)) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 =   
    gcd-gt i0 (suc i0) (suc j) (suc (suc j))  k k>1 (decf (DtoF i0f)) i0f (decf jf) (FtoD jf {!!} {!!}) {!!} (decf-step k>1 jf {!!} jr=j0 )
gcd-gt (suc zero) i0 zero j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = 
     ⊥-elim ( nfk k>1 (subst (λ g → Dividable k g ) (minus<=0 {zero} {remain jf} z≤n) jr=j0)) -- can't happen
gcd-gt (suc (suc i)) i0 zero zero k k>1 if i0f jf j0f ir=i0 jr=j0 = i0f
gcd-gt (suc (suc i)) i0 zero (suc j0) k k>1 if i0f jf j0f ir=i0 jr=j0 =
     gcd-gt (suc i) (suc (suc i)) j0 (suc j0) k k>1 (decf if) {!!} (decf (DtoF j0f)) j0f (decf-step k>1 if jf ir=i0 ) {!!}
gcd-gt (suc zero) i0 (suc j) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 =  
     gcd-gt zero i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step k>1 if jf ir=i0 ) (decf-step k>1 jf if jr=j0 )
gcd-gt (suc (suc i)) i0 (suc j) j0 k k>1 if i0f jf j0f ir=i0 jr=j0 = 
     gcd-gt (suc i) i0 j j0 k k>1 (decf if) i0f (decf jf) j0f (decf-step k>1 if jf ir=i0 ) (decf-step k>1 jf if jr=j0 )

gcd-div : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j ) 
   → Dividable k ( gcd i  j ) 
gcd-div i j k k>1 if jf = gcd-gt i i j j k k>1 (DtoF if) if (DtoF jf) jf {!!} {!!} 


-- gcd26 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
-- gcd27 : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n k ≡ k → k ≤ n

gcd22 : ( i i0 o o0 : ℕ ) → gcd1 (suc i) i0 (suc o) o0 ≡ gcd1 i i0 o o0
gcd22 zero i0 zero o0 = refl
gcd22 zero i0 (suc o) o0 = refl
gcd22 (suc i) i0 zero o0 = refl
gcd22 (suc i) i0 (suc o) o0 = refl 

gcd20 : (i : ℕ) → gcd i 0 ≡ i
gcd20 zero = refl
gcd20 (suc i) = gcd201 (suc i) where
    gcd201 : (i : ℕ ) → gcd1 i i zero zero ≡ i
    gcd201 zero = refl
    gcd201 (suc zero) = refl
    gcd201 (suc (suc i)) = refl

gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m
gcdmm zero m with <-cmp m m
... | tri< a ¬b ¬c = refl
... | tri≈ ¬a refl ¬c = refl
... | tri> ¬a ¬b c = refl
gcdmm (suc n) m  = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m )

gcdsym2 : (i j : ℕ) → gcd1 zero i zero j ≡ gcd1 zero j zero i
gcdsym2 i j with <-cmp i j | <-cmp j i
... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ⊥-elim (nat-<> a a₁) 
... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl
... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) 
... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) 
... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl
... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) 
... | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = ⊥-elim (nat-<> c c₁) 
gcdsym1 : ( i i0 j j0 : ℕ ) → gcd1 i i0 j j0 ≡ gcd1 j j0 i i0
gcdsym1 zero zero zero zero = refl
gcdsym1 zero zero zero (suc j0) = refl
gcdsym1 zero (suc i0) zero zero = refl
gcdsym1 zero (suc i0) zero (suc j0) = gcdsym2 (suc i0) (suc j0)
gcdsym1 zero zero (suc zero) j0 = refl
gcdsym1 zero zero (suc (suc j)) j0 = refl
gcdsym1 zero (suc i0) (suc zero) j0 = refl
gcdsym1 zero (suc i0) (suc (suc j)) j0 = gcdsym1 i0 (suc i0) (suc j) (suc (suc j))
gcdsym1 (suc zero) i0 zero j0 = refl
gcdsym1 (suc (suc i)) i0 zero zero = refl
gcdsym1 (suc (suc i)) i0 zero (suc j0) = gcdsym1 (suc i) (suc (suc i))j0 (suc j0) 
gcdsym1 (suc i) i0 (suc j) j0 = subst₂ (λ j k → j ≡ k ) (sym (gcd22 i _ _ _)) (sym (gcd22 j _ _ _)) (gcdsym1 i i0 j j0 )

gcdsym : { n m : ℕ} → gcd n m ≡ gcd m n
gcdsym {n} {m} = gcdsym1 n n m m 

gcd11 : ( i  : ℕ ) → gcd i i ≡ i
gcd11 i = gcdmm i i 

gcd203 : (i : ℕ) → gcd1 (suc i) (suc i) i i ≡ 1
gcd203 zero = refl
gcd203 (suc i) = gcd205 (suc i) where
   gcd205 : (j : ℕ) → gcd1 (suc j) (suc (suc i)) j (suc i) ≡ 1
   gcd205 zero = refl
   gcd205 (suc j) = subst (λ k → k ≡ 1) (gcd22 (suc j)  (suc (suc i)) j (suc i)) (gcd205 j)
gcd204 : (i : ℕ) → gcd1 1 1 i i ≡ 1
gcd204 zero = refl
gcd204 (suc zero) = refl
gcd204 (suc (suc zero)) = refl
gcd204 (suc (suc (suc i))) = gcd204 (suc (suc i)) 

gcd2 : ( i j : ℕ ) → gcd (i + j) j ≡ gcd i j
gcd2 i j = gcd200 i i j j refl refl where
       gcd202 : (i j1 : ℕ) → (i + suc j1) ≡ suc (i + j1)
       gcd202 zero j1 = refl
       gcd202 (suc i) j1 = cong suc (gcd202 i j1)
       gcd201 : (i i0 j j0 j1 : ℕ) → gcd1 (i + j1) (i0 + suc j) j1 j0 ≡ gcd1 i (i0 + suc j) zero j0
       gcd201 i i0 j j0 zero = subst (λ k → gcd1 k (i0 + suc j) zero j0 ≡ gcd1 i (i0 + suc j) zero j0 ) (+-comm zero i) refl
       gcd201 i i0 j j0 (suc j1) = begin
          gcd1 (i + suc j1)   (i0 + suc j) (suc j1) j0 ≡⟨ cong (λ k → gcd1 k (i0 + suc j) (suc j1) j0 ) (gcd202 i j1) ⟩
          gcd1 (suc (i + j1)) (i0 + suc j) (suc j1) j0 ≡⟨ gcd22 (i + j1) (i0 + suc j) j1 j0 ⟩
          gcd1 (i + j1) (i0 + suc j) j1 j0 ≡⟨ gcd201 i i0 j j0 j1 ⟩
          gcd1 i (i0 + suc j) zero j0 ∎ where open ≡-Reasoning
       gcd200 : (i i0 j j0 : ℕ) → i ≡ i0 → j ≡ j0 → gcd1 (i + j) (i0 + j) j j0 ≡ gcd1 i i j0 j0
       gcd200 i .i zero .0 refl refl = subst (λ k → gcd1 k k zero zero ≡ gcd1 i i zero zero ) (+-comm zero i) refl 
       gcd200 (suc (suc i)) i0 (suc j) (suc j0) i=i0 j=j0 = gcd201 (suc (suc i)) i0 j (suc j0) (suc j)
       gcd200 zero zero (suc zero) .1 i=i0 refl = refl
       gcd200 zero zero (suc (suc j)) .(suc (suc j)) i=i0 refl = begin
          gcd1 (zero + suc (suc j)) (zero + suc (suc j)) (suc (suc j)) (suc (suc j)) ≡⟨ gcdmm (suc (suc j)) (suc (suc j)) ⟩
          suc (suc j) ≡⟨ sym (gcd20 (suc (suc j))) ⟩
          gcd1 zero zero (suc (suc j)) (suc (suc j)) ∎ where open ≡-Reasoning
       gcd200 zero (suc i0) (suc j) .(suc j) () refl
       gcd200 (suc zero) .1 (suc j) .(suc j) refl refl = begin
          gcd1 (1 + suc j) (1 + suc j) (suc j) (suc j) ≡⟨ gcd203 (suc j) ⟩
          1 ≡⟨ sym ( gcd204 (suc j)) ⟩
          gcd1 1 1 (suc j) (suc j) ∎ where open ≡-Reasoning
       gcd200 (suc (suc i)) i0 (suc j) zero i=i0 ()

gcd52 : {i : ℕ } → 1 < suc (suc i)
gcd52 {zero} = a<sa
gcd52 {suc i} = <-trans (gcd52 {i}) a<sa

gcd50 : (i i0 j j0 : ℕ) → 1 < i0 → i ≤ i0 → j ≤ j0 →  gcd1 i i0 j j0 ≤ i0 
gcd50 zero i0 zero j0 0<i i<i0 j<j0 with <-cmp i0 j0
... | tri< a ¬b ¬c = ≤-refl    
... | tri≈ ¬a refl ¬c =  ≤-refl 
... | tri> ¬a ¬b c = ≤-trans refl-≤s c  
gcd50 zero (suc i0) (suc zero) j0 0<i i<i0 j<j0 = gcd51 0<i where 
   gcd51 : 1 < suc i0 → gcd1 zero (suc i0) 1 j0 ≤ suc i0
   gcd51 1<i = <to≤ 1<i
gcd50 zero (suc i0) (suc (suc j)) j0 0<i i<i0 j<j0 = gcd50 i0 (suc i0) (suc j) (suc (suc j)) 0<i refl-≤s refl-≤s
gcd50 (suc zero) i0 zero j0 0<i i<i0 j<j0 = <to≤ 0<i
gcd50 (suc (suc i)) i0 zero zero 0<i i<i0 j<j0 = ≤-refl
gcd50 (suc (suc i)) i0 zero (suc j0) 0<i i<i0 j<j0 = ≤-trans (gcd50 (suc i) (suc (suc i))  j0 (suc j0) gcd52  refl-≤s refl-≤s) i<i0
gcd50 (suc i) i0 (suc j) j0 0<i i<i0 j<j0 = subst (λ k → k ≤ i0 ) (sym (gcd22 i i0 j j0))
   (gcd50 i i0 j j0 0<i (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0)) 

gcd5 : ( n k : ℕ ) → 1 < n → gcd n k ≤ n
gcd5 n k 0<n = gcd50 n n k k 0<n ≤-refl ≤-refl 

gcd6 : ( n k : ℕ ) → 1 < n → gcd k n ≤ n
gcd6 n k 1<n = subst (λ m → m ≤ n) (gcdsym {n} {k}) (gcd5 n k 1<n)

gcd4 : ( n k : ℕ ) → 1 < n  → gcd n k ≡ k → k ≤ n
gcd4 n k 1<n eq = subst (λ m → m ≤ n ) eq (gcd5 n k 1<n)

gcdmul+1 : ( m n : ℕ ) → gcd (m * n + 1) n ≡ 1
gcdmul+1 zero n = gcd204 n
gcdmul+1 (suc m) n = begin
      gcd (suc m * n + 1) n ≡⟨⟩
      gcd (n + m * n + 1) n ≡⟨ cong (λ k → gcd k n ) (begin
         n + m * n + 1 ≡⟨ cong (λ k → k + 1) (+-comm n _) ⟩
         m * n + n + 1 ≡⟨ +-assoc (m * n) _ _ ⟩
         m * n + (n + 1)  ≡⟨ cong (λ k → m * n + k) (+-comm n _) ⟩
         m * n + (1 + n)  ≡⟨ sym ( +-assoc (m * n) _ _ ) ⟩
         m * n + 1 + n ∎ 
       ) ⟩
      gcd (m * n + 1 + n) n ≡⟨ gcd2 (m * n + 1) n ⟩
      gcd (m * n + 1) n ≡⟨ gcdmul+1 m n ⟩
      1 ∎ where open ≡-Reasoning