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 "n200. 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 "x3. 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