Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
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
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))
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.