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

import gcd as GCD
open import even
open import nat
open import logic

record Rational : Set where
  field
    i j : ℕ
    0<j : j > 0
    coprime : GCD.gcd i j ≡ 1

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

gcd : (i j : ℕ) → ℕ
gcd = GCD.gcd

gcd-euclid : ( p a b : ℕ )  → 1 < p  → 0 < a → 0 < b → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)
   →  Dividable p (a * b)  → Dividable p a ∨ Dividable p b
gcd-euclid = GCD.gcd-euclid

gcd-div1 : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j ) 
   → Dividable k ( gcd i  j ) 
gcd-div1 = GCD.gcd-div

open _∧_

open import prime

divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
divdable^2 zero zero () 1<n pk dn2
divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
... | yes y = y
... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2 
... | case1 dn = dn
... | case2 dm = dm

-- p * n * n ≡ m * m means (m/n)^2 = p
-- rational m/n requires m and n is comprime each other which contradicts the condition

root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1  →  p * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
root-prime-irrational n m 0 n>1 pn m>1 pnm = ⊥-elim ( nat-≡< refl (<-trans a<sa (Prime.p>1 pn))) 
root-prime-irrational n m (suc p0) n>1 pn m>1 pnm = rot13 ( gcd-div1 n m (suc p0) 1<sp dn dm ) where 
    p = suc p0
    1<sp : 1 < p
    1<sp = Prime.p>1 pn
    rot13 : {m : ℕ } → Dividable (suc p0) m →  m ≡ 1 → ⊥
    rot13 d refl with Dividable.factor d | Dividable.is-factor d
    ... | zero | ()   -- gcd 0 m ≡ 1
    ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * p + 0) ≡ 1 
        rot17 : suc n * (suc p0) + 0 > 1
        rot17 = begin
           2 ≡⟨ refl ⟩
           suc (1 * 1 ) ≤⟨ 1<sp  ⟩
           suc p0  ≡⟨ cong suc (+-comm 0 _) ⟩ 
           suc (p0 + 0) ≤⟨ s≤s (+-monoʳ-≤ p0 z≤n) ⟩ 
           suc (p0 + n * p )  ≡⟨ +-comm 0 _ ⟩
           suc n * p + 0 ∎   where open ≤-Reasoning
    dm : Dividable p m
    dm = divdable^2 m p 1<sp m>1 pn record { factor = n * n ; is-factor = begin
       (n * n) * p + 0 ≡⟨  +-comm _ 0 ⟩
       (n * n) * p  ≡⟨ *-comm (n * n) p ⟩
       p * (n * n)  ≡⟨ sym (*-assoc p n n)  ⟩
       (p * n) * n ≡⟨ pnm ⟩
       m * m ∎ }  where open ≡-Reasoning
     -- p * n * n = 2m' 2m'
     --  n * n = m' 2m'
    df = Dividable.factor dm
    dn : Dividable p n
    dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df  ; is-factor = begin
        df * df * p + 0  ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin 
          (df * df * p + 0) * p ≡⟨  cong (λ k → k * p)  (+-comm (df * df * p) 0)  ⟩
          ((df * df) * p  ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
            (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p)  ⟩
            (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩
            ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p  ⟩
            (df * p) * (df * p) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * p)) (+-comm 0 _) ⟩
          (df * p + 0) * (df * p + 0)   ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
          m * m   ≡⟨ sym pnm ⟩
          p * n * n     ≡⟨ cong (λ k → k * n) (*-comm p n) ⟩
          n * p * n     ≡⟨ *-assoc n p n ⟩
          n * (p * n)   ≡⟨ cong (λ k → n * k) (*-comm p n) ⟩
          n * (n * p)   ≡⟨ sym (*-assoc n n p) ⟩
          n * n * p ∎  ) ⟩
       n * n ∎ }  where open ≡-Reasoning

mkRational : ( i j : ℕ ) → 0 < j → Rational
mkRational zero j 0<j = record { i = 0 ; j = 1 ; coprime = refl  ; 0<j = s≤s z≤n } 
mkRational (suc i) j (s≤s 0<j) = record { i = Dividable.factor id ; j = Dividable.factor jd ; coprime = cop ; 0<j = 0<fj } where
   d : ℕ
   d = gcd (suc i) j
   d>0 : gcd (suc i) j > 0
   d>0 = GCD.gcd>0 (suc i) j (s≤s z≤n) (s≤s z≤n )
   0<fj : Dividable.factor jd > 0
   0<fj = 0<factor d>0  (s≤s z≤n ) jd
   id  : Dividable d (suc i)
   id  = proj1 (GCD.gcd-dividable (suc i) j)
   jd  : Dividable d j 
   jd  = proj2 (GCD.gcd-dividable (suc i) j)
   cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1
   cop with (gcd (Dividable.factor id) (Dividable.factor jd)) | inspect (gcd (Dividable.factor id)) (Dividable.factor jd)
   ... | zero | record { eq  = eq1 } = ⊥-elim ( nat-≡< (sym eq1) (GCD.gcd>0 (Dividable.factor id) (Dividable.factor jd)
       (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) ))
   ... | suc zero | record { eq  = eq1 } = refl
   ... | suc (suc t) | record { eq  = eq1 } = ⊥-elim ( nat-≤> (GCD.gcd-is-gratest {suc i} {j} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where
        -- gcd-is-gratest :  { i j  k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j
        d1 : ℕ
        d1 = gcd (Dividable.factor id) (Dividable.factor jd) 
        d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1
        d1>1 = subst (λ k → 1 < k ) (sym eq1) (s≤s (s≤s z≤n))
        mul1 :  {x : ℕ} → 1 * x ≡ x
        mul1 {zero} = refl
        mul1 {suc x} = begin
              1 * suc x  ≡⟨ cong suc (+-comm x _ ) ⟩ 
              suc x ∎   where open ≡-Reasoning
        co1  : gcd (suc i) j * d1 > 1
        co1  = begin
              2 ≤⟨ d1>1 ⟩ 
              d1  ≡⟨ sym mul1 ⟩ 
              1 * d1  ≤⟨ *≤ {1} {gcd (suc i) j } {d1} d>0 ⟩ 
              gcd (suc i) j * d1 ∎   where open ≤-Reasoning
        gcdd1 = GCD.gcd-dividable (Dividable.factor id) (Dividable.factor jd)
        gcdf1 = Dividable.factor (proj1 gcdd1)
        gcdf2 = Dividable.factor (proj2 gcdd1)
        d1id :  Dividable (gcd (suc i) j * d1) (suc i)
        d1id = record { factor = gcdf1 ; is-factor = begin
              gcdf1 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ 
              gcdf1 * (d * d1) ≡⟨ cong (λ k1 → gcdf1 * k1) (*-comm d d1) ⟩ 
              gcdf1 * (d1 * d) ≡⟨ sym (*-assoc gcdf1 d1 d) ⟩ 
              gcdf1 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ 
              (gcdf1 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf1 * d1) 0)) ⟩ 
              (gcdf1 * d1 + 0  ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj1 gcdd1) ) ⟩ 
              Dividable.factor id * d + 0 ≡⟨ Dividable.is-factor id ⟩ 
              suc i ∎ }  where open ≡-Reasoning
        d1jd :  Dividable (gcd (suc i) j * d1) j
        d1jd = record { factor = gcdf2 ; is-factor = begin
              gcdf2 * (d * d1) + 0 ≡⟨ +-comm _ 0 ⟩ 
              gcdf2 * (d * d1) ≡⟨ cong (λ k1 → gcdf2 * k1) (*-comm d d1) ⟩ 
              gcdf2 * (d1 * d) ≡⟨ sym (*-assoc gcdf2 d1 d) ⟩ 
              gcdf2 * d1 * d ≡⟨ sym ( +-comm _ 0) ⟩ 
              (gcdf2 * d1) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) (sym (+-comm (gcdf2 * d1) 0)) ⟩ 
              (gcdf2 * d1 + 0  ) * d + 0 ≡⟨ cong (λ k1 → k1 * d + 0 ) ( Dividable.is-factor (proj2 gcdd1) ) ⟩ 
              Dividable.factor jd * d + 0 ≡⟨ Dividable.is-factor jd ⟩ 
              j ∎ }  where open ≡-Reasoning
        mul2 : {g d1 : ℕ } → g > 0 → d1 > 1 → g < g * d1
        mul2 {suc g} {suc zero} g>0 (s≤s ())
        mul2 {suc g} {suc (suc d2)} g>0 d1>1 = begin
              suc (suc g) ≡⟨ cong suc (+-comm 0 _ ) ⟩ 
              suc (suc g + 0) ≤⟨ s≤s (≤-plus-0  z≤n) ⟩ 
              suc (suc g + (g + d2 * suc g)) ≡⟨ cong suc (sym (+-assoc  1 g _) ) ⟩ 
              suc ((1 + g) + (g + d2 * suc g)) ≡⟨  cong (λ k → suc (k + (g + d2 * suc g) )) (+-comm 1 g) ⟩ 
              suc ((g + 1) + (g + d2 * suc g)) ≡⟨ cong suc (+-assoc g 1 _ )  ⟩ 
              suc (g + (1 + (g + d2 * suc g))) ≡⟨⟩ 
              suc (g + suc (g + d2 * suc g)) ≡⟨⟩ 
              suc (suc d2) * suc g  ≡⟨ *-comm (suc (suc d2)) _ ⟩ 
              suc g * suc (suc d2) ∎   where open ≤-Reasoning
        gcd<d1 : gcd (suc i) j < gcd (suc i ) j * d1
        gcd<d1 = mul2 (GCD.gcd>0 (suc i) j (s≤s z≤n) (s≤s z≤n) ) d1>1 


Rational* : (r s : Rational) → Rational
Rational* r s = mkRational (Rational.i r * Rational.i s) (Rational.j r * Rational.j s) (r1 (Rational.0<j r) (Rational.0<j s) ) where
    r1 : {x y : ℕ} → x > 0 → y > 0 → x * y > 0
    r1 {x} {y} x>0 y>0 = begin
        1 * 1 ≤⟨ *≤ {1} {x} {1} x>0 ⟩
        x * 1 ≡⟨ *-comm x 1  ⟩
        1 * x ≤⟨ *≤ {1} {y} {x} y>0 ⟩
        y * x ≡⟨ *-comm y x ⟩
        x * y ∎ where open ≤-Reasoning

_r=_ : Rational → ℕ → Set
r r= n  = (Rational.i r ≡ n) ∧ (Rational.j r ≡ 1)

root-prime-irrational1 : ( p : ℕ ) → Prime p → ( r  : Rational ) → ¬ ( Rational* r r r= p )
root-prime-irrational1 p pr r div = root-prime-irrational (Rational.i r) (Rational.j r) {!!} {!!} pr {!!} {!!} (Rational.coprime r)