imports Matrix_Comparison Complexity_Carrier Show_Arctic

(* Author: RenĂ© Thiemann Akihisa Yamada License: BSD *) 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