Theory Submodularity

section "Appendix"

theory Submodularity
imports
  StronglyJoinableRBT
begin

text ‹
  \<^cite>‹blelloch2022joinable› states the submodularity rule in two parts, a decreasing
  and an increasing side. The locale below states both verbatim as ‹rule_dec› and
  ‹rule_inc›; in particular the increasing side bounds the rank of the join from
  below as well as from above.
›

locale PaperJoinable =
  Set2_Join join inv +
  BalancedTree rank c⇩l c⇩u inv
  for rank :: "('a::linorder * 'b) tree ⇒ real"
  and c⇩l c⇩u :: real
  and join :: "('a*'b) tree ⇒ 'a ⇒ ('a*'b) tree ⇒ ('a*'b) tree"
  and inv :: "('a*'b) tree ⇒ bool"
  +
  assumes join_size: "⟦inv l; inv r⟧ ⟹ size (join l a r) = size l + size r + 1"
  assumes rule_dec:
    "⟦ rank l' ≤ rank l; rank r' ≤ rank r; inv l'; inv r'; inv (Node l (a,b) r) ⟧ ⟹
       rank (join l' a r') ≤ rank (Node l (a,b) r)"
  assumes rule_inc:
    "⟦ rank l ≤ rank l'; rank l' ≤ rank l + x; rank r ≤ rank r'; rank r' ≤ rank r + x;
       inv l'; inv r'; inv (Node l (a,b) r) ⟧ ⟹
       rank (Node l (a,b) r) ≤ rank (join l' a r') ∧
       rank (join l' a r') ≤ rank (Node l (a,b) r) + x"
begin
end

text ‹
  The main locale recovers the decreasing side verbatim and the upper bound of 
  the increasing side.
›

lemma (in StronglyJoinable) rule_sub_inc_upper:
  "⟦ rank l ≤ rank l'; rank l' ≤ rank l + x; rank r ≤ rank r'; rank r' ≤ rank r + x;
     inv l'; inv r'; inv (Node l (a,b) r) ⟧ ⟹
     rank (join l' a r') ≤ rank (Node l (a,b) r) + x"
  by (blast intro: rule_sub)

text ‹
  The lower bound of the increasing side is not recovered, and it cannot be. Red-black
  trees are an instance of @{locale StronglyJoinable}, but over red-black trees the two
  bounds of the increasing rule contradict each other already at a singleton, for any
  ‹join› of the type fixed by @{locale Set2_Join}.

  Conversely, the rules of \<^cite>‹blelloch2022joinable› do not imply ‹rule_sub›
  either, which is stated for arbitrary real ‹x› and thus also covers mixed and strictly
  decreasing rank changes. A counterexample can be constructed but is outside the scope
  of this formalization.
›

lemma no_join_satisfies_paper_inc_rule:
  fixes J :: "'a rbt ⇒ 'a ⇒ 'a rbt ⇒ 'a rbt"
  assumes inc:
    "⋀l l' r r' a b x.
       ⟦ real (rk l) ≤ real (rk l'); real (rk l') ≤ real (rk l) + x;
         real (rk r) ≤ real (rk r'); real (rk r') ≤ real (rk r) + x;
         rbt l'; rbt r'; rbt (Node l (a,b) r) ⟧ ⟹
       real (rk (Node l (a,b) r)) ≤ real (rk (J l' a r')) ∧
       real (rk (J l' a r')) ≤ real (rk (Node l (a,b) r)) + x"
  shows False
proof -
  let ?t_red = "Node Leaf (a::'a, (Red, 0)) Leaf"
  let ?t_black = "Node Leaf (a, (Black, Suc 0)) Leaf"
  let ?join = "J Leaf a Leaf"

  have "rbt ?t_red" and "rbt ?t_black"
    by auto

  have "real (rk ?t_red) ≤ real (rk ?join) ∧
        real (rk ?join) ≤ real (rk ?t_red) + 0"
    by (intro inc) auto
  then have upper: "real (rk ?join) ≤ 1"
    by simp

  have "real (rk ?t_black) ≤ real (rk ?join) ∧
        real (rk ?join) ≤ real (rk ?t_black) + 0"
    by (intro inc) auto
  then have lower: "2 ≤ real (rk ?join)"
    by simp

  from upper lower show False
    by linarith
qed

text ‹
  Stated against the locale; no ‹join› whatsoever makes red-black trees an instance of
  the rules of \<^cite>‹blelloch2022joinable›.
›

corollary no_PaperJoinable_rbt:
  fixes J :: "('a::linorder) rbt ⇒ 'a ⇒ 'a rbt ⇒ 'a rbt"
  shows "¬ PaperJoinable (λt. real (rk t)) 1 2 J rbt"
proof
  assume A: "PaperJoinable (λt. real (rk t)) 1 2 J rbt"
  show False
    by (rule no_join_satisfies_paper_inc_rule[of J]) (rule PaperJoinable.rule_inc[OF A])
qed

text ‹
  The flag of the paper resolves the contradiction. Ported to this setting, the
  flagged join receives the colour of the node being rebuilt and consults it in the
  case of equal black heights, where a flag-free ‹join› has to commit to one colour.
›

fun join⇩f :: "color ⇒ 'a rbt ⇒ 'a ⇒ 'a rbt ⇒ 'a rbt" where
"join⇩f c l x r =
  (if bh r < bh l then blacken (joinR l x r)
   else if bh l < bh r then blacken (joinL l x r)
   else if c = Red ∧ col l = Black ∧ col r = Black then R l x r else B l x r)"

corollary join⇩f_rebuilds:
  assumes "rbt (Node l (a, (c, h)) r)"
  shows "join⇩f c l a r = Node l (a, (c, h)) r"
using assms by auto

text ‹
  In particular the two anchors of ‹no_join_satisfies_paper_inc_rule› now constrain
  two distinct calls, and both are satisfied exactly.
›

corollary join⇩f_resolves_singletons:
  "join⇩f Red Leaf a Leaf = Node Leaf (a, (Red, 0)) Leaf"
  "join⇩f Black Leaf a Leaf = Node Leaf (a, (Black, Suc 0)) Leaf"
  by auto

text ‹
  The author concedes, that this appendix does not represent a comprehensive 
  argument for stating the submodularity rule(s) one way or another. In 
  particular, it might be possible to define @{term rk} or the @{term rbt} 
  variant in a way that resolves the problem at hand, but this direction was
  not explored thoroughly.
  Rather, the aim is to provide an argument for why the submodularity rule 
  was modified and why the author considers it sound to have done so.
›

end