Theory Matrix_Complexity
section ‹Application: Complexity of Matrix Orderings›
text ‹In this theory we provide various carriers which can be used for matrix interpretations.›
theory Matrix_Complexity
imports
Matrix_Comparison
Complexity_Carrier
Show_Arctic
begin
subsection ‹Locales for Carriers of Matrix Interpretations and Polynomial Orders›
locale matrix_carrier = SN_one_mono_ordered_semiring_1 d gt
for gt :: "'a :: {show,ordered_semiring_1} ⇒ 'a ⇒ bool" (infix "≻" 50) and d :: "'a"
locale mono_matrix_carrier = complexity_one_mono_ordered_semiring_1 gt d bound
for gt :: "'a :: {show,large_real_ordered_semiring_1} ⇒ 'a ⇒ bool" (infix "≻" 50) and d :: 'a
and bound :: "'a ⇒ nat"
+ fixes mono :: "'a ⇒ bool"
assumes mono: "⋀ x y z. mono x ⟹ y ≻ z ⟹ x ≥ 0 ⟹ x * y ≻ x * z"
text ‹The weak version make comparison with $>$ and then synthesize a suitable
$\delta$-ordering by choosing the least difference in the finite set of
comparisons.›
locale weak_complexity_linear_poly_order_carrier =
fixes weak_gt :: "'a :: {large_real_ordered_semiring_1,show} ⇒ 'a ⇒ bool"
and default :: "'a"
and mono :: "'a ⇒ bool"
assumes weak_gt_mono: "∀ x y. (x,y) ∈ set xys ⟶ weak_gt x y
⟹ ∃ gt bound. mono_matrix_carrier gt default bound mono ∧ (∀ x y. (x,y) ∈ set xys ⟶ gt x y)"
begin
abbreviation weak_mat_gt :: "nat ⇒ 'a mat ⇒ 'a mat ⇒ bool"
where "weak_mat_gt ≡ mat_gt weak_gt"
lemma weak_mat_gt_mono: assumes sd_n: "sd ≤ n" and
orient: "⋀ A B. A ∈ carrier_mat n n ⟹ B ∈ carrier_mat n n ⟹ (A,B) ∈ set ABs ⟹ weak_mat_gt sd A B"
shows "∃ gt bound. mono_matrix_carrier gt default bound mono
∧ (∀ A B. A ∈ carrier_mat n n ⟶ B ∈ carrier_mat n n ⟶ (A, B) ∈ set ABs ⟶ mat_gt gt sd A B)"
proof -
let ?n = "[0 ..< n]"
let ?m1x = "[ A $$ (i,j) . A <- map fst ABs, i <- ?n, j <- ?n]"
let ?m2y = "[ B $$ (i,j) . B <- map snd ABs, i <- ?n, j <- ?n]"
let ?pairs = "concat (map (λ x. map (λ y. (x,y)) ?m2y) ?m1x)"
let ?strict = "filter (λ (x,y). weak_gt x y) ?pairs"
have "∀ x y. (x,y) ∈ set ?strict ⟶ weak_gt x y" by auto
from weak_gt_mono[OF this] obtain gt bound where order: "mono_matrix_carrier gt default bound mono"
and orient2: "⋀ x y. (x, y) ∈ set ?strict ⟹ gt x y" by auto
show ?thesis
proof (intro exI allI conjI impI, rule order)
fix A B
assume A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n"
and AB: "(A, B) ∈ set ABs"
from orient[OF this] have "mat_gt weak_gt sd A B" by auto
from mat_gtD[OF this] obtain i j where
ge: "A ≥⇩m B" and ij: "i < sd" "j < sd" and wgt: "weak_gt (A $$ (i,j)) (B $$ (i,j))"
by auto
from ij ‹sd ≤ n› have ij': "i < n" "j < n" by auto
have gt: "gt (A $$ (i,j)) (B $$ (i,j))"
by (rule orient2, insert ij' AB wgt, force)
show "mat_gt gt sd A B" using ij gt ge by auto
qed
qed
end
sublocale mono_matrix_carrier ⊆ SN_strict_mono_ordered_semiring_1 d gt mono
proof
show "SN {(x,y). y ≥ 0 ∧ x ≻ y}"
unfolding SN_def
by (intro allI deriv_bound_SN_on[OF bound])
qed (rule mono)
sublocale mono_matrix_carrier ⊆ matrix_carrier ..
subsection ‹The Integers as Carrier›
lemma int_complexity:
"mono_matrix_carrier ((>) :: int ⇒ int ⇒ bool) 1 nat int_mono"
proof (unfold_locales)
fix x
let ?R = "{(x, y). 0 ≤ (y :: int) ∧ y < x}"
show "deriv_bound ?R x (nat x)"
unfolding deriv_bound_def
proof
assume "(∃ y. (x,y) ∈ ?R ^^ Suc (nat x))"
then obtain y where xy: "(x,y) ∈ ?R ^^ Suc (nat x)" ..
from xy have y: "0 ≤ y" by auto
obtain n where n: "n = Suc (nat x)" by auto
from xy[unfolded n[symmetric]]
have "x ≥ y + int n"
proof (induct n arbitrary: x y)
case 0 thus ?case by auto
next
case (Suc n)
from Suc(2) obtain z where xz: "(x,z) ∈ ?R ^^ n" and zy: "(z,y) ∈ ?R"
by auto
from Suc(1)[OF xz] have le: "z + int n ≤ x" .
from zy have le2: "y + 1 ≤ z" by simp
with le show ?case by auto
qed
with y have nx: "int n ≤ x" by simp
from nx have x0: "x ≥ 0" by simp
with nx n
show False by simp
qed
qed (insert int_SN.mono, auto)
lemma int_weak_complexity:
"weak_complexity_linear_poly_order_carrier (>) 1 int_mono"
by (unfold_locales, intro exI[of _ "(>)"] exI[of _ nat] conjI, rule int_complexity, auto)
subsection ‹The Rational and Real Numbers as Carrier›
definition delta_bound :: "'a :: floor_ceiling ⇒ 'a ⇒ nat"
where
"delta_bound d x = nat (ceiling (x * of_int (ceiling (1 / d))))"
lemma delta_complexity:
assumes d0: "d > 0" and d1: "d ≤ def"
shows "mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono"
proof -
from d0 have d00: "0 ≤ d" by simp
define N where "N = ceiling (1 / d)"
let ?N = "of_int N :: 'a"
from d0 have "1 / d > 0" by (auto simp: field_simps)
with ceiling_correct[of "1 / d"] have Nd: "1 / d ≤ ?N" and N: "N > 0" unfolding N_def by auto
let ?nat = "λ x. nat (ceiling (x * ?N))"
let ?gt = "delta_gt d"
have nn: "delta_bound d = ?nat" unfolding fun_eq_iff N_def by (simp add: delta_bound_def)
from delta_interpretation[OF d0 d1]
interpret SN_strict_mono_ordered_semiring_1 "def" ?gt delta_mono .
show ?thesis unfolding nn
proof(unfold_locales)
show "?nat 0 = 0" by auto
next
fix x y :: 'a
assume xy: "x ≥ y"
show "?nat x ≥ ?nat y"
by (rule nat_mono, rule ceiling_mono, insert xy N, auto simp: field_simps)
next
have "1 ≤ nat 1" by simp
also have "... ≤ ?nat 1"
proof (rule nat_mono)
have "1 = ceiling (1 :: rat)" by simp
also have "... ≤ ceiling (1 * ?N)" using N by simp
finally show "1 ≤ ceiling (1 * ?N)" .
qed
finally show "1 ≤ ?nat 1" .
next
fix x y :: 'a
have "ceiling ((x + y) * ?N) = ceiling (x * ?N + y * ?N)" by (simp add: field_simps)
also have "... ≤ ceiling (x * ?N) + ceiling (y * ?N)" by (rule ceiling_add_le)
finally show "?nat (x + y) ≤ ?nat x + ?nat y" by auto
next
fix x :: 'a and n :: nat
assume x: "0 ≤ x"
interpret mono_matrix_carrier "(>)" 1 nat int_mono by (rule int_complexity)
have "?nat (x + of_nat n) = nat (ceiling (x * ?N + of_nat n * ?N))"
by (simp add: field_simps)
also have id: "of_nat n * ?N = of_int (of_nat (n * nat N))" using N by (simp add: field_simps)
also have "ceiling (x * ?N + of_int (of_nat (n * nat N))) = ceiling (x * ?N) + of_nat (n * nat N)" unfolding ceiling_add_of_int ..
also have "nat (ceiling (x * ?N) + of_nat (n * nat N)) = ?nat x + nat (int (n * nat N))"
proof (rule bound_plus_of_nat)
have "x * ?N ≥ 0"
by (rule mult_nonneg_nonneg, insert x N, auto)
thus "ceiling (x * ?N) ≥ 0" by auto
qed
also have "(nat (int (n * nat N))) = n * nat N" by presburger
also have "n * nat N = ?nat (of_nat n)" using N by (metis id ceiling_of_int nat_int)
finally
show "?nat (x + of_nat n) = ?nat x + ?nat (of_nat n)" .
next
fix x y z :: 'a
assume *: "delta_mono x" "delta_gt d y z" and x: "0 ≤ x"
from mono[OF * x]
show "delta_gt d (x * y) (x * z)" .
next
fix x :: 'a
let ?R = "{(x,y). 0 ≤ y ∧ ?gt x y}"
show "deriv_bound ?R x (?nat x)" unfolding deriv_bound_def
proof
assume "(∃ y. (x,y) ∈ ?R ^^ Suc (?nat x))"
then obtain y where xy: "(x,y) ∈ ?R ^^ Suc (?nat x)" ..
from xy have y: "0 ≤ y" by auto
obtain n where n: "n = Suc (?nat x)" by auto
from xy[unfolded n[symmetric]]
have "x ≥ y + d * of_nat n"
proof (induct n arbitrary: x y)
case 0 thus ?case by auto
next
case (Suc n)
from Suc(2) obtain z where xz: "(x,z) ∈ ?R ^^ n" and zy: "(z,y) ∈ ?R"
by auto
from Suc(1)[OF xz] have le: "z + d * of_nat n ≤ x" .
from zy[unfolded delta_gt_def] have le2: "y + d ≤ z" by simp
with le show ?case by (auto simp: field_simps)
qed
with y have nx: "d * of_nat n ≤ x" by simp
have "0 ≤ d * of_nat n" by (rule mult_nonneg_nonneg, insert d00, auto)
with nx have x0: "x ≥ 0" by auto
have xd0: "0 ≤ x / d"
by (rule divide_nonneg_pos[OF x0 d0])
from nx[unfolded n]
have "d + d * of_nat (?nat x) ≤ x" by (simp add: field_simps)
with d0 have less: "d * of_nat (?nat x) < x" by simp
from Nd d0 have "1 ≤ d * ?N" by (auto simp: field_simps)
from mult_left_mono[OF this x0]
have "x ≤ d * (x * ?N)" by (simp add: ac_simps)
also have "… ≤ d * of_nat (?nat x)"
proof (rule mult_left_mono[OF _ d00])
show "x * ?N ≤ of_nat (nat ⌈x * ?N⌉)" using x0 ceiling_correct[of "x * ?N"]
by (metis int_nat_eq le_cases of_int_0_le_iff of_int_of_nat_eq order_trans)
qed
also have "… < x" using less .
finally show False by simp
qed
qed
qed
lemma delta_weak_complexity_carrier:
assumes d0: "def > 0"
shows "weak_complexity_linear_poly_order_carrier (>) def delta_mono"
proof
fix xys :: "('a × 'a) list"
assume ass: "∀x y. (x, y) ∈ set xys ⟶ y < x"
let ?cs = "map (λ (x,y). x - y) xys"
let ?ds = "def # ?cs"
define d where "d = Min (set ?ds)"
have d: "d ≤ def" and dcs: "⋀ x. x ∈ set ?cs ⟹ d ≤ x" unfolding d_def by auto
have "d ∈ set ?ds" unfolding d_def by (rule Min_in, auto)
hence "d = def ∨ d ∈ set ?cs" by auto
hence d0: "d > 0"
by (cases, insert d0 ass, auto simp: field_simps)
show "∃gt bound. mono_matrix_carrier gt def bound delta_mono ∧ (∀x y. (x, y) ∈ set xys ⟶ gt x y)"
by (intro exI conjI, rule delta_complexity[OF d0 d], insert dcs, force simp: delta_gt_def)
qed
subsection ‹The Arctic Numbers as Carrier›
lemma arctic_delta_weak_carrier:
"weak_SN_both_mono_ordered_semiring_1 weak_gt_arctic_delta 1 pos_arctic_delta" ..
lemma arctic_weak_carrier:
"weak_SN_both_mono_ordered_semiring_1 (>) 1 pos_arctic"
proof -
have SN: "SN_both_mono_ordered_semiring_1 1 (>) pos_arctic" ..
show ?thesis
by (unfold_locales, intro conjI exI, rule SN, auto)
qed
end