# Theory Landau_Simprocs

theory Landau_Simprocs
imports Landau_Real_Products
(*
File:   Landau_Simprocs.thy
Author: Manuel Eberl <eberlm@in.tum.de>

Simplification procedures for Landau symbols, with a particular focus on functions into the reals.
*)
section ‹Simplification procedures›

theory Landau_Simprocs
imports Landau_Real_Products
begin

subsection ‹Simplification under Landau symbols›

text ‹
The following can be seen as simpset for terms under Landau symbols.
When given a rule @{term "f ∈ Θ(g)"}, the simproc will attempt to rewrite any occurrence of
@{term "f"} under a Landau symbol to @{term "g"}.
›

named_theorems landau_simp "BigTheta rules for simplification of Landau symbols"
setup ‹
let
val eq_thms = @{thms landau_theta.cong_bigtheta}
fun eq_rule thm = get_first (try (fn eq_thm => eq_thm OF [thm])) eq_thms
in
(@{binding landau_simps},
fn context =>
Named_Theorems.get (Context.proof_of context) @{named_theorems landau_simp}
|> map_filter eq_rule)
end
›

lemma bigtheta_const [landau_simp]:
"NO_MATCH 1 c ⟹ c ≠ 0 ⟹ (λx. c) ∈ Θ(λx. 1)" by simp

lemmas [landau_simp] = bigtheta_const_ln bigtheta_const_ln_powr bigtheta_const_ln_pow

lemma bigtheta_const_ln' [landau_simp]:
"0 < a ⟹ (λx::real. ln (x * a)) ∈ Θ(ln)"
by (subst mult.commute) (rule bigtheta_const_ln)

lemma bigtheta_const_ln_powr' [landau_simp]:
"0 < a ⟹ (λx::real. ln (x * a) powr p) ∈ Θ(λx. ln x powr p)"
by (subst mult.commute) (rule bigtheta_const_ln_powr)

lemma bigtheta_const_ln_pow' [landau_simp]:
"0 < a ⟹ (λx::real. ln (x * a) ^ p) ∈ Θ(λx. ln x ^ p)"
by (subst mult.commute) (rule bigtheta_const_ln_pow)

subsection ‹Simproc setup›

lemma landau_gt_1_cong:
"landau_symbol L L' Lr ⟹ (⋀x::real. x > 1 ⟹ f x = g x) ⟹ L at_top (f) = L at_top (g)"
by (auto intro: eventually_mono [OF eventually_gt_at_top[of 1]] elim!: landau_symbol.cong)

lemma landau_gt_1_in_cong:
"landau_symbol L L' Lr ⟹ (⋀x::real. x > 1 ⟹ f x = g x) ⟹ f ∈ L at_top (h) ⟷ g ∈ L at_top (h)"
by (auto intro: eventually_mono [OF eventually_gt_at_top[of 1]] elim!: landau_symbol.in_cong)

lemma landau_prop_equalsI:
"landau_symbol L L' Lr ⟹ (⋀x::real. x > 1 ⟹ f1 x = f2 x) ⟹ (⋀x. x > 1 ⟹ g1 x = g2 x) ⟹
f1 ∈ L at_top (g1) ⟷ f2 ∈ L at_top (g2)"
apply (subst landau_gt_1_cong, assumption+)
apply (subst landau_gt_1_in_cong, assumption+)
apply (rule refl)
done

lemma extract_diff_middle: "(a::_::ab_group_add) - (x + b) = -x + (a - b)" by simp

lemma divide_inverse': "(a::_::{division_ring,ab_semigroup_mult}) / b = inverse b * a"
lemma extract_divide_middle:"(a::_::{field}) / (x * b) = inverse x * (a / b)"

lemmas landau_cancel = landau_symbol.mult_cancel_left

lemmas mult_cancel_left' = landau_symbol.mult_cancel_left[OF _ bigtheta_refl eventually_nonzeroD]

lemma mult_cancel_left_1:
assumes "landau_symbol L L' Lr" "eventually_nonzero F f"
shows   "f ∈ L F (λx. f x * g2 x) ⟷ (λ_. 1) ∈ L F (g2)"
"(λx. f x * f2 x) ∈ L F (f) ⟷ f2 ∈ L F (λ_. 1)"
"f ∈ L F (f) ⟷ (λ_. 1) ∈ L F (λ_. 1)"
using mult_cancel_left'[OF assms, of "λ_. 1"] mult_cancel_left'[OF assms, of _ "λ_. 1"]
mult_cancel_left'[OF assms, of "λ_. 1" "λ_. 1"] by simp_all

lemmas landau_mult_cancel_simps = mult_cancel_left' mult_cancel_left_1

ML_file ‹landau_simprocs.ML›

lemmas bigtheta_simps =
landau_theta.cong_bigtheta[OF bigtheta_const_ln]
landau_theta.cong_bigtheta[OF bigtheta_const_ln_powr]

text ‹
The following simproc attempts to cancel common factors in Landau symbols, i.\,e.\ in a
goal like $f(x) h(x) \in L(g(x) h(x))$, the common factor $h(x)$ will be cancelled. This only
works if the simproc can prove that $h(x)$ is eventually non-zero, for which it uses some
heuristics.
›
simproc_setup landau_cancel_factor (
"f ∈ o[F](g)" | "f ∈ O[F](g)" | "f ∈ ω[F](g)" | "f ∈ Ω[F](g)" | "f ∈ Θ[F](g)"
) = ‹K Landau.cancel_factor_simproc›

text ‹
The next simproc attempts to cancel dominated summands from Landau symbols; e.\,g.\ $O(x + \ln x)$
is simplified to $O(x)$, since $\ln x \in o(x)$. This can be very slow on large terms, so it
is not enabled by default.
›
simproc_setup simplify_landau_sum (
"o[F](λx. f x)" | "O[F](λx. f x)" | "ω[F](λx. f x)" | "Ω[F](λx. f x)" | "Θ[F](λx. f x)" |
"f ∈ o[F](g)" | "f ∈ O[F](g)" | "f ∈ ω[F](g)" | "f ∈ Ω[F](g)" | "f ∈ Θ[F](g)"
) = ‹K (Landau.lift_landau_simproc Landau.simplify_landau_sum_simproc)›

text ‹
This simproc attempts to simplify factors of an expression in a Landau symbol statement
independently from another, i.\,e.\ in something like $O(f(x) g(x)$, a simp rule that rewrites
$O(f(x))$ to $O(f'(x))$ will also rewrite $O(f(x) g(x))$ to $O(f'(x) g(x))$ without any further
setup.
›
simproc_setup simplify_landau_product (
"o[F](λx. f x)" | "O[F](λx. f x)" | "ω[F](λx. f x)" | "Ω[F](λx. f x)" | "Θ[F](λx. f x)" |
"f ∈ o[F](g)" | "f ∈ O[F](g)" | "f ∈ ω[F](g)" | "f ∈ Ω[F](g)" | "f ∈ Θ[F](g)"
) = ‹K (Landau.lift_landau_simproc Landau.simplify_landau_product_simproc)›

text ‹
Lastly, the next very specialised simproc can solve goals of the form
$f(x) \in L(g(x))$ where $f$ and $g$ are real-valued functions consisting only of multiplications,
powers of $x$, and powers of iterated logarithms of $x$. This is done by rewriting both sides
into the form $x^a (\ln x)^b (\ln \ln x)^c$ etc.\ and then comparing the exponents
lexicographically.

Note that for historic reasons, this only works for $x\to\infty$.
›
simproc_setup landau_real_prod (
"(f :: real ⇒ real) ∈ o(g)" | "(f :: real ⇒ real) ∈ O(g)" |
"(f :: real ⇒ real) ∈ ω(g)" | "(f :: real ⇒ real) ∈ Ω(g)" |
"(f :: real ⇒ real) ∈ Θ(g)"
) = ‹K Landau.simplify_landau_real_prod_prop_simproc›

subsection ‹Tests›

lemma asymp_equiv_plus_const_left: "(λn. c + real n) ∼[at_top] (λn. real n)"
by (subst asymp_equiv_add_left) (auto intro!: asymp_equiv_intros eventually_gt_at_top)

lemma asymp_equiv_plus_const_right: "(λn. real n + c) ∼[at_top] (λn. real n)"

subsubsection ‹Product simplification tests›

lemma "(λx::real. f x * x) ∈ O(λx. g x / (h x / x)) ⟷ f ∈ O(λx. g x / h x)"
by simp

lemma "(λx::real. x) ∈ ω(λx. g x / (h x / x)) ⟷ (λx. 1) ∈ ω(λx. g x / h x)"
by simp

subsubsection ‹Real product decision procure tests›

lemma "(λx. x powr 1) ∈ O(λx. x powr 2 :: real)"
by simp

lemma "Θ(λx::real. 2*x powr 3 - 4*x powr 2) = Θ(λx::real. x powr 3)"

lemma "p < q ⟹ (λx::real. c * x powr p * ln x powr r) ∈ o(λx::real. x powr q)"
by simp

lemma "c ≠ 0 ⟹ p > q ⟹ (λx::real. c * x powr p * ln x powr r) ∈ ω(λx::real. x powr q)"
by simp

lemma "b > 0 ⟹ (λx::real. x / ln (2*b*x) * 2) ∈ o(λx. x * ln (b*x))"
by simp
lemma "o(λx::real. x * ln (3*x)) = o(λx. ln x * x)"
lemma "(λx::real. x) ∈ o(λx. x * ln (3*x))" by simp

ML_val ‹
Landau.simplify_landau_real_prod_prop_conv @{context}
@{cterm "(λx::real. 5 * ln (ln x) ^ 2 / (2*x) powr 1.5 * inverse 2) ∈
ω(λx. 3 * ln x * ln x / x * ln (ln (ln (ln x))))"}
›

lemma "(λx. 3 * ln x * ln x / x * ln (ln (ln (ln x)))) ∈
ω(λx::real. 5 * ln (ln x) ^ 2 / (2*x) powr 1.5 * inverse 2)"
by simp

subsubsection ‹Sum cancelling tests›

lemma "Θ(λx::real. 2 * x powr 3 + x * x^2/ln x) = Θ(λx::real. x powr 3)"
by simp

(* TODO: tweak simproc with size threshold *)
lemma "Θ(λx::real. 2 * x powr 3 + x * x^2/ln x + 42 * x powr 9 + 213 * x powr 5 - 4 * x powr 7) =
Θ(λx::real. x ^ 3 + x / ln x * x powr (3/2) - 2*x powr 9)"
using [[landau_sum_limit = 5]] by simp

lemma "(λx::real. x + x * ln (3*x)) ∈ o(λx::real. x^2 + ln (2*x) powr 3)" by simp

end