Theory TortoiseHare

(*<*)
theory TortoiseHare
imports
  Basis
begin

(*>*)
section‹ The Tortoise and the Hare \label{sec:th} ›

text (in properties) ‹

The key to the Tortoise and Hare algorithm is that any @{term "nu"}
such that @{term "seq (nu + nu) = seq nu"} must be divisible by @{term
"lambda"}. Intuitively the first @{term "nu"} steps get us into the
loop. If the second @{term "nu"} steps return us to the same value of
the sequence, then we must have gone around the loop one or more
times.

›

lemma (in properties) lambda_dvd_nu:
  assumes "seq (i + i) = seq i"
  shows "lambda dvd i"
proof(cases "i = 0")
  case False
  with assms have "mu ≤ i" by (auto simp: properties_loops_ge_mu)
  with assms have "seq (i + i mod lambda) = seq i"
    using properties_loop[where i="i + i mod lambda" and j="i div lambda"] by simp
  from properties_distinct_contrapos[OF this] show ?thesis
    by simp (meson dvd_eq_mod_eq_0 mod_less_divisor not_less properties_lambda_gt_0)
qed simp

text (in properties) ‹

The program is split into three loops; we find @{term "nu"}, @{term
"mu"} and @{term "lambda"} in that order.

›

subsection‹ Finding ‹nu› ›

text‹

The state space of the program tracks each of the variables we wish to
discover, and the current positions of the Tortoise and Hare.

›

record 'a state =
  nu :: nat ― ‹‹ν››
  m :: nat  ― ‹‹μ››
  l :: nat  ― ‹‹λ››
  hare :: "'a"
  tortoise :: "'a"

context properties
begin

text‹

The Hare proceeds at twice the speed of the Tortoise. The program
tracks how many steps the Tortoise has taken in @{term "nu"}.

›

definition (in fx0) find_nu :: "'a state ⇒ 'a state" where
  "find_nu ≡
    (λs. s⦇ nu := 1, tortoise := f(x0), hare := f(f(x0)) ⦈) ;;
    while (hare ❙≠ tortoise)
          (λs. s⦇ nu := nu s + 1, tortoise := f(tortoise s), hare := f(f(hare s)) ⦈)"

text‹

If this program terminates, we expect ‹seq ∘ (nu
❙+ nu) ❙= seq ∘ nu› to hold in the final state.

The simplest approach to showing termination is to define a suitable
‹nu› in terms of ‹lambda› and ‹mu›, which also
gives us an upper bound on the number of calls to ‹f›.

›

definition nu_witness :: nat where
  "nu_witness ≡ mu + lambda - mu mod lambda"

text‹

This constant has the following useful properties:

›

lemma nu_witness_properties:
  "mu < nu_witness"
  "nu_witness ≤ lambda + mu"
  "lambda dvd nu_witness"
  "mu = 0 ⟹ nu_witness = lambda"
unfolding nu_witness_def
using properties_lambda_gt_0
apply (simp_all add: less_diff_conv divide_simps)
apply (metis minus_mod_eq_div_mult [symmetric] dvd_def mod_add_self2 mult.commute)
done

text‹

These demonstrate that @{term "nu_witness"} has the key property:

›

lemma nu_witness:
  shows "seq (nu_witness + nu_witness) = seq nu_witness"
using nu_witness_properties properties_loop
by (clarsimp simp: dvd_def field_simps)

text‹

Termination amounts to showing that the Tortoise gets closer to @{term
"nu_witness"} on each iteration of the loop.

›

definition find_nu_measure :: "(nat × nat) set" where
  "find_nu_measure ≡ measure (λν. nu_witness - ν)"

lemma find_nu_measure_wellfounded:
  "wf find_nu_measure"
by (simp add: find_nu_measure_def)

lemma find_nu_measure_decreases:
  assumes "seq (ν + ν) ≠ seq ν"
  assumes "ν ≤ nu_witness"
  shows "(Suc ν, ν) ∈ find_nu_measure"
using nu_witness_properties nu_witness assms
by (auto simp: find_nu_measure_def le_eq_less_or_eq)

text‹

The remainder of the Hoare proof is straightforward.

›

lemma find_nu:
  "⦃⟨True⟩⦄ find_nu ⦃nu ❙∈ ⟨{0<..lambda + mu}⟩ ❙∧ seq ∘ (nu ❙+ nu) ❙= seq ∘ nu ❙∧ hare ❙= seq ∘ nu⦄"
apply (simp add: find_nu_def)
apply (rule hoare_pre)
 apply (rule whileI[where I="nu ❙∈ ⟨{0<..nu_witness}⟩ ❙∧ (❙∀i. ⟨0 < i⟩ ❙∧ ⟨i⟩ ❙< nu ❙⟶ ⟨seq (i + i) ≠ seq i⟩)
                            ❙∧ tortoise ❙= seq ∘ nu ❙∧ hare ❙= seq ∘ (nu ❙+ nu)"
                       and r="inv_image find_nu_measure nu"]
             wp_intro)+
    using nu_witness_properties nu_witness
    apply (fastforce simp: le_eq_less_or_eq elim: less_SucE)
   apply (simp add: find_nu_measure_wellfounded)
  apply (simp add: find_nu_measure_decreases)
 apply (rule wp_intro)
using nu_witness_properties
apply auto
done


subsubsection‹ Side observations ›

text‹

We can also show termination ala \<^citet>‹"Filliatre:2007"›.

›

definition find_nu_measures :: "(nat × nat) set" where
  "find_nu_measures ≡
    measures [λν. mu - ν, λν. LEAST i. seq (ν + ν + i) = seq ν]"

lemma find_nu_measures_wellfounded:
  "wf find_nu_measures"
by (simp add: find_nu_measures_def)

lemma find_nu_measures_existence:
  assumes ν: "mu ≤ ν"
  shows "∃i. seq (ν + ν + i) = seq ν"
proof(cases "seq (ν + ν) = seq ν")
 case False
 from properties_lambda_gt_0 obtain k where k: "ν ≤ k * lambda"
   by (metis One_nat_def Suc_leI mult.right_neutral mult_le_mono order_refl)
 from ν k have "seq (ν + ν + (k * lambda - ν)) = seq (mu + (ν - mu) + k * lambda)" by (simp add: field_simps)
 also from ν properties_loop have "… = seq ν" by simp
 finally show ?thesis by blast
qed (simp add: exI[where x=0])

lemma find_nu_measures_decreases:
  assumes ν: "seq (ν + ν) ≠ seq ν"
  shows "(Suc ν, ν) ∈ find_nu_measures"
proof(cases "mu ≤ ν")
  case True
  then have "mu ≤ Suc ν" by simp
  have "(LEAST i. seq (Suc ν + Suc ν + i) = seq (Suc ν)) < (LEAST i. seq (ν + ν + i) = seq ν)"
  proof(rule LeastI2_wellorder_ex[OF find_nu_measures_existence[OF ‹mu ≤ Suc ν›]],
        rule LeastI2_wellorder_ex[OF find_nu_measures_existence[OF ‹mu ≤ ν›]])
    fix x y
    assume x: "seq (Suc ν + Suc ν + x) = seq (Suc ν)"
              "∀z. seq (Suc ν + Suc ν + z) = seq (Suc ν) ⟶ x ≤ z"
    assume y: "seq (ν + ν + y) = seq ν"
    from ν ‹mu ≤ ν› y have "0 < y" by (cases y) simp_all
    with y have "seq (Suc ν + Suc ν + (y - 1)) = seq (Suc ν)" by (auto elim: seq_inj)
    with ‹0 < y› spec[OF x(2), where x="y - 1"] y show "x < y" by simp
  qed
  with True ν show ?thesis by (simp add: find_nu_measures_def)
qed (auto simp: find_nu_measures_def)

lemma "find_nu_Filliâtre":
  "⦃⟨True⟩⦄ find_nu ⦃⟨0⟩ ❙< nu ❙∧ seq ∘ (nu ❙+ nu) ❙= seq ∘ nu ❙∧ hare ❙= seq ∘ nu⦄"
apply (simp add: find_nu_def)
apply (rule hoare_pre)
 apply (rule whileI[where I="⟨0⟩ ❙< nu ❙∧ tortoise ❙= seq ∘ nu ❙∧ hare ❙= seq ∘ (nu ❙+ nu)"
                      and r="inv_image find_nu_measures nu"]
             wp_intro)+
    apply clarsimp
   apply (simp add: find_nu_measures_wellfounded)
  apply (simp add: find_nu_measures_decreases)
 apply (rule wp_intro)
apply (simp add: properties_lambda_gt_0)
done

text‹

This approach does not provide an upper bound on ‹nu› however.

\<^cite>‹"Harper:PiSML:2011"› observes (in his \S13.5.2) that if ‹mu› is zero then ‹nu = lambda›.

›

lemma Harper:
  assumes "mu = 0"
  shows "⦃⟨True⟩⦄ find_nu ⦃nu ❙= ⟨lambda⟩⦄"
by (rule hoare_post_imp[OF find_nu]) (fastforce simp: assms dvd_def dest: lambda_dvd_nu)


subsection‹ Finding ‹mu› \label{sec:th-finding-mu} ›

text‹

We recover ‹mu› from ‹nu› by exploiting the fact that
lambda divides @{term "nu"}: the Tortoise, reset to @{term "x0"}
and the Hare, both now moving at the same speed, will meet at @{term
"mu"}.

›

lemma mu_nu:
  assumes si: "seq (i + i) = seq i"
  assumes j: "mu ≤ j"
  shows "seq (j + i) = seq j"
using lambda_dvd_nu[OF si] properties_loop[OF j]
by (clarsimp simp: dvd_def field_simps)

definition (in fx0) find_mu :: "'a state ⇒ 'a state" where
  "find_mu ≡
    (λs. s⦇ m := 0, tortoise := x0 ⦈) ;;
    while (hare ❙≠ tortoise)
          (λs. s⦇ tortoise := f (tortoise s), hare := f (hare s), m := m s + 1 ⦈)"

lemma find_mu:
  "⦃nu ❙∈ ⟨{0<..lambda + mu}⟩ ❙∧ seq ∘ (nu ❙+ nu) ❙= seq ∘ nu ❙∧ hare ❙= seq ∘ nu⦄
     find_mu
   ⦃nu ❙∈ ⟨{0<..lambda + mu}⟩ ❙∧ tortoise ❙= ⟨seq mu⟩ ❙∧ m ❙= ⟨mu⟩⦄"
apply (simp add: find_mu_def)
apply (rule hoare_pre)
 apply (rule whileI[where I="nu ❙∈ ⟨{0<..lambda + mu}⟩ ❙∧ seq ∘ (nu ❙+ nu) ❙= seq ∘ nu ❙∧ m ❙≤ ⟨mu⟩
                           ❙∧ tortoise ❙= seq ∘ m ❙∧ hare ❙= seq ∘ (m ❙+ nu)"
                      and r="measure (⟨mu⟩ ❙- m)"]
             wp_intro)+
    using properties_loops_ge_mu
    apply (force dest: mu_nu simp: less_eq_Suc_le[symmetric])
   apply simp
  apply (force dest: mu_nu simp: le_eq_less_or_eq)
 apply (rule wp_intro)
apply simp
done


subsection‹ Finding ‹lambda› ›

text‹

With the Tortoise parked at @{term "mu"}, we find ‹lambda› by
walking the Hare around the loop.

›

definition (in fx0) find_lambda :: "'a state ⇒ 'a state" where
  "find_lambda ≡
    (λs. s⦇ l := 1, hare := f (tortoise s) ⦈) ;;
    while (hare ❙≠ tortoise)
          (λs. s⦇ hare := f (hare s), l := l s + 1 ⦈)"

lemma find_lambda:
  "⦃nu ❙∈ ⟨{0<..lambda + mu}⟩ ❙∧ tortoise ❙= ⟨seq mu⟩ ❙∧ m ❙= ⟨mu⟩⦄
     find_lambda
   ⦃nu ❙∈ ⟨{0<..lambda + mu}⟩ ❙∧ l ❙= ⟨lambda⟩ ❙∧ m ❙= ⟨mu⟩⦄"
apply (simp add: find_lambda_def)
apply (rule hoare_pre)
 apply (rule whileI[where I="nu ❙∈ ⟨{0<..lambda + mu}⟩ ❙∧ l ❙∈ ⟨{0<..lambda}⟩
                           ❙∧ tortoise ❙= ⟨seq mu⟩ ❙∧ hare ❙= seq ∘ (⟨mu⟩ ❙+ l) ❙∧ m ❙= ⟨mu⟩"
                      and r="measure (⟨lambda⟩ ❙- l)"]
             wp_intro)+
    using properties_lambda_gt_0 properties_mod_lambda[where i="mu + lambda"] properties_distinct[where i=mu]
    apply (fastforce simp: less_eq_Suc_le[symmetric])
   apply simp
  using properties_mod_lambda[where i="mu + lambda"]
  apply (fastforce simp: le_eq_less_or_eq)
 apply (rule wp_intro)
using properties_lambda_gt_0
apply simp
done


subsection‹ Top level ›

text‹

The complete program is simply the steps composed in order.

›

definition (in fx0) tortoise_hare :: "'a state ⇒ 'a state" where
  "tortoise_hare ≡ find_nu ;; find_mu ;; find_lambda"

theorem tortoise_hare:
  "⦃⟨True⟩⦄ tortoise_hare ⦃nu ❙∈ ⟨{0<..lambda + mu}⟩ ❙∧ l ❙= ⟨lambda⟩ ❙∧ m ❙= ⟨mu⟩⦄"
unfolding tortoise_hare_def
by (rule find_nu find_mu find_lambda wp_intro)+

end

corollary tortoise_hare_correct:
  assumes s': "s' = fx0.tortoise_hare f x arbitrary"
  shows "fx0.properties f x (l s') (m s')"
using assms properties.tortoise_hare[where f=f and ?x0.0=x]
by (fastforce intro: fx0.properties_existence[where f=f and ?x0.0=x]
               simp:  Basis.properties_def valid_def)

text‹

Isabelle can generate code from these definitions.

›

schematic_goal tortoise_hare_code[code]:
  "fx0.tortoise_hare f x = ?code"
unfolding fx0.tortoise_hare_def fx0.find_nu_def fx0.find_mu_def fx0.find_lambda_def fcomp_assoc[symmetric] fcomp_comp
by (rule refl)

export_code fx0.tortoise_hare in SML
(*<*)

end
(*>*)