new example: Tortoise and Hare algorithm

parent 4aa66580
(* Floyd's cycle detection, also known as ``tortoise and hare'' algorithm.
See The Art of Computer Programming, vol 2, exercise 6 page 7. *)
module TortoiseAndHare
use import int.Int
(* let f be a function from 0..m-1 to 0..m-1 *)
function f int : int
function m : int
axiom dom_f: forall x: int. 0 <= x < m -> 0 <= f x < m
(* let x0 be in 0..m-1 *)
function x0: int
axiom x0_range: 0 <= x0 < m
(* let x_{i+1} = f(x_i) *)
clone import int.Iter with type t = int, function f = f
function x (i: int): int = iter i x0
(* lambda and mu are skomlemized *)
function mu : int
function lambda : int
(* they are defined as follows *)
axiom mu_range: 0 <= mu
axiom lambda_range: 1 <= lambda
(* values x0 ... x_{mu+lambda-1} are all distinct *)
axiom distinct:
forall i j: int. 0 <= i < mu+lambda -> 0 <= j < mu+lambda ->
i <> j -> x i <> x j
(* cycle is lambda-long *)
axiom cycle: forall n: int. mu <= n -> x (n + lambda) = x n
(* Now comes the code.
Two references, tortoise and hare, traverses the xi at speed 1 and 2.
The challenge is to prove termination.
Actually, we even prove that the code runs in time O(lambda + mu). *)
use import module ref.Ref
predicate rel (t2 t1: int) =
exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= lambda + mu
let tortoise_hare () =
let tortoise = ref (f x0) in
let hare = ref (f (f x0)) in
while !tortoise <> !hare do
invariant {
exists t: int.
1 <= t <= lambda+mu /\ !tortoise = x t /\ !hare = x (2 * t) /\
forall i: int. 1 <= i < t -> x i <> x (2*i) }
variant { !tortoise } with rel
tortoise := f !tortoise;
hare := f (f !hare)
done
(* TODO: code to find out lambda and mu. See wikipedia. *)
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/tortoise_and_hare.gui"
End:
*)
(* 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 mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Parameter f: Z -> Z.
Parameter m: Z.
Axiom dom_f : forall (x:Z), ((0%Z <= x)%Z /\ (x < (m ))%Z) ->
((0%Z <= (f x))%Z /\ ((f x) < (m ))%Z).
Parameter x0: Z.
Axiom x0_range : (0%Z <= (x0 ))%Z /\ ((x0 ) < (m ))%Z.
Parameter iter: Z -> Z -> Z.
Axiom iter_0 : forall (x:Z), ((iter 0%Z x) = x).
Axiom iter_s : forall (k:Z) (x:Z), (0%Z < k)%Z -> ((iter k
x) = (iter (k - 1%Z)%Z (f x))).
Axiom iter_1 : forall (x:Z), ((iter 1%Z x) = (f x)).
Axiom iter_s2 : forall (k:Z) (x:Z), (0%Z < k)%Z -> ((iter k
x) = (f (iter (k - 1%Z)%Z x))).
Parameter mu: Z.
Parameter lambda: Z.
Axiom mu_range : (0%Z <= (mu ))%Z.
Axiom lambda_range : (1%Z <= (lambda ))%Z.
Axiom distinct : forall (i:Z) (j:Z), ((0%Z <= i)%Z /\
(i < ((mu ) + (lambda ))%Z)%Z) -> (((0%Z <= j)%Z /\
(j < ((mu ) + (lambda ))%Z)%Z) -> ((~ (i = j)) -> ~ ((iter i
(x0 )) = (iter j (x0 ))))).
Axiom cycle : forall (n:Z), ((mu ) <= n)%Z -> ((iter (n + (lambda ))%Z
(x0 )) = (iter n (x0 ))).
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Definition rel(t2:Z) (t1:Z): Prop := exists i:Z, (t1 = (iter i (x0 ))) /\
((t2 = (iter (i + 1%Z)%Z (x0 ))) /\ ((1%Z <= i)%Z /\
(i <= ((lambda ) + (mu ))%Z)%Z)).
Theorem WP_parameter_tortoise_hare : forall (hare:Z), forall (tortoise:Z),
(exists t:Z, ((1%Z <= t)%Z /\ (t <= ((lambda ) + (mu ))%Z)%Z) /\
((tortoise = (iter t (x0 ))) /\ ((hare = (iter (2%Z * t)%Z (x0 ))) /\
forall (i:Z), ((1%Z <= i)%Z /\ (i < t)%Z) -> ~ ((iter i
(x0 )) = (iter (2%Z * i)%Z (x0 )))))) -> ((~ (tortoise = hare)) ->
forall (tortoise1:Z), (tortoise1 = (f tortoise)) -> forall (hare1:Z),
(hare1 = (f (f hare))) -> exists t:Z, ((1%Z <= t)%Z /\
(t <= ((lambda ) + (mu ))%Z)%Z) /\ ((tortoise1 = (iter t (x0 ))) /\
((hare1 = (iter (2%Z * t)%Z (x0 ))) /\ forall (i:Z), ((1%Z <= i)%Z /\
(i < t)%Z) -> ~ ((iter i (x0 )) = (iter (2%Z * i)%Z (x0 )))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros hare tortoise (t, (ht, (eqt, (eqh, h)))).
intros; subst.
assert (dis: forall i : Z, (1 <= i <= t)%Z -> iter i x0 <> iter (2 * i) x0).
intros i hi.
assert (case: (i < t \/ i = t)%Z) by omega. destruct case.
apply (h i); omega.
subst; omega. clear h H.
exists (t + 1)%Z; intuition.
assert (case: (t+1 <= lambda + mu \/ t+1> lambda+mu)%Z) by omega.
destruct case.
assumption.
assert (t = lambda+mu)%Z by omega. subst.
clear H0 H1.
pose (i := (lambda+mu-(lambda+mu) mod lambda)%Z).
generalize lambda_range mu_range. intros hlam hmu.
assert (lambda_pos: (lambda > 0)%Z) by omega.
generalize (Z_mod_lt (lambda+mu) lambda lambda_pos)%Z. intro hr.
generalize (Z_div_mod_eq (lambda+mu) lambda lambda_pos)%Z. intro hq.
absurd (iter i x0 = iter (2*i) x0).
red; intro; apply (dis i); auto.
subst i; omega.
assert (hi: (mu <= i)%Z) by (subst i; omega).
assert (ind: (forall k: Z, 0 <= k -> iter (i + lambda*k) x0 = iter i x0)%Z).
apply natlike_ind.
ring_simplify (i + lambda * 0)%Z; auto.
intros.
unfold Zsucc.
replace (i + lambda * (x + 1))%Z with ((i+lambda*x)+lambda)%Z by ring.
rewrite cycle; auto.
assert (0 <= lambda * x)%Z.
apply Zmult_le_0_compat; omega.
omega.
replace (2*i)%Z with (i + lambda * ((lambda + mu) / lambda))%Z.
symmetry. apply ind.
apply Z_div_pos; omega.
subst i; omega.
rewrite (iter_s2 (t+1)%Z); intuition.
ring_simplify (t+1-1)%Z; auto.
rewrite (iter_s2 (2*(t+1))%Z); intuition.
ring_simplify (2 * (t + 1) - 1) %Z.
rewrite (iter_s2 (2*t+1)%Z); intuition.
ring_simplify (2 * t + 1 - 1) %Z; auto.
apply (dis i); omega.
Qed.
(* DO NOT EDIT BELOW *)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/tortoise_and_hare/why3session.xml">
<file name="../tortoise_and_hare.mlw" verified="true" expanded="true">
<theory name="WP TortoiseAndHare" verified="true" expanded="true">
<goal name="WP_parameter tortoise_hare" expl="correctness of parameter tortoise_hare" sum="91ac7ea5fd1fbbcfbed05554d037d955" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter tortoise_hare.1" expl="loop invariant init" sum="0e9d405eb4b310f9ee22eb3505ef5db9" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal name="WP_parameter tortoise_hare.2" expl="loop invariant preservation" sum="f343cf215fbafc7b514fb7822f857df9" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="tortoise_and_hare_WP_TortoiseAndHare_WP_parameter_tortoise_hare_2.v" obsolete="false">
<result status="valid" time="1.08"/>
</proof>
</goal>
<goal name="WP_parameter tortoise_hare.3" expl="loop variant decreases" sum="fe982931e3cc2f7497132a090909caa0" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.61"/>
</proof>
</goal>
<goal name="WP_parameter tortoise_hare.4" expl="normal postcondition" sum="ba0632d0db74b0437824be9335f09621" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
(* Floyd's ``the tortoise and the hare'' algorithm. *)
module TortoiseHare
use import int.Int
(* We consider a function f over an abstract type t *)
type t
function f t : t
(* Given some x0 in t, we consider the sequence of the repeated calls
to f starting from x0. *)
function x int : t
axiom xdef: forall n:int. n >= 0 -> x (n+1) = f (x n)
function x0 : t = x 0
(* If t is finite, this sequence will eventually end up on a cycle.
Let us simply assume the existence of this cycle, that is
x (i + lambda) = x i, for some lambda > 0 and i large enough. *)
function mu : int
axiom mu: mu >= 0
function lambda : int
axiom lambda: lambda >= 1
axiom cycle: forall i:int. mu <= i -> x (i + lambda) = x i
lemma cycle_gen:
forall i:int. mu <= i -> forall k:int. 0 <= k -> x (i + lambda * k) = x i
(* The challenge is to prove that the recursive function
let rec run x1 x2 = if x1 <> x2 then run (f x1) (f (f x2))
terminates when called on x0 and (f x0).
*)
function dist int int : int
axiom dist_def1:
forall n m: int. 0 <= n <= m ->
x (n + dist n m) = x m
axiom dist_def2:
forall n m: int. 0 <= n <= m ->
forall k: int. x (n + k) = x m -> dist n m <= k
predicate r (x12 : (t, t)) (x'12 : (t, t)) =
let x1, x2 = x12 in
let x'1, x'2 = x'12 in
exists m:int.
x1 = x (m+1) /\ x2 = x (2*m+2) /\ x'1 = x m /\ x'2 = x (2*m) /\
m < mu \/ (mu <= m /\ dist (m+1) (2*m+2) < dist m (2*m))
let rec run x1 x2 variant { (x1, x2) } with r =
{ exists m:int [x m]. x1 = x m /\ x2 = x (2*m) }
if x1 <> x2 then
run (f x1) (f (f x2))
{ }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/tortoise_hare.gui"
End:
*)
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