# Library TortoiseHareAlgorithm.TortoiseHareAlgorithm

Correctness proof of Floyd's cycle-finding algorithm, also known as the "tortoise and the hare"-algorithm (see http://en.wikipedia.org/wiki/Floyd's_cycle-finding_algorithm)

If is a function over a finite set , then the iterations of from will ultimately cycle. The following code finds out an integer such that :
```let rec race m x y = if x = y then m else race (m+1) (f x) (f (f y))
in race 1 (f x0) (f (f x0))
```
The difficulty is to prove 's termination.

Require Export Arith.
Require Export Omega.
Open Scope nat_scope.

Let f be a function over a set A

Parameter A : Set.
Parameter eq_A_dec : forall (x y:A), {x=y}+{~x=y}.
Parameter f : A -> A.
Parameter x0 : A.

We consider the sequence

Fixpoint x (i:nat) { struct i } : A := match i with
| O => x0
| S j => f (x j)
end.

We assume this sequence cycles after lambda+mu iterations, mu being the length of the cycle (we actually don't require lambda and mu to be minimal, because it is not needed for the remaining of the proof

Parameter lambda : nat.
Parameter mu : nat.
Axiom mu_positive : mu > 0.
Axiom lambda_mu : forall i j, x (lambda+i) = x (lambda+i+j*mu).

Hilbert's epsilon operator.

Parameter epsilon : (nat -> Prop) -> nat.
Axiom epsilon_spec : forall P, ex P -> P (epsilon P).

The distance between x (2m) and x m defined using epsilon

Definition sep_x2m_xm m i := x (2*m+i) = x m.

Definition min P i := P i /\ forall j, P j -> i <= j.

Definition dist_x2m_xm m := epsilon (min (sep_x2m_xm m)).

Existence of this distance whenever lambda <= m

Axiom ex_min_P : forall P, (forall x, {P x}+{~(P x)}) -> ex P -> ex (min P).

Axiom div : forall a, a > 0 -> forall b, exists k, k*a >= b.

Lemma ex_dist_x2m_xm : forall m, lambda <= m -> ex (min (sep_x2m_xm m)).
Proof.
intros m hm; apply ex_min_P.
intro i; unfold sep_x2m_xm.
case (eq_A_dec (x (2 * m + i)) (x m)); auto.
generalize (div mu mu_positive m); intros (k,hk).
exists (k*mu - m); unfold sep_x2m_xm.
replace (2 * m + (k * mu - m)) with (lambda + (m-lambda)+k*mu) by omega.
rewrite <- lambda_mu.
replace (lambda+(m-lambda)) with m by omega; auto.
Qed.

Variant to prove the termination of Floyd's algorithm:
• either x m has not entered the loop yet and lambda-m is decreasing
• or bot x m and x (2m) are inside the loop and the distance between x (2m) and x m is decreasing
Thus we use a lexicographic order.

Definition variant m := (lambda - m, dist_x2m_xm m).

Definition lex x y := fst x < fst y \/ (fst x = fst y /\ snd x < snd y).

Correctness proof

Theorem rec_call_is_wf :
forall m, x m <> x (2*m) -> lex (variant (S m)) (variant m).
Proof.
unfold lex,variant; simpl.
intros.
assert (h: m < lambda \/ m >= lambda) by omega.
destruct h.
left; omega.
right.
split; auto with *.
unfold dist_x2m_xm.
assert (exd1: ex (min (sep_x2m_xm (S m)))).
apply ex_dist_x2m_xm; auto with *.
generalize (epsilon_spec (min (sep_x2m_xm (S m))) exd1).
assert (exd0: ex (min (sep_x2m_xm m))).
apply ex_dist_x2m_xm; auto with *.
generalize (epsilon_spec (min (sep_x2m_xm m)) exd0).
generalize (epsilon (min (sep_x2m_xm m))).
generalize (epsilon (min (sep_x2m_xm (S m)))).
intros d1 d0.
unfold min,sep_x2m_xm.
intros (h1,h2) (h3,h4).
assert (x (S(2*m+d0)) = x (S m)).
simpl; simpl in h1; congruence.
assert (d0 > 0).
assert (h: d0=0 \/ d0>0) by omega. destruct h; auto.
subst d0; absurd (x (2*m)=x m); auto.
replace (2*m+0) with (2*m) in h1; auto.
assert (d1 <= d0-1).
apply h4.
replace (2 * (S m) + (d0 - 1)) with (S (2 * m + d0)) by omega.
auto.
omega.
Save.

Definition R x y := lex (variant x) (variant y).
Axiom R_wf : well_founded R.

Definition find_cycle_rec :
forall (m:nat) (xm x2m:A), m > 0 -> xm=x m -> x2m=x (2*m) ->
{ m:nat | m > 0 /\ x m = x (2*m) }.
Proof.
induction m using (well_founded_induction R_wf).
intros xm x2m h hm h2m.
destruct (eq_A_dec xm x2m).
exists m; subst xm x2m; auto.
apply (H (S m)) with (f xm) (f (f x2m)); subst xm x2m; auto with *.
unfold R; apply rec_call_is_wf; auto.
replace (2*(S m)) with (S (S (2*m))) by omega; auto.
Defined.

Definition find_cycle : { m:nat | m > 0 /\ x m = x (2*m) }.
Proof.
apply (find_cycle_rec (S O) (f x0) (f (f x0))); auto with *.
Defined.