fibonacci.mlw 7.43 KB
 MARCHE Claude committed Apr 07, 2011 1 `````` `````` Jean-Christophe Filliâtre committed Apr 11, 2011 2 3 ``````theory FibonacciTest `````` Jean-Christophe Filliâtre committed Feb 18, 2014 4 `````` use import int.Fibonacci `````` Jean-Christophe Filliâtre committed Apr 11, 2011 5 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 6 `````` lemma isfib_2_1 : fib 2 = 1 `````` Jean-Christophe Filliâtre committed Apr 11, 2011 7 8 9 `````` lemma isfib_6_8 : fib 6 = 8 lemma not_isfib_2_2 : fib 2 <> 2 `````` MARCHE Claude committed Apr 07, 2011 10 11 12 13 14 `````` end module FibonacciLinear `````` Jean-Christophe Filliâtre committed Feb 18, 2014 15 `````` use import int.Fibonacci `````` MARCHE Claude committed Apr 07, 2011 16 `````` use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 17 `````` use import ref.Ref `````` MARCHE Claude committed Apr 07, 2011 18 `````` `````` Andrei Paskevich committed Oct 13, 2012 19 20 21 22 `````` let fib (n:int) : int requires { n >= 0 } ensures { fib n = result} = let y = ref 0 in `````` MARCHE Claude committed Apr 07, 2011 23 `````` let x = ref 1 in `````` Jean-Christophe Filliâtre committed Apr 11, 2011 24 `````` for i = 0 to n - 1 do `````` Andrei Paskevich committed Jun 29, 2011 25 `````` invariant { 0 <= i <= n /\ fib (i+1) = !x /\ fib i = !y } `````` MARCHE Claude committed Apr 07, 2011 26 `````` let aux = !y in `````` Jean-Christophe Filliâtre committed May 20, 2011 27 `````` y := !x; `````` MARCHE Claude committed Apr 07, 2011 28 29 30 31 32 `````` x := !x + aux done; !y end `````` Jean-Christophe Filliâtre committed Apr 08, 2011 33 `````` `````` Jean-Christophe Filliâtre committed Sep 12, 2013 34 35 ``````module FibRecGhost "recursive version, using ghost code" `````` Jean-Christophe Filliâtre committed Feb 18, 2014 36 `````` use import int.Fibonacci `````` Jean-Christophe Filliâtre committed Sep 12, 2013 37 38 39 `````` use import int.Int let rec fib_aux (ghost n: int) (a b k: int) : int `````` MARCHE Claude committed Jan 21, 2014 40 `````` requires { k >= 0 } `````` Jean-Christophe Filliâtre committed Sep 12, 2013 41 `````` requires { 0 <= n && a = fib n && b = fib (n+1) } `````` MARCHE Claude committed Jan 21, 2014 42 `````` variant { k } `````` Jean-Christophe Filliâtre committed Sep 12, 2013 43 44 45 46 47 48 49 50 `````` ensures { result = fib (n+k) } = if k = 0 then a else fib_aux (n+1) b (a+b) (k-1) let fib (n: int) : int requires { 0 <= n } ensures { result = fib n } = fib_aux 0 0 1 n `````` MARCHE Claude committed Jan 16, 2014 51 52 53 54 55 56 57 `````` let test42 () = fib 42 exception BenchFailure let bench () raises { BenchFailure -> true } = if test42 () <> 267914296 then raise BenchFailure `````` Jean-Christophe Filliâtre committed Sep 12, 2013 58 59 60 61 ``````end module FibRecNoGhost "recursive version, without ghost code" `````` Jean-Christophe Filliâtre committed Feb 18, 2014 62 `````` use import int.Fibonacci `````` Jean-Christophe Filliâtre committed Sep 12, 2013 63 64 65 `````` use import int.Int let rec fib_aux (a b k: int) : int `````` MARCHE Claude committed Jan 21, 2014 66 `````` requires { k >= 0 } `````` Jean-Christophe Filliâtre committed Sep 12, 2013 67 `````` requires { exists n: int. 0 <= n && a = fib n && b = fib (n+1) } `````` MARCHE Claude committed Jan 21, 2014 68 `````` variant { k } `````` Jean-Christophe Filliâtre committed Sep 12, 2013 69 70 71 72 73 74 75 76 77 78 79 `````` ensures { forall n: int. 0 <= n && a = fib n && b = fib (n+1) -> result = fib (n+k) } = if k = 0 then a else fib_aux b (a+b) (k-1) let fib (n: int) : int requires { 0 <= n } ensures { result = fib n } = fib_aux 0 1 n end `````` Jean-Christophe Filliâtre committed Jun 03, 2014 80 81 82 83 84 85 86 87 88 ``````module SmallestFibAbove use import int.Fibonacci use import int.Int use import int.MinMax use import ref.Ref let smallest_fib_above (x: int) : int requires { 0 <= x } `````` Martin Clochard committed Jun 03, 2014 89 `````` ensures { exists k: int. 0 <= k /\ fib k <= x < fib (k+1) = result } `````` Jean-Christophe Filliâtre committed Jun 03, 2014 90 91 92 93 94 `````` = let a = ref 0 in let b = ref 1 in while !b <= x do invariant { exists k: int. 0 <= k /\ !a = fib k <= x /\ !b = fib (k+1) } `````` Jean-Christophe Filliâtre committed Jun 05, 2014 95 `````` invariant { 0 <= !a /\ 1 <= !b } `````` Jean-Christophe Filliâtre committed Jun 03, 2014 96 97 98 99 100 101 102 103 104 `````` variant { 2*x - (!a + !b) } let f = !a + !b in a := !b; b := f done; !b end `````` Jean-Christophe Filliâtre committed Jun 06, 2014 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 ``````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 `````` Jean-Christophe Filliâtre committed Jun 06, 2014 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 `````` (* a more efficient, linear implementation *) let zeckendorf_fast (n: int) : list int requires { 0 <= n } ensures { wf 2 result } ensures { n = sum result } = if n = 0 then Nil else let a = ref 1 in let b = ref 1 in let k = ref 1 in while !b <= n do invariant { 1 <= !k /\ !a = fib !k <= n /\ !b = fib (!k + 1) } invariant { 1 <= !a /\ 1 <= !b } variant { 2*n - (!a + !b) } let f = !a + !b in a := !b; b := f; k := !k + 1 done; assert { 2 <= !k /\ 1 <= !a = fib !k <= n < fib (!k + 1) = !b }; let l = ref (Cons !k Nil) in let x = ref (n - !a) in while !x > 0 do invariant { 1 <= !k /\ !a = fib !k <= n /\ !x < !b = fib (!k + 1) } invariant { 1 <= !a /\ 1 <= !b } 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 { !k } if !a <= !x then begin x := !x - !a; l := Cons !k !l end; k := !k - 1; let tmp = !b - !a in b := !a; a := tmp done; !l `````` Jean-Christophe Filliâtre committed Jun 06, 2014 216 217 218 `````` end `````` Jean-Christophe Filliâtre committed Apr 08, 2011 219 220 221 222 ``````theory Mat22 "2x2 integer matrices" use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 223 `````` type t = { a11: int; a12: int; a21: int; a22: int } `````` Jean-Christophe Filliâtre committed Apr 08, 2011 224 `````` `````` Andrei Paskevich committed Oct 13, 2012 225 `````` constant id : t = { a11 = 1; a12 = 0; a21 = 0; a22 = 1 } `````` Jean-Christophe Filliâtre committed Apr 08, 2011 226 `````` `````` Andrei Paskevich committed Jun 29, 2011 227 `````` function mult (x: t) (y: t) : t = `````` Andrei Paskevich committed Oct 13, 2012 228 `````` { `````` Jean-Christophe Filliâtre committed Apr 08, 2011 229 `````` a11 = x.a11 * y.a11 + x.a12 * y.a21; a12 = x.a11 * y.a12 + x.a12 * y.a22; `````` Jean-Christophe Filliâtre committed Apr 11, 2011 230 `````` a21 = x.a21 * y.a11 + x.a22 * y.a21; a22 = x.a21 * y.a12 + x.a22 * y.a22; `````` Andrei Paskevich committed Oct 13, 2012 231 `````` } `````` Jean-Christophe Filliâtre committed Apr 08, 2011 232 `````` `````` Jean-Christophe Filliâtre committed Apr 11, 2011 233 `````` (* holds, but not useful *) `````` Andrei Paskevich committed Jun 29, 2011 234 `````` (* clone algebra.Assoc with type t = t, function op = mult, lemma Assoc *) `````` Jean-Christophe Filliâtre committed Apr 08, 2011 235 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 236 `````` clone export `````` Andrei Paskevich committed Jun 29, 2011 237 `````` int.Exponentiation with type t = t, function one = id, function (*) = mult `````` Jean-Christophe Filliâtre committed Apr 08, 2011 238 239 240 241 242 `````` end module FibonacciLogarithmic `````` Jean-Christophe Filliâtre committed Feb 18, 2014 243 `````` use import int.Fibonacci `````` Jean-Christophe Filliâtre committed Apr 08, 2011 244 `````` use import int.EuclideanDivision `````` Jean-Christophe Filliâtre committed Apr 08, 2011 245 `````` use import Mat22 `````` Jean-Christophe Filliâtre committed Apr 08, 2011 246 `````` `````` Andrei Paskevich committed Oct 13, 2012 247 248 `````` constant m1110 : t = { a11 = 1; a12 = 1; a21 = 1; a22 = 0 } `````` Jean-Christophe Filliâtre committed Apr 08, 2011 249 `````` `````` Jean-Christophe Filliâtre committed Apr 08, 2011 250 251 `````` (* computes ((1 1) (1 0))^n in O(log(n)) time `````` Jean-Christophe Filliâtre committed May 20, 2011 252 `````` since it is a matrix of the shape ((a+b b) (b a)), `````` Jean-Christophe Filliâtre committed Apr 08, 2011 253 254 `````` we only return the pair (a, b) *) `````` Andrei Paskevich committed Oct 13, 2012 255 256 257 258 259 `````` let rec logfib n variant { n } requires { n >= 0 } ensures { let a, b = result in power m1110 n = { a11 = a+b; a12 = b; a21 = b; a22 = a } } = if n = 0 then `````` Jean-Christophe Filliâtre committed Apr 08, 2011 260 `````` (1, 0) `````` Jean-Christophe Filliâtre committed Apr 08, 2011 261 262 263 264 `````` else begin let a, b = logfib (div n 2) in let c = a + b in if mod n 2 = 0 then `````` Jean-Christophe Filliâtre committed Apr 11, 2011 265 `````` (a*a + b*b, b*(a + c)) `````` Jean-Christophe Filliâtre committed Apr 08, 2011 266 `````` else `````` Jean-Christophe Filliâtre committed Apr 11, 2011 267 `````` (b*(a + c), c*c + b*b) `````` Jean-Christophe Filliâtre committed Apr 08, 2011 268 269 `````` end `````` Jean-Christophe Filliâtre committed Apr 08, 2011 270 271 272 273 274 275 276 277 `````` (* by induction, we easily prove that (1 1)^n = (F(n+1) F(n) ) (1 0) (F(n) F(n-1)) thus, we can compute F(n) in O(log(n)) using funtion logfib above *) `````` Jean-Christophe Filliâtre committed May 20, 2011 278 `````` lemma fib_m : `````` Jean-Christophe Filliâtre committed Apr 08, 2011 279 `````` forall n: int. n >= 0 -> `````` Andrei Paskevich committed Jun 29, 2011 280 `````` let p = power m1110 n in fib (n+1) = p.a11 /\ fib n = p.a21 `````` Jean-Christophe Filliâtre committed Apr 08, 2011 281 `````` `````` Andrei Paskevich committed Oct 13, 2012 282 `````` let fibo n requires { n >= 0 } ensures { result = fib n } = `````` Jean-Christophe Filliâtre committed Apr 08, 2011 283 284 `````` let _, b = logfib n in b `````` MARCHE Claude committed Sep 14, 2013 285 286 287 288 289 `````` let test0 () = fibo 0 let test1 () = fibo 1 let test7 () = fibo 7 let test42 () = fibo 42 `````` MARCHE Claude committed Jan 08, 2014 290 `````` let test2014 () = fibo 2014 `````` MARCHE Claude committed Sep 14, 2013 291 `````` `````` MARCHE Claude committed Jan 14, 2014 292 293 294 295 `````` exception BenchFailure let bench () raises { BenchFailure -> true } = if test42 () <> 267914296 then raise BenchFailure; `````` MARCHE Claude committed Jan 14, 2014 296 `````` if test2014 () <> 3561413997540486142674781564382874188700994538849211456995042891654110985470076818421080236961243875711537543388676277339875963824466334432403730750376906026741819889036464401788232213002522934897299928844192803507157647764542466327613134605502785287441134627457615461304177503249289874066244145666889138852687147544158443155204157950294129177785119464446668374163746700969372438526182906768143740891051274219441912520127 `````` MARCHE Claude committed Jan 14, 2014 297 `````` then raise BenchFailure `````` MARCHE Claude committed Jan 14, 2014 298 `````` `````` Jean-Christophe Filliâtre committed Apr 08, 2011 299 ``end``