Theory Brent

(*<*)
theory Brent
imports
  Basis
begin
(*>*)
section‹ Brent's algorithm \label{sec:brent} ›

text‹

\<^cite>‹"Brent:1980"› improved on the Tortoise and Hare algorithm and
used it to factor large primes. In practice it makes significantly
fewer calls to the function ‹f› before detecting a loop.

We begin by defining the base-2 logarithm.

›

fun lg :: "nat ⇒ nat" where
[simp del]: "lg x = (if x ≤ 1 then 0 else 1 + lg (x div 2))"

lemma lg_safe:
  "lg 0 = 0"
  "lg (Suc 0) = 0"
  "lg (Suc (Suc 0)) = 1"
  "0 < x ⟹ lg (x + x) = 1 + lg x"
by (simp_all add: lg.simps)

lemma lg_inv:
  "0 < x ⟹ lg (2 ^ x) = x"
proof(induct x)
  case (Suc x) then show ?case
    by (cases x, simp_all add: lg.simps Suc_lessI not_le)
qed simp

lemma lg_inv2:
  ‹2 ^ lg x = x› if ‹2 ^ i = x› for x
proof -
  have ‹2 ^ lg (2 ^ i) = (2::nat) ^ i›
    by (induction i) (simp_all add: lg_safe mult_2)
  with that show ?thesis
    by simp
qed

lemmas lg_simps = lg_safe lg_inv lg_inv2

subsection‹ Finding ‹lambda› ›

text (in properties) ‹

Imagine now that the Tortoise carries an unbounded number of carrots,
which he passes to the Hare when they meet, and the Hare has a
teleporter. The Hare eats a carrot each time she waits for the
function @{term "f"} to execute, and initially has just one. If she
runs out of carrots before meeting the Tortoise again, she teleports
him to her position, and he gives her twice as many carrots as the
last time they met (tracked by the variable ‹carrots›). By
counting how many carrots she has eaten from when she last teleported
the Tortoise (recorded in ‹l›) until she finally has surplus
carrots when she meets him again, the Hare directly discovers @{term
"lambda"}.

›

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

context properties
begin

definition (in fx0) find_lambda :: "'a state ⇒ 'a state" where
  "find_lambda ≡
    (λs. s⦇ carrots := 1, l := 1, tortoise := x0, hare := f x0 ⦈) ;;
    while (hare ❙≠ tortoise)
          ( ( ❙if carrots ❙= l ❙then (λs. s⦇ tortoise := hare s, carrots := 2 * carrots s, l := 0 ⦈)
                             ❙else SKIP ) ;;
            (λs. s⦇ hare := f (hare s), l := l s + 1 ⦈) )"

text‹

The termination argument goes intuitively as follows. The Hare eats as
many carrots as it takes to teleport the Tortoise into the
loop. Afterwards she continues the teleportation dance until the
Tortoise has given her enough carrots to make it all the way around
the loop and back to him.

We can calculate the Tortoise's position as a function of ‹carrots›.

›

definition carrots_total :: "nat ⇒ nat" where
  "carrots_total c ≡ ∑i<lg c. 2 ^ i"

lemma carrots_total_simps:
  "carrots_total (Suc 0) = 0"
  "carrots_total (Suc (Suc 0)) = 1"
  "2 ^ i = c ⟹ carrots_total (c + c) = c + carrots_total c"
by (auto simp: carrots_total_def lg_simps)

definition find_lambda_measures :: "( (nat × nat) × (nat × nat) ) set" where
  "find_lambda_measures ≡
    measures [λ(l, c). mu - carrots_total c,
              λ(l, c). LEAST i. lambda ≤ c * 2^i,
              λ(l, c). c - l]"

lemma find_lambda_measures_wellfounded:
  "wf find_lambda_measures"
by (simp add: find_lambda_measures_def)

lemma find_lambda_measures_decreases1:
  assumes "c = 2 ^ i"
  assumes "mu ≤ carrots_total c ⟶ c ≤ lambda"
  assumes "seq (carrots_total c) ≠ seq (carrots_total c + c)"
  shows "( (c', 2 * c), (c, c) ) ∈ find_lambda_measures"
proof(cases "mu ≤ carrots_total c")
  case False with assms show ?thesis
    by (auto simp: find_lambda_measures_def carrots_total_simps mult_2 field_simps diff_less_mono2)
next
  case True
  { fix x assume x: "(0::nat) < x" have "∃n. lambda ≤ x * 2 ^ n"
    proof(induct lambda)
      case (Suc i)
      then obtain n where "i ≤ x * 2 ^ n" by blast
      with x show ?case
        by (clarsimp intro!: exI[where x="Suc n"] simp: field_simps mult_2)
           (metis Nat.add_0_right Suc_leI linorder_neqE_nat mult_eq_0_iff add_left_cancel not_le numeral_2_eq_2 old.nat.distinct(2) power_not_zero trans_le_add2)
    qed simp } note ex = this
  have "(LEAST j. lambda ≤ 2 ^ (i + 1) * 2 ^ j) < (LEAST j. lambda ≤ 2 ^ i * 2 ^ j)"
  proof(rule LeastI2_wellorder_ex[OF ex, rotated], rule LeastI2_wellorder_ex[OF ex, rotated])
    fix x y
    assume "lambda ≤ 2 ^ i * 2 ^ y"
           "lambda ≤ 2 ^ (i + 1) * 2 ^ x"
           "∀z. lambda ≤ 2 ^ (i + 1) * 2 ^ z ⟶ x ≤ z"
    with True assms properties_loop[where i="carrots_total c" and j=1]
    show "x < y" by (cases y, auto simp: less_Suc_eq_le)
  qed simp_all
  with True ‹c = 2 ^ i› show ?thesis
    by (clarsimp simp: find_lambda_measures_def mult_2 carrots_total_simps field_simps power_add)
qed

lemma find_lambda_measures_decreases2:
  assumes "ls < c"
  shows "( (Suc ls, c), (ls, c) ) ∈ find_lambda_measures"
using assms by (simp add: find_lambda_measures_def)

lemma find_lambda:
  "⦃⟨True⟩⦄ find_lambda ⦃l ❙= ⟨lambda⟩⦄"
apply (simp add: find_lambda_def)
apply (rule hoare_pre)
apply (rule whileI[where I="⟨0⟩ ❙< l ❙∧ l ❙≤ carrots ❙∧ (⟨mu⟩ ❙≤ carrots_total ∘ carrots ❙⟶ l ❙≤ ⟨lambda⟩) ❙∧ (❙∃i. carrots ❙= ⟨2^i⟩)
                           ❙∧ tortoise ❙= seq ∘ carrots_total ∘ carrots ❙∧ hare ❙= seq ∘ (l ❙+ (carrots_total ∘ carrots))"
                      and r="inv_image find_lambda_measures (l ❙⨝ carrots)"]
            wp_intro)+
   using properties_lambda_gt_0
   apply (clarsimp simp: field_simps mult_2_right carrots_total_simps)
   apply (intro conjI impI)
      apply (metis mult_2 power_Suc)
     apply (case_tac "mu ≤ carrots_total (l s)")
      apply (cut_tac i="carrots_total (l s)" and j="l s" in properties_distinct_contrapos, simp_all add: field_simps)[1]
     apply (cut_tac i="carrots_total (l s)" and j="l s" in properties_loops_ge_mu, simp_all add: field_simps)[1]
    apply (cut_tac i="carrots_total (2 ^ x)" and j=1 in properties_loop, simp)
    apply (fastforce simp: le_eq_less_or_eq field_simps)
   apply (cut_tac i="carrots_total (2 ^ x)" and j="l s" in properties_loops_ge_mu, simp_all add: field_simps)[1]
   apply (cut_tac i="carrots_total (2 ^ x)" and j="l s" in properties_distinct_contrapos, simp_all add: field_simps)[1]
  apply (simp add: find_lambda_measures_wellfounded)
 apply (clarsimp simp: add.commute find_lambda_measures_decreases1 find_lambda_measures_decreases2)
apply (rule wp_intro)
using properties_lambda_gt_0
apply (simp add: carrots_total_simps exI[where x=0])
done

subsection‹ Finding ‹mu› ›

text‹

With @{term "lambda"} in hand, we can find ‹mu› using the same
approach as for the Tortoise and Hare (\S\ref{sec:th-finding-mu}),
after we first move the Hare to @{term "lambda"}.

›

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

lemma find_mu:
  "⦃l ❙= ⟨lambda⟩⦄ find_mu ⦃l ❙= ⟨lambda⟩ ❙∧ m ❙= ⟨mu⟩⦄"
apply (simp add: find_mu_def)
apply (rule hoare_pre)
apply (rule whileI[where I="l ❙= ⟨lambda⟩ ❙∧ m ❙≤ ⟨mu⟩ ❙∧ tortoise ❙= seq ∘ m ❙∧ hare ❙= seq ∘ (m ❙+ l)"
                      and r="measure (⟨mu⟩ ❙- m)"]
            wp_intro)+
   using properties_lambda_gt_0 properties_loop[where i=mu and j=1]
   apply (fastforce simp: le_less dest: properties_loops_ge_mu)
  apply simp
 using properties_loop[where i=mu and j=1, simplified]
 apply (fastforce simp: le_eq_less_or_eq)
apply (rule wp_intro)
apply simp
done


subsection‹ Top level ›

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

theorem brent:
  "⦃⟨True⟩⦄ brent ⦃l ❙= ⟨lambda⟩ ❙∧ m ❙= ⟨mu⟩⦄"
unfolding brent_def
by (rule find_lambda find_mu wp_intro)+

end

corollary brent_correct:
  assumes s': "s' = fx0.brent f x arbitrary"
  shows "fx0.properties f x (l s') (m s')"
using assms properties.brent[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)

schematic_goal brent_code[code]:
  "fx0.brent f x = ?code"
unfolding fx0.brent_def fx0.find_lambda_def fx0.find_mu_def fcomp_assoc[symmetric] fcomp_comp
by (rule refl)

export_code fx0.brent in SML
(*<*)

end
(*>*)