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

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)

gcd1 : ( i i0 j j0 : ℕ ) → ℕ
gcd1 zero i0 zero j0 = 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

open import nat

gcd24' : { n m : ℕ} → n > 1 → m > 1 → n - m > 0 → gcd n m ≡ gcd (n - m) m
gcd24' = {!!}

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
   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 
   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 .1 zero j0 o o0 1<i 1<j 1<o gn gm refl = nat-<≡ 1<i
   gcd21 zero i0 (suc zero) j0 zero o0 1<i 1<j 1<o refl gm gnm = nat-≡< gm 1<i
   gcd21 zero (suc i0) (suc (suc j)) j0 zero (suc o0) 1<i 1<j 1<o refl gm gnm = {!!} where
      gcd23 : gcd1 (suc j) (suc (suc j)) o0 (suc o0) ≡ suc i0 → gcd1 i0 (suc i0) (suc j) (suc (suc j)) ≡ 1 → ⊥
      gcd23 = {!!}
   gcd21 zero i0 (suc j) j0 (suc zero) o0 1<i 1<j 1<o refl gm gnm = ⊥-elim ( nat-<≡ 1<k )
   gcd21 zero i0 (suc j) j0 (suc (suc o)) o0 1<i 1<j 1<o gn gm gnm = {!!}
   gcd21 (suc i) i0 zero j0 o o0 1<i 1<j 1<o gn refl 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 ))))))

record Rational : Set where
  field
    i j : ℕ
    coprime : gcd i j ≡ 1

root2-irrational : ( n m : ℕ ) → n > 1 → m > 1  →  2 * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
root2-irrational n m n>1 m>1 2nm = gcd24 {n} {m} n>1 m>1 (s≤s (s≤s z≤n)) (even→gcd=2 rot7 (rot5 n>1)) (even→gcd=2 ( even^2 {m} ( rot1)) (rot5 m>1))where
    rot5 : {n : ℕ} → n > 1 → n > 0
    rot5 {n} lt = <-trans a<sa lt 
    rot1 : even ( m * m )
    rot1 = subst (λ k → even k ) rot4 (n*even {n * n} {2} tt ) where
       rot4 : (n * n) * 2 ≡ m * m  
       rot4 = begin
          (n * n) * 2     ≡⟨ *-comm (n * n) 2 ⟩
          2 * ( n * n )   ≡⟨ sym (*-assoc 2 n n) ⟩
          2 *  n * n      ≡⟨ 2nm ⟩
          m * m           ∎ where open ≡-Reasoning
    E : Even m
    E = e2 m ( even^2 {m} ( rot1 ))
    rot2 : 2 * n * n ≡ 2 * Even.j E * m
    rot2 = subst (λ k → 2 * n * n ≡ k * m ) (Even.is-twice E) 2nm
    rot3 : n * n ≡ Even.j E * m
    rot3 = e3 ( begin
          2 * (n * n)   ≡⟨ sym (*-assoc 2 n _) ⟩
          2 *  n * n    ≡⟨ rot2 ⟩
          2 * Even.j E * m ≡⟨  *-assoc 2 (Even.j E)  m  ⟩
          2 * (Even.j E * m)  ∎ ) where open ≡-Reasoning
    rot7 : even n  
    rot7 =  even^2 {n} (subst (λ k → even k) (sym rot3) ((n*even {Even.j E} {m} ( even^2 {m} ( rot1 )))))