diff --git a/examples/programs/fibonacci.mlw b/examples/programs/fibonacci.mlw index 97f5ce45677fde837f18ee30212df5a0c605ab07..87ad9425b6bd3c6bc5ff392f3698f3fb83f9917e 100644 --- a/examples/programs/fibonacci.mlw +++ b/examples/programs/fibonacci.mlw @@ -1,20 +1,24 @@ -theory Fibonacci +theory Fibonacci "Fibonacci numbers" - use import int.Int + use export int.Int - 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) - - lemma isfib_2_1 : isfib 2 1 - lemma isfib_6_8 : isfib 6 8 + logic fib int : int - (* provable only if def is inductive (least fix point) *) - lemma not_isfib_2_2 : not (isfib 2 2) + 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 + + use import Fibonacci + + lemma isfib_2_1 : fib 2 = 1 + lemma isfib_6_8 : fib 6 = 8 + + 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 diff --git a/examples/programs/fibonacci/fibonacci.mlw_FibonacciLogarithmic_WP_logfib_2.v b/examples/programs/fibonacci/fibonacci.mlw_FibonacciLogarithmic_WP_logfib_2.v index 88e4914d96ff2d0a4a071be3cfb945bc6155b6e2..0685fe08de7c97bb742b812afe1bb1bb2cb3ce83 100644 --- a/examples/programs/fibonacci/fibonacci.mlw_FibonacciLogarithmic_WP_logfib_2.v +++ b/examples/programs/fibonacci/fibonacci.mlw_FibonacciLogarithmic_WP_logfib_2.v @@ -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. diff --git a/examples/programs/fibonacci/fibonacci.mlw_FibonacciLogarithmic_fib_m_1.v b/examples/programs/fibonacci/fibonacci.mlw_FibonacciLogarithmic_fib_m_1.v index 20a376d45680046dcff6aab6064aa95853fc30f4..0310145118761710db1e44b9bb429429604104e8 100644 --- a/examples/programs/fibonacci/fibonacci.mlw_FibonacciLogarithmic_fib_m_1.v +++ b/examples/programs/fibonacci/fibonacci.mlw_FibonacciLogarithmic_fib_m_1.v @@ -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.