module prime 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 gcd
open import nat

record Prime (i : ℕ ) : Set where
   field
      p>0 : i > 1
      isPrime : ( j : ℕ ) → j < i → gcd i j ≡ 1


record NonPrime ( n : ℕ ) : Set where
   field
      factor : ℕ
      prime : Prime factor
      dividable : Dividable factor n

PrimeP : ( n : ℕ ) → Dec ( Prime n )
PrimeP 0 = no (λ p → ⊥-elim ( nat-<> (Prime.p>0 p) (s≤s z≤n))) 
PrimeP 1 = no (λ p → ⊥-elim ( nat-≤> (Prime.p>0 p) (s≤s (≤-refl))))
PrimeP (suc n) = isPrime1 (suc n) n a<sa (λ i m<i i<n → {!!} ) where
   isPrime1 : ( n m : ℕ ) → m < n → ( (i : ℕ) → m ≤ i → i < n  →  gcd n i ≡ 1 )  → Dec ( Prime n )
   isPrime1 n zero m<n lt = yes record { isPrime = λ j j<i → lt j z≤n {!!} ; p>0 = {!!} }
   isPrime1 n (suc m) m<n lt with <-cmp (gcd n (suc m)) 1
   ... | tri< a ¬b ¬c = {!!}
   ... | tri≈ ¬a b ¬c = isPrime1 n m {!!} {!!}
   ... | tri> ¬a ¬b c = no ( λ p → nat-≡< (sym (Prime.isPrime p (suc m) {!!} )) c )

nonPrime : { n : ℕ } → ¬ Prime n → NonPrime n
nonPrime {n} np = np1 n (λ j n≤j j<n → ⊥-elim (nat-≤>  n≤j j<n ) ) where
    np1 : ( m : ℕ ) → ( (j : ℕ ) → m ≤ j → j < n → gcd n j ≡ 1  ) → NonPrime n
    np1 zero mg = ⊥-elim ( np record { isPrime = λ j lt → mg j z≤n lt ; p>0 = {!!} } ) -- zero < j , j < n
    np1 (suc m) mg with <-cmp ( gcd n (suc m) ) 1
    ... | tri< a ¬b ¬c = {!!}
    ... | tri≈ ¬a b ¬c = np1 m {!!}
    ... | tri> ¬a ¬b c = record { factor = gcd n (suc m) ; prime = {!!} ;  dividable = record { factor = {!!} ; is-factor = {!!} } }


prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
prime-is-infinite zero pmax = pmax 3 (s≤s z≤n) record { isPrime = λ n lt → {!!} ; p>0 = {!!} }
prime-is-infinite (suc m) pmax = getPrime where 
  factorial : (n : ℕ) → ℕ
  factorial zero = 1
  factorial (suc n) = (suc n) * (factorial n)
  prime<max : (n : ℕ ) → Prime n → n < suc (suc m)
  prime<max n p with <-cmp n (suc m) 
  ... | tri< a ¬b ¬c = ≤-trans a refl-≤s 
  ... | tri≈ ¬a refl ¬c = ≤-refl 
  ... | tri> ¬a ¬b c = ⊥-elim ( pmax n c p ) 
  factorial-mono : (n : ℕ) → factorial n ≤ factorial (suc n)
  factorial-mono n = begin
     factorial n  ≤⟨ x≤x+y ⟩
     factorial n + n * factorial n ≡⟨ refl ⟩
     (suc n) * factorial n  ≡⟨ refl ⟩
     factorial (suc n)  ∎  where open ≤-Reasoning
  factorial≥1 : {m : ℕ} → 1 ≤ factorial m
  factorial≥1 {zero} = ≤-refl
  factorial≥1 {suc m} = begin
     1 ≤⟨ s≤s z≤n ⟩
     (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
     (suc m) * factorial m ≡⟨ refl ⟩
     factorial (suc m)  ∎  where open ≤-Reasoning
  factorial⟩m : (m : ℕ) → m ≤ factorial m
  factorial⟩m zero = z≤n
  factorial⟩m (suc m) = begin
     suc m ≡⟨ cong suc (+-comm 0 _) ⟩
     1 * suc m ≡⟨ *-comm 1 _ ⟩
     (suc m) * 1 ≤⟨  *-monoʳ-≤ (suc m) (factorial≥1 {m}) ⟩
     (suc m) * factorial m  ≡⟨ refl ⟩
     factorial (suc m)  ∎  where open ≤-Reasoning
  -- *-monoˡ-≤ (suc m) {!!}
  f>m :  suc m < suc (factorial (suc m))
  f>m = begin
     suc (suc m)  ≡⟨ cong (λ k → 1 + suc k ) (+-comm _ m) ⟩
     suc (1 + 1 * m)  ≡⟨ cong (λ k → suc (1 + k )) (*-comm 1 m)  ⟩
     suc (1 + m * 1)  ≤⟨ s≤s (s≤s (*-monoʳ-≤ m  (factorial≥1 {m}) )) ⟩
     suc (1 + m * factorial m) ≤⟨ s≤s  (+-monoˡ-≤ _ (factorial≥1 {m})) ⟩
     suc (factorial m + m * factorial m)  ≡⟨ refl ⟩
     suc (factorial (suc m)) ∎  where open ≤-Reasoning
  fact< : (n : ℕ) → 0 < n → n < suc (suc m) → Dividable n ( factorial (suc m) )
  fact< n 0<n n<m = record { factor = F.f1 (fact1 m ) n 0<n n<m ; is-factor = last } where
     record F (m : ℕ) : Set where
        field
          f1 : (n : ℕ ) → 0 < n →  n < suc (suc m ) → ℕ
          is-f1 : (n : ℕ) (0<n : 0 < n ) →  (n<m : n < suc (suc m )) → f1 n 0<n n<m * n ≡ factorial (suc m)
     init0 : (n : ℕ) → 0 < n → n < 2 → 1 * n ≡ factorial 1
     init0 (suc zero) (s≤s lt) (s≤s (s≤s z≤n)) = refl
     init : F 0
     init = record { f1 = λ n lt lt1 → 1 ; is-f1 = λ n 0<n lt → init0 n 0<n lt } where
     fact1 : (j : ℕ ) → F j
     fact1 zero = init
     fact1 (suc m) = record { f1 = fact2 ; is-f1 = fact3 }  where
        fact2 : (n : ℕ ) →  0 < n →  n < suc (suc (suc m )) → ℕ
        fact2 (suc zero) 0<n n<m = factorial (suc (suc m))
        fact2 (suc (suc n)) (s≤s 0<n) n<m  with <-cmp (suc n) (suc m)
        ... | tri< a ¬b ¬c = F.f1 (fact1 m) (suc n) (s≤s z≤n) (≤-trans a refl-≤s) -- suc (suc n) ≤ suc m → suc n < suc (suc m)
        ... | tri≈ ¬a refl ¬c = F.f1 (fact1 m) (suc m) (s≤s z≤n) a<sa * suc m
        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s c) n<m ) -- suc (suc m) ≤ suc n
        fact3 : (n : ℕ ) (0<n : 0 < n) (n<m : n < suc (suc (suc m))) → fact2 n 0<n n<m * n ≡ factorial (suc (suc m))
        fact3 n 0<n n<m with  fact2 n 0<n n<m | inspect (fact2 n 0<n ) n<m  
        fact3 (suc zero) 0<n n<m     | t | record { eq = refl } = m*1=m
        fact3 (suc (suc n))  0<n n<m | t | record { eq = eq1 }  with <-cmp (suc n) (suc m)
        ... | tri< a ¬b ¬c = {!!}
        ... | tri≈ ¬a refl ¬c = begin
            t * suc (suc m) ≡⟨ cong ( λ k → k * suc (suc m)) (sym eq1) ⟩
            fact2 (suc (suc n)) 0<n n<m * suc (suc n) ≡⟨ {!!} ⟩
            suc (suc m) * (F.f1 (fact1 m) (suc m) (s≤s z≤n) a<sa * suc m) ≡⟨ cong ( λ k → suc (suc m) * k ) (F.is-f1 (fact1 m) (suc n) (s≤s z≤n) a<sa) ⟩
            suc (suc m) * factorial (suc m) ≡⟨ refl ⟩
            factorial (suc (suc m)) ∎  where open ≡-Reasoning
        ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s c) n<m ) -- suc (suc m) ≤ suc n
     last :  F.f1 (fact1 m) n 0<n n<m * n + 0 ≡ factorial (suc m)
     last = begin
         F.f1 (fact1 m ) n 0<n n<m * n + 0 ≡⟨ +-comm _ 0 ⟩
         F.f1 (fact1 m ) n 0<n n<m * n ≡⟨  F.is-f1 (fact1 m) n 0<n n<m ⟩
         factorial (suc m) ∎  where open ≡-Reasoning
  fact : (n : ℕ) → Prime n → Dividable n ( factorial (suc m) )
  fact n p = fact< n (<-trans (s≤s z≤n) (Prime.p>0 p)) ( prime<max n p )
  -- div+1 : { i k : ℕ } → k > 1 →  Dividable k i →  ¬ Dividable k (suc i)
  getPrime : ⊥
  getPrime with PrimeP ( suc (factorial (suc m)) )
  ... | yes p = pmax _ f>m p 
  ... | no np = div+1 (Prime.p>0 (NonPrime.prime p1)) (fact (NonPrime.factor p1) (NonPrime.prime p1) ) (NonPrime.dividable p1) where
      p1 : NonPrime  ( suc (factorial (suc m)) )
      p1 = nonPrime  np