fibonacci: fixed proof

parent dad64546
......@@ -86,16 +86,10 @@ module FibonacciLogarithmic
logic m1110 : t = {| a11 = 1; a12 = 1;
a21 = 1; a22 = 0 |}
lemma fib_m :
forall n: int. n >= 0 ->
let p = power m1110 n in
isfib p.a11 (n+1) and isfib p.a12 n and isfib p.a21 n and
(n = 0 -> p.a22 = 1) and (n > 0 -> isfib p.a22 (n-1))
let rec logfib n =
{ n >= 0 }
if n = 0 then
(1, 1)
(1, 0)
else begin
let a, b = logfib (div n 2) in
let c = a + b in
......@@ -107,10 +101,19 @@ module FibonacciLogarithmic
{ let a, b = result in
power m1110 n = {| a11 = a+b; a12 = b; a21 = b; a22 = a |} }
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 fibo n =
{ n >= 0 }
let _, b = logfib n in b
{ isfib result n }
{ isfib n result }
end
......
(* 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 :=
| mk_t : Z -> Z -> Z -> Z -> t .
Definition a11(u:t): Z := match u with
| mk_t a111 _ _ _ => a111
end.
Definition a12(u:t): Z := match u with
| mk_t _ a121 _ _ => a121
end.
Definition a21(u:t): Z := match u with
| mk_t _ _ a211 _ => a211
end.
Definition a22(u:t): Z := match u with
| mk_t _ _ _ a221 => a221
end.
Definition mult(x:t) (y:t): t :=
(mk_t (((a11 x) * (a11 y))%Z + ((a12 x) * (a21 y))%Z)%Z
(((a11 x) * (a12 y))%Z + ((a12 x) * (a22 y))%Z)%Z
(((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.
Axiom Power_0 : forall (x:t), ((power x 0%Z) = (mk_t 1%Z 0%Z 0%Z 1%Z)).
Axiom Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
(n + 1%Z)%Z) = (mult x (power x n))).
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),
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))
end ->
match result with
| (a, b) => (~ ((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 (mk_t 1%Z 1%Z 1%Z 0%Z) n) = (mk_t (a1 + b1)%Z b1
b1 a1))
end
end)).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
destruct result as (a,b).
intro.
assert (n mod 2 = 1)%Z.
generalize (Mod_bound n 2).
intuition.
simpl in H6.
omega.
assert (n = 2 * (n/2) + 1)%Z.
generalize (Div_mod n 2); intuition.
rewrite H5.
rewrite Power_s. 2:omega.
replace (2 * (n/2))%Z with (n/2 + n/2)%Z by omega.
rewrite power_sum; try omega.
rewrite H2; clear H2 H3 H4 H5.
unfold mult, a11, a12, a21, a22.
apply f_equal4; ring.
Qed.
(* DO NOT EDIT BELOW *)
(* 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 :=
| mk_t : Z -> Z -> Z -> Z -> t .
Definition a11(u:t): Z := match u with
| mk_t a111 _ _ _ => a111
end.
Definition a12(u:t): Z := match u with
| mk_t _ a121 _ _ => a121
end.
Definition a21(u:t): Z := match u with
| mk_t _ _ a211 _ => a211
end.
Definition a22(u:t): Z := match u with
| mk_t _ _ _ a221 => a221
end.
Definition mult(x:t) (y:t): t :=
(mk_t (((a11 x) * (a11 y))%Z + ((a12 x) * (a21 y))%Z)%Z
(((a11 x) * (a12 y))%Z + ((a12 x) * (a22 y))%Z)%Z
(((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.
Axiom Power_0 : forall (x:t), ((power x 0%Z) = (mk_t 1%Z 0%Z 0%Z 1%Z)).
Axiom Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
(n + 1%Z)%Z) = (mult x (power x n))).
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))).
(* YOU MAY EDIT THE PROOF BELOW *)
Hint Constructors isfib.
intuition.
apply Induction; auto.
unfold p; intros.
assert (h: (n0 = 0 \/ n0>0)%Z) by omega.
destruct h.
subst n0.
rewrite Power_0.
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.
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.
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.
replace (n0 + 1 - 2)%Z with (n0-1)%Z by omega.
trivial.
replace (n0 + 1 - 1)%Z with (n0)%Z by omega.
trivial.
unfold mult, a11, a12, a21, a22.
omega.
unfold mult, a11, a12, a21, a22.
intuition.
Qed.
(* DO NOT EDIT BELOW *)
(* Beware! Only edit allowed sections below *)
(* This file is generated by Why3's Coq driver *)
Require Import ZArith.
Require Import Rbase.
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 t :=
| mk_t : Z -> Z -> Z -> Z -> t .
Definition a11(u:t): Z := match u with
| mk_t a111 _ _ _ => a111
end.
Definition a12(u:t): Z := match u with
| mk_t _ a121 _ _ => a121
end.
Definition a21(u:t): Z := match u with
| mk_t _ _ a211 _ => a211
end.
Definition a22(u:t): Z := match u with
| mk_t _ _ _ a221 => a221
end.
Definition mult(x:t) (y:t): t :=
(mk_t (((a11 x) * (a11 y))%Z + ((a12 x) * (a21 y))%Z)%Z
(((a11 x) * (a12 y))%Z + ((a12 x) * (a22 y))%Z)%Z
(((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.
Axiom Power_0 : forall (x:t), ((power x 0%Z) = (mk_t 1%Z 0%Z 0%Z 1%Z)).
Axiom Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
(n + 1%Z)%Z) = (mult x (power x n))).
Axiom mult_id : forall (m:t), ((mult m (mk_t 1%Z 0%Z 0%Z 1%Z)) = m).
Axiom id_mult : forall (m:t), ((mult (mk_t 1%Z 0%Z 0%Z 1%Z) m) = m).
Definition p(n:Z): Prop := forall (x:t) (m:Z), (0%Z <= m)%Z -> ((power x
(n + m)%Z) = (mult (power x n) (power x m))).
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 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)))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
apply Induction; auto.
unfold p.
intros.
assert (h: (n0 = 0 \/ n0>0)%Z) by omega.
destruct h.
subst n0.
rewrite Power_0.
symmetry.
apply id_mult.
replace (n0 + m0)%Z with ((n0-1) + (m0+1))%Z by omega.
rewrite H2.
rewrite Power_s.
rewrite <- Assoc.
replace (mult (power x0 (n0 - 1)) x0) with (mult (power x0 (n0-1)) (power x0 1)).
rewrite <- H2.
replace (n0 - 1 + 1)%Z with n0 by omega.
reflexivity.
omega.
omega.
apply f_equal.
replace 1%Z with (0+1)%Z by omega.
rewrite Power_s.
rewrite Power_0.
apply mult_id.
omega.
omega.
omega.
omega.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -59,6 +59,7 @@
let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']*
rule scan fmt = parse
| "(*)" { fprintf fmt "(*)"; scan fmt lexbuf }
| "(*" { fprintf fmt "<font color=\"990000\">(*";
comment fmt lexbuf;
fprintf fmt "</font>";
......
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