Commit bbac360c by Jean-Christophe Filliâtre

fibonacci in logarithmic time (proof completed)

parent a225f208
 ... ... @@ -66,7 +66,7 @@ theory Mat22 "2x2 integer matrices" forall m: t. power m 0 = id axiom power_n : forall m: t, n: int. n > 0 -> power m n = mult (power m (n-1)) m forall m: t, n: int. n >= 0 -> power m (n+1) = mult (power m n) m lemma power_square : forall m: t, n: int. n >= 0 -> mult (power m n) (power m n) = power m (2*n) ... ...
 (* Beware! Only edit allowed sections below *) (* This file is generated by Why3's Coq driver *) Require Import ZArith. Require Import Rbase. Require Import Zdiv. Parameter ghost : forall (a:Type), Type. Definition unit := unit. Parameter ignore: forall (a:Type), a -> unit. Implicit Arguments ignore. Parameter label_ : Type. Parameter at1: forall (a:Type), a -> label_ -> a. Implicit Arguments at1. 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). Axiom isfib_2_1 : (isfib 2%Z 1%Z). Axiom isfib_6_8 : (isfib 6%Z 8%Z). Axiom not_isfib_2_2 : ~ (isfib 2%Z 2%Z). Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z. Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z). Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z). Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) < (Zabs y))%Z). Axiom Mod_1 : forall (x:Z), ((Zmod x 1%Z) = 0%Z). Axiom Div_1 : forall (x:Z), ((Zdiv x 1%Z) = x). Inductive t := | M : Z -> Z -> Z -> Z -> t . Definition a11(u:t): Z := match u with | M a111 _ _ _ => a111 end. Definition a12(u:t): Z := match u with | M _ a121 _ _ => a121 end. Definition a21(u:t): Z := match u with | M _ _ a211 _ => a211 end. Definition a22(u:t): Z := match u with | M _ _ _ a221 => a221 end. Definition mult(x:t) (y:t): t := match x with | M x11 x12 x21 x22 => match y with | M y11 y12 y21 y22 => (M ((x11 * y11)%Z + (x12 * y21)%Z)%Z ((x11 * y12)%Z + (x12 * y22)%Z)%Z ((x21 * y11)%Z + (x22 * y21)%Z)%Z ((x21 * y12)%Z + (x22 * y22)%Z)%Z) end end. Axiom Assoc : forall (x:t) (y:t) (z:t), ((mult (mult x y) z) = (mult x (mult y z))). Parameter power: t -> Z -> t. Axiom power_0 : forall (m:t), ((power m 0%Z) = (M 1%Z 0%Z 0%Z 1%Z)). Axiom power_n : forall (m:t) (n:Z), (0%Z < n)%Z -> ((power m n) = (mult (power m (n - 1%Z)%Z) m)). Axiom power_square : forall (m:t) (n:Z), (0%Z <= n)%Z -> ((mult (power m n) (power m n)) = (power m (2%Z * n)%Z)). Axiom fib_m : forall (n:Z), (0%Z <= n)%Z -> match (power (M 1%Z 1%Z 1%Z 0%Z) n) with | M a112 a122 a212 a222 => (isfib a112 (n + 1%Z)%Z) /\ ((isfib a122 n) /\ ((isfib a212 n) /\ (((n = 0%Z) -> (a222 = 1%Z)) /\ ((0%Z < n)%Z -> (isfib a222 (n - 1%Z)%Z))))) end. 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), match result with | (a, b) => ((power (M 1%Z 1%Z 1%Z 0%Z) (Zdiv n 2%Z)) = (M (a + b)%Z b b a)) end -> match result with | (a, b) => (isfib (a + b)%Z ((2%Z * (Zdiv n 2%Z))%Z + 1%Z)%Z) -> ((~ ((Zmod n 2%Z) = 0%Z)) -> match ((b * (a + (a + b)%Z)%Z)%Z, (((a + b)%Z * (a + b)%Z)%Z + (b * b)%Z)%Z) with | (a1, b1) => ((power (M 1%Z 1%Z 1%Z 0%Z) n) = (M (a1 + b1)%Z b1 b1 a1)) end) end)). (* YOU MAY EDIT THE PROOF BELOW *) intuition. destruct result as (a,b). intros. assert (n mod 2 = 1)%Z. assert (0 <= n mod 2 < 2)%Z. apply Mod_bound. omega. omega. assert (n = 2*(n / 2) + 1)%Z. rewrite <- H5. apply Div_mod. omega. rewrite H6. rewrite power_n; [idtac | omega]. replace (2 * (n / 2) + 1 - 1)%Z with (2 * (n / 2))%Z by omega. rewrite <- power_square; [idtac | assumption]. rewrite H2. unfold mult. apply f_equal4; ring. Qed. (* DO NOT EDIT BELOW *)
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!