Theory Master_Theorem_Examples

(*
  File:   Master_Theorem_Examples.thy
  Author: Manuel Eberl <manuel@pruvisto.org>

  Examples for the application of the Master theorem and related proof methods.
*)

section ‹Examples›
theory Master_Theorem_Examples
imports
  Complex_Main
  Akra_Bazzi_Method
  Akra_Bazzi_Approximation
begin

subsection ‹Merge sort›

(* A merge sort cost function that is parametrised with the recombination costs *)
function merge_sort_cost :: "(nat ⇒ real) ⇒ nat ⇒ real" where
  "merge_sort_cost t 0 = 0"
| "merge_sort_cost t 1 = 1"
| "n ≥ 2 ⟹ merge_sort_cost t n = 
     merge_sort_cost t (nat ⌊real n / 2⌋) + merge_sort_cost t (nat ⌈real n / 2⌉) + t n"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma merge_sort_nonneg[simp]: "(⋀n. t n ≥ 0) ⟹ merge_sort_cost t x ≥ 0"
  by (induction t x rule: merge_sort_cost.induct) (simp_all del: One_nat_def)

lemma "t ∈ Θ(λn. real n) ⟹ (⋀n. t n ≥ 0) ⟹ merge_sort_cost t ∈ Θ(λn. real n * ln (real n))"
  by (master_theorem 2.3) simp_all

subsection ‹Karatsuba multiplication›

function karatsuba_cost :: "nat ⇒ real" where
  "karatsuba_cost 0 = 0"
| "karatsuba_cost 1 = 1"
| "n ≥ 2 ⟹ karatsuba_cost n = 
     3 * karatsuba_cost (nat ⌈real n / 2⌉) + real n"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma karatsuba_cost_nonneg[simp]: "karatsuba_cost n ≥ 0"
  by (induction n rule: karatsuba_cost.induct) (simp_all del: One_nat_def)

lemma "karatsuba_cost ∈ O(λn. real n powr log 2 3)"
   by (master_theorem 1 p': 1) (simp_all add: powr_divide)

lemma karatsuba_cost_pos: "n ≥ 1 ⟹ karatsuba_cost n > 0"
  by (induction n rule: karatsuba_cost.induct) (auto intro!: add_nonneg_pos simp del: One_nat_def)

lemma "karatsuba_cost ∈ Θ(λn. real n powr log 2 3)"
  using karatsuba_cost_pos
  by (master_theorem 1 p': 1) (auto simp add: powr_divide eventually_at_top_linorder)


subsection ‹Strassen matrix multiplication›

function strassen_cost :: "nat ⇒ real" where
  "strassen_cost 0 = 0"
| "strassen_cost 1 = 1"
| "n ≥ 2 ⟹ strassen_cost n = 7 * strassen_cost (nat ⌈real n / 2⌉) + real (n^2)"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma strassen_cost_nonneg[simp]: "strassen_cost n ≥ 0"
  by (induction n rule: strassen_cost.induct) (simp_all del: One_nat_def)

lemma "strassen_cost ∈ O(λn. real n powr log 2 7)"
  by (master_theorem 1 p': 2) (auto simp: powr_divide eventually_at_top_linorder)

lemma strassen_cost_pos: "n ≥ 1 ⟹ strassen_cost n > 0"
  by (cases n rule: strassen_cost.cases) (simp_all add: add_nonneg_pos del: One_nat_def)

lemma "strassen_cost ∈ Θ(λn. real n powr log 2 7)"
  using strassen_cost_pos
  by (master_theorem 1 p': 2) (auto simp: powr_divide eventually_at_top_linorder)


subsection ‹Deterministic select›

(* This is not possible with the standard Master theorem from literature *)
function select_cost :: "nat ⇒ real" where
  "n ≤ 20 ⟹ select_cost n = 0"
| "n > 20 ⟹ select_cost n = 
     select_cost (nat ⌊real n / 5⌋) + select_cost (nat ⌊7 * real n / 10⌋ + 6) + 12 * real n / 5"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma "select_cost ∈ Θ(λn. real n)"
  by (master_theorem 3) auto


subsection ‹Decreasing function›

function dec_cost :: "nat ⇒ real" where
  "n ≤ 2 ⟹ dec_cost n = 1"
| "n > 2 ⟹ dec_cost n = 0.5*dec_cost (nat ⌊real n / 2⌋) + 1 / real n"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma "dec_cost ∈ Θ(λx::nat. ln x / x)"
  by (master_theorem 2.3) simp_all


subsection ‹Example taken from Drmota and Szpakowski›

function drmota1 :: "nat ⇒ real" where
  "n < 20 ⟹ drmota1 n = 1"
| "n ≥ 20 ⟹ drmota1 n = 2 * drmota1 (nat ⌊real n/2⌋) + 8/9 * drmota1 (nat ⌊3*real n/4⌋) + real n^2 / ln (real n)"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma "drmota1 ∈ Θ(λn::real. n^2 * ln (ln n))"
  by (master_theorem 2.2) (simp_all add: power_divide)


function drmota2 :: "nat ⇒ real" where
  "n < 20 ⟹ drmota2 n = 1"
| "n ≥ 20 ⟹ drmota2 n = 1/3 * drmota2 (nat ⌊real n/3 + 1/2⌋) + 2/3 * drmota2 (nat ⌊2*real n/3 - 1/2⌋) + 1"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma "drmota2 ∈ Θ(λx. ln (real x))"
  by master_theorem simp_all

(* Average phrase length of Boncelet arithmetic coding. See Drmota and Szpankowski. *)
lemma boncelet_phrase_length:
  fixes p δ :: real assumes p: "p > 0" "p < 1" and δ: "δ > 0" "δ < 1" "2*p + δ < 2"
  fixes d :: "nat ⇒ real"
  defines "q ≡ 1 - p"
  assumes d_nonneg: "⋀n. d n ≥ 0"
  assumes d_rec: "⋀n. n ≥ 2 ⟹ d n = 1 + p * d (nat ⌊p * real n + δ⌋) + q * d (nat ⌊q * real n - δ⌋)"
  shows   "d ∈ Θ(λx. ln x)"
  using assms by (master_theorem recursion: d_rec, simp_all)



subsection ‹Transcendental exponents›

(* Certain number-theoretic conjectures would imply that if all the parameters are rational,
   the Akra-Bazzi parameter is either rational or transcendental. That makes this case 
   probably transcendental *)
function foo_cost :: "nat ⇒ real" where
  "n < 200 ⟹ foo_cost n = 0"
| "n ≥ 200 ⟹ foo_cost n = 
     foo_cost (nat ⌊real n / 3⌋) + foo_cost (nat ⌊3 * real n / 4⌋ + 42) + real n"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma foo_cost_nonneg [simp]: "foo_cost n ≥ 0"
  by (induction n rule: foo_cost.induct) simp_all

lemma "foo_cost ∈ Θ(λn. real n powr akra_bazzi_exponent [1,1] [1/3,3/4])"
proof (master_theorem 1 p': 1) 
  have "∀n≥200. foo_cost n > 0" by (simp add: add_nonneg_pos)
  thus "eventually (λn. foo_cost n > 0) at_top" unfolding eventually_at_top_linorder by blast
qed simp_all

lemma "akra_bazzi_exponent [1,1] [1/3,3/4] ∈ {1.1519623..1.1519624}"
  by (akra_bazzi_approximate 29)


subsection ‹Functions in locale contexts›

locale det_select =
  fixes b :: real
  assumes b: "b > 0" "b < 7/10"
begin

function select_cost' :: "nat ⇒ real" where
  "n ≤ 20 ⟹ select_cost' n = 0"
| "n > 20 ⟹ select_cost' n = 
     select_cost' (nat ⌊real n / 5⌋) + select_cost' (nat ⌊b * real n⌋ + 6) + 6 * real n + 5"
by force simp_all
termination using b by akra_bazzi_termination simp_all

lemma "a ≥ 0 ⟹ select_cost' ∈ Θ(λn. real n)"
  using b by (master_theorem 3, force+)

end


subsection ‹Non-curried functions›

(* Note: either a or b could be seen as recursion variables. *)
function baz_cost :: "nat × nat ⇒ real" where
  "n ≤ 2 ⟹ baz_cost (a, n) = 0"
| "n > 2 ⟹ baz_cost (a, n) = 3 * baz_cost (a, nat ⌊real n / 2⌋) + real a"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma baz_cost_nonneg [simp]: "a ≥ 0 ⟹ baz_cost (a, n) ≥ 0"
  by (induction a n rule: baz_cost.induct[split_format (complete)]) simp_all

lemma
  assumes "a > 0"
  shows   "(λx. baz_cost (a, x)) ∈ Θ(λx. x powr log 2 3)"
proof (master_theorem 1 p': 0)
  from assms have "∀x≥3. baz_cost (a, x) > 0" by (auto intro: add_nonneg_pos)
  thus "eventually (λx. baz_cost (a, x) > 0) at_top" by (force simp: eventually_at_top_linorder)
qed (insert assms, simp_all add: powr_divide)

(* Non-"Akra-Bazzi" variables may even be modified without impacting the termination proof.
   However, the Akra-Bazzi theorem and the Master theorem itself do not apply anymore, 
   because bar_cost cannot be seen as a recursive function with one parameter *)
function bar_cost :: "nat × nat ⇒ real" where
  "n ≤ 2 ⟹ bar_cost (a, n) = 0"
| "n > 2 ⟹ bar_cost (a, n) = 3 * bar_cost (2 * a, nat ⌊real n / 2⌋) + real a"
by force simp_all
termination by akra_bazzi_termination simp_all


subsection ‹Ham-sandwich trees›
(* f(n) = f(n/4) + f(n/2) + 1 *)
function ham_sandwich_cost :: "nat ⇒ real" where
  "n < 4 ⟹ ham_sandwich_cost n = 1"
| "n ≥ 4 ⟹ ham_sandwich_cost n = 
      ham_sandwich_cost (nat ⌊n/4⌋) + ham_sandwich_cost (nat ⌊n/2⌋) + 1"
by force simp_all
termination by akra_bazzi_termination simp_all

lemma ham_sandwich_cost_pos [simp]: "ham_sandwich_cost n > 0"
  by (induction n rule: ham_sandwich_cost.induct) simp_all


text ‹The golden ratio›

definition "φ = ((1 + sqrt 5) / 2 :: real)"

lemma φ_pos [simp]: "φ > 0" and φ_nonneg [simp]: "φ ≥ 0" and φ_nonzero [simp]: "φ ≠ 0"
proof-
  show "φ > 0" unfolding φ_def by (simp add: add_pos_nonneg)
  thus "φ ≥ 0" "φ ≠ 0" by simp_all
qed


lemma "ham_sandwich_cost ∈ Θ(λn. n powr (log 2 φ))"
proof (master_theorem 1 p': 0)
  have "(1 / 4) powr log 2 φ + (1 / 2) powr log 2 φ =
            inverse (2 powr log 2 φ)^2 + inverse (2 powr log 2 φ)"
        by (simp add: powr_divide field_simps powr_powr power2_eq_square powr_mult[symmetric]
                 del: powr_log_cancel)
  also have "... = inverse (φ^2) + inverse φ" by (simp add: power2_eq_square)
  also have "φ + 1 = φ*φ" by (simp add: φ_def field_simps)
  hence "inverse (φ^2) + inverse φ = 1" by (simp add: field_simps power2_eq_square)
  finally show "(1 / 4) powr log 2 φ + (1 / 2) powr log 2 φ = 1" by simp
qed simp_all

end