cleaning up fibonacci spec

parent bbac360c
......@@ -4,21 +4,23 @@ module M
use import list.List
use import list.Length
let rec length_ (l : list 'a) variant { length l } =
{}
match l with
| Nil -> 0
| Cons _ r -> 1 + length_ r
end
{ result = length l }
(*
let rec length_ (l : list 'a) variant { length l } =
{}
match l with
| Nil -> 0
| Cons _ r -> 1 + length_ r
end
{ result = length l }
*)
let rec append (l1 : list 'a) (l2 : list 'a) variant { length l1 } =
{ }
match l1 with
| Nil -> l2
| Cons x r -> Cons x (append r l2)
end
{ length result = length l1 + length l2 }
let rec append (l1 : list 'a) (l2 : list 'a) variant { length l1 } =
{ }
match l1 with
| Nil -> l2
| Cons x r -> Cons x (append r l2)
end
{ length result = length l1 + length l2 }
end
......
......@@ -10,11 +10,11 @@ theory Fibonacci
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
lemma isfib_2_1 : isfib 2 1
lemma isfib_6_8 : isfib 6 8
(* provable only if def is inductive (least fix point) *)
lemma not_isfib_2_2 : not (isfib 2 2)
(* provable only if def is inductive (least fix point) *)
lemma not_isfib_2_2 : not (isfib 2 2)
end
......@@ -44,32 +44,35 @@ theory Mat22 "2x2 integer matrices"
use import int.Int
type t = M (a11: int) (a12: int) (a21: int) (a22: int)
type t = {| a11: int; a12: int; a21: int; a22: int |}
logic id : t = M 1 0 0 1
logic id : t = {| a11 = 1; a12 = 0; a21 = 0; a22 = 1 |}
logic mult (x: t) (y: t) : t =
let M x11 x12
x21 x22 = x
in
let M y11 y12
y21 y22 = y
in
M (x11 * y11 + x12 * y21) (x11 * y12 + x12 * y22)
(x21 * y11 + x22 * y21) (x21 * y12 + x22 * y22)
{|
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
|}
clone algebra.Assoc with type t = t, logic op = mult, lemma Assoc
logic power t int : t
clone export
int.Exponentiation with type t = t, logic one = id, logic (*) = mult
axiom power_0 :
forall m: t. power m 0 = id
(* to prove power_sum below, we would also need
axiom power_n :
forall m: t, n: int. n >= 0 -> power m (n+1) = mult (power m n) m
lemma mult_id : forall m: t. mult m id = m
lemma id_mult : forall m: t. mult id m = m
lemma power_square :
forall m: t, n: int. n >= 0 -> mult (power m n) (power m n) = power m (2*n)
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)
end
......@@ -78,15 +81,16 @@ module FibonacciLogarithmic
use import Fibonacci
use import int.Int
use import int.EuclideanDivision
use Mat22 as M
use import Mat22
logic m1110 : M.t = M.M 1 1 1 0
logic m1110 : t = {| a11 = 1; a12 = 1;
a21 = 1; a22 = 0 |}
lemma fib_m :
forall n: int. n >= 0 ->
let M.M a11 a12 a21 a22 = M.power m1110 n in
isfib a11 (n+1) and isfib a12 n and isfib a21 n and
(n = 0 -> a22 = 1) and (n > 0 -> isfib a22 (n-1))
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 }
......@@ -95,13 +99,13 @@ module FibonacciLogarithmic
else begin
let a, b = logfib (div n 2) in
let c = a + b in
assert { isfib c (2 * (div n 2) + 1) };
if mod n 2 = 0 then
(a*a + b*b, b * (a + c))
else
(b * (a + c), c*c + b*b)
end
{ let a, b = result in M.power m1110 n = M.M (a+b) b b a }
{ let a, b = result in
power m1110 n = {| a11 = a+b; a12 = b; a21 = b; a22 = a |} }
let fibo n =
{ n >= 0 }
......
......@@ -85,8 +85,8 @@ 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_n : forall (m:t) (n:Z), (0%Z <= n)%Z -> ((power m
(n + 1%Z)%Z) = (mult (power m n) 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)).
......
......@@ -108,3 +108,4 @@ theory OrderedField
axiom CompatOrderAdd : forall x y z : t. x <= y -> x + z <= y + z
axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
end
......@@ -104,15 +104,27 @@ theory ComputerDivision
end
theory Power
theory Exponentiation
use import Int
logic power int int : int
type t
logic one : t
logic (*) t t : t
logic power t int : t
axiom Power_0 : forall x: t. power x 0 = one
axiom Power_s : forall x: t, n: int. n >= 0 -> power x (n+1) = x * power x n
axiom Power_0 : forall x : int. power x 0 = 1
end
theory Power
axiom Power_s : forall x n : int. 0 < n -> power x n = x * power x (n-1)
use import Int
clone export
Exponentiation with type t = int, logic one = one, logic (*) = (*)
lemma Power_1 : forall x : int. power x 1 = x
......@@ -239,6 +251,17 @@ theory Gcd
end
theory Induction
use import Int
logic p int
axiom Induction :
(forall n:int. 0 <= n -> (forall k:int. 0 <= k < n -> p k) -> p n) ->
forall n:int. 0 <= n -> p n
end
(*
Local Variables:
compile-command: "make -C .. theories/int.gui"
......
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