Primes.agda

module Primes where

open import Level using (_⊔_)
open import Coinduction
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility
-- open import Data.Nat.Primality -- This is NAD's new primality predicate, which has advantages and disadvantages over mine
open import Data.Nat.InfinitelyOften
open import Data.Stream
open import Data.Vec using (Vec; []; _∷_)
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Unary hiding (_∈_)
open import Relation.Binary.PropositionalEquality

-- From https://gist.github.com/1286093
open import Prime hiding (primes)

n+0≡n : ∀ n → n + 0 ≡ n
n+0≡n zero    = refl
n+0≡n (suc n) = cong suc $ n+0≡n n

m+1+n≡1+m+n : ∀ m n → m + suc n ≡ suc (m + n)
m+1+n≡1+m+n zero    n = refl
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)


data All {p} {A : Set} (P : A → Set p) : Stream A → Set p where
  _∷_ : ∀ {x xs} (px : P x) (pxs : ∞ (All P (♭ xs))) → All P (x ∷ xs)

data Infinite {p} (P : ℕ → Set p) (x : ℕ) : Set p where
  yes : ( px :   P x) (pxs : ∞ (Infinite P (1 + x))) → Infinite P x
  no  : (¬px : ¬ P x) (pxs :    Infinite P (1 + x))  → Infinite P x

toStream : ∀ {p} {P : ℕ → Set p} {x} → Infinite P x → Stream ℕ
toStream {x = x} (yes px pxs) = x ∷ ♯ toStream (♭ pxs)
toStream (no ¬px pxs) = toStream pxs

toAll : ∀ {p} {P : ℕ → Set p} {x} (i : Infinite P x) → All P (toStream i)
toAll (yes px pxs) = px ∷ ♯ (toAll (♭ pxs))
toAll (no ¬px pxs) = toAll pxs

member : ∀ {p} {P : ℕ → Set p} m (inf : Infinite P m) → ∀ n → P (m + n) → m + n ∈ toStream inf
member m (yes px pxs) zero    pn rewrite n+0≡n m = here
member m (no ¬px pxs) zero    pn rewrite n+0≡n m = ⊥-elim (¬px pn)
member m (yes px pxs) (suc n) pn rewrite m+1+n≡1+m+n m n = there (member (suc m) (♭ pxs) n pn)
member m (no ¬px pxs) (suc n) pn rewrite m+1+n≡1+m+n m n = member (suc m) pxs n pn

Inf′ : (ℕ → Set) → Set
Inf′ P = ∀ n → ∃ λ i → P (i + n)

infinite : (P : ℕ → Set) → Decidable P → Inf′ P → ∀ n → Infinite P n
infinite P p? inf n with p? n
infinite P p? inf n | yes p = yes p (♯ infinite P p? inf (suc n))
infinite P p? inf n | no ¬p = helper _ (proj₁ (inf n)) (proj₂ (inf n))
  where
  helper : ∀ n i → P (i + n) → Infinite P n
  helper n zero pni = yes pni (♯ (infinite P p? inf _))
  helper n (suc i) pni with p? n
  helper n (suc i) pni | yes q = yes q (♯ (infinite P p? inf _))
  helper n (suc i) pni | no ¬q rewrite sym (m+1+n≡1+m+n i n) = no ¬q (helper (suc n) i pni)


diff : ∀ {m n} → m ≤′ n → ∃ λ i → i + m ≡ n
diff ≤′-refl = 0 , refl
diff (≤′-step pf) with diff pf
diff (≤′-step pf) | i , eq = suc i , cong suc eq

inf : Inf′ Prime
inf n with generate n
inf n | i  , pf , p with diff (≤⇒≤′ pf)
inf n | ._ , pf , p | j , refl rewrite m+1+n≡1+m+n j n = suc j , p

prime? : Decidable Prime
prime? zero = no λ { (prime () pf) }
prime? (suc zero) = no λ { (prime (s≤s ()) pf) }
prime? (suc (suc n)) with primality (2 + n) (s≤s (s≤s z≤n))
prime? (suc (suc n)) | inj₁ x = yes x
prime? (suc (suc n)) | inj₂ y = no (λ p → ¬Prime×Composite p y)

infinitePrimes : Infinite Prime 0
infinitePrimes = infinite Prime prime? inf 0

primes : Stream ℕ
primes = toStream infinitePrimes

allPrimes : All Prime primes
allPrimes = toAll infinitePrimes

everyPrime : ∀ n → Prime n → n ∈ primes
everyPrime = member 0 infinitePrimes