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
      isPrime : ( j : ℕ ) → j < i → gcd i j ≡ 1

open ≡-Reasoning

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

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 } ) -- 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) ; dividable = record { factor = {!!} ; is-factor = {!!} } }

prime-is-infinite : (max-prime : ℕ ) → ¬ ( (j : ℕ) → max-prime < j → ¬ Prime j ) 
prime-is-infinite zero pmax = pmax 1 {!!} record { isPrime = λ n lt → {!!} }
prime-is-infinite (suc m) pmax = pmax (suc (factorial (suc m))) f>m record { isPrime = λ n lt → fact n lt } where
  factorial : (n : ℕ) → ℕ
  factorial zero = 1
  factorial (suc n) = (suc n) * (factorial n)
  f>m :  suc m < suc (factorial (suc m))
  f>m = {!!}
  factm : (n m : ℕ ) → n < (suc m) →  Dividable n (factorial m )
  factm = {!!}
  fact : (n : ℕ ) → n < (suc (factorial (suc m))) →   gcd (suc (factorial (suc m))) n ≡ 1
  fact n lt = begin
     gcd (suc (factorial (suc m))) n ≡⟨ cong (λ k → gcd k n) (Dividable.is-factor {!!}) ⟩
     gcd ( (NonPrime.factor d * n + 0) + 1)  n   ≡⟨ cong (λ k → gcd ( k + 1 ) n ) (+-comm (NonPrime.factor d * n) 0) ⟩
     gcd ( NonPrime.factor d * n + 1)  n   ≡⟨  gcdmul+1 (NonPrime.factor d)  n  ⟩
     1 ∎  where
       d :  NonPrime (factorial (suc m ))
       d with <-cmp n (suc m)
       ... | tri< a ¬b ¬c = record { factor = {!!} ; dividable = factm n (suc m) {!!} } 
       ... | tri≈ ¬a b ¬c = record { factor = {!!} ; dividable = factm n (suc m) {!!} } 
       ... | tri> ¬a ¬b c = nonPrime {!!} {!!}