{-# 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

even : (n : ℕ ) → Set
even zero = ⊤
even (suc zero) = ⊥
even (suc (suc n)) = even n

even? : (n : ℕ ) → Dec ( even n )
even? zero = yes tt
even? (suc zero) = no (λ ())
even? (suc (suc n)) = even? n

n+even : {n m : ℕ } → even n → even m  → even ( n + m )
n+even {zero} {zero} tt tt = tt
n+even {zero} {suc m} tt em = em
n+even {suc (suc n)} {m} en em = n+even {n} {m} en em

n*even : {m n : ℕ } → even n → even ( m * n )
n*even {zero} {n} en = tt
n*even {suc m} {n} en = n+even {n} {m * n} en (n*even {m} {n} en) 

even*n : {n m : ℕ } → even n → even ( n * m )
even*n {n} {m} en = subst even (*-comm m n) (n*even {m} {n} en)

gcd2 : ( i i0 j j0 : ℕ ) → i ≤ i0 → j ≤ j0 → i0 < j0  → ℕ
gcd2 zero i0 zero j0 i<i0 j<j0 i<j = j0
gcd2 zero i0 (suc zero) j0 i<i0 j<j0 i<j = 1
gcd2 zero zero (suc (suc j)) j0 i<i0 j<j0 i<j = j0
-- i<i0 : zero ≤ suc i0
-- j<j0 : suc (suc j) ≤ j0
-- i<j  : suc i0 < j0
gcd2 zero (suc i0) (suc (suc j)) j0 i<i0 j<j0 i<j with <-cmp (suc (suc j)) (suc i0)  -- non terminating
... | tri< a ¬b ¬c = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s {!!}
... | tri≈ ¬a refl ¬c = suc i0
... | tri> ¬a ¬b c = gcd2 i0 (suc i0) (suc j) (suc (suc j)) refl-≤s refl-≤s {!!}
-- = gcd2  (suc j) (suc (suc j))  i0 (suc i0) refl-≤s refl-≤s {!!} -- suc (suc j) < suc i0
gcd2 (suc zero) i0 zero j0 i<i0 j<j0 i<j = 1
gcd2 (suc (suc i)) i0 zero zero i<i0 j<j0 i<j = i0
gcd2 (suc (suc i)) i0 zero (suc j0) i<i0 j<j0 i<j  = gcd2 (suc i) (suc (suc i))  j0 (suc j0)   refl-≤s refl-≤s {!!} --  suc (suc i) < suc j0
gcd2 (suc i) i0 (suc j) j0 i<i0 j<j0 i<j = gcd2 i i0 j j0 (≤-trans refl-≤s i<i0) (≤-trans refl-≤s j<j0) i<j  

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

even→gcd=2 : {n : ℕ} → even n → n > 0 → gcd n 2 ≡ 2
even→gcd=2 {suc (suc zero)} en (s≤s z≤n) = refl
even→gcd=2 {suc (suc (suc (suc n)))} en (s≤s z≤n) = begin
       gcd (suc (suc (suc (suc n)))) 2
    ≡⟨⟩
       gcd (suc (suc n)) 2
    ≡⟨ even→gcd=2 {suc (suc n)} en (s≤s z≤n) ⟩
       2
    ∎ where open ≡-Reasoning

-- 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 

-- gcd27 : ( i i0 : ℕ ) → gcd1 i i0 0 1 ≤ 1
-- gcd27 zero zero = ≤-refl
-- gcd27 zero (suc i0) = {!!}
-- gcd27 (suc i) zero = {!!}
-- gcd27 (suc i) (suc i0) = {!!}

gcd-kk : ( i : ℕ ) → gcd1 i i i i ≡ i
gcd-kk zero = refl
gcd-kk (suc i) = gcd-kk1 i i i i refl refl where
   gcd-kk1 : (i i0 j j0 : ℕ) → i ≡ j → i0 ≡ j0 →  gcd1 (suc i) (suc i0) (suc j) (suc j0) ≡ suc i0
   gcd-kk1 zero i0 zero j0 i=j i0=j0 with <-cmp (suc i0) (suc j0)
   ... | tri< a ¬b ¬c = ⊥-elim (¬b (cong suc i0=j0))
   ... | tri≈ ¬a refl ¬c = refl
   ... | tri> ¬a ¬b c = ⊥-elim (¬b (cong suc i0=j0))
   gcd-kk1 (suc i) i0 (suc j) j0 refl i0=j0 = 
        gcd-kk1 i i0 j j0 refl i0=j0 

gcd26 : (n m i : ℕ) → 1 < n → 1 < m  → gcd n i ≡ m → ¬ ( gcd n m ≡ 1 )
gcd26 n m i 1<n 1<m gi g1 = gcd261 n n m m i i 1<n 1<m gi g1 where
    gcd261 : (n n0 m m0 i i0 : ℕ) → 1 < n → 1 < m0  → gcd1 n n0 i i0 ≡ m0 → ¬ ( gcd1 n n0 m m0 ≡ 1 )
    gcd261 zero n0 m m0 i i0 () 1<m gi g1
    -- gi       : gcd1 (suc n) n0 zero i0 ≡ m0
    -- g1       : gcd1 (suc n) n0 m m0 ≡ 1
    gcd261 (suc n) n0 m m0 zero i0 1<n 1<m gi g1 = {!!}
    -- gi       : gcd1 (suc n) n0 (suc i) i0 ≡ m0
    -- g1       : gcd1 (suc n) n0 zero m0 ≡ 1
    gcd261 (suc n) n0 zero m0 (suc i) i0 1<n 1<m gi g1 = {!!}
    gcd261 (suc zero) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = ⊥-elim ( nat-<≡ 1<n  )
    gcd261 (suc (suc zero)) n0 (suc m) m0 (suc zero) i0 1<n 1<m gi g1 = ⊥-elim (  nat-≡< gi 1<m )
    -- gi       : gcd1 0 n0 i i0 ≡ m0
    gcd261 (suc (suc zero)) n0 (suc zero) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}
    -- gi       : gcd1 0 n0 i i0 ≡ m0
    -- g1       : gcd1 0 n0 m m0 ≡ 1
    gcd261 (suc (suc zero)) n0 (suc (suc m)) m0 (suc (suc i)) i0 1<n 1<m gi g1 = {!!}
    gcd261 (suc (suc (suc n))) n0 (suc m) m0 (suc i) i0 1<n 1<m gi g1 = 
        gcd261 (suc (suc n)) n0 m m0 i i0 (s≤s (s≤s z≤n)) 1<m gi g1

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 

gcd24 : { n m k : ℕ} → n > 1 → m > 1 → k > 1 → gcd n k ≡ k → gcd m k ≡ k → ¬ ( gcd n m ≡ 1 )
gcd24 {n} {m} {k} 1<n 1<m 1<k gn gm gnm = gcd21 n n m m k k 1<n 1<m 1<k gn gm gnm where
   gcd23 : {i0 j0 : ℕ } → 1 < i0  → 1 < j0 → 1 < gcd1 zero i0 zero j0
   gcd23 {i0} {j0} 1<i 1<j with <-cmp i0 j0
   ... | tri< a ¬b ¬c = 1<j
   ... | tri≈ ¬a refl ¬c = 1<i
   ... | tri> ¬a ¬b c = 1<i
   1<ss : {j : ℕ} → 1 < suc (suc j)
   1<ss = s≤s (s≤s z≤n)
   gcd21 : ( i i0 j j0 o o0 : ℕ ) → 1 < i0 → 1 < j0 → 1 < o0 →  gcd1 i i0 o o0 ≡ k → gcd1 j j0 o o0 ≡ k → gcd1 i i0 j j0 ≡ 1 → ⊥
   gcd21 zero i0 zero j0 o o0 1<i 1<j 1<o refl gm gnm = nat-≡< (sym gnm) (gcd23 1<i 1<j)
   gcd21 zero i0 (suc j) j0 zero o0 1<i 1<j 1<o refl gm gnm = gcd25 i0 o0 j j0 1<o 1<i 1<k gm (subst (λ k → k ≡ 1) (gcdsym1 zero _ (suc j) _) gnm)  where
      -- gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ suc (suc i0) , gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡ 1
      gcd25 : (i0 o0 j j0 : ℕ) → 1 < o0 → 1 < i0
            → 1 < gcd1 zero i0 zero o0 
            → ( gm : gcd1 (suc j) j0 zero o0 ≡ gcd1 zero i0 zero o0 ) → (gnm : gcd1 (suc j) j0 zero i0 ≡ 1) → ⊥
      gcd25 i0 o0 zero j0 1<o 1<i 1<k gm refl with <-cmp i0 o0
      ... | tri< a ¬b ¬c    = ⊥-elim ( nat-≡< gm 1<o )
      ... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< gm 1<o )
      ... | tri> ¬a ¬b c    = ⊥-elim ( nat-≡< gm 1<i )
      -- gm       : gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡ (gcd1 zero (suc i0) zero (suc (suc o0))
      --            gcd1 j       (suc (suc j))       o0 (suc (suc o0)) 
      -- gnm      : gcd1 (suc j) (suc (suc j)) i0 (suc i0) ≡ 1
      gcd25 i0       (suc zero)     (suc j) j0 1<o 1<i 1<k gm gnm = {!!} -- ⊥-elim ( nat-≤> (subst (λ k → k ≤ 1 ) gm (gcd27 (suc j) (suc (suc j)))) 1<k )
      gcd25 (suc zero) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm = {!!}
      --     (suc (suc i0)) > (suc (suc o0)) → gm = gnm → (suc (suc i0)) ≡ 1
      --     (suc (suc i0)) < (suc (suc o0)) → ? gcd1 (suc j) (suc (suc j)) (suc o0) (suc (suc o0)) ≡  (suc (suc o0)) 
      --                                         gcd1 (suc j) (suc (suc j)) (suc i0) (suc (suc i0)) ≡  1
      gcd25 (suc (suc i0)) (suc (suc o0)) (suc j) j0 1<o 1<i 1<k gm gnm with <-cmp  (suc (suc i0))   (suc (suc o0))
      ... | tri< a ¬b ¬c = {!!}
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b c = gcd26 {!!} {!!} {!!} {!!} {!!} {!!} {!!}
   gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = nat-<≡ 1<k
   gcd21 zero (suc i0) (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm = 
       gcd21 i0 {!!} (suc j) j0 (suc o) (suc (suc o)) 1<i 1<j {!!} gn {!!} {!!}
   gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn gm gnm = {!!}
   gcd21 (suc i) i0 (suc j) j0 zero o0 1<i 1<j 1<o gn gm gnm = {!!}
   gcd21 (suc i) i0 (suc j) j0 (suc o) o0 1<i 1<j 1<o gn gm gnm = 
       gcd21 i i0 j j0 o o0 1<i 1<j 1<o (subst (λ m → m ≡ k) (gcd22 i i0 _ _ ) gn)
                                        (subst (λ m → m ≡ k) (gcd22 j j0 _ _ ) gm) (subst (λ k → k ≡ 1) (gcd22 i i0 _ _ ) gnm)

record Even (i : ℕ) : Set where
  field
     j : ℕ
     is-twice : i ≡ 2 * j

e2 : (i : ℕ) → even i → Even i
e2 zero en = record { j = 0 ; is-twice = refl }
e2 (suc (suc i)) en = record { j = suc (Even.j (e2 i en )) ; is-twice = e21 } where
   e21 : suc (suc i) ≡ 2 * suc (Even.j (e2 i en))
   e21 = begin
    suc (suc i)  ≡⟨ cong (λ k → suc (suc k)) (Even.is-twice (e2 i en))  ⟩
    suc (suc (2 * Even.j (e2 i en)))  ≡⟨ sym (*-distribˡ-+ 2 1 _) ⟩
    2 * suc (Even.j (e2 i en))      ∎ where open ≡-Reasoning

record Odd (i : ℕ) : Set where
  field
     j : ℕ
     is-twice : i ≡ suc (2 * j )

odd2 : (i : ℕ) → ¬ even i → even (suc i) 
odd2 zero ne = ⊥-elim ( ne tt )
odd2 (suc zero) ne = tt
odd2 (suc (suc i)) ne = odd2 i ne 

odd3 : (i : ℕ) → ¬ even i →  Odd i
odd3 zero ne = ⊥-elim ( ne tt )
odd3 (suc zero) ne = record { j = 0 ; is-twice = refl }
odd3 (suc (suc i))  ne = record { j = Even.j (e2 (suc i) (odd2 i ne)) ; is-twice = odd31 } where
  odd31 : suc (suc i) ≡ suc (2 * Even.j (e2 (suc i) (odd2 i ne)))
  odd31 = begin
    suc (suc i) ≡⟨  cong suc (Even.is-twice (e2 (suc i) (odd2 i ne)))  ⟩
    suc (2 * (Even.j (e2 (suc i) (odd2 i ne))))      ∎ where open ≡-Reasoning

odd4 : (i : ℕ) → even i → ¬ even ( suc i )
odd4 (suc (suc i)) en en1 = odd4 i en en1 

even^2 : {n : ℕ} → even ( n * n ) → even n
even^2 {n} en with even? n
... | yes y = y
... | no ne = ⊥-elim ( odd4 ((2 * m) + 2 * m * suc (2 * m)) (n+even {2 * m} {2 * m * suc (2 * m)} ee3 ee4) (subst (λ k → even k) ee2 en )) where
    m : ℕ
    m = Odd.j ( odd3 n ne )
    ee3 : even (2 * m)
    ee3 = subst (λ k → even k ) (*-comm m 2) (n*even {m} {2} tt )
    ee4 : even ((2 * m) * suc (2 * m))
    ee4 = even*n {(2 * m)} {suc (2 * m)} (even*n {2} {m} tt )
    ee2 : n * n ≡ suc (2 * m) + ((2 * m) * (suc (2 * m) ))
    ee2 = begin n * n ≡⟨ cong ( λ k → k * k) (Odd.is-twice (odd3 n ne)) ⟩
       suc (2 * m) * suc (2 * m) ≡⟨ *-distribʳ-+ (suc (2 * m)) 1 ((2 * m) ) ⟩
        (1 * suc (2 * m)) + 2 * m * suc (2 * m) ≡⟨ cong (λ k → k + 2 * m * suc (2 * m)) (begin
        suc m + 1 * m + 0 * (suc m + 1 * m ) ≡⟨ +-comm (suc m + 1 * m) 0 ⟩
        suc m + 1 * m  ≡⟨⟩
        suc (2 * m)  
        ∎) ⟩ suc (2 * m)  + 2 * m * suc (2 * m) ∎ where open ≡-Reasoning

open import nat

e3 : {i j : ℕ } → 2 * i ≡ 2 * j →  i ≡ j
e3 {zero} {zero} refl = refl
e3 {suc x} {suc y} eq with <-cmp x y
... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (s≤s (<-trans (<-plus a) (<-plus-0 (s≤s (<-plus a ))))))
... | tri≈ ¬a b ¬c = cong suc b
... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-trans (<-plus c) (<-plus-0 (s≤s (<-plus c ))))))