Commit 9ebc9463 by Jean-Christophe Filliâtre

### fibonacci: fixed proof (using Coq)

parent ecd13186
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Parameter fib: Z -> Z. Axiom fib0 : ((fib 0%Z) = 0%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_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\ (x <= y)%Z). Parameter div: Z -> Z -> Z. Parameter mod1: Z -> Z -> Z. Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x y))%Z + (mod1 x y))%Z). Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z). Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x y))%Z /\ ((mod1 x y) < (Zabs y))%Z). Axiom Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z). Axiom Div_1 : forall (x:Z), ((div 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). 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_1 : forall (x:t), ((power x 1%Z) = 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))). Axiom Power_mult : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z -> ((power x (n * m)%Z) = (power (power x n) m))). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_logfib : forall (n:Z), (0%Z <= n)%Z -> ((~ (n = 0%Z)) -> ((((0%Z <= n)%Z /\ ((div n 2%Z) < n)%Z) /\ (0%Z <= (div n 2%Z))%Z) -> forall (result:Z) (result1:Z), ((power (mk_t 1%Z 1%Z 1%Z 0%Z) (div n 2%Z)) = (mk_t (result + result1)%Z result1 result1 result)) -> ((((mod1 n 2%Z) = 0%Z) -> match (((result * result)%Z + (result1 * result1)%Z)%Z, (result1 * (result + (result + result1)%Z)%Z)%Z) with | (a, b) => ((power (mk_t 1%Z 1%Z 1%Z 0%Z) n) = (mk_t (a + b)%Z b b a)) end) /\ ((~ ((mod1 n 2%Z) = 0%Z)) -> match ( (result1 * (result + (result + result1)%Z)%Z)%Z, (((result + result1)%Z * (result + result1)%Z)%Z + (result1 * result1)%Z)%Z) with | (a, b) => ((power (mk_t 1%Z 1%Z 1%Z 0%Z) n) = (mk_t (a + b)%Z b b a)) end)))). (* YOU MAY EDIT THE PROOF BELOW *) intros. assert (h: (2 <> 0)%Z) by omega. generalize (Div_mod n 2 h)%Z. intuition. rewrite H4 in H3. rewrite H3. replace (2 * div n 2 + 0)%Z with (div n 2 + div n 2)%Z by omega. rewrite Power_sum. rewrite H2; simpl. unfold mult; simpl. apply f_equal4; ring. intuition. generalize (Mod_bound n 2 h)%Z. simpl. intro. assert (h': (mod1 n 2 = 1)%Z) by omega. rewrite h' in H3. rewrite H3. replace (2 * div n 2 + 1)%Z with ((div n 2 + div n 2) + 1)%Z by omega. rewrite Power_s. rewrite Power_sum. rewrite H2; simpl. unfold mult at 2; simpl. unfold mult. apply f_equal4; unfold a11, a12, a21, a22; try ring. intuition. omega. Qed. (* DO NOT EDIT BELOW *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Definition unit := unit. Parameter qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Parameter fib: Z -> Z. Axiom fib0 : ((fib 0%Z) = 0%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_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\ (x <= y)%Z). Parameter div: Z -> Z -> Z. Parameter mod1: Z -> Z -> Z. Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x y))%Z + (mod1 x y))%Z). Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z). Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x y))%Z /\ ((mod1 x y) < (Zabs y))%Z). Axiom Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z). Axiom Div_1 : forall (x:Z), ((div 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). 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_1 : forall (x:t), ((power x 1%Z) = 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))). Axiom Power_mult : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z -> ((power x (n * m)%Z) = (power (power x n) m))). (* YOU MAY EDIT THE CONTEXT BELOW *) Hint Resolve fib0 fib1. (* DO NOT EDIT BELOW *) 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 *) intros n hn. pattern n; apply natlike_ind; intuition. rewrite Power_0. unfold a11, a21; simpl; auto. replace (Zsucc x) with (x+1)%Z by omega. rewrite Power_s; auto. destruct H0 as (h1,h2). split. rewrite fibn; try omega. ring_simplify (x+1+1-1)%Z. ring_simplify (x+1+1-2)%Z. unfold a11, mult. rewrite <- h1. rewrite <- h2. unfold a11, a12. ring. unfold a21, mult. rewrite <- h1. rewrite <- h2. unfold a21, a22. ring. Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -5,7 +5,7 @@ version="0.93.1"/> version="0.8 Steinthal"/> version="0.15.0"/> version="1.0.27"/> expanded="false"> expanded="false"> proved="true" expanded="false"> ... ... @@ -283,91 +244,23 @@ ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!