cleaning up fibonacci

parent 3381699c
theory Fibonacci
theory Fibonacci "Fibonacci numbers"
use import int.Int
use export int.Int
logic fib int : int
axiom fib0: fib 0 = 0
axiom fib1: fib 1 = 1
axiom fibn: forall n:int [fib n]. n >= 2 -> fib n = fib (n-1) + fib (n-2)
end
theory FibonacciTest
inductive isfib int int =
| isfib0: isfib 0 0
| isfib1: isfib 1 1
| isfibn:
forall n r p: int.
n >= 2 && isfib (n-2) r && isfib (n-1) p -> isfib n (p+r)
use import Fibonacci
lemma isfib_2_1 : isfib 2 1
lemma isfib_6_8 : isfib 6 8
lemma isfib_2_1 : fib 2 = 1
lemma isfib_6_8 : fib 6 = 8
(* provable only if def is inductive (least fix point) *)
lemma not_isfib_2_2 : not (isfib 2 2)
lemma not_isfib_2_2 : fib 2 <> 2
end
......@@ -29,14 +33,14 @@ module FibonacciLinear
let y = ref 0 in
let x = ref 1 in
for i=0 to n-1 do
invariant { 0 <= i <= n && isfib (i+1) x && isfib i y }
for i = 0 to n - 1 do
invariant { 0 <= i <= n and fib (i+1) = x and fib i = y }
let aux = !y in
y := !x;
x := !x + aux
done;
!y
{ isfib n result}
{ fib n = result}
end
......@@ -51,25 +55,15 @@ theory Mat22 "2x2 integer matrices"
logic mult (x: t) (y: t) : t =
{|
a11 = x.a11 * y.a11 + x.a12 * y.a21; a12 = x.a11 * y.a12 + x.a12 * y.a22;
a21 = x.a21 * y.a11 + x.a22 * y.a21; a22 = x.a21 * y.a12 + x.a22 * y.a22
a21 = x.a21 * y.a11 + x.a22 * y.a21; a22 = x.a21 * y.a12 + x.a22 * y.a22;
|}
clone algebra.Assoc with type t = t, logic op = mult, lemma Assoc
(* holds, but not useful *)
(* clone algebra.Assoc with type t = t, logic op = mult, lemma Assoc *)
clone export
int.Exponentiation with type t = t, logic one = id, logic (*) = mult
(* to prove power_sum below, we would also need
lemma mult_id : forall m: t. mult m id = m
lemma id_mult : forall m: t. mult id m = m
logic p (n:int) =
forall x: t, m: int.
m >= 0 -> power x (n + m) = mult (power x n) (power x m)
clone int.Induction with logic p = p
*)
lemma power_sum :
forall x: t, n m: int.
n >= 0 -> m >= 0 -> power x (n + m) = mult (power x n) (power x m)
......@@ -79,7 +73,6 @@ end
module FibonacciLogarithmic
use import Fibonacci
use import int.Int
use import int.EuclideanDivision
use import Mat22
......@@ -91,7 +84,7 @@ module FibonacciLogarithmic
since it is a matrix of the shape ((a+b b) (b a)),
we only return the pair (a, b) *)
let rec logfib n =
let rec logfib n variant { n } =
{ n >= 0 }
if n = 0 then
(1, 0)
......@@ -99,9 +92,9 @@ module FibonacciLogarithmic
let a, b = logfib (div n 2) in
let c = a + b in
if mod n 2 = 0 then
(a*a + b*b, b * (a + c))
(a*a + b*b, b*(a + c))
else
(b * (a + c), c*c + b*b)
(b*(a + c), c*c + b*b)
end
{ let a, b = result in
power m1110 n = {| a11 = a+b; a12 = b; a21 = b; a22 = a |} }
......@@ -114,19 +107,14 @@ module FibonacciLogarithmic
thus, we can compute F(n) in O(log(n)) using funtion logfib above
*)
logic p (n:int) =
let p = power m1110 n in
isfib (n+1) p.a11 and isfib n p.a21
clone int.Induction with logic p = p
lemma fib_m :
forall n: int. n >= 0 ->
let p = power m1110 n in
isfib (n+1) p.a11 and isfib n p.a21
let p = power m1110 n in fib (n+1) = p.a11 and fib n = p.a21
let fibo n =
{ n >= 0 }
let _, b = logfib n in b
{ isfib n result }
{ result = fib n }
end
......
......@@ -21,17 +21,15 @@ Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive isfib : Z -> Z -> Prop :=
| isfib0 : (isfib 0%Z 0%Z)
| isfib1 : (isfib 1%Z 1%Z)
| isfibn : forall (n:Z) (r:Z) (p:Z), ((2%Z <= n)%Z /\ ((isfib (n - 2%Z)%Z
r) /\ (isfib (n - 1%Z)%Z p))) -> (isfib n (p + r)%Z).
Parameter fib: Z -> Z.
Axiom isfib_2_1 : (isfib 2%Z 1%Z).
Axiom isfib_6_8 : (isfib 6%Z 8%Z).
Axiom fib0 : ((fib 0%Z) = 0%Z).
Axiom not_isfib_2_2 : ~ (isfib 2%Z 2%Z).
Axiom fib1 : ((fib 1%Z) = 1%Z).
Axiom fibn : forall (n:Z), (2%Z <= n)%Z ->
((fib n) = ((fib (n - 1%Z)%Z) + (fib (n - 2%Z)%Z))%Z).
Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
......@@ -88,7 +86,8 @@ Axiom power_sum : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n + m)%Z) = (mult (power x n) (power x m)))).
Theorem WP_logfib : forall (n:Z), (0%Z <= n)%Z -> ((~ (n = 0%Z)) ->
((0%Z <= (Zdiv n 2%Z))%Z -> forall (result:(Z* Z)%type),
((((0%Z <= n)%Z /\ ((Zdiv n 2%Z) < n)%Z) /\ (0%Z <= (Zdiv n 2%Z))%Z) ->
forall (result:(Z* Z)%type),
match result with
| (a, b) => ((power (mk_t 1%Z 1%Z 1%Z 0%Z) (Zdiv n 2%Z)) = (mk_t (a + b)%Z
b b a))
......@@ -107,11 +106,11 @@ intro.
assert (n mod 2 = 1)%Z.
generalize (Mod_bound n 2).
intuition.
simpl in H6.
simpl in H8.
omega.
assert (n = 2 * (n/2) + 1)%Z.
generalize (Div_mod n 2); intuition.
rewrite H5.
rewrite H7.
rewrite Power_s. 2:omega.
replace (2 * (n/2))%Z with (n/2 + n/2)%Z by omega.
rewrite power_sum; try omega.
......
......@@ -21,17 +21,15 @@ Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive isfib : Z -> Z -> Prop :=
| isfib0 : (isfib 0%Z 0%Z)
| isfib1 : (isfib 1%Z 1%Z)
| isfibn : forall (n:Z) (r:Z) (p:Z), ((2%Z <= n)%Z /\ ((isfib (n - 2%Z)%Z
r) /\ (isfib (n - 1%Z)%Z p))) -> (isfib n (p + r)%Z).
Parameter fib: Z -> Z.
Axiom isfib_2_1 : (isfib 2%Z 1%Z).
Axiom isfib_6_8 : (isfib 6%Z 8%Z).
Axiom fib0 : ((fib 0%Z) = 0%Z).
Axiom not_isfib_2_2 : ~ (isfib 2%Z 2%Z).
Axiom fib1 : ((fib 1%Z) = 1%Z).
Axiom fibn : forall (n:Z), (2%Z <= n)%Z ->
((fib n) = ((fib (n - 1%Z)%Z) + (fib (n - 2%Z)%Z))%Z).
Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z.
......@@ -73,9 +71,6 @@ Definition mult(x:t) (y:t): t :=
(((a21 x) * (a11 y))%Z + ((a22 x) * (a21 y))%Z)%Z
(((a21 x) * (a12 y))%Z + ((a22 x) * (a22 y))%Z)%Z).
Axiom Assoc : forall (x:t) (y:t) (z:t), ((mult (mult x y) z) = (mult x
(mult y z))).
Parameter power: t -> Z -> t.
......@@ -87,20 +82,14 @@ Axiom Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
Axiom power_sum : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n + m)%Z) = (mult (power x n) (power x m)))).
Definition p(n:Z): Prop := let p1 := (power (mk_t 1%Z 1%Z 1%Z 0%Z) n) in
((isfib (n + 1%Z)%Z (a11 p1)) /\ (isfib n (a21 p1))).
Axiom Induction : (forall (n:Z), (0%Z <= n)%Z -> ((forall (k:Z),
((0%Z <= k)%Z /\ (k < n)%Z) -> (p k)) -> (p n))) -> forall (n:Z),
(0%Z <= n)%Z -> (p n).
Theorem fib_m : forall (n:Z), (0%Z <= n)%Z -> let p2 := (power (mk_t 1%Z 1%Z
1%Z 0%Z) n) in ((isfib (n + 1%Z)%Z (a11 p2)) /\ (isfib n (a21 p2))).
Theorem fib_m : forall (n:Z), (0%Z <= n)%Z -> let p := (power (mk_t 1%Z 1%Z
1%Z 0%Z) n) in (((fib (n + 1%Z)%Z) = (a11 p)) /\ ((fib n) = (a21 p))).
(* YOU MAY EDIT THE PROOF BELOW *)
Hint Constructors isfib.
Require Import Zwf.
Hint Resolve fib0 fib1 fibn.
intuition.
apply Induction; auto.
unfold p; intros.
pattern n; apply Zlt_0_ind; auto.
intro n0; intros.
assert (h: (n0 = 0 \/ n0>0)%Z) by omega.
destruct h.
subst n0.
......@@ -109,8 +98,8 @@ intuition.
replace (n0)%Z with ((n0-1) + 1)%Z by omega.
rewrite Power_s; [idtac | omega].
assert (h: (0 <= n0-1 < n0)%Z) by omega.
generalize (H1 (n0-1)%Z h).
clear H1.
generalize (H0 (n0-1)%Z h).
clear H0.
destruct (power (mk_t 1 1 1 0) (n0 - 1)).
replace (n0-1+1)%Z with n0 by omega.
replace (a11 (mk_t z z0 z1 z2)) with z by auto.
......@@ -118,12 +107,11 @@ replace (a21 (mk_t z z0 z1 z2)) with z1 by auto.
replace (a21 (mult (mk_t 1 1 1 0) (mk_t z z0 z1 z2))) with z.
intuition.
replace (a11 (mult (mk_t 1 1 1 0) (mk_t z z0 z1 z2))) with (z+z1)%Z.
apply (isfibn (n0+1)%Z).
intuition.
rewrite (fibn (n0+1)%Z).
replace (n0+1-1)%Z with n0 by omega.
replace (n0 + 1 - 2)%Z with (n0-1)%Z by omega.
trivial.
replace (n0 + 1 - 1)%Z with (n0)%Z by omega.
trivial.
intuition.
omega.
unfold mult, a11, a12, a21, a22.
omega.
unfold mult, a11, a12, a21, a22.
......
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