Package haskell-prime: Prime numbers

Information

name	haskell-prime
version	1.29
description	Prime numbers
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
haskell-category	Number Theory
requires	base haskell natural-divides natural-prime stream
show	Data.Bool Data.List Data.Pair Data.Stream Function Haskell.Data.Stream as H Haskell.Number.Natural as H Haskell.Number.Natural.Prime.Sieve as H Number.Natural Number.Natural.Prime.Sieve Probability.Random

Files

Package tarball haskell-prime-1.29.tgz
Theory source file haskell-prime.thy (included in the package tarball)

Defined Type Operator

Haskell
- Number
  - Natural
    - Prime
      - Sieve
        H.Sieve

Defined Constants

Haskell
- Number
  - Natural
    - Prime
      - H.Prime.all
      - Sieve
        H.fromHol
        H.increment
        H.increment.inc
        H.initial
        H.next
        H.perimeter
        H.toHol
        H.unSieve
        H.Sieve

Theorems

⊦ H.Prime.all = Prime.all

⊦ H.increment.inc = increment.inc

⊦ H.initial = H.fromHol initial

⊦ H.Prime.all = H.unfold H.next H.initial

⊦ H.perimeter = mapDomain H.toHol max

⊦ H.unSieve = mapDomain H.toHol dest

⊦ H.Sieve = mapRange H.fromHol mk

⊦ ¬(H.nth H.Prime.all 0 = 0)

⊦ ∀s. H.Sieve (H.unSieve s) = s

⊦ H.initial = H.Sieve (1, [])

⊦ ∀s. H.perimeter s = fst (H.unSieve s)

⊦ H.increment = (mapRange (mapSnd H.fromHol) ∘ mapDomain H.toHol) increment

⊦ H.next = (mapRange (mapSnd H.fromHol) ∘ mapDomain H.toHol) next

⊦ (∀h. H.fromHol (H.toHol h) = h) ∧ ∀x. H.toHol (H.fromHol x) = x

⊦ ∀s.
    H.next s =
    let (b, s') ← H.increment s in
    if b then (H.perimeter s', s') else H.next s'

⊦ ∀r.
    let (i, r') ← H.Geometric.fromRandom r in
    let (j, r'') ← H.Geometric.fromRandom r' in
    H.nth H.Prime.all i ≤ H.nth H.Prime.all j ⇔ i ≤ j

⊦ ∀r.
    let (i, r') ← H.Geometric.fromRandom r in
    let (j, r'') ← H.Geometric.fromRandom r' in
    ¬H.divides (H.nth H.Prime.all i) (H.nth H.Prime.all (i + j + 1))

⊦ H.increment =
  λs.
    let (n, ps) ← H.unSieve s in
    let n' ← n + 1 in
    let (b, ps') ← H.increment.inc n' 1 ps in
    (b, H.Sieve (n', ps'))

⊦ ∀r.
    let (n, r') ← H.fromRandom r in
    let (i, r'') ← H.Geometric.fromRandom r' in
    any (λp. H.divides p (n + 2)) (H.take' H.Prime.all i) ∨
    H.nth H.Prime.all i ≤ n + 2

⊦ (∀n i. H.increment.inc n i [] = (⊤, (n, 0, 0) :: [])) ∧
  ∀n i p k j ps.
    H.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') ← H.increment.inc n j' ps in (b, (p, k', 0) :: ps')

External Type Operators

→
bool
Data
- List
  - list
- Pair
  - ×
- Stream
  - stream
Number
- Natural
  - natural
  - Prime
    - Sieve
      - sieve
Probability
- Random
  - random

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - []
  - any
- Pair
  - ,
  - fst
  - mapSnd
- Stream
  - ::
  - nth
  - take
  - unfold
Function
- id
- mapDomain
- mapRange
- ∘
Haskell
- Data
  - Stream
    - H.nth
    - H.take'
    - H.unfold
- Number
  - Natural
    - H.divides
    - H.fromRandom
    - Geometric
      - H.Geometric.fromRandom
Number
- Natural
  - +
  - ≤
  - bit0
  - bit1
  - divides
  - mod
  - suc
  - zero
  - Prime
    - Prime.all
    - Sieve
      - dest
      - increment
        increment.inc
      - initial
      - max
      - mk
      - next

Assumptions

⊦ ⊤

⊦ H.divides = divides

⊦ H.nth = nth

⊦ H.take' = take

⊦ H.unfold = unfold

⊦ unfold next initial = Prime.all

⊦ ∀x. id x = x

⊦ (∃) = λp. p ((select) p)

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

⊦ ∀t. (λx. t x) = t

⊦ (∀) = λp. p = λx. ⊤

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ⇒ ⊤ ⇔ ⊤

⊦ ∀a. mk (dest a) = a

⊦ initial = mk (1, [])

⊦ ∀s. max s = fst (dest s)

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀p x. p x ⇒ p ((select) p)

⊦ ∀x. ∃a b. x = (a, b)

⊦ ∀x y. x = y ⇔ y = x

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

⊦ ∀f g. mapDomain f g = g ∘ f

⊦ ∀f g. mapRange f g = f ∘ g

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀f g x. (f ∘ g) x = f (g x)

⊦ ∀f g. (∀x. f x = g x) ⇔ f = g

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀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

⊦ ∀f x y. mapSnd f (x, y) = (x, f y)

⊦ ∀p. (∀x y. p x y) ⇔ ∀y x. p x y

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

⊦ ∀s₁ s₂. (∀n. nth s₁ n = nth s₂ n) ⇒ s₁ = s₂

⊦ ∀f g h. f ∘ (g ∘ h) = f ∘ g ∘ h

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

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

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

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

⊦ ∀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')

⊦ ∀ps.
    ps = Prime.all ⇔
    ¬(nth ps 0 = 0) ∧ (∀i j. nth ps i ≤ nth ps j ⇔ i ≤ j) ∧
    (∀i j. ¬divides (nth ps i) (nth ps (i + (j + 1)))) ∧
    ∀n i. any (λp. divides p (n + 2)) (take ps i) ∨ nth ps i ≤ n + 2