Package natural-prime-sieve: The sieve of Eratosthenes

Information

namenatural-prime-sieve
version1.23
descriptionThe sieve of Eratosthenes
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
requiresbool
function
list
natural
natural-divides
natural-prime-stream
pair
relation
stream
showData.Bool
Data.List
Data.Pair
Data.Stream
Function
Number.Natural
Number.Natural.Prime.Sieve

Files

Defined Type Operator

Defined Constants

Theorems

max initial = 1

unfold next initial = Prime.all

a. mk (dest a) = a

n i. invariant.inv n i []

initial = mk (1, [])

s. max s = fst (dest s)

s. primes s = map fst (snd (dest s))

r. invariant r dest (mk r) = r

s. primes s = Prime.below (max s + 1)

n i. increment.inc n i [] = (, (n, 0, 0) :: [])

s.
    next s =
    let (b, s') increment s in if b then (max s', s') else next s'

s b s'.
    increment s = (b, s') max s' = max s + 1 (b prime (max s'))

n ps.
    invariant (n, ps)
    ¬(n = 0) map fst ps = Prime.below (n + 1) invariant.inv n 0 ps

n i p k j ps.
    invariant.inv n i ((p, k, j) :: ps)
    ¬(p = 0) (k + i) mod p = n mod p invariant.inv n (i + j) ps

s.
    increment s =
    let (n, ps) dest s in
    let n' n + 1 in
    let (b, ps') increment.inc n' 1 ps in
    (b, mk (n', ps'))

n i p k j ps.
    increment.inc n i ((p, k, j) :: ps) =
    let k' (k + i) mod p in
    let j' j + i in
    if k' = 0 then (, (p, 0, j') :: ps)
    else let (b, ps') increment.inc n j' ps in (b, (p, k', 0) :: ps')

External Type Operators

External Constants

Assumptions

¬

¬

bit0 0 = 0

t. t t

n. 0 n

n. n n

p. all p []

p. p

t. t ¬t

n. 0 < suc n

n. n < suc n

(¬) = λp. p

() = λp. p ((select) p)

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

Prime.below 2 = []

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t t

t. t t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

n. ¬(suc n = 0)

n. 0 * n = 0

n. 0 + n = n

m. m + 0 = m

l. [] @ l = l

l. l @ [] = l

f. map f [] = []

nth Prime.all 0 = 2

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. 1 * m = m

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

x. (fst x, snd x) = x

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

a b. fst (a, b) = a

a b. snd (a, b) = b

p x. p x p ((select) p)

n. bit0 (suc n) = suc (suc (bit0 n))

x. a b. x = (a, b)

x y. x = y y = x

h t. nth (h :: t) 0 = h

t1 t2. t1 t2 t2 t1

m n. m + n = n + m

m n. m < n m n

Prime.below 3 = 2 :: []

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. m < suc n m n

p. prime p i. nth Prime.all i = p

() = λp q. (λf. f p q) = λf. f

n. ¬(n = 0) 0 mod n = 0

n. ¬(n = 0) n mod n = 0

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. suc m = suc n m = n

m n. suc m < suc n m < n

f g x. (f g) x = f (g x)

t1 t2. ¬(t1 t2) ¬t1 ¬t2

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. m n d. n = m + d

f g. (x. f x = g x) f = g

() = λp q. r. (p r) (q r) r

m n. m n n m m = n

i j. nth Prime.all i < nth Prime.all j i < j

f. fn. a b. fn (a, b) = f a b

h t n. nth (h :: t) (suc n) = nth t n

m n. m < n d. n = m + suc d

p. (x y. p x y) y x. p x y

p q. p (x. q x) x. p q x

x y z. x = y y = z x = z

p q r. p q r p q r

t1 t2 t3. (t1 t2) t3 t1 t2 t3

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p. m + (n + p) = m + n + p

m n p. m + n < m + p n < p

n. Prime.below (suc n) = Prime.below n @ if prime n then n :: [] else []

l h t. (h :: t) @ l = h :: t @ l

s1 s2. (n. nth s1 n = nth s2 n) s1 = s2

p f l. all p (map f l) all (p f) l

r. (x. y. r x y) f. x. r x (f x)

f h t. map f (h :: t) = f h :: map f t

p h t. all p (h :: t) p h all p t

p. p 0 (n. p n p (suc n)) n. p n

a b. ¬(a = 0) (divides a b b mod a = 0)

n m. ¬(n = 0) m mod n mod n = m mod n

p g h. f. x. f x = if p x then f (g x) else h x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x) (x. q x) x. p x q x

p. p [] (h t. p t p (h :: t)) l. p l

h1 h2 t1 t2. h1 :: t1 = h2 :: t2 h1 = h2 t1 = t2

a b a' b'. (a, b) = (a', b') a = a' b = b'

p c x y. p (if c then x else y) (c p x) (¬c p y)

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)

m n q r. m = q * n + r r < n m div n = q

m n q r. m = q * n + r r < n m mod n = r

n.
    prime n ¬(n = 0) ¬(n = 1) all (λp. ¬divides p n) (Prime.below n)

f b. unfold f b = let (a, b') f b in a :: unfold f b'

n a b. ¬(n = 0) (a mod n + b mod n) mod n = (a + b) mod n

n a b. ¬(n = 0) (suc a mod n = suc b mod n a mod n = b mod n)