diff --git a/examples/tortoise_and_hare.mlw b/examples/tortoise_and_hare.mlw index cbfd1deb6c704d15a893376097b7ccacd15b3314..d80e2ab8164d5928e89cf4cdacd0894a1c136881 100644 --- a/examples/tortoise_and_hare.mlw +++ b/examples/tortoise_and_hare.mlw @@ -3,88 +3,162 @@ See The Art of Computer Programming, vol 2, exercise 6 page 7. *) -module TortoiseAndHare +module TortoiseAndHareAlgorithm use import int.Int - use int.Iter + use import int.EuclideanDivision + use import int.Iter + use import seq.Seq + use import seq.Distinct + use import ref.Refint + use import pigeon.Pigeonhole - type t - val predicate eq (x y : t) - ensures { result <-> x = y } + val function f int : int - (* let f be a function from t to t *) - val function f t : t + (* f maps 0..m-1 to 0..m-1 *) + constant m: int + axiom m_positive: m > 0 + + axiom f_range: forall x. 0 <= x < m -> 0 <= f x < m (* given some initial value x0 *) - val constant x0: t + val constant x0: int + ensures { 0 <= result < m } (* we can build the infinite sequence defined by x{i+1} = f(xi) *) - function x (i: int): t = Iter.iter f i x0 - - (* let use assume now that the sequence (x_i) has finitely many distinct - values (e.g. f is an integer function with values in 0..m) - - it means that there exists values lambda and mu such that - (1) x0, x1, ... x{mu+lambda-1} are all distinct, - and - (2) x{n+lambda} = x_n when n >= mu. *) - - (* lambda and mu are skomlemized *) - constant mu : int - constant lambda : int - - (* they are axiomatized as follows *) - axiom mu_range: 0 <= mu - - axiom lambda_range: 1 <= lambda - - axiom distinct: - forall i j: int. 0 <= i < mu+lambda -> 0 <= j < mu+lambda -> - i <> j -> x i <> x j - - axiom cycle: forall n: int. mu <= n -> x (n + lambda) = x n - - lemma cycle_induction: - forall n: int. mu <= n -> forall k: int. 0 <= k -> x (n + lambda * k) = x n - - (* Now comes the code. - Two references, tortoise and hare, traverses the sequence (xi) - at speed 1 and 2 respectively. We stop whenever they are equal. - - The challenge is to prove termination. - Actually, we even prove that the code runs in time O(lambda + mu). *) - - use import ref.Ref - use import relations.WellFounded - - (* the minimal distance between x i and x j *) - function dist int int : int - - (* it is defined as soon as i,j >= mu *) - axiom dist_def: forall i j: int. mu <= i -> mu <= j -> - dist i j >= 0 /\ - x (i + dist i j) = x j /\ - forall k: int. 0 <= k -> x (i + k) = x j -> dist i j <= k - - predicate rel (t2 t1: t) = - exists i: int. t1 = x i /\ t2 = x (i+1) /\ 1 <= i <= mu + lambda /\ - (i >= mu -> dist (2*i+2) (i+1) < dist (2*i) i) - - axiom wfrel: well_founded rel - - let tortoise_hare () = + function x (i: int): int = iter f i x0 + + let rec lemma x_in_range (n: int) + requires { 0 <= n } ensures { 0 <= x n < m } + variant { n } + = if n > 0 then x_in_range (n - 1) + + (* First, we prove the existence of mu and lambda, with a ghost program. + Starting with x0, we repeteadly apply f, storing the elements in + a sequence, until we find a repetition. *) + let ghost periodicity () : (int, int) + returns { mu, lambda -> + 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\ + x (mu + lambda) = x mu /\ + forall i j. 0 <= i < j < mu + lambda -> x i <> x j + } + = let s = ref (singleton x0) in + let cur = ref x0 in + for k = 1 to m do + invariant { 1 <= length !s = k <= m /\ !cur = !s[length !s - 1] } + invariant { forall i. 0 <= i < length !s -> !s[i] = x i } + invariant { distinct !s } + cur := f !cur; + (* look for a repetition *) + for mu = 0 to length !s - 1 do + invariant { forall i. 0 <= i < mu -> !s[i] <> !cur } + if !cur = !s[mu] then return (mu, length !s - mu) + done; + s := snoc !s !cur; + if k = m then pigeonhole (m+1) m (pure { fun i -> !s[i] }) + done; + absurd + + (* Then we can state the condition for two elements to be equal. *) + let lemma equality (mu lambda: int) + requires { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\ + x (mu + lambda) = x mu } + requires { forall i j. 0 <= i < j < mu + lambda -> x i <> x j } + ensures { forall r n. r > n >= 0 -> + x r = x n <-> n >= mu /\ exists k. k >= 1 /\ r-n = k*lambda } + = let rec lemma plus_lambda (n: int) variant { n } + requires { mu <= n } + ensures { x (n + lambda) = x n } = + if n > mu then plus_lambda (n - 1) in + let rec lemma plus_lambdas (n k: int) variant { k } + requires { mu <= n } requires { 0 <= k } + ensures { x (n + k * lambda) = x n } = + if k > 0 then begin + plus_lambdas n (k - 1); plus_lambda (n + (k - 1) * lambda) end in + let decomp (i: int) : (int, int) + requires { i >= mu } + returns { qi,mi -> i = mu + qi * lambda + mi && qi >= 0 && + 0 <= mi < lambda && x i = x (mu + mi) } = + let qi = div (i - mu) lambda in + let mi = mod (i - mu) lambda in + plus_lambdas (mu + mi) qi; + qi, mi in + let lemma equ (r n: int) + requires { r > n >= 0 } requires { x r = x n } + ensures { n >= mu /\ exists k. k >= 1 /\ r-n = k*lambda } = + if n < mu then (if r >= mu then let _ = decomp r in absurd) + else begin + let qr,mr = decomp r in let qn, mn = decomp n in + assert { mr = mn }; + assert { r-n = (qr-qn) * lambda } + end in + () + + (* Finally, we implement the tortoise and hare algorithm that computes + the values of mu and lambda in linear time and constant space *) + let tortoise_and_hare () : (int, int) + returns { mu, lambda -> + 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\ + x (mu + lambda) = x mu /\ + forall i j. 0 <= i < j < mu + lambda -> x i <> x j + } + = 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) *) let tortoise = ref (f x0) in let hare = ref (f (f x0)) in - while not (eq !tortoise !hare) do + let n = ref 1 in + while !tortoise <> !hare do invariant { - exists t: int. - 1 <= t <= mu+lambda /\ !tortoise = x t /\ !hare = x (2 * t) /\ - forall i: int. 1 <= i < t -> x i <> x (2*i) } - variant { !tortoise with rel } + 1 <= !n <= mu+lambda /\ !tortoise = x !n /\ !hare = x (2 * !n) /\ + forall i. 1 <= i < !n -> x i <> x (2*i) } + variant { mu + lambda - !n } tortoise := f !tortoise; - hare := f (f !hare) - done - - (* TODO: code to find out lambda and mu. See wikipedia. *) + hare := f (f !hare); + incr n; + if !n > mu + lambda then begin + let m = lambda - mod mu lambda in + let i = mu + m in + assert { 2*i - i = (div mu lambda + 1) * lambda }; + absurd + end + done; + let n = !n in + assert { n >= mu }; + 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 *) + let i = ref 0 in + let xi = ref x0 in (* = x i *) + let xni = ref xn in (* = x (n+i) *) + 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) } + variant { mu - !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 end diff --git a/examples/tortoise_and_hare/why3session.xml b/examples/tortoise_and_hare/why3session.xml index dc0139e7f3055c326f36606afe4efbaea4c6f5ed..193523bdf0c475c2a28454578e11938f22a133c5 100644 --- a/examples/tortoise_and_hare/why3session.xml +++ b/examples/tortoise_and_hare/why3session.xml @@ -2,30 +2,370 @@ - - - - + + + + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + diff --git a/examples/tortoise_and_hare/why3shapes.gz b/examples/tortoise_and_hare/why3shapes.gz index 018df525ad04fa02c183c9992cd539081db4946d..93fa28bc56a5fbd5c1b12e88ef3845e4a9d5e570 100644 Binary files a/examples/tortoise_and_hare/why3shapes.gz and b/examples/tortoise_and_hare/why3shapes.gz differ