Package natural-fibonacci: Fibonacci numbers

Information

namenatural-fibonacci
version1.74
descriptionFibonacci numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
hol-light-int-filehol-light.int
hol-light-thm-filehol-light.art
haskell-nameopentheory-fibonacci
haskell-categoryNumber Theory
haskell-int-filehaskell.int
haskell-src-filehaskell.art
haskell-test-filehaskell-test.art
checksume9054391815ed790ea31afd03812f456012ff426
requiresbase
probability
stream
showData.Bool
Data.List
Data.Pair
Data.Stream
Function
Number.Natural
Number.Natural.Fibonacci
Probability.Random
Relation

Files

Defined Constants

Theorems

zeckendorf []

all = fromFunction fibonacci

fibonacci 0 = 0

decode [] = 0

encode 0 = []

n. zeckendorf (encode n)

decode = decode.dest 1 0

fibonacci 1 = 1

n. decode (encode n) = n

n. k. n fibonacci k

fibonacci 2 = 1

n. nth all n = fibonacci n

encode = λn. encode.find n 1 0

n. null (encode n) n = 0

f p. decode.dest f p [] = 0

n. encode n = encode.find n 1 0

k. fibonacci k = 0 k = 0

l. zeckendorf l encode (decode l) = l

l. decode l = decode.dest 1 0 l

h t. zeckendorf (h :: t) zeckendorf t

j k. j k fibonacci j fibonacci k

j k. fibonacci j < fibonacci k j < k

k. fibonacci (suc (suc k)) = fibonacci (suc k) + fibonacci k

j. ¬(j = 1) fibonacci j < fibonacci (suc j)

r. random r = random.dest 0 1 0 r - 1

n. k. fibonacci k n n < fibonacci (k + 1)

n. fibonacci (n + 2) = fibonacci (n + 1) + fibonacci n

l. ¬null l zeckendorf l fibonacci (length l + 1) decode l

l1 l2. zeckendorf (l1 @ l2) decode l1 < fibonacci (length l1 + 2)

l1 l2. zeckendorf l1 zeckendorf l2 decode l1 = decode l2 l1 = l2

h t.
    zeckendorf (h :: t)
    if null t then h else ¬(h head t) zeckendorf t

l1 l2.
    zeckendorf l1 zeckendorf l2 length l1 < length l2
    decode l1 < decode l2

f r.
    Fibonacci.random f r =
    let (r1, r2) split r in random f (random r1) r2

all = unfold (λ(p, f). (p, f, p + f)) (0, 1)

j k. ¬(j = 1 k = 2) j < k fibonacci j < fibonacci k

j k. ¬(j = 2 k = 1) fibonacci j fibonacci k j k

(zeckendorf [] )
  h t.
    zeckendorf (h :: t)
    if null t then h else ¬(h head t) zeckendorf t

n f p.
    encode.find n f p =
    let s f + p in
    if n < s then encode.mk [] n f p else encode.find n s f

f p h t.
    decode.dest f p (h :: t) =
    let s f + p in let n decode.dest s f t in if h then s + n else n

j k.
    fibonacci (j + (k + 1)) =
    fibonacci j * fibonacci k + fibonacci (j + 1) * fibonacci (k + 1)

p. p 0 p 1 (n. p n p (n + 1) p (n + 2)) n. p n

j k.
    nth all (j + (k + 1)) =
    nth all j * nth all k + nth all (j + 1) * nth all (k + 1)

(f p. decode.dest f p [] = 0)
  f p h t.
    decode.dest f p (h :: t) =
    let s f + p in let n decode.dest s f t in if h then s + n else n

l n f p.
    encode.mk l n f p =
    if p = 0 then l
    else if f n then encode.mk ( :: l) (n - f) p (f - p)
    else encode.mk ( :: l) n p (f - p)

h.
    (f g n. (m. m + 1 = n m + 2 = n f m = g m) h f n = h g n)
    f. n. f n = h f n

b n f p r.
    random.dest b n f p r =
    let (r1, r2) split r in
    let b' bit r1 in
    if b' b then n
    else let s f + p in random.dest b' (if b' then s + n else n) s f r2

External Type Operators

External Constants

Assumptions

null []

wellFounded (<)

¬

¬

length [] = 0

bit0 0 = 0

t. t t

n. 0 n

n. n n

p. p

t. t ¬t

m. ¬(m < 0)

n. n < suc n

n. n suc n

(¬) = λp. p

() = λ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 ) 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. nth (fromFunction f) = f

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. 1 * m = m

l. null l l = []

s. head s = nth s 0

h t. ¬null (h :: t)

m n. m m + n

m n. n m + n

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

m. m 0 m = 0

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

h t. head (h :: t) = h

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

n. 0 < n ¬(n = 0)

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

s. nth s 1 = head (tail s)

f y. (let x y in f x) = f y

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

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

m n. m + n = n + m

m n. m + n - m = n

m n. m + n - n = m

h t. length (h :: t) = suc (length t)

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

m. m = 0 n. m = suc n

p. (b. p b) p p

f b. head (unfold f b) = fst (f b)

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

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

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

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

h t. (h :: []) @ t = h :: t

t1 t2. ¬t1 ¬t2 t2 t1

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

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

m n. m < m + n 0 < n

m n. n < m + n 0 < m

m n. suc m = suc n m = n

m n. suc m < suc n m < n

m n. suc m suc n m n

s n. nth s (suc n) = nth (tail s) n

r s. subrelation r s wellFounded s wellFounded r

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

l1 l2. length (l1 @ l2) = length l1 + length l2

f b. tail (unfold f b) = unfold f (snd (f b))

p. (x. p x) a b. p (a, b)

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. n m m - n + n = m

m n. m n n m m = n

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

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

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

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

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

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

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

p q r. p q r p q r

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

p m n. m + p = n + p m = n

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

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

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

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

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

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

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

m n p. m n n p m p

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

l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3

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

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

m n. m + n = 0 m = 0 n = 0

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

r s. subrelation r s x y. r x y s x y

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

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

b f x y. f (if b then x else y) = if b then f x else f y

p. (n. (m. m < n p m) p n) n. p 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

p. (n. p n) p ((minimal) p) m. m < (minimal) p ¬p m

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

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)

f b n k. nth (unfold f b) (n + k) = nth (unfold f (((snd f) n) b)) k

r.
    wellFounded r
    h.
      (f g x. (z. r z x f z = g z) h f x = h g x)
      f. x. f x = h f x