even nicer tortoise and hare example

now this is exactly TAOCP, vol 2, exercise 6 page 7
with a second loop finding out mu and lambda in time O(mu)
parent 63e43346
......@@ -93,7 +93,7 @@ module TortoiseAndHareAlgorithm
()
(* Finally, we implement the tortoise and hare algorithm that computes
the values of mu and lambda in linear time and constant space *)
the values of mu and lambda in time O(mu+lambda) and constant space *)
let tortoise_and_hare () : (mu:int, lambda:int)
ensures { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\
x (mu + lambda) = x mu }
......@@ -101,7 +101,7 @@ module TortoiseAndHareAlgorithm
= let mu, lambda = periodicity () in
equality mu lambda;
(* the first loop implements the tortoise and hare,
and finds the smallest n >= 1 such that x n = x (2n) *)
and finds the smallest n >= 1 such that x n = x (2n), in O(mu+lambda) *)
let tortoise = ref (f x0) in
let hare = ref (f (f x0)) in
let n = ref 1 in
......@@ -125,36 +125,27 @@ module TortoiseAndHareAlgorithm
assert { exists k. k >= 1 /\ n = k * lambda >= 1 };
assert { forall j. j >= mu -> x j = x (j + n) };
let xn = !tortoise in
(* a first loop to find mu *)
(* then a second loop finds mu and lambda, in O(mu) *)
let i = ref 0 in
let xi = ref x0 in (* = x i *)
let xni = ref xn in (* = x (n+i) *)
let lam = ref 0 in (* 0 or lambda *)
while !xi <> !xni do
invariant { 0 <= !i <= mu }
invariant { !xi = x !i /\ !xni = x (n + !i) }
invariant { forall j. 0 <= j < !i -> x j <> x (n + j) }
invariant { if !lam = 0 then forall j. 0 < j < !i -> x (n + j) <> x n
else !lam = lambda }
variant { mu - !i }
if !lam = 0 && !i > 0 && !xni = xn then lam := !i;
xi := f !xi;
xni := f !xni;
incr i;
done;
let m = !i in
assert { m = mu };
(* and a second loop to find lambda
(this is slightly less efficient than the argument in TAOCP,
but since the first loop is already O(mu+lambda), using two loops
respectively O(mu) and O(lambda) is not a problem). *)
i := 1;
xni := f xn;
while !xni <> xn do
invariant { !xni = x (n + !i) }
invariant { forall j. 1 <= j < !i -> x (n + j) <> x n }
invariant { 1 <= !i <= lambda }
variant { lambda - !i }
xni := f !xni;
incr i
done;
assert { !i = lambda };
m, !i
let l = if !lam = 0 then n else !lam in
assert { l = lambda };
m, l
end
......@@ -264,107 +264,207 @@
<goal name="VC tortoise_and_hare.13" expl="loop invariant init" proved="true">
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC tortoise_and_hare.14" expl="loop variant decrease" proved="true">
<goal name="VC tortoise_and_hare.14" expl="loop invariant init" proved="true">
<proof prover="6"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC tortoise_and_hare.15" expl="loop variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC tortoise_and_hare.16" expl="loop invariant preservation" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC tortoise_and_hare.16.0" expl="VC for tortoise_and_hare" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.16.1" expl="VC for tortoise_and_hare" proved="true">
<transf name="assert" proved="true" arg1="(x (n+lambda) = x n)">
<goal name="VC tortoise_and_hare.16.1.0" proved="true">
<transf name="instantiate" proved="true" arg1="H21" arg2="(n+lambda),n">
<goal name="VC tortoise_and_hare.16.1.0.0" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.16.1.1" expl="VC for tortoise_and_hare" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.17" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.51"/></proof>
</goal>
<goal name="VC tortoise_and_hare.18" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="45"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(lam1 = 0)">
<goal name="VC tortoise_and_hare.19.0" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(x (n + i1) = x n)">
<goal name="VC tortoise_and_hare.19.1.0" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1" expl="loop invariant preservation" proved="true">
<transf name="instantiate" proved="true" arg1="H24" arg2="(n+i1),n">
<goal name="VC tortoise_and_hare.19.1.1.0" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(exists k. k &gt;= 1 /\ i1 = k * lambda)">
<goal name="VC tortoise_and_hare.19.1.1.0.0" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1" expl="loop invariant preservation" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="((k-1) * lambda &gt;= 0)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.0" proved="true">
<proof prover="7"><result status="valid" time="9.59"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(i1 &gt;= lambda)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.0" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1" expl="loop invariant preservation" proved="true">
<transf name="case" proved="true" arg1="(k=1)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.0" expl="true case (loop invariant preservation)" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(x (n + lambda) &lt;&gt; x n)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0" proved="true">
<transf name="assert" proved="true" arg1="(lambda &lt; i1)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.80" steps="276"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0.1" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.1" expl="false case (loop invariant preservation)" proved="true">
<proof prover="6"><result status="valid" time="0.47"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.20" expl="loop variant decrease" proved="true">
<transf name="case" proved="true" arg1="(i = mu+1)">
<goal name="VC tortoise_and_hare.14.0" expl="true case (loop variant decrease)" proved="true">
<goal name="VC tortoise_and_hare.20.0" expl="true case (loop variant decrease)" proved="true">
<transf name="assert" proved="true" arg1="(x mu = x (mu + n))">
<goal name="VC tortoise_and_hare.14.0.0" proved="true">
<goal name="VC tortoise_and_hare.20.0.0" proved="true">
<proof prover="6"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC tortoise_and_hare.14.0.1" expl="true case (loop variant decrease)" proved="true">
<goal name="VC tortoise_and_hare.20.0.1" expl="true case (loop variant decrease)" proved="true">
<proof prover="6"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.14.1" expl="false case (loop variant decrease)" proved="true">
<goal name="VC tortoise_and_hare.20.1" expl="false case (loop variant decrease)" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.15" expl="loop invariant preservation" proved="true">
<goal name="VC tortoise_and_hare.21" expl="loop invariant preservation" proved="true">
<transf name="replace" proved="true" arg1="n" arg2="(2*n - n)">
<goal name="VC tortoise_and_hare.15.0" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="36"/></proof>
<goal name="VC tortoise_and_hare.21.0" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="39"/></proof>
</goal>
<goal name="VC tortoise_and_hare.15.1" proved="true">
<goal name="VC tortoise_and_hare.21.1" proved="true">
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.16" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="VC tortoise_and_hare.17" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC tortoise_and_hare.18" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.60"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19" expl="loop invariant init" proved="true">
<proof prover="6"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC tortoise_and_hare.20" expl="loop invariant init" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.21" expl="loop invariant init" proved="true">
<proof prover="6"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC tortoise_and_hare.22" expl="loop variant decrease" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
<goal name="VC tortoise_and_hare.22" expl="loop invariant preservation" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC tortoise_and_hare.22.0" expl="VC for tortoise_and_hare" proved="true">
<proof prover="6"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC tortoise_and_hare.22.1" expl="VC for tortoise_and_hare" proved="true">
<proof prover="6"><result status="valid" time="0.33"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.23" expl="loop invariant preservation" proved="true">
<proof prover="6"><result status="valid" time="0.06"/></proof>
<proof prover="6"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC tortoise_and_hare.24" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="41"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC tortoise_and_hare.25" expl="loop invariant preservation" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC tortoise_and_hare.25.0" expl="VC for tortoise_and_hare" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.25.1" expl="VC for tortoise_and_hare" proved="true">
<transf name="assert" proved="true" arg1="(x (n+lambda) = x n)">
<goal name="VC tortoise_and_hare.25.1.0" proved="true">
<proof prover="6"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="VC tortoise_and_hare.25.1.1" expl="VC for tortoise_and_hare" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
<goal name="VC tortoise_and_hare.25" expl="assertion" proved="true">
<transf name="instantiate" proved="true" arg1="H16" arg2="(n+i),n">
<goal name="VC tortoise_and_hare.25.0" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.09"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.26" expl="assertion" proved="true">
<transf name="instantiate" proved="true" arg1="H23" arg2="(n+i),n">
<goal name="VC tortoise_and_hare.26.0" expl="assertion" proved="true">
<transf name="assert" proved="true" arg1="(exists k. k &gt;= 1 /\ i = k * lambda)">
<transf name="case" proved="true" arg1="(lam = 0)">
<goal name="VC tortoise_and_hare.26.0" expl="true case (assertion)" proved="true">
<transf name="assert" proved="true" arg1="(lambda &gt;= mu)">
<goal name="VC tortoise_and_hare.26.0.0" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC tortoise_and_hare.26.0.1" expl="assertion" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="VC tortoise_and_hare.26.0.1.0" expl="assertion" proved="true">
<transf name="case" proved="true" arg1="(k=1)">
<goal name="VC tortoise_and_hare.26.0.1.0.0" expl="true case (assertion)" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
<transf name="case" proved="true" arg1="(lambda &lt; mu)">
<goal name="VC tortoise_and_hare.26.0.0.0" expl="true case" proved="true">
<transf name="assert" proved="true" arg1="(x (n + lambda) &lt;&gt; x n)">
<goal name="VC tortoise_and_hare.26.0.0.0.0" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.26.0.1.0.1" expl="false case (assertion)" proved="true">
<transf name="assert" proved="true" arg1="(x (n + (k-1) * lambda) = x n)">
<goal name="VC tortoise_and_hare.26.0.1.0.1.0" proved="true">
<proof prover="6"><result status="valid" time="0.52"/></proof>
<goal name="VC tortoise_and_hare.26.0.0.0.1" expl="true case" proved="true">
<transf name="assert" proved="true" arg1="(x (n + lambda) = x n)">
<goal name="VC tortoise_and_hare.26.0.0.0.1.0" proved="true">
<transf name="instantiate" proved="true" arg1="H18" arg2="(n+lambda),n">
<goal name="VC tortoise_and_hare.26.0.0.0.1.0.0" proved="true">
<proof prover="6"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.26.0.1.0.1.1" expl="false case (assertion)" proved="true">
<proof prover="6"><result status="valid" time="0.60"/></proof>
<goal name="VC tortoise_and_hare.26.0.0.0.1.1" expl="true case" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.26.0.0.1" expl="false case" proved="true">
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.26.0.1" expl="true case (assertion)" proved="true">
<transf name="destruct" proved="true" arg1="H10">
<goal name="VC tortoise_and_hare.26.0.1.0" expl="true case (assertion)" proved="true">
<transf name="assert" proved="true" arg1="(n = lambda \/ n = 2*lambda)">
<goal name="VC tortoise_and_hare.26.0.1.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="36"/></proof>
</goal>
<goal name="VC tortoise_and_hare.26.0.1.0.1" expl="true case (assertion)" proved="true">
<proof prover="6"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.26.1" expl="false case (assertion)" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.27" expl="postcondition" proved="true">
......
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