Zeckendorf decomposition

parent 8d3f825a
......@@ -102,6 +102,80 @@ module SmallestFibAbove
end
module Zeckendorf
use import int.Fibonacci
use import int.Int
use import int.MinMax
use import ref.Ref
use import list.List
use import SmallestFibAbove
function sum (l: list int) : int = match l with
| Nil -> 0
| Cons k r -> fib k + sum r
end
(* sorted in increasing order, above min, and non consecutive *)
predicate wf (min: int) (l: list int) = match l with
| Nil -> true
| Cons k r -> min <= k /\ wf (k + 2) r
end
let rec lemma fib_nonneg (n: int) : unit
requires { 0 <= n }
ensures { 0 <= fib n }
variant { n }
= if n > 1 then begin fib_nonneg (n-2); fib_nonneg (n-1) end
let rec lemma fib_increasing (k1 k2: int) : unit
requires { 0 <= k1 <= k2 }
ensures { fib k1 <= fib k2 }
variant { k2 - k1 }
= if k1 < k2 then fib_increasing (k1+1) k2
let greatest_fib (x: int) : (int, int)
requires { 0 < x }
ensures { let (k, fk) = result in
2 <= k /\ 1 <= fk = fib k <= x < fib (k + 1) }
=
let a = ref 1 in
let b = ref 1 in
let k = ref 1 in
while !b <= x do
invariant { 1 <= !k /\ !a = fib !k <= x /\ !b = fib (!k + 1) }
invariant { 1 <= !a /\ 1 <= !b }
variant { 2*x - (!a + !b) }
let f = !a + !b in
a := !b;
b := f;
k := !k + 1
done;
(!k, !a)
let zeckendorf (n: int) : list int
requires { 0 <= n }
ensures { wf 2 result }
ensures { n = sum result }
=
let x = ref n in
let l = ref Nil in
while !x > 0 do
invariant { 0 <= !x <= n }
invariant { wf 2 !l }
invariant { !x + sum !l = n }
invariant { match !l with Nil -> true | Cons k _ -> !x < fib (k-1) end }
variant { !x }
let (k, fk) = greatest_fib !x in
x := !x - fk;
l := Cons k !l
done;
!l
(* TODO: a linear implementation *)
end
theory Mat22 "2x2 integer matrices"
use import int.Int
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment