Imports

import Mathlib

18.1. B-Tree Model

Defines the B-tree data type, key membership, and the full structural invariants (Sorted, ChildBounded, Occupancy, SameDepth). Proves that the B-TREE-SPLIT-CHILD operation preserves every invariant: splitChild_preserves_sorted, splitChild_preserves_childBounded, splitChild_preserves_occupancy, and splitChild_preserves_sameDepth, combined into splitChild_preserves_wellFormed (all with 0 sorry).

Implementation details

              namespace CLRSnamespace Chapter18inductive BTree where
  | node (keys : List Nat) (children : List BTree) : BTree
  deriving Reprnamespace BTreeopen List

Keys and membership

def keysOf : BTree -> List Nat
  | node keys children => keys ++ children.flatMap keysOf

def mem (x : Nat) (t : BTree) : Prop := x ∈ keysOf t

No represented key occurs more than once anywhere in the tree.

def UniqueKeys (tr : BTree) : Prop :=
  (keysOf tr).Nodup

              instance decidableMem (x : Nat) (t : BTree) : Decidable (mem x t) :=
  inferInstanceAs (Decidable (x ∈ keysOf t))def Valid (minDegree : Nat) (_t : BTree) : Prop := 2 <= minDegreedef search (x : Nat) (t : BTree) : Bool := decide (mem x t)theorem search_true_iff (x : Nat) (t : BTree) :
    search x t = true ↔ mem x t := by simp [search]theorem search_true_of_mem (x : Nat) (t : BTree) (hx : mem x t) :
    search x t = true := (search_true_iff x t).mpr hxtheorem mem_of_search_true (x : Nat) (t : BTree) (hx : search x t = true) :
    mem x t := (search_true_iff x t).mp hxtheorem search_false_iff (x : Nat) (t : BTree) :
    search x t = false ↔ ¬ mem x t := by simp [search]theorem search_false_of_not_mem (x : Nat) (t : BTree) (hx : ¬ mem x t) :
    search x t = false := (search_false_iff x t).mpr hxtheorem not_mem_of_search_false (x : Nat) (t : BTree) (hx : search x t = false) :
    ¬ mem x t := (search_false_iff x t).mp hxtheorem search_correct {minDegree x : Nat} {t : BTree}
    (_hvalid : Valid minDegree t) : search x t = true ↔ mem x t :=
  search_true_iff x t

Minimum-key lower bound expression

              def minKeys (minDegree height : Nat) : Nat := 2 * minDegree ^ height - 1theorem minKeys_zero (minDegree : Nat) : minKeys minDegree 0 = 1 := by simp [minKeys]
theorem minKeys_pos {minDegree height : Nat} (hdegree : 0 < minDegree) :
    0 < minKeys minDegree height := by
  unfold minKeys
  have hpow : 0 < minDegree ^ height := pow_pos hdegree height
  have hlt : 1 < 2 * minDegree ^ height := by omega
  exact Nat.sub_pos_of_lt hlttheorem one_le_minKeys {minDegree height : Nat} (hdegree : 0 < minDegree) :
    1 <= minKeys minDegree height := Nat.succ_le_of_lt (minKeys_pos hdegree)theorem minKeys_lower_bound {minDegree height : Nat} (_hdegree : 2 <= minDegree) :
    2 * minDegree ^ height - 1 <= minKeys minDegree height := by rfl
theorem minKeys_succ {minDegree height : Nat} (hdegree : 2 <= minDegree) :
    minKeys minDegree (height + 1) + 1 = minDegree * (minKeys minDegree height + 1) := by
  unfold minKeys; have hpos : 0 < minDegree := by omega
  have hpowPos : 0 < minDegree ^ height := pow_pos hpos height
  have hnextPowPos : 0 < minDegree ^ (height + 1) := pow_pos hpos (height + 1)
  have hnextTermPos : 0 < 2 * minDegree ^ (height + 1) := Nat.mul_pos (by decide) hnextPowPos
  have htermPos : 0 < 2 * minDegree ^ height := Nat.mul_pos (by decide) hpowPos
  rw [Nat.sub_add_cancel (Nat.succ_le_of_lt hnextTermPos)]
  rw [Nat.sub_add_cancel (Nat.succ_le_of_lt htermPos)]
  rw [Nat.pow_succ]; ring
theorem minKeys_le_succ {minDegree height : Nat} (hdegree : 2 <= minDegree) :
    minKeys minDegree height <= minKeys minDegree (height + 1) := by
  unfold minKeys; have hpos : 0 < minDegree := by omega
  have hpow : minDegree ^ height <= minDegree ^ (height + 1) := by
    rw [Nat.pow_succ]; exact Nat.le_mul_of_pos_right _ hpos
  exact Nat.sub_le_sub_right (Nat.mul_le_mul_left 2 hpow) 1theorem minKeys_monotone_height {minDegree h₁ h₂ : Nat}
    (hdegree : 2 <= minDegree) (hheight : h₁ <= h₂) :
    minKeys minDegree h₁ <= minKeys minDegree h₂ := by
  induction hheight with | refl => rfl | step _ ih =>
    exact Nat.le_trans ih (minKeys_le_succ hdegree)

Structural invariants

def Sorted : BTree → Prop
  | node keys children =>
    List.Pairwise (· ≤ ·) keys ∧ ∀ child ∈ children, Sorted child

def ChildBounded : BTree → Prop
  | node keys children =>
    (children.isEmpty ∨ children.length = keys.length + 1) ∧
    (∀ (i : Nat) (hi_child : i < children.length),
      let child := children.get ⟨i, hi_child⟩
      (i = 0 ∨ (match keys[i-1]? with
        | some lo => ∀ k ∈ keysOf child, lo ≤ k
        | none => True)) ∧
      (match keys[i]? with
        | some hi => ∀ k ∈ keysOf child, k ≤ hi
        | none => True)) ∧
    ∀ child ∈ children, ChildBounded child

The B-tree occupancy bounds. A non-empty root has at least one key and an internal root has at least two children; non-root nodes use the ordinary minDegree - 1 key and minDegree child lower bounds.

def Occupancy (minDegree : Nat) (isRoot : Bool) : BTree → Prop
  | node keys children =>
    let lower := if isRoot then
      (if keys.length = 0 ∧ children.isEmpty then 0 else 1) else minDegree - 1
    let upper := 2 * minDegree - 1
    let childLower := if isRoot then 2 else minDegree
    lower ≤ keys.length ∧ keys.length ≤ upper ∧
    (children.isEmpty ∨
      (childLower ≤ children.length ∧ children.length ≤ 2 * minDegree)) ∧
    ∀ child ∈ children, Occupancy minDegree false child

              def heightOf : BTree → Nat
  | node _ [] => 0
  | node _ cs => 1 + ((cs.map heightOf).foldl max 0)inductive SameDepth : BTree → Prop
  | leaf (ks : List Nat) : SameDepth (node ks [])
  | internal (ks : List Nat) (c0 : BTree) (cs : List BTree) :
      (∀ c ∈ cs, heightOf c = heightOf c0) → SameDepth c0 → (∀ c ∈ cs, SameDepth c) →
      SameDepth (node ks (c0 :: cs))def WellFormed (minDegree : Nat) (t : BTree) : Prop :=
  Sorted t ∧ ChildBounded t ∧ Occupancy minDegree true t ∧ SameDepth t

Structural B-tree well-formedness plus global key uniqueness.

def WellFormedUnique (t : Nat) (tr : BTree) : Prop :=
  WellFormed t tr ∧ UniqueKeys tr

theorem WellFormed.valid {minDegree : Nat} {t : BTree}
    (hmin : 2 ≤ minDegree) (_h : WellFormed minDegree t) : Valid minDegree t := by
  unfold Valid; exact hmin

theorem wellFormed_empty (minDegree : Nat) (Variable name `hmin` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hmin : 2 ≤ minDegree) :
    WellFormed minDegree (node [] []) := by
  unfold WellFormed Sorted ChildBounded Occupancy
  refine ⟨?_, ?_, ?_, SameDepth.leaf []⟩
  · unfold Sorted; simp
  · unfold ChildBounded; simp
  · unfold Occupancy; simp

B-TREE-SPLIT-CHILD operation

def splitChild (t : Nat) : BTree → Nat → BTree
  | node keys children, i =>
    if h : i < children.length then
      match children.get ⟨i, h⟩ with
      | node cKeys cChildren =>
        if cKeys.length = 2 * t - 1 then
          match cKeys.splitAt (t - 1), cChildren.splitAt t with
          | (leftKeys, medianKey :: rightKeys), (leftCh, rightCh) =>
            BTree.node (keys.take i ++ medianKey :: keys.drop i)
              (children.take i ++ [BTree.node leftKeys leftCh, BTree.node rightKeys rightCh] ++
                children.drop (i + 1))
          | _, _ => node keys children
        else
          node keys children
    else
      node keys children

Occupancy preservation under splitChild

              lemma splitAt_first_half_length (cKeys : List Nat) (t : Nat) (hfull : cKeys.length = 2 * t - 1) :
    (cKeys.splitAt (t - 1)).1.length = t - 1 := by
  simp [hfull]; omega

lemma splitAt_second_half_length (cKeys : List Nat) (t : Nat)
    (hfull : cKeys.length = 2 * t - 1) (ht : 1 ≤ t) :
    ((cKeys.splitAt (t - 1)).2.drop 1).length = t - 1 := by
  have h_snd_len : (cKeys.splitAt (t - 1)).2.length = t := by
    simp [hfull]; omega
  simp [This simp argument is unused:
  h_snd_len

Hint: Omit it from the simp argument list.
  simp ̵[̵h̵_̵s̵n̵d̵_̵l̵e̵n̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`h_snd_len]; omega

theorem splitChild_new_children_key_counts (t : Nat) (ht : 2 ≤ t)
    (cKeys : List Nat) (hfull : cKeys.length = 2 * t - 1) :
    ((cKeys.splitAt (t - 1)).1).length = t - 1 ∧
    ((cKeys.splitAt (t - 1)).2.drop 1).length = t - 1 := by
  have ht_pos : 1 ≤ t := by omega
  exact ⟨splitAt_first_half_length cKeys t hfull,
          splitAt_second_half_length cKeys t hfull ht_pos⟩theorem splitChild_parent_key_bound (t : Nat) (Variable name `ht` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`ht : 2 ≤ t) (keys : List Nat)
    (hparent_nonfull : keys.length < 2 * t - 1) :
    keys.length + 1 ≤ 2 * t - 1 := by
  omega

List utility: foldl max over uniform values



lemma foldl_max_idem (l : List Nat) (a : Nat) (h : ∀ b ∈ l, b = a) : foldl max a l = a := by
  induction l with
  | nil => simp
  | cons x xs ih =>
    have hx : x = a := h x (by simp)
    have hxs : ∀ b ∈ xs, b = a := by
      intro b hb; exact h b (by simp [hb])
    rw [hx]
    simp [ih hxs]



lemma foldl_max_eq_of_all_eq (l : List Nat) (v : Nat) (h_ne : l ≠ [])
    (h : ∀ a ∈ l, a = v) : l.foldl max 0 = v := by
  cases l with
  | nil => contradiction
  | cons x xs =>
    have hx : x = v := h x (by simp)
    have hxs : ∀ a ∈ xs, a = v := by
      intro a ha; exact h a (by simp [ha])
    rw [hx]
    simp
    exact foldl_max_idem xs v hxs

SameDepth infrastructure and preservation

              Try this: intro ks' c0' cs' h_heights _h_sd_c0' _h_sd_children' c₁ hc₁ c₂ hc₂Try this: intro ks' c0' cs' h_heights _h_sd_c0' _h_sd_children' c₁ hc₁ c₂ hc₂Try this: intro ks' c0' cs' h_heights _h_sd_c0' _h_sd_children' c₁ hc₁ c₂ hc₂Try this: intro ks' c₁ hc₁Try this: intro ks' c₁ hc₁Try this: intro ks' c₁ hc₁

lemma sameDepth_children_eq_height {ks : List Nat} {c0 : BTree} {cs : List BTree}
    (hsd : SameDepth (node ks (c0 :: cs))) :
    ∀ c₁ ∈ (c0 :: cs), ∀ c₂ ∈ (c0 :: cs), heightOf c₁ = heightOf c₂ := by
  refine SameDepth.casesOn hsd
    (motive := λ t _ => match t with
      | node _ children => ∀ c₁ ∈ children, ∀ c₂ ∈ children, heightOf c₁ = heightOf c₂)
    ?leaf ?internal
  · Try this: intro ks' c₁ hc₁intro ks'; intro c₁ hc₁; simp at hc₁
  · Try this: intro ks' c0' cs' h_heights _h_sd_c0' _h_sd_children' c₁ hc₁ c₂ hc₂intro ks' c0' cs' h_heights _h_sd_c0' _h_sd_children'
    intro c₁ hc₁ c₂ hc₂
    simp at hc₁ hc₂
    rcases hc₁ with (rfl | hc₁')
    · rcases hc₂ with (rfl | hc₂')
      · rfl
      · symm; exact h_heights c₂ hc₂'
    · rcases hc₂ with (rfl | hc₂')
      · exact h_heights c₁ hc₁'
      · rw [h_heights c₁ hc₁', h_heights c₂ hc₂']lemma sameDepth_head_sd {ks : List Nat} {c0 : BTree} {cs : List BTree}
    (hsd : SameDepth (node ks (c0 :: cs))) : SameDepth c0 := by
  refine SameDepth.casesOn hsd (motive := λ t _ => match t with
    | node _ (c0' :: _) => SameDepth c0'
    | node _ [] => True) ?leaf ?internal
  · intro ks'; trivial
  · intro ks' c0' cs' _ h_sd_c0' _; exact h_sd_c0'lemma sameDepth_tail_sd {ks : List Nat} {c0 : BTree} {cs : List BTree}
    (hsd : SameDepth (node ks (c0 :: cs))) (c : BTree) (hc : c ∈ cs) : SameDepth c := by
  refine SameDepth.casesOn hsd (motive := λ t _ => match t with
    | node _ (c0' :: cs') => ∀ c' ∈ cs', SameDepth c'
    | node _ [] => ∀ c' ∈ [], SameDepth c') ?leaf ?internal c hc
  · intro ks' c' hc'; simp at hc'
  · intro ks' c0' cs' _ _ h_sd_children'; exact h_sd_children'

lemma sameDepth_take (cKeys : List Nat) (cChildren : List BTree) (t : Nat)
    (hsd : SameDepth (node cKeys cChildren)) (ht_pos : 1 ≤ t) :
    SameDepth (node ((cKeys.splitAt (t - 1)).1) ((cChildren.splitAt t).1)) := by
  cases cChildren with
  | nil => simp; exact SameDepth.leaf _
  | cons d0 ds =>
    have h_take : ((d0 :: ds).splitAt t).1 = d0 :: (ds.take (t-1)) := by
      cases t; omega; rename_i n; simp
    rw [h_take]
    have h_sd_d0 : SameDepth d0 := sameDepth_head_sd hsd
    have h_sd_ds : ∀ d ∈ ds.take (t-1), SameDepth d := by
      intro d hd
      exact sameDepth_tail_sd hsd d ((take_sublist (t-1) ds).subset hd)
    have h_heights : ∀ d ∈ ds.take (t-1), heightOf d = heightOf d0 := by
      intro d hd
      have hmem : d ∈ d0 :: ds := by
        apply mem_cons_of_mem d0
        exact (take_sublist (t-1) ds).subset hd
      exact (sameDepth_children_eq_height hsd) d hmem d0 (by simp)
    exact SameDepth.internal ((cKeys.splitAt (t - 1)).1) d0 (ds.take (t-1))
      h_heights h_sd_d0 h_sd_ds

lemma sameDepth_drop (cKeys : List Nat) (cChildren : List BTree) (t : Nat)
    (hsd : SameDepth (node cKeys cChildren)) (ht_pos : 1 ≤ t) :
    SameDepth (node ((cKeys.splitAt (t - 1)).2.drop 1) ((cChildren.splitAt t).2)) := by
  cases cChildren with
  | nil => simp; exact SameDepth.leaf _
  | cons d0 ds =>
    have h_drop : ((d0 :: ds).splitAt t).2 = ds.drop (t-1) := by
      cases t; omega; rename_i n; simp
    rw [h_drop]
    by_cases h_empty : ds.drop (t-1) = []
    · simp [h_empty]; exact SameDepth.leaf _
    · match h_drop_suffix : ds.drop (t-1) with
      | [] => exact (h_empty h_drop_suffix).elim
      | e0 :: es =>
        have he0_mem_drop : e0 ∈ ds.drop (t-1) := by rw [h_drop_suffix]; simp
        have he0_ds : e0 ∈ ds := (drop_sublist (t-1) ds).subset he0_mem_drop
        have h_sd_e0 : SameDepth e0 := sameDepth_tail_sd hsd e0 he0_ds
        have h_sd_es : ∀ e ∈ es, SameDepth e := by
          intro e he
          have he_mem_drop : e ∈ ds.drop (t-1) := by rw [h_drop_suffix]; simp [he]
          have he_ds : e ∈ ds := (drop_sublist (t-1) ds).subset he_mem_drop
          exact sameDepth_tail_sd hsd e he_ds
        have h_heights : ∀ e ∈ es, heightOf e = heightOf e0 := by
          intro e he
          have he_mem_drop : e ∈ ds.drop (t-1) := by rw [h_drop_suffix]; simp [he]
          have he_ds : e ∈ ds := (drop_sublist (t-1) ds).subset he_mem_drop
          have he0_cons : e0 ∈ d0 :: ds := by simp [he0_ds]
          have he_cons : e ∈ d0 :: ds := by simp [he_ds]
          exact (sameDepth_children_eq_height hsd) e he_cons e0 he0_cons
        refine SameDepth.internal ((cKeys.splitAt (t - 1)).2.drop 1) e0 es
          h_heights h_sd_e0 h_sd_es

Height of a SameDepth internal node

              

lemma heightOf_uniform_children {ks : List Nat} {c0 : BTree} {cs : List BTree}
    (h : ∀ c ∈ cs, heightOf c = heightOf c0) :
    heightOf (node ks (c0 :: cs)) = 1 + heightOf c0 := by
  simp [heightOf]
  refine (Nat.succ_inj).mp ?_
  simp
  refine foldl_max_idem (List.map heightOf cs) (heightOf c0) ?_
  intro x hx
  rw [List.mem_map] at hx
  rcases hx with ⟨c, hc, rfl⟩
  exact h c hclemma heightOf_internal_of_sameDepth {ks : List Nat} {c0 : BTree} {cs : List BTree}
    (hsd : SameDepth (node ks (c0 :: cs))) : heightOf (node ks (c0 :: cs)) = 1 + heightOf c0 := by
  match hsd with
  | SameDepth.internal ks' c0' cs' h_heights _ _ =>
    exact heightOf_uniform_children h_heightstry 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`

lemma heightOf_split_parts_eq (cKeys : List Nat) (cChildren : List BTree) (t : Nat)
    (hsd : SameDepth (node cKeys cChildren))
    (ht_pos : 0 < t)
    (h_children : cChildren = [] ∨ t < cChildren.length) :
    heightOf (node ((cKeys.splitAt (t - 1)).1) ((cChildren.splitAt t).1)) =
    heightOf (node cKeys cChildren) ∧
    heightOf (node ((cKeys.splitAt (t - 1)).2.drop 1) ((cChildren.splitAt t).2)) =
    heightOf (node cKeys cChildren) := by
  rcases h_children with (h_empty | h_gt)
  · subst h_empty; simp [heightOf]
  · have h_nonempty : cChildren ≠ [] := by
      intro h; rw [h] at h_gt; simp at h_gt
    cases h_cases : cChildren with
    | nil => exact (h_nonempty h_cases).elim
    | cons d0 ds =>
      have hsd_internal : heightOf (node cKeys (d0 :: ds)) = 1 + heightOf d0 :=
        heightOf_internal_of_sameDepth (by rwa [h_cases] at hsd)
      have h_all_eq : ∀ c₁ ∈ (d0 :: ds), ∀ c₂ ∈ (d0 :: ds), heightOf c₁ = heightOf c₂ :=
        sameDepth_children_eq_height (by rwa [h_cases] at hsd)
      have h_take_head : ((d0 :: ds).splitAt t).1 = d0 :: (ds.take (t - 1)) := by
        cases t; omega; rename_i n; simp
      rw [h_take_head]
      have h_left_heights : ∀ c ∈ ds.take (t - 1), heightOf c = heightOf d0 := by
        intro c hc
        have hc_mem : c ∈ d0 :: ds :=
          List.mem_cons_of_mem _ ((List.take_sublist (t - 1) ds).subset hc)
        exact h_all_eq c hc_mem d0 (by simp)
      have h_left_height : heightOf (node ((cKeys.splitAt (t - 1)).1) (d0 :: ds.take (t - 1))) =
          1 + heightOf d0 :=
        heightOf_uniform_children h_left_heights
      have h_drop_eq : ((d0 :: ds).splitAt t).2 = ds.drop (t - 1) := by
        cases t; omega; rename_i n; simp
      rw [h_drop_eq]
      have h_right_nonempty : ds.drop (t - 1) ≠ [] := by
        have hlen_cons : t < (d0 :: ds).length := by simpa [h_cases] using h_gt
        intro h
        have hlen0 : (ds.drop (t - 1)).length = 0 := by try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [h]
        rw [List.length_drop] at hlen0
        have : ds.length ≤ t - 1 := by omega
        have : ds.length + 1 ≤ t := by omega
        simp at hlen_cons
        omega
      match h_drop_suffix : ds.drop (t - 1) with
      | nil => exact (h_right_nonempty h_drop_suffix).elim
      | cons e0 es =>
        have h_right_heights : ∀ c ∈ es, heightOf c = heightOf e0 := by
          intro c hc
          have hc_mem : c ∈ d0 :: ds := by
            apply List.mem_cons_of_mem _
            have hmem_drop : c ∈ ds.drop (t - 1) := by rw [h_drop_suffix]; simp [hc]
            exact (List.drop_sublist (t - 1) ds).subset hmem_drop
          have he0_mem : e0 ∈ d0 :: ds := by
            apply List.mem_cons_of_mem _
            have he0_drop : e0 ∈ ds.drop (t - 1) := by rw [h_drop_suffix]; simp
            exact (List.drop_sublist (t - 1) ds).subset he0_drop
          exact h_all_eq c hc_mem e0 he0_mem
        have h_right_height : heightOf (node ((cKeys.splitAt (t - 1)).2.drop 1) (e0 :: es)) =
            1 + heightOf e0 :=
          heightOf_uniform_children h_right_heights
        have h_d0_e0_height : heightOf e0 = heightOf d0 := by
          have he0_mem : e0 ∈ d0 :: ds := by
            apply List.mem_cons_of_mem _
            have he0_drop : e0 ∈ ds.drop (t - 1) := by rw [h_drop_suffix]; simp
            exact (List.drop_sublist (t - 1) ds).subset he0_drop
          exact h_all_eq e0 he0_mem d0 (by simp)
        rw [h_d0_e0_height] at h_right_height
        rw [h_left_height, h_right_height, hsd_internal]
        exact ⟨rfl, rfl⟩

theorem splitChild_preserves_sameDepth (t : Nat) (ht : 2 ≤ t)
    (keys : List Nat) (children : List BTree)
    (cKeys : List Nat) (cChildren : List BTree) (i : Nat)
    (h_lt : i < children.length)
    (hchild_eq : children.get ⟨i, h_lt⟩ = node cKeys cChildren)
    (hchild_full : cKeys.length = 2 * t - 1)
    (hchild_children : cChildren = [] ∨ t < cChildren.length)
    (hsd : SameDepth (node keys children)) :
    SameDepth (splitChild t (node keys children) i) := by
  have ht_pos : 1 ≤ t := by omega
  have ht_pos' : 0 < t := by omega
  have h_keys_snd_nonempty : (cKeys.splitAt (t - 1)).2 ≠ [] := by
    have hlen : (cKeys.splitAt (t - 1)).2.length = t := by simp [hchild_full]; omega
    intro h; rw [h] at hlen; simp at hlen; omega
  dsimp [splitChild]
  rw [dif_pos h_lt]
  have h_get : children[i] = node cKeys cChildren := by simpa using hchild_eq
  rw [h_get]
  dsimp
  rw [if_pos hchild_full]
  cases hk : cKeys.splitAt (t - 1) with
  | mk leftKeys keysRest =>
    have h_keysRest_nonempty : keysRest ≠ [] := by
      have : (cKeys.splitAt (t - 1)).2 = keysRest := by rw [hk]
      rw [← this]; exact h_keys_snd_nonempty
    cases hkr : keysRest with
    | nil => exact (h_keysRest_nonempty hkr).elim
    | cons medianKey rightKeys =>
      cases hc : cChildren.splitAt t with
      | mk leftCh rightCh =>
        -- The match reduces to the success branch
        show SameDepth (BTree.node (take i keys ++ medianKey :: drop i keys)
          (take i children ++ [BTree.node leftKeys leftCh, BTree.node rightKeys rightCh] ++
            drop (i + 1) children))
        cases hsd with
        | leaf ks => simp at h_lt
        | internal ks c0 cs h_heights h_sd_c0 h_sd_cs =>
          have h_sd_child : SameDepth (node cKeys cChildren) := by
            rcases Nat.eq_zero_or_pos i with (rfl | hi_pos')
            · have hc0_eq : c0 = node cKeys cChildren := by simpa using hchild_eq
              rw [← hc0_eq]; exact h_sd_c0
            · have h_get' : (c0 :: cs).get ⟨i, h_lt⟩ = cs.get ⟨i - 1, by
                simp at h_lt; omega⟩ := by
                rcases i with (rfl | i)
                · exact (Nat.not_lt_zero _ hi_pos').elim
                · simp
              have hmem : cs.get ⟨i - 1, by simp at h_lt; omega⟩ ∈ cs := by
                apply List.get_mem
              rw [← hchild_eq, h_get']
              exact h_sd_cs _ hmem
          have h_keys_left : ((cKeys.splitAt (t - 1)).1) = leftKeys := by rw [hk]
          have h_keys_right : ((cKeys.splitAt (t - 1)).2.drop 1) = rightKeys := by
            rw [hk]; simp [hkr]
          have h_ch_left : ((cChildren.splitAt t).1) = leftCh := by rw [hc]
          have h_ch_right : ((cChildren.splitAt t).2) = rightCh := by rw [hc]
          have h_sd_left : SameDepth (node leftKeys leftCh) := by
            rw [← h_keys_left, ← h_ch_left]; exact sameDepth_take cKeys cChildren t h_sd_child ht_pos
          have h_sd_right : SameDepth (node rightKeys rightCh) := by
            rw [← h_keys_right, ← h_ch_right]; exact sameDepth_drop cKeys cChildren t h_sd_child ht_pos
          have h_heights_split := heightOf_split_parts_eq cKeys cChildren t h_sd_child ht_pos' hchild_children
          have h_height_left : heightOf (node leftKeys leftCh) = heightOf (node cKeys cChildren) := by
            rw [← h_keys_left, ← h_ch_left]; exact h_heights_split.1
          have h_height_right : heightOf (node rightKeys rightCh) = heightOf (node cKeys cChildren) := by
            rw [← h_keys_right, ← h_ch_right]; exact h_heights_split.2
          have h_child_eq_c0_height : heightOf (node cKeys cChildren) = heightOf c0 := by
            rcases Nat.eq_zero_or_pos i with (rfl | hi_pos')
            · have hc0_eq : c0 = node cKeys cChildren := by simpa using hchild_eq
              rw [← hc0_eq]
            · have h_get' : (c0 :: cs).get ⟨i, h_lt⟩ = cs.get ⟨i - 1, by
                simp at h_lt; omega⟩ := by
                rcases i with (rfl | i)
                · exact (Nat.not_lt_zero _ hi_pos').elim
                · simp
              have hmem : cs.get ⟨i - 1, by simp at h_lt; omega⟩ ∈ cs := by
                apply List.get_mem
              rw [← hchild_eq, h_get']
              exact h_heights _ hmem
          rcases Nat.eq_zero_or_pos i with (rfl | hi_pos)
          · -- i = 0: result children = newLeft :: newRight :: cs
            have h_rest_heights : ∀ c ∈ (node rightKeys rightCh :: cs),
                heightOf c = heightOf (node leftKeys leftCh) := by
              intro c hc; simp at hc; rcases hc with (rfl | hc_cs)
              · rw [h_height_right, h_height_left]
              · rw [h_heights c hc_cs, ← h_child_eq_c0_height, h_height_left]
            have h_rest_sd : ∀ c ∈ (node rightKeys rightCh :: cs), SameDepth c := by
              intro c hc; simp at hc; rcases hc with (rfl | hc_cs)
              · exact h_sd_right
              · exact h_sd_cs c hc_cs
            refine SameDepth.internal (take 0 keys ++ medianKey :: drop 0 keys)
              (node leftKeys leftCh) (node rightKeys rightCh :: cs) h_rest_heights h_sd_left h_rest_sd
          · -- i > 0: result children = c0 :: take(i-1)cs ++ left :: right :: drop i cs
            have h_take : take i (c0 :: cs) = c0 :: take (i - 1) cs := by
              rcases i with (rfl | i)
              · exact (Nat.not_lt_zero _ hi_pos).elim
              · simp
            have h_drop_succ : drop (i + 1) (c0 :: cs) = drop i cs := by simp
            rw [h_take, h_drop_succ]
            simp only [List.cons_append, List.append_assoc, List.nil_append]
            have h_rest_heights : ∀ c ∈ (take (i - 1) cs ++ (node leftKeys leftCh :: node rightKeys rightCh :: drop i cs)),
                heightOf c = heightOf c0 := by
              intro c hc
              rw [List.mem_append] at hc
              rcases hc with (hc | hc)
              · have hmem : c ∈ cs := (List.take_sublist _ _).subset hc
                exact h_heights c hmem
              · simp at hc; rcases hc with (rfl | rfl | hc)
                · rw [h_height_left, h_child_eq_c0_height]
                · rw [h_height_right, h_child_eq_c0_height]
                · have hmem : c ∈ cs := (List.drop_sublist _ _).subset hc
                  exact h_heights c hmem
            have h_rest_sd : ∀ c ∈ (take (i - 1) cs ++ (node leftKeys leftCh :: node rightKeys rightCh :: drop i cs)),
                SameDepth c := by
              intro c hc
              rw [List.mem_append] at hc
              rcases hc with (hc | hc)
              · have hmem : c ∈ cs := (List.take_sublist _ _).subset hc
                exact h_sd_cs c hmem
              · simp at hc; rcases hc with (rfl | rfl | hc)
                · exact h_sd_left
                · exact h_sd_right
                · have hmem : c ∈ cs := (List.drop_sublist _ _).subset hc
                  exact h_sd_cs c hmem
            refine SameDepth.internal (take i keys ++ medianKey :: drop i keys) c0
              (take (i - 1) cs ++ (node leftKeys leftCh :: node rightKeys rightCh :: drop i cs))
              h_rest_heights h_sd_c0 h_rest_sd

splitChild occupancy preservation (stub)

The following theorem states that splitChild preserves the Occupancy invariant. The proof requires:

Arithmetic showing that the two new children have t-1 keys each (from splitAt_first_half_length / splitAt_second_half_length)
Arithmetic showing that children counts stay within [t, 2t] (requires ChildBounded to know cChildren.length = 2t when non-empty)
Propagation of sub-node occupancy from the original child.

              -- Helper: extract child occupancy from parent occupancy
lemma occupancy_of_child {minDegree : Nat} {isRoot : Bool} {keys : List Nat} {children : List BTree}
    (h_occ : Occupancy minDegree isRoot (node keys children))
    (i : Nat) (hi : i < children.length) :
    Occupancy minDegree false (children.get ⟨i, hi⟩) := by
  unfold Occupancy at h_occ
  rcases h_occ with ⟨_, _, _, h_sub⟩
  apply h_sub
  apply List.get_mem

-- Helper: from ChildBounded of a full node, children length is 0 or 2t
lemma child_children_len_of_full_cb {t : Nat} (ht : 2 ≤ t) {cKeys : List Nat} {cChildren : List BTree}
    (h_cb : ChildBounded (node cKeys cChildren)) (h_full : cKeys.length = 2 * t - 1) :
    cChildren.length = 0 ∨ cChildren.length = 2 * t := by
  unfold ChildBounded at h_cb
  rcases h_cb with ⟨h_rel, _, _⟩
  rcases h_rel with (h_empty | h_eq)
  · left; cases cChildren with | nil => rfl | cons x xs => simp at h_empty
  · right; rw [h_eq, h_full]; omega

theorem splitChild_preserves_occupancy (t : Nat) (ht : 2 ≤ t)
    (keys : List Nat) (children : List BTree)
    (cKeys : List Nat) (cChildren : List BTree) (i : Nat)
    (h_lt : i < children.length)
    (hchild_eq : children.get ⟨i, h_lt⟩ = node cKeys cChildren)
    (hchild_full : cKeys.length = 2 * t - 1)
    (hparent_nonfull : keys.length < 2 * t - 1)
    (h_occ : Occupancy t true (node keys children))
    (h_cb : ChildBounded (node keys children)) :
    Occupancy t true (splitChild t (node keys children) i) := by
  have ht_pos : 0 < t := by omega
  have ht_pos' : 1 ≤ t := by omega
  -- Extract child invariants
  have hchild_occ : Occupancy t false (node cKeys cChildren) := by
    rw [← hchild_eq]; exact occupancy_of_child h_occ i h_lt
  have hchild_cb : ChildBounded (node cKeys cChildren) := by
    rw [← hchild_eq]; unfold ChildBounded at h_cb
    rcases h_cb with ⟨_, _, h_sub⟩; apply h_sub; apply List.get_mem
  have h_cChildren_len := child_children_len_of_full_cb ht hchild_cb hchild_full
  -- Unfold splitChild (same pattern as splitChild_preserves_sameDepth)
  have h_keys_snd_nonempty : (cKeys.splitAt (t - 1)).2 ≠ [] := by
    have hlen : (cKeys.splitAt (t - 1)).2.length = t := by simp [hchild_full]; omega
    intro h; rw [h] at hlen; simp at hlen; omega
  dsimp [splitChild]; rw [dif_pos h_lt]
  have h_get : children[i] = node cKeys cChildren := by simpa using hchild_eq
  rw [h_get]; dsimp; rw [if_pos hchild_full]
  cases hk : cKeys.splitAt (t - 1) with
  | mk leftKeys keysRest =>
    have h_keysRest_nonempty : keysRest ≠ [] := by
      have : (cKeys.splitAt (t - 1)).2 = keysRest := by rw [hk]
      rw [← this]; exact h_keys_snd_nonempty
    cases hkr : keysRest with
    | nil => exact (h_keysRest_nonempty hkr).elim
    | cons medianKey rightKeys =>
      cases hc : cChildren.splitAt t with
      | mk leftCh rightCh =>
        show Occupancy t true (BTree.node (take i keys ++ medianKey :: drop i keys)
          (take i children ++ [BTree.node leftKeys leftCh, BTree.node rightKeys rightCh] ++
            drop (i + 1) children))
        -- Relate local names to splitAt results (matching SameDepth proof pattern)
        have h_keys_left : ((cKeys.splitAt (t - 1)).1) = leftKeys := by rw [hk]
        have h_keys_right : ((cKeys.splitAt (t - 1)).2.drop 1) = rightKeys := by
          rw [hk]; simp [hkr]
        have h_ch_left : ((cChildren.splitAt t).1) = leftCh := by rw [hc]
        have h_ch_right : ((cChildren.splitAt t).2) = rightCh := by rw [hc]
        -- Key length facts (using ← to apply splitAt lemmas)
        have h_leftKeys_len : leftKeys.length = t - 1 := by
          rw [← h_keys_left]; exact splitAt_first_half_length cKeys t hchild_full
        have h_rightKeys_len : rightKeys.length = t - 1 := by
          rw [← h_keys_right]; exact splitAt_second_half_length cKeys t hchild_full ht_pos'
        -- Children count bounds for the two new children
        have h_leftCh_bound : leftCh.isEmpty ∨ (t ≤ leftCh.length ∧ leftCh.length ≤ 2 * t) := by
          rcases h_cChildren_len with (h0 | h2t)
          · -- cChildren.length = 0 → cChildren = [] → leftCh = []
            have hnil : cChildren = [] := by
              cases cChildren with | nil => rfl | cons x xs => simp at h0
            left; rw [← h_ch_left, hnil]; simp
          · -- cChildren.length = 2t → leftCh.length = t
            right; rw [← h_ch_left]; simp [h2t]; omega
        have h_rightCh_bound : rightCh.isEmpty ∨ (t ≤ rightCh.length ∧ rightCh.length ≤ 2 * t) := by
          rcases h_cChildren_len with (h0 | h2t)
          · have hnil : cChildren = [] := by
              cases cChildren with | nil => rfl | cons x xs => simp at h0
            left; rw [← h_ch_right, hnil]; simp
          · right; rw [← h_ch_right]; simp [h2t]; omega
        -- Occupancy for the two new children (non-root)
        have h_occ_left : Occupancy t false (BTree.node leftKeys leftCh) := by
          unfold Occupancy
          refine ⟨?_, ?_, h_leftCh_bound, ?_⟩
          · rw [h_leftKeys_len]; exact le_rfl
          · rw [h_leftKeys_len]; omega
          · intro child hchild
            rw [← h_ch_left] at hchild; simp at hchild
            have : child ∈ cChildren :=
              (take_sublist t cChildren).subset hchild
            unfold Occupancy at hchild_occ
            rcases hchild_occ with ⟨_, _, _, h_occ_sub⟩
            exact h_occ_sub child this
        have h_occ_right : Occupancy t false (BTree.node rightKeys rightCh) := by
          unfold Occupancy
          refine ⟨?_, ?_, h_rightCh_bound, ?_⟩
          · rw [h_rightKeys_len]; exact le_rfl
          · rw [h_rightKeys_len]; omega
          · intro child hchild
            rw [← h_ch_right] at hchild; simp at hchild
            have : child ∈ cChildren :=
              (drop_sublist t cChildren).subset hchild
            unfold Occupancy at hchild_occ
            rcases hchild_occ with ⟨_, _, _, h_occ_sub⟩
            exact h_occ_sub child this
        -- Parent occupancy after split: prove the four conjuncts
        -- Derive i ≤ keys.length from ChildBounded and h_lt
        have h_i_le_keys : i ≤ keys.length := by
          unfold ChildBounded at h_cb; rcases h_cb with ⟨h_cb_rel, _, _⟩
          rcases h_cb_rel with (h_cb_empty | h_cb_eq)
          · have h_len0 : children.length = 0 := by simpa using h_cb_empty
            have : i < 0 := by rwa [h_len0] at h_lt
            omega
          · rw [h_cb_eq] at h_lt; omega
        unfold Occupancy
        have h_newKeys_len : (take i keys ++ medianKey :: drop i keys).length = keys.length + 1 := by
          simp [h_i_le_keys]; omega
        have h_newChildren_len : (take i children ++
            [BTree.node leftKeys leftCh, BTree.node rightKeys rightCh] ++
            drop (i + 1) children).length = children.length + 1 := by
          simp; omega
        refine ⟨?_, ?_, ?_, ?_⟩
        · -- lower bound: the newKeys list is non-empty (contains medianKey)
          have h_ne_nil : take i keys ++ medianKey :: drop i keys ≠ [] := by simp
          have h_pos : 0 < (take i keys ++ medianKey :: drop i keys).length := by omega
          have h_one_le : 1 ≤ (take i keys ++ medianKey :: drop i keys).length := by omega
          have h_if_val : (if (take i keys ++ medianKey :: drop i keys).length = 0 ∧
              (take i children ++ [BTree.node leftKeys leftCh, BTree.node rightKeys rightCh] ++
                drop (i+1) children).isEmpty then 0 else 1) = 1 := by
            by_cases hzero : (take i keys ++ medianKey :: drop i keys).length = 0
            · exfalso; exact h_pos.ne' hzero
            · simp [This simp argument is unused:
  hzero

Hint: Omit it from the simp argument list.
  simp ̵[̵h̵z̵e̵r̵o̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hzero]
          rw [h_if_val]; exact h_one_le
        · -- newKeys.length ≤ 2t-1 (parent was not full, added 1 key)
          rw [h_newKeys_len]; omega
        · -- children count: newChildren non-empty, length = children.length + 1
          rw [h_newChildren_len]; right
          have h_low : 2 ≤ children.length + 1 := by
            omega
          have h_high : children.length + 1 ≤ 2 * t := by
            unfold ChildBounded at h_cb; rcases h_cb with ⟨h_cb_rel, _, _⟩
            rcases h_cb_rel with (h_cb_empty | h_cb_eq)
            · have h_len0 : children.length = 0 := by simpa using h_cb_empty
              rw [h_len0]; omega
            · rw [h_cb_eq]
              have h_add := Nat.add_lt_add_right hparent_nonfull 1
              rw [Nat.sub_add_cancel (show 1 ≤ 2 * t from by omega)] at h_add
              rw [← Nat.succ_eq_add_one (keys.length + 1)]
              exact Nat.succ_le_of_lt h_add
          exact ⟨h_low, h_high⟩
        · -- sub-node occupancy propagation
          -- newChildren = (take i children) ++ [newLeft, newRight] ++ (drop (i+1) children)
          -- Due to ++ associativity: (take ++ [a,b]) ++ drop
          intro child hchild
          have h_or := List.mem_append.mp hchild
          rcases h_or with (h_take_or_new | h_drop)
          · -- child ∈ take i children ++ [newLeft, newRight]
            have h_or2 := List.mem_append.mp h_take_or_new
            rcases h_or2 with (h_take | h_new)
            · -- child ∈ take i children → inherits from parent occupancy
              have hmem : child ∈ children := (take_sublist i children).subset h_take
              unfold Occupancy at h_occ; rcases h_occ with ⟨_, _, _, h_pocc_sub⟩
              exact h_pocc_sub child hmem
            · -- child ∈ [newLeft, newRight]
              simp at h_new; rcases h_new with (rfl | rfl)
              · exact h_occ_left
              · exact h_occ_right
          · -- child ∈ drop (i+1) children → inherits from parent occupancy
            have hmem : child ∈ children := (drop_sublist (i+1) children).subset h_drop
            unfold Occupancy at h_occ; rcases h_occ with ⟨_, _, _, h_pocc_sub⟩
            exact h_pocc_sub child hmem

lemma pairwise_get_mono {l : List Nat} (hp : List.Pairwise (· ≤ ·) l) {j k : Nat}
    (hjk : j ≤ k) (hj : j < l.length) (hk : k < l.length) : l.get ⟨j, hj⟩ ≤ l.get ⟨k, hk⟩ := by
  induction' hp with a l' h_all hp_tail ih generalizing j k
  · exfalso; exact Nat.not_lt_zero j hj
  · rcases k with (rfl | k)
    · have hj0 : j = 0 := Nat.eq_zero_of_le_zero hjk
      subst hj0; exact Nat.le_refl _
    · have hk_lt : k < l'.length := by
        have : k+1 < (a :: l').length := hk; simpa using this
      rcases j with (rfl | j)
      · simp; apply h_all; apply List.get_mem
      · have hj_lt : j < l'.length := by
          have : j+1 < (a :: l').length := hj; simpa using this
        simp; apply ih (by omega) hj_lt hk_lt

theorem splitChild_preserves_sorted (t : Nat) (ht : 2 ≤ t)
    (keys : List Nat) (children : List BTree)
    (cKeys : List Nat) (cChildren : List BTree) (i : Nat)
    (h_lt : i < children.length)
    (hchild_eq : children.get ⟨i, h_lt⟩ = node cKeys cChildren)
    (hchild_full : cKeys.length = 2 * t - 1)
    (h_sorted : Sorted (node keys children))
    (h_cb : ChildBounded (node keys children)) :
    Sorted (splitChild t (node keys children) i) := by
  have h_keys_snd_nonempty : (cKeys.splitAt (t - 1)).2 ≠ [] := by
    have hlen : (cKeys.splitAt (t - 1)).2.length = t := by simp [hchild_full]; omega
    intro h; rw [h] at hlen; simp at hlen; omega
  dsimp [splitChild]; rw [dif_pos h_lt]
  have h_get : children[i] = node cKeys cChildren := by simpa using hchild_eq
  rw [h_get]; dsimp; rw [if_pos hchild_full]
  cases hk : cKeys.splitAt (t - 1) with
  | mk leftKeys keysRest =>
    have h_keysRest_nonempty : keysRest ≠ [] := by
      have : (cKeys.splitAt (t - 1)).2 = keysRest := by rw [hk]
      rw [← this]; exact h_keys_snd_nonempty
    cases hkr : keysRest with
    | nil => exact (h_keysRest_nonempty hkr).elim
    | cons medianKey rightKeys =>
      cases hc : cChildren.splitAt t with
      | mk leftCh rightCh =>
        show Sorted (BTree.node (take i keys ++ medianKey :: drop i keys)
          (take i children ++ [BTree.node leftKeys leftCh, BTree.node rightKeys rightCh] ++
            drop (i + 1) children))
        unfold Sorted at h_sorted; rcases h_sorted with ⟨h_keys_pairwise, h_children_sorted⟩
        have hchild_sorted : Sorted (BTree.node cKeys cChildren) := by
          rw [← hchild_eq]; apply h_children_sorted; apply List.get_mem
        unfold Sorted at hchild_sorted
        rcases hchild_sorted with ⟨h_cKeys_pairwise, h_cChildren_sorted⟩
        -- Children sorted: same pattern as occupancy sub-node proof
        have h_newChildren_sorted : ∀ child ∈ (take i children ++
            [BTree.node leftKeys leftCh, BTree.node rightKeys rightCh] ++
            drop (i + 1) children), Sorted child := by
          intro child hchild
          have h_or := List.mem_append.mp hchild
          rcases h_or with (h_take_or_new | h_drop)
          · have h_or2 := List.mem_append.mp h_take_or_new
            rcases h_or2 with (h_take | h_new)
            · have hmem : child ∈ children := (take_sublist i children).subset h_take
              exact h_children_sorted child hmem
            · simp at h_new; rcases h_new with (rfl | rfl)
              · unfold Sorted
                have h_lk : leftKeys = cKeys.take (t-1) := by
                  calc
                    leftKeys = (cKeys.splitAt (t-1)).1 := by rw [hk]
                    _ = cKeys.take (t-1) := by simp
                have h_left_pairwise : List.Pairwise (· ≤ ·) leftKeys := by
                  rw [h_lk]; exact List.Pairwise.take (i := t-1) h_cKeys_pairwise
                refine ⟨h_left_pairwise, ?_⟩
                intro c hc_mem
                have h_left_eq : leftCh = cChildren.take t := by
                  calc
                    leftCh = (cChildren.splitAt t).1 := by rw [hc]
                    _ = cChildren.take t := by simp
                rw [h_left_eq] at hc_mem
                apply h_cChildren_sorted
                exact (take_sublist t cChildren).subset hc_mem
              · unfold Sorted
                have h_rk : rightKeys = cKeys.drop t := by
                  calc
                    rightKeys = keysRest.drop 1 := by rw [hkr]; simp
                    _ = (cKeys.splitAt (t-1)).2.drop 1 := by rw [hk]
                    _ = (cKeys.drop (t-1)).drop 1 := by simp
                    _ = cKeys.drop ((t-1)+1) := by rw [← List.drop_drop]
                    _ = cKeys.drop t := by rw [show (t-1)+1 = t by omega]
                have h_right_pairwise : List.Pairwise (· ≤ ·) rightKeys := by
                  rw [h_rk]; exact List.Pairwise.drop (i := t) h_cKeys_pairwise
                refine ⟨h_right_pairwise, ?_⟩
                intro c hc_mem
                have h_right_eq : rightCh = cChildren.drop t := by
                  calc
                    rightCh = (cChildren.splitAt t).2 := by rw [hc]
                    _ = cChildren.drop t := by simp
                rw [h_right_eq] at hc_mem
                apply h_cChildren_sorted
                exact (drop_sublist t cChildren).subset hc_mem
          · have hmem : child ∈ children := (drop_sublist (i+1) children).subset h_drop
            exact h_children_sorted child hmem
        -- Keys pairwise: proved using pairwise_get_mono + ChildBounded bounds + pairwise_append.
        have h_keys_ok : List.Pairwise (· ≤ ·) (take i keys ++ medianKey :: drop i keys) := by
          -- pairwise properties of the two parts
          have h_take_pw : List.Pairwise (· ≤ ·) (take i keys) :=
            List.Pairwise.take (i := i) h_keys_pairwise
          have h_drop_pw : List.Pairwise (· ≤ ·) (drop i keys) :=
            List.Pairwise.drop (i := i) h_keys_pairwise
          -- cross-bound from original pairwise
          have h_keys_eq : take i keys ++ drop i keys = keys := by simp
          have h_pw_app : List.Pairwise (· ≤ ·) (take i keys ++ drop i keys) := by
            rw [h_keys_eq]; exact h_keys_pairwise
          have h_full := (List.pairwise_append (l₁ := take i keys) (l₂ := drop i keys)).mp h_pw_app
          rcases h_full with ⟨_, _, h_cross⟩
          -- medianKey is in cKeys (from the split)
          have h_median_in_cKeys : medianKey ∈ cKeys := by
            have h_cKeys_eq : cKeys = leftKeys ++ medianKey :: rightKeys := by
              calc
                cKeys = cKeys.take (t-1) ++ cKeys.drop (t-1) := by simp
                _ = (cKeys.splitAt (t-1)).1 ++ (cKeys.splitAt (t-1)).2 := by simp
                _ = leftKeys ++ keysRest := by rw [hk]
                _ = leftKeys ++ (medianKey :: rightKeys) := by rw [hkr]
            rw [h_cKeys_eq]; simp
          have h_median_mem : medianKey ∈ keysOf (BTree.node cKeys cChildren) := by
            unfold keysOf; simp [h_median_in_cKeys]
          -- Extract ChildBounded bounds (unfold once, using REPL-proven pattern)
          unfold ChildBounded at h_cb
          rcases h_cb with ⟨h_cb_rel, h_cb_bounds, _⟩
          have h_ilen : children.length = keys.length + 1 := by
            rcases h_cb_rel with (h_empty | h_eq)
            · exfalso
              have hlen0 : children.length = 0 := by simpa using h_empty
              rw [hlen0] at h_lt; exact Nat.not_lt_zero i h_lt
            · exact h_eq
          rcases h_cb_bounds i h_lt with ⟨h_lo_raw, h_hi_raw⟩
          have hi_le : i ≤ keys.length := by rw [h_ilen] at h_lt; omega
          have hchild_eq_get : children[i] = BTree.node cKeys cChildren := by simpa using hchild_eq
          -- lower bound (when i>0): keys[i-1] ≤ medianKey
          have h_lower (hi_pos : 0 < i) (hi_sub : i-1 < keys.length) :
              keys.get ⟨i-1, hi_sub⟩ ≤ medianKey := by
            rcases h_lo_raw with (hi0 | h_lo_match)
            · exact (Nat.ne_of_gt hi_pos hi0).elim
            · simp [hi_sub] at h_lo_match
              rw [hchild_eq_get] at h_lo_match
              exact h_lo_match medianKey h_median_mem
          -- Two cases: i < keys.length or i = keys.length
          by_cases hi_len : i < keys.length
          · -- i < keys.length: the upper bound keys[i] exists
            have h_upper_val : medianKey ≤ keys.get ⟨i, hi_len⟩ := by
              simp [hi_len] at h_hi_raw
              rw [hchild_eq_get] at h_hi_raw
              exact h_hi_raw medianKey h_median_mem
            -- Build take i keys ++ [medianKey] pairwise
            have h_take_le : ∀ a ∈ take i keys, a ≤ medianKey := by
              intro a ha
              rcases List.mem_iff_get.mp ha with ⟨n, h_eq⟩
              -- n : Fin (take i keys).length, so n.val < i (since length ≤ i)
              have hn_val_lt_i : n.val < i :=
                calc n.val < (take i keys).length := n.isLt
                _ ≤ i := by simp
              have hn_len : n.val < keys.length :=
                calc n.val < (take i keys).length := n.isLt
                _ ≤ keys.length := by simp
              -- (take i keys).get n = keys.get ⟨n.val, hn_len⟩
              have h_val : a = keys.get ⟨n.val, hn_len⟩ := by
                calc a = (take i keys).get n := by rw [h_eq]
                _ = keys.get ⟨n.val, hn_len⟩ := by simp
              rw [h_val]
              -- keys[j] ≤ keys[i-1] (pairwise, j < i) ≤ medianKey (h_lower)
              by_cases hi0 : i = 0
              · subst hi0; omega
              · have hi_pos : 0 < i := Nat.pos_of_ne_zero hi0
                have hi_sub : i-1 < keys.length := by omega
                have h_pw : keys.get ⟨n.val, hn_len⟩ ≤ keys.get ⟨i-1, hi_sub⟩ :=
                  pairwise_get_mono h_keys_pairwise (by omega) hn_len hi_sub
                exact Nat.le_trans h_pw (h_lower hi_pos hi_sub)
            -- Build medianKey ≤ ∀ b ∈ drop i keys
            have h_drop_le : ∀ b ∈ drop i keys, medianKey ≤ b := by
              intro b hb
              rcases List.mem_iff_get.mp hb with ⟨n, h_eq⟩
              -- n : Fin (drop i keys).length
              -- (drop i keys).get n = keys.get ⟨i + n.val, ...⟩
              have hn_total_len : i + n.val < keys.length := by
                have : (drop i keys).length = keys.length - i := by simp
                have : n.val < keys.length - i := by
                  rw [← this]; exact n.isLt
                omega
              have h_val : b = keys.get ⟨i + n.val, hn_total_len⟩ := by
                calc b = (drop i keys).get n := by rw [h_eq]
                _ = keys.get ⟨i + n.val, hn_total_len⟩ := by simp
              rw [h_val]
              -- medianKey ≤ keys[i] (h_upper_val) ≤ keys[i + n.val] (pairwise, i ≤ i+n.val)
              have h_pw : keys.get ⟨i, hi_len⟩ ≤ keys.get ⟨i + n.val, hn_total_len⟩ :=
                pairwise_get_mono h_keys_pairwise (by omega) hi_len hn_total_len
              exact Nat.le_trans h_upper_val h_pw
            -- Assemble with pairwise_append
            have h_singleton : List.Pairwise (· ≤ ·) [medianKey] := by simp
            have h_prefix : List.Pairwise (· ≤ ·) (take i keys ++ [medianKey]) :=
              (List.pairwise_append (l₁ := take i keys) (l₂ := [medianKey])).mpr
                ⟨h_take_pw, h_singleton, λ a ha b hb => by
                  simp at hb; subst hb; exact h_take_le a ha⟩
            -- Need to rewrite the goal to match pairwise_append's l₁ ++ l₂ pattern
            have h_assoc : take i keys ++ medianKey :: drop i keys = (take i keys ++ [medianKey]) ++ drop i keys := by simp
            rw [h_assoc]
            exact ((List.pairwise_append (l₁ := take i keys ++ [medianKey]) (l₂ := drop i keys)).mpr
              ⟨h_prefix, h_drop_pw, λ a ha b hb => by
                rw [List.mem_append] at ha; rcases ha with (ha | ha)
                · exact h_cross a ha b hb
                · simp at ha; subst ha; exact h_drop_le b hb⟩)
          · -- i = keys.length: no upper bound key, drop i keys = []
            have hi_eq : i = keys.length := by omega
            have h_drop_empty : drop i keys = [] := by rw [hi_eq]; simp
            rw [h_drop_empty]
            -- Goal: List.Pairwise (· ≤ ·) (take i keys ++ medianKey :: [])
            -- medianKey :: [] = [medianKey]
            have h_cons_nil : medianKey :: [] = [medianKey] := by simp
            rw [h_cons_nil]
            -- Goal: List.Pairwise (· ≤ ·) (take i keys ++ [medianKey])
            -- Same as the h_prefix proof above, but we use h_take_pw from the outer scope
            have h_take_le : ∀ a ∈ take i keys, a ≤ medianKey := by
              intro a ha
              rcases List.mem_iff_get.mp ha with ⟨n, h_eq⟩
              have hn_len : n.val < keys.length :=
                Nat.lt_of_lt_of_le n.isLt (by simp)
              have h_val : a = keys.get ⟨n.val, hn_len⟩ := by
                calc a = (take i keys).get n := by rw [h_eq]
                _ = keys.get ⟨n.val, hn_len⟩ := by simp
              rw [h_val]
              by_cases hi0 : i = 0
              · subst hi0; omega
              · have hi_pos : 0 < i := Nat.pos_of_ne_zero hi0
                have hi_sub : i-1 < keys.length := by omega
                have h_pw : keys.get ⟨n.val, hn_len⟩ ≤ keys.get ⟨i-1, hi_sub⟩ :=
                  pairwise_get_mono h_keys_pairwise (by omega) hn_len hi_sub
                exact Nat.le_trans h_pw (h_lower hi_pos hi_sub)
            have h_singleton : List.Pairwise (· ≤ ·) [medianKey] := by simp
            exact (List.pairwise_append (l₁ := take i keys) (l₂ := [medianKey])).mpr
              ⟨h_take_pw, h_singleton, λ a ha b hb => by simp at hb; subst hb; exact h_take_le a ha⟩
        unfold Sorted
        refine ⟨h_keys_ok, h_newChildren_sorted⟩

ChildBounded preservation infrastructure

The proof of splitChild_preserves_childBounded relies on:

keysOf_node_subset: the keys of a node built from sublists is a subset.
childBounded_node_nil: a node with no children is trivially bounded.
keysOf_take_le_pivot / keysOf_drop_ge_pivot: the median key sandwiches the two new children (this is the ordering content that needs Sorted).
childBounded_take_of_full / childBounded_drop_of_full: ChildBounded survives truncating a full node's keys/children to a prefix/suffix.

If ks ⊆ ks' and cs ⊆ cs', then the flattened keys of node ks cs are a subset of those of node ks' cs'. This is the user-suggested keysOf_subset lemma, phrased for arbitrary sublists (used for both the left and right split children).

lemma keysOf_node_subset {ks ks' : List Nat} {cs cs' : List BTree}
    (hk : ks ⊆ ks') (hc : cs ⊆ cs') :
    keysOf (node ks cs) ⊆ keysOf (node ks' cs') := by
  intro x hx
  simp only [keysOf, List.mem_append, List.mem_flatMap] at hx ⊢
  rcases hx with hxk | ⟨c, hcm, hxc⟩
  · exact Or.inl (hk hxk)
  · exact Or.inr ⟨c, hc hcm, hxc⟩

A node with no children is trivially ChildBounded.

lemma childBounded_node_nil (ks : List Nat) : ChildBounded (node ks []) := by
  unfold ChildBounded
  refine ⟨Or.inl (by simp), ?_, ?_⟩
  · intro j hj; simp at hj
  · intro c hc; simp at hc

Every key beneath the left split node node (ks.take m) (cs.take (m+1)) is ≤ ks[m] (the median key). Uses sortedness of ks and the child's own ChildBounded upper bounds.


lemma keysOf_take_le_pivot {ks : List Nat} {cs : List BTree} {m : Nat}
    (h_pw : List.Pairwise (· ≤ ·) ks)
    (h_cb : ChildBounded (node ks cs))
    (hm : m < ks.length) :
    ∀ k ∈ keysOf (node (ks.take m) (cs.take (m + 1))), k ≤ ks[m] := by
  intro k hk
  simp only [keysOf, List.mem_append, List.mem_flatMap] at hk
  rcases hk with hk | ⟨c, hc, hkc⟩
  · -- key from the truncated key list: monotone since `ks` is sorted
    rcases List.mem_iff_get.mp hk with ⟨n, h_eq⟩
    have hn_m : n.val < m := Nat.lt_of_lt_of_le n.isLt (List.length_take_le m ks)
    have hn_ks : n.val < ks.length := by omega
    have h_val : k = ks.get ⟨n.val, hn_ks⟩ := by
      calc k = (ks.take m).get n := by rw [h_eq]
        _ = ks.get ⟨n.val, hn_ks⟩ := by simp
    rw [h_val]
    exact pairwise_get_mono h_pw (by omega) hn_ks hm
  · -- key from a child subtree: bounded by `ks[n] ≤ ks[m]`
    rcases List.mem_iff_get.mp hc with ⟨n, h_eq⟩
    have hn_m1 : n.val < m + 1 := Nat.lt_of_lt_of_le n.isLt (List.length_take_le (m + 1) cs)
    have hn_cs : n.val < cs.length := Nat.lt_of_lt_of_le n.isLt (List.length_take_le' (m + 1) cs)
    have hn_ks : n.val < ks.length := by omega
    have hc_eq : c = cs.get ⟨n.val, hn_cs⟩ := by
      calc c = (cs.take (m + 1)).get n := by rw [h_eq]
        _ = cs.get ⟨n.val, hn_cs⟩ := by simp
    unfold ChildBounded at h_cb
    rcases h_cb with ⟨_, h_bounds, _⟩
    have hub := (h_bounds n.val hn_cs).2
    simp only [List.getElem?_eq_getElem hn_ks] at hub
    rw [← hc_eq] at hub
    have h1 : k ≤ ks[n.val] := hub k hkc
    have h2 := pairwise_get_mono h_pw (show n.val ≤ m by omega) hn_ks hm
    simp only [List.get_eq_getElem] at h2
    exact le_trans h1 h2

Every key beneath the right split node node (ks.drop (m+1)) (cs.drop (m+1)) is ≥ ks[m] (the median key). Symmetric to keysOf_take_le_pivot.


lemma keysOf_drop_ge_pivot {ks : List Nat} {cs : List BTree} {m : Nat}
    (h_pw : List.Pairwise (· ≤ ·) ks)
    (h_cb : ChildBounded (node ks cs))
    (hm : m < ks.length) :
    ∀ k ∈ keysOf (node (ks.drop (m + 1)) (cs.drop (m + 1))), ks[m] ≤ k := by
  intro k hk
  simp only [keysOf, List.mem_append, List.mem_flatMap] at hk
  rcases hk with hk | ⟨c, hc, hkc⟩
  · -- key from the truncated key list
    rcases List.mem_iff_get.mp hk with ⟨n, h_eq⟩
    have hn_len : (m + 1) + n.val < ks.length := by
      have h : n.val < ks.length - (m + 1) := by rw [← List.length_drop]; exact n.isLt
      omega
    have h_val : k = ks.get ⟨(m + 1) + n.val, hn_len⟩ := by
      calc k = (ks.drop (m + 1)).get n := by rw [h_eq]
        _ = ks.get ⟨(m + 1) + n.val, hn_len⟩ := by simp
    rw [h_val]
    exact pairwise_get_mono h_pw (by omega) hm hn_len
  · -- key from a child subtree: bounded by `ks[m] ≤ ks[(m+1)+n-1]`
    rcases List.mem_iff_get.mp hc with ⟨n, h_eq⟩
    have hn_cs : (m + 1) + n.val < cs.length := by
      have h : n.val < cs.length - (m + 1) := by rw [← List.length_drop]; exact n.isLt
      omega
    unfold ChildBounded at h_cb
    rcases h_cb with ⟨h_rel, h_bounds, _⟩
    have h_len : cs.length = ks.length + 1 := by
      rcases h_rel with h_empty | h_len
      · have hnil : cs = [] := List.isEmpty_iff.mp h_empty
        have hlen0 : cs.length = 0 := by simp [hnil]
        omega
      · exact h_len
    have hidx : (m + 1) + n.val - 1 < ks.length := by omega
    have hc_eq : c = cs.get ⟨(m + 1) + n.val, hn_cs⟩ := by
      calc c = (cs.drop (m + 1)).get n := by rw [h_eq]
        _ = cs.get ⟨(m + 1) + n.val, hn_cs⟩ := by simp
    have hlb := (h_bounds ((m + 1) + n.val) hn_cs).1
    rcases hlb with h0 | hlbmatch
    · omega
    · simp only [List.getElem?_eq_getElem hidx] at hlbmatch
      rw [← hc_eq] at hlbmatch
      have h1 : ks[(m + 1) + n.val - 1] ≤ k := hlbmatch k hkc
      have h2 := pairwise_get_mono h_pw (show m ≤ (m + 1) + n.val - 1 by omega) hm hidx
      simp only [List.get_eq_getElem] at h2
      exact le_trans h2 h1

ChildBounded survives truncating a node's keys to take m and children to take (m+1) (the left result of a split).


lemma childBounded_take_of_full {ks : List Nat} {cs : List BTree} {m : Nat}
    (h_cb : ChildBounded (node ks cs)) (hm : m < ks.length) :
    ChildBounded (node (ks.take m) (cs.take (m + 1))) := by
  have h_cb' := h_cb
  unfold ChildBounded at h_cb'
  rcases h_cb' with ⟨h_rel, h_bounds, h_sub⟩
  rcases h_rel with h_empty | h_len
  · have hcs : cs = [] := by cases cs with | nil => rfl | cons x xs => simp at h_empty
    subst hcs
    simpa using childBounded_node_nil (ks.take m)
  · unfold ChildBounded
    refine ⟨?_, ?_, ?_⟩
    · right; rw [List.length_take, List.length_take]; omega
    · intro j hj
      have hj_cs : j < cs.length := by have := hj; rw [List.length_take] at this; omega
      have hchild : (cs.take (m + 1)).get ⟨j, hj⟩ = cs.get ⟨j, hj_cs⟩ := by simp
      refine ⟨?_, ?_⟩
      · rcases Nat.eq_zero_or_pos j with hj0 | hjpos
        · exact Or.inl hj0
        · right
          have hj1_m : j - 1 < m := by have := hj; rw [List.length_take] at this; omega
          have hj1_ks : j - 1 < ks.length := by omega
          rw [List.getElem?_take_of_lt hj1_m, List.getElem?_eq_getElem hj1_ks]
          have hlb := (h_bounds j hj_cs).1
          rcases hlb with h0 | hlbmatch
          · omega
          · simp only [List.getElem?_eq_getElem hj1_ks] at hlbmatch
            intro k hk; rw [hchild] at hk; exact hlbmatch k hk
      · by_cases hj_m : j < m
        · have hj_ks : j < ks.length := by omega
          rw [List.getElem?_take_of_lt hj_m, List.getElem?_eq_getElem hj_ks]
          have hub := (h_bounds j hj_cs).2
          simp only [List.getElem?_eq_getElem hj_ks] at hub
          intro k hk; rw [hchild] at hk; exact hub k hk
        · have hnone : (ks.take m)[j]? = none := by
            apply List.getElem?_eq_none; rw [List.length_take]; omega
          rw [hnone]; exact trivial
    · intro c hc
      exact h_sub c ((List.take_subset (m + 1) cs) hc)

ChildBounded survives dropping d keys and d children (the right result of a split, with d = t).


lemma childBounded_drop_of_full {ks : List Nat} {cs : List BTree} {d : Nat}
    (h_cb : ChildBounded (node ks cs)) (hd : 0 < d) (hd_cs : d < cs.length) :
    ChildBounded (node (ks.drop d) (cs.drop d)) := by
  have h_cb' := h_cb
  unfold ChildBounded at h_cb'
  rcases h_cb' with ⟨h_rel, h_bounds, h_sub⟩
  have h_len : cs.length = ks.length + 1 := by
    rcases h_rel with h_empty | h_len
    · have hnil : cs = [] := by cases cs with | nil => rfl | cons x xs => simp at h_empty
      rw [hnil] at hd_cs; simp at hd_cs
    · exact h_len
  unfold ChildBounded
  refine ⟨?_, ?_, ?_⟩
  · right; rw [List.length_drop, List.length_drop]; omega
  · intro j hj
    have hj_len : j < cs.length - d := by have := hj; rw [List.length_drop] at this; exact this
    have hdj_cs : d + j < cs.length := by omega
    have hchild : (cs.drop d).get ⟨j, hj⟩ = cs.get ⟨d + j, hdj_cs⟩ := by simp
    refine ⟨?_, ?_⟩
    · rcases Nat.eq_zero_or_pos j with hj0 | hjpos
      · exact Or.inl hj0
      · right
        have hidx : d + j - 1 < ks.length := by omega
        have heq_idx : d + (j - 1) = d + j - 1 := by omega
        rw [List.getElem?_drop, heq_idx, List.getElem?_eq_getElem hidx]
        have hlb := (h_bounds (d + j) hdj_cs).1
        rcases hlb with h0 | hlbmatch
        · omega
        · simp only [List.getElem?_eq_getElem hidx] at hlbmatch
          intro k hk; rw [hchild] at hk; exact hlbmatch k hk
    · by_cases hdj : d + j < ks.length
      · rw [List.getElem?_drop, List.getElem?_eq_getElem hdj]
        have hub := (h_bounds (d + j) hdj_cs).2
        simp only [List.getElem?_eq_getElem hdj] at hub
        intro k hk; rw [hchild] at hk; exact hub k hk
      · have hnone : (ks.drop d)[j]? = none := by
          rw [List.getElem?_drop]; apply List.getElem?_eq_none; omega
        rw [hnone]; exact trivial
  · intro c hc
    exact h_sub c ((List.drop_subset d cs) hc)

B-TREE-SPLIT-CHILD preserves ChildBounded. Splitting a full child of a non-full node keeps the key-range invariant: the promoted median key becomes a new separator that sandwiches the two halves, and every other separator/child relation is inherited from the original tree.


theorem splitChild_preserves_childBounded (t : Nat) (ht : 2 ≤ t)
    (keys : List Nat) (children : List BTree)
    (cKeys : List Nat) (cChildren : List BTree) (i : Nat)
    (h_lt : i < children.length)
    (hchild_eq : children.get ⟨i, h_lt⟩ = node cKeys cChildren)
    (hchild_full : cKeys.length = 2 * t - 1)
    (h_cb : ChildBounded (node keys children))
    (h_sorted : Sorted (node keys children)) :
    ChildBounded (splitChild t (node keys children) i) := by
  -- Extract the parent's ChildBounded components.
  have h_cb' := h_cb
  unfold ChildBounded at h_cb'
  obtain ⟨h_cb_rel, h_cb_bounds, h_cb_sub⟩ := h_cb'
  have h_ch_len : children.length = keys.length + 1 := by
    rcases h_cb_rel with h_empty | h_eq
    · have hnil : children = [] := List.isEmpty_iff.mp h_empty
      have : children.length = 0 := by simp [hnil]
      omega
    · exact h_eq
  have h_i_le_keys : i ≤ keys.length := by omega
  -- Unfold `splitChild` (same pattern as `splitChild_preserves_sorted`).
  have h_keys_snd_nonempty : (cKeys.splitAt (t - 1)).2 ≠ [] := by
    have hlen : (cKeys.splitAt (t - 1)).2.length = t := by simp [hchild_full]; omega
    intro h; rw [h] at hlen; simp at hlen; omega
  dsimp [splitChild]; rw [dif_pos h_lt]
  have h_get : children[i] = node cKeys cChildren := by simpa using hchild_eq
  rw [h_get]; dsimp; rw [if_pos hchild_full]
  cases hk : cKeys.splitAt (t - 1) with
  | mk leftKeys keysRest =>
    have h_keysRest_nonempty : keysRest ≠ [] := by
      have : (cKeys.splitAt (t - 1)).2 = keysRest := by rw [hk]
      rw [← this]; exact h_keys_snd_nonempty
    cases hkr : keysRest with
    | nil => exact (h_keysRest_nonempty hkr).elim
    | cons medianKey rightKeys =>
      cases hc : cChildren.splitAt t with
      | mk leftCh rightCh =>
        show ChildBounded (BTree.node (take i keys ++ medianKey :: drop i keys)
          (take i children ++ [BTree.node leftKeys leftCh, BTree.node rightKeys rightCh] ++
            drop (i + 1) children))
        -- Relate the local split names to `take`/`drop` of the child's keys/children.
        have h_lk : leftKeys = cKeys.take (t - 1) := by
          calc leftKeys = (cKeys.splitAt (t - 1)).1 := by rw [hk]
            _ = cKeys.take (t - 1) := by simp
        have h_keysRest_eq : keysRest = cKeys.drop (t - 1) := by
          calc keysRest = (cKeys.splitAt (t - 1)).2 := by rw [hk]
            _ = cKeys.drop (t - 1) := by simp
        have h_rk : rightKeys = cKeys.drop t := by
          calc rightKeys = keysRest.drop 1 := by rw [hkr]; simp
            _ = (cKeys.drop (t - 1)).drop 1 := by rw [h_keysRest_eq]
            _ = cKeys.drop ((t - 1) + 1) := by rw [← List.drop_drop]
            _ = cKeys.drop t := by rw [show (t - 1) + 1 = t from by omega]
        have h_left_eq : leftCh = cChildren.take t := by
          calc leftCh = (cChildren.splitAt t).1 := by rw [hc]
            _ = cChildren.take t := by simp
        have h_right_eq : rightCh = cChildren.drop t := by
          calc rightCh = (cChildren.splitAt t).2 := by rw [hc]
            _ = cChildren.drop t := by simp
        have h_t1_lt : t - 1 < cKeys.length := by omega
        have h_median : cKeys[t - 1]? = some medianKey := by
          have hh : (cKeys.drop (t - 1))[0]? = some medianKey := by
            rw [← h_keysRest_eq, hkr]; rfl
          rw [List.getElem?_drop] at hh; simpa using hh
        have h_median_eq : medianKey = cKeys[t - 1] := by
          rw [List.getElem?_eq_getElem h_t1_lt] at h_median
          injection h_median with h_median; exact h_median.symm
        -- Child invariants.
        have h_child_cb : ChildBounded (node cKeys cChildren) := by
          rw [← hchild_eq]; apply h_cb_sub; apply List.get_mem
        have h_cKeys_pw : List.Pairwise (· ≤ ·) cKeys := by
          have h_cs : Sorted (node cKeys cChildren) := by
            rw [← hchild_eq]
            unfold Sorted at h_sorted; rcases h_sorted with ⟨_, h_sc⟩
            apply h_sc; apply List.get_mem
          unfold Sorted at h_cs; exact h_cs.1
        have h_cChildren_len := child_children_len_of_full_cb ht h_child_cb hchild_full
        -- The median key sandwiches the two new children.
        have h_left_le : ∀ k ∈ keysOf (node leftKeys leftCh), k ≤ medianKey := by
          intro k hk
          rw [h_lk, h_left_eq] at hk
          rw [h_median_eq]
          have hp := keysOf_take_le_pivot h_cKeys_pw h_child_cb h_t1_lt
          rw [show (t - 1) + 1 = t from by omega] at hp
          exact hp k hk
        have h_right_ge : ∀ k ∈ keysOf (node rightKeys rightCh), medianKey ≤ k := by
          intro k hk
          rw [h_rk, h_right_eq] at hk
          rw [h_median_eq]
          have hp := keysOf_drop_ge_pivot h_cKeys_pw h_child_cb h_t1_lt
          rw [show (t - 1) + 1 = t from by omega] at hp
          exact hp k hk
        -- The two new children are themselves ChildBounded.
        have h_cb_left : ChildBounded (node leftKeys leftCh) := by
          have hh := childBounded_take_of_full h_child_cb h_t1_lt
          rw [show (t - 1) + 1 = t from by omega] at hh
          rw [h_lk, h_left_eq]; exact hh
        have h_cb_right : ChildBounded (node rightKeys rightCh) := by
          rcases h_cChildren_len with h0 | h2t
          · have hnil : cChildren = [] := by
              cases cChildren with | nil => rfl | cons x xs => simp at h0
            have hrc : rightCh = [] := by rw [h_right_eq, hnil]; simp
            rw [hrc]; exact childBounded_node_nil rightKeys
          · have hd_cs : t < cChildren.length := by rw [h2t]; omega
            have hh := childBounded_drop_of_full h_child_cb (by omega) hd_cs
            rw [h_rk, h_right_eq]; exact hh
        -- `newKeys[·]?` computed by position relative to the inserted median.
        have h_P_len : (take i keys).length = i := by rw [List.length_take]; omega
        have hNK_lt : ∀ j', j' < i →
            (take i keys ++ medianKey :: drop i keys)[j']? = keys[j']? := by
          intro j' hj'
          rw [List.getElem?_append_left (by rw [h_P_len]; exact hj'), List.getElem?_take_of_lt hj']
        have hNK_eq : (take i keys ++ medianKey :: drop i keys)[i]? = some medianKey := by
          rw [List.getElem?_append_right (le_of_eq h_P_len), h_P_len]; simp
        have hNK_gt : ∀ j', i < j' →
            (take i keys ++ medianKey :: drop i keys)[j']? = keys[j' - 1]? := by
          intro j' hj'
          rw [List.getElem?_append_right (by rw [h_P_len]; omega), h_P_len,
              show j' - i = (j' - i - 1) + 1 from by omega, List.getElem?_cons_succ,
              List.getElem?_drop, show i + (j' - i - 1) = j' - 1 from by omega]
        unfold ChildBounded
        refine ⟨?_, ?_, ?_⟩
        · -- Count relation.
          right
          simp only [List.length_append, List.length_cons, List.length_nil,
            List.length_take, List.length_drop]
          omega
        · -- Parent key-range bounds.
          have h_A_len : (take i children).length = i := by rw [List.length_take]; omega
          have h_AB_len : (take i children ++
              [node leftKeys leftCh, node rightKeys rightCh]).length = i + 2 := by
            simp [List.length_append, h_A_len]
          have h_nc_len : (take i children ++
              [node leftKeys leftCh, node rightKeys rightCh] ++ drop (i + 1) children).length
              = children.length + 1 := by
            simp only [List.length_append, List.length_cons, List.length_nil,
              List.length_take, List.length_drop]
            omega
          have hsub_left : keysOf (node leftKeys leftCh) ⊆ keysOf (node cKeys cChildren) :=
            keysOf_node_subset (by rw [h_lk]; exact List.take_subset _ _)
              (by rw [h_left_eq]; exact List.take_subset _ _)
          have hsub_right : keysOf (node rightKeys rightCh) ⊆ keysOf (node cKeys cChildren) :=
            keysOf_node_subset (by rw [h_rk]; exact List.drop_subset _ _)
              (by rw [h_right_eq]; exact List.drop_subset _ _)
          intro j hj
          have hj' : j < children.length + 1 := h_nc_len ▸ hj
          rcases Nat.lt_trichotomy j i with hlt | heq | hgt
          · -- Region 1: `j < i` — unchanged left children.
            have hj_ch : j < children.length := by omega
            have hlt_AB : j < (take i children ++
                [node leftKeys leftCh, node rightKeys rightCh]).length := by rw [h_AB_len]; omega
            have hlt_A : j < (take i children).length := by rw [h_A_len]; omega
            have hchild : (take i children ++ [node leftKeys leftCh, node rightKeys rightCh] ++
                drop (i + 1) children).get ⟨j, hj⟩ = children.get ⟨j, hj_ch⟩ := by
              simp only [List.get_eq_getElem]
              rw [List.getElem_append_left hlt_AB, List.getElem_append_left hlt_A]; simp
            refine ⟨?_, ?_⟩
            · rcases Nat.eq_zero_or_pos j with hj0 | hjpos
              · exact Or.inl hj0
              · right
                rw [hNK_lt (j - 1) (by omega), hchild]
                rcases (h_cb_bounds j hj_ch).1 with h0 | hbmatch
                · omega
                · exact hbmatch
            · rw [hNK_lt j hlt, hchild]
              exact (h_cb_bounds j hj_ch).2
          · -- Region 2: `j = i` — the new left child.
            have hlt_AB : j < (take i children ++
                [node leftKeys leftCh, node rightKeys rightCh]).length := by rw [h_AB_len]; omega
            have hge_A : (take i children).length ≤ j := by rw [h_A_len]; omega
            have hchild : (take i children ++ [node leftKeys leftCh, node rightKeys rightCh] ++
                drop (i + 1) children).get ⟨j, hj⟩ = node leftKeys leftCh := by
              simp only [List.get_eq_getElem]
              rw [List.getElem_append_left hlt_AB, List.getElem_append_right hge_A]
              simp [h_A_len, show j - i = 0 from by omega]
            refine ⟨?_, ?_⟩
            · rcases Nat.eq_zero_or_pos j with hj0 | hjpos
              · exact Or.inl hj0
              · right
                rw [hNK_lt (j - 1) (by omega), hchild, show j - 1 = i - 1 from by omega]
                have hb := (h_cb_bounds i h_lt).1
                rw [hchild_eq] at hb
                rcases hb with h0 | hbmatch
                · omega
                · revert hbmatch
                  cases keys[i - 1]? with
                  | none => intro _; trivial
                  | some lo => intro hbmatch; exact fun k hk => hbmatch k (hsub_left hk)
            · have hjk : (take i keys ++ medianKey :: drop i keys)[j]? = some medianKey := by
                rw [show j = i from heq]; exact hNK_eq
              rw [hjk, hchild]; exact h_left_le
          · rcases Nat.lt_or_ge j (i + 2) with hj2 | hj2
            · -- Region 3: `j = i + 1` — the new right child.
              have hlt_AB : j < (take i children ++
                  [node leftKeys leftCh, node rightKeys rightCh]).length := by rw [h_AB_len]; omega
              have hge_A : (take i children).length ≤ j := by rw [h_A_len]; omega
              have hchild : (take i children ++ [node leftKeys leftCh, node rightKeys rightCh] ++
                  drop (i + 1) children).get ⟨j, hj⟩ = node rightKeys rightCh := by
                simp only [List.get_eq_getElem]
                rw [List.getElem_append_left hlt_AB, List.getElem_append_right hge_A]
                simp [h_A_len, show j - i = 1 from by omega]
              refine ⟨?_, ?_⟩
              · right
                rw [show j - 1 = i from by omega, hNK_eq, hchild]
                exact h_right_ge
              · rw [hNK_gt j (by omega), show j - 1 = i from by omega, hchild]
                have hb := (h_cb_bounds i h_lt).2
                rw [hchild_eq] at hb
                revert hb
                cases keys[i]? with
                | none => intro _; trivial
                | some hi => intro hb; exact fun k hk => hb k (hsub_right hk)
            · -- Region 4: `j ≥ i + 2` — unchanged right children (shifted by one).
              have hj1_ch : j - 1 < children.length := by omega
              have hge_AB : (take i children ++
                  [node leftKeys leftCh, node rightKeys rightCh]).length ≤ j := by
                rw [h_AB_len]; omega
              have hchild : (take i children ++ [node leftKeys leftCh, node rightKeys rightCh] ++
                  drop (i + 1) children).get ⟨j, hj⟩ = children.get ⟨j - 1, hj1_ch⟩ := by
                simp only [List.get_eq_getElem]
                rw [List.getElem_append_right hge_AB]
                simp only [h_AB_len, List.getElem_drop,
                  show (i + 1) + (j - (i + 2)) = j - 1 from by omega]
              refine ⟨?_, ?_⟩
              · right
                rw [hNK_gt (j - 1) (by omega), hchild]
                rcases (h_cb_bounds (j - 1) hj1_ch).1 with h0 | hbmatch
                · omega
                · exact hbmatch
              · rw [hNK_gt j (by omega), hchild]
                exact (h_cb_bounds (j - 1) hj1_ch).2
        · -- Recursive ChildBounded of every new child.
          intro child hchild
          rcases List.mem_append.mp hchild with h_take_new | h_drop
          · rcases List.mem_append.mp h_take_new with h_take | h_new
            · exact h_cb_sub child ((List.take_subset i children) h_take)
            · simp at h_new; rcases h_new with rfl | rfl
              · exact h_cb_left
              · exact h_cb_right
          · exact h_cb_sub child ((List.drop_subset (i + 1) children) h_drop)

B-TREE-SPLIT-CHILD preserves WellFormed. Splitting a full child i of a non-full node keeps all four structural invariants simultaneously. This is the capstone that combines splitChild_preserves_sorted, splitChild_preserves_childBounded, splitChild_preserves_occupancy, and splitChild_preserves_sameDepth. The side condition cChildren = [] ∨ t < cChildren.length needed by the SameDepth lemma is derived from the child's own ChildBounded invariant.


theorem splitChild_preserves_wellFormed (t : Nat) (ht : 2 ≤ t)
    (keys : List Nat) (children : List BTree)
    (cKeys : List Nat) (cChildren : List BTree) (i : Nat)
    (h_lt : i < children.length)
    (hchild_eq : children.get ⟨i, h_lt⟩ = node cKeys cChildren)
    (hchild_full : cKeys.length = 2 * t - 1)
    (hparent_nonfull : keys.length < 2 * t - 1)
    (h_wf : WellFormed t (node keys children)) :
    WellFormed t (splitChild t (node keys children) i) := by
  obtain ⟨h_sorted, h_cb, h_occ, h_sd⟩ := h_wf
  -- The split child is itself `ChildBounded`, so its child count is `0` or `2t`.
  have h_child_cb : ChildBounded (node cKeys cChildren) := by
    rw [← hchild_eq]
    have hcb := h_cb
    unfold ChildBounded at hcb; rcases hcb with ⟨_, _, h_sub⟩
    apply h_sub; apply List.get_mem
  have hchild_children : cChildren = [] ∨ t < cChildren.length := by
    rcases child_children_len_of_full_cb ht h_child_cb hchild_full with h0 | h2t
    · left; cases cChildren with | nil => rfl | cons x xs => simp at h0
    · right; rw [h2t]; omega
  exact ⟨splitChild_preserves_sorted t ht keys children cKeys cChildren i h_lt hchild_eq
            hchild_full h_sorted h_cb,
         splitChild_preserves_childBounded t ht keys children cKeys cChildren i h_lt hchild_eq
            hchild_full h_cb h_sorted,
         splitChild_preserves_occupancy t ht keys children cKeys cChildren i h_lt hchild_eq
            hchild_full hparent_nonfull h_occ h_cb,
         splitChild_preserves_sameDepth t ht keys children cKeys cChildren i h_lt hchild_eq
            hchild_full hchild_children h_sd⟩

B-TREE-SPLIT-CHILD preserves the key multiset. Splitting a full child neither loses nor introduces keys: the flattened key list of the result is a permutation of the original. No ordering hypotheses are needed — this is a pure contents fact, complementing the structural-invariant theorems above.


theorem splitChild_keys_perm (t : Nat) (ht : 2 ≤ t)
    (keys : List Nat) (children : List BTree)
    (cKeys : List Nat) (cChildren : List BTree) (i : Nat)
    (h_lt : i < children.length)
    (hchild_eq : children.get ⟨i, h_lt⟩ = node cKeys cChildren)
    (hchild_full : cKeys.length = 2 * t - 1) :
    (keysOf (splitChild t (node keys children) i)).Perm (keysOf (node keys children)) := by
  have h_keys_snd_nonempty : (cKeys.splitAt (t - 1)).2 ≠ [] := by
    have hlen : (cKeys.splitAt (t - 1)).2.length = t := by simp [hchild_full]; omega
    intro h; rw [h] at hlen; simp at hlen; omega
  dsimp [splitChild]; rw [dif_pos h_lt]
  have h_get : children[i] = node cKeys cChildren := by simpa using hchild_eq
  rw [h_get]; dsimp; rw [if_pos hchild_full]
  cases hk : cKeys.splitAt (t - 1) with
  | mk leftKeys keysRest =>
    have h_keysRest_nonempty : keysRest ≠ [] := by
      have : (cKeys.splitAt (t - 1)).2 = keysRest := by rw [hk]
      rw [← this]; exact h_keys_snd_nonempty
    cases hkr : keysRest with
    | nil => exact (h_keysRest_nonempty hkr).elim
    | cons medianKey rightKeys =>
      cases hc : cChildren.splitAt t with
      | mk leftCh rightCh =>
        show (keysOf (BTree.node (take i keys ++ medianKey :: drop i keys)
          (take i children ++ [BTree.node leftKeys leftCh, BTree.node rightKeys rightCh] ++
            drop (i + 1) children))).Perm (keysOf (node keys children))
        have h_lk : leftKeys = cKeys.take (t - 1) := by
          calc leftKeys = (cKeys.splitAt (t - 1)).1 := by rw [hk]
            _ = cKeys.take (t - 1) := by simp
        have h_keysRest_eq : keysRest = cKeys.drop (t - 1) := by
          calc keysRest = (cKeys.splitAt (t - 1)).2 := by rw [hk]
            _ = cKeys.drop (t - 1) := by simp
        have h_left_eq : leftCh = cChildren.take t := by
          calc leftCh = (cChildren.splitAt t).1 := by rw [hc]
            _ = cChildren.take t := by simp
        have h_right_eq : rightCh = cChildren.drop t := by
          calc rightCh = (cChildren.splitAt t).2 := by rw [hc]
            _ = cChildren.drop t := by simp
        -- The three list decompositions that make the multiset match up.
        have h_cKeys_decomp : cKeys = leftKeys ++ medianKey :: rightKeys := by
          conv_lhs => rw [← List.take_append_drop (t - 1) cKeys]
          rw [← h_lk, ← h_keysRest_eq, hkr]
        have h_cChildren_decomp : cChildren = leftCh ++ rightCh := by
          conv_lhs => rw [← List.take_append_drop t cChildren]
          rw [← h_left_eq, ← h_right_eq]
        have h_children_decomp :
            children = take i children ++ node cKeys cChildren :: drop (i + 1) children := by
          conv_lhs => rw [← List.take_append_drop i children]
          rw [List.drop_eq_getElem_cons h_lt, h_get]
        -- Reduce the permutation to a multiset equality and linearise both sides.
        rw [← Multiset.coe_eq_coe]
        conv_rhs => rw [keysOf, h_children_decomp]
        conv_lhs => rw [keysOf]
        simp only [List.flatMap_append, List.flatMap_cons, List.flatMap_nil, List.append_nil,
          keysOf, h_cKeys_decomp, h_cChildren_decomp, ← Multiset.coe_add, This simp argument is unused:
  ← Multiset.coe_nil

Hint: Omit it from the simp argument list.
  simp only [List.flatMap_append, List.flatMap_cons, List.flatMap_nil, List.append_nil,
            keysOf, h_cKeys_decomp, h_cChildren_decomp, ← Multiset.coe_add, ← Multiset.con̲s̲_̲c̲o̲e_̵n̵i̵l̵,
            ← Multiset.c̵o̵n̵s_̵c̵o̵e̵,̵ ̵←̵ ̵M̵u̵l̵t̵is̵e̵t̵.̵s̵i̵ngleton_add]

Note: Simp arguments with `←` have the additional effect of removing the other direction from the simp set, even if the simp argument itself is unused. If the hint above does not work, try replacing `←` with `-` to only get that effect and silence this warning.

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`← Multiset.coe_nil,
          ← Multiset.cons_coe, ← Multiset.singleton_add]
        rw [show (↑keys : Multiset Nat) = ↑(take i keys) + ↑(drop i keys) from by
          rw [Multiset.coe_add, List.take_append_drop]]
        abel

              end BTreeend Chapter18end CLRS

Definitions and proofs

CLRSLean.FourthEdition.Chapter_18.Section_18_1_B_Tree_Model.HeightBound

CLRS Section 18.1 - B-tree key count and height bound

This module counts every key slot represented by a B-tree. Its exact accounting identity rewrites an internal node's augmented key count as the sum of the augmented counts of its children. That recurrence is the arithmetic foundation for the structural minimum-key and logarithmic-height bounds.

              namespace CLRSnamespace Chapter18namespace BTree

Exact key accounting

The number of key slots represented by a B-tree.

def totalKeys (tr : BTree) : Nat :=
  (keysOf tr).length

A node's total key count is its local key count plus all child counts.

theorem totalKeys_node (ks : List Nat) (cs : List BTree) :
    totalKeys (node ks cs) =
      ks.length + (cs.map totalKeys).sum := by
  unfold totalKeys
  simp [keysOf, List.length_flatMap]

For an internal node, adding one to the total key count exactly absorbs every separator key into one augmented count per child.


private lemma totalKeys_add_one_eq_sum_children
    {ks : List Nat} {c0 : BTree} {cs : List BTree}
    (hcb : ChildBounded (node ks (c0 :: cs))) :
    totalKeys (node ks (c0 :: cs)) + 1 =
      ((c0 :: cs).map (fun child => totalKeys child + 1)).sum := by
  have hlen : (c0 :: cs).length = ks.length + 1 := by
    unfold ChildBounded at hcb
    simpa using hcb.1
  rw [totalKeys_node, List.sum_map_add, List.map_const', List.sum_const_nat]
  simp only [Nat.mul_one]
  omega

A pointwise lower bound lifts to the sum over all list positions.


private lemma length_mul_le_sum_map
    {α : Type} (xs : List α) (q : Nat) (f : α → Nat)
    (hpoint : ∀ x ∈ xs, q ≤ f x) :
    xs.length * q ≤ (xs.map f).sum := by
  have hsum : (xs.map (fun _ => q)).sum ≤ (xs.map f).sum :=
    List.sum_le_sum hpoint
  rw [List.map_const', List.sum_const_nat] at hsum
  exact hsum

Internal-child projections

Every child position of a child-bounded internal node is child-bounded.

private lemma childBounded_of_mem
    {ks : List Nat} {c0 child : BTree} {cs : List BTree}
    (hcb : ChildBounded (node ks (c0 :: cs)))
    (hc : child ∈ c0 :: cs) :
    ChildBounded child := by
  unfold ChildBounded at hcb
  exact hcb.2.2 child hc

Every child position of an occupied node satisfies non-root occupancy.

private lemma occupancy_false_of_mem
    {t : Nat} {isRoot : Bool} {ks : List Nat} {c0 child : BTree}
    {cs : List BTree}
    (hocc : Occupancy t isRoot (node ks (c0 :: cs)))
    (hc : child ∈ c0 :: cs) :
    Occupancy t false child := by
  unfold Occupancy at hocc
  exact hocc.2.2.2 child hc

Every child position of a same-depth internal node is itself same-depth.

private lemma sameDepth_of_mem
    {ks : List Nat} {c0 child : BTree} {cs : List BTree}
    (hsd : SameDepth (node ks (c0 :: cs)))
    (hc : child ∈ c0 :: cs) :
    SameDepth child := by
  rcases List.mem_cons.mp hc with rfl | hcTail
  · exact sameDepth_head_sd hsd
  · exact sameDepth_tail_sd hsd child hcTail

Every child of a same-depth internal node has the head child's height.

private lemma heightOf_eq_head_of_mem
    {ks : List Nat} {c0 child : BTree} {cs : List BTree}
    (hsd : SameDepth (node ks (c0 :: cs)))
    (hc : child ∈ c0 :: cs) :
    heightOf child = heightOf c0 :=
  sameDepth_children_eq_height hsd child hc c0 (by simp)

Non-root minimum-key bound

Every non-root B-tree subtree contains enough key slots for its height. The augmented form avoids natural-number subtraction and is the induction theorem used by the root-level CLRS bound.


theorem nonRoot_totalKeys_add_one_lower_bound
    (t : Nat) (_ht : 2 ≤ t) {tr : BTree}
    (hcb : ChildBounded tr)
    (hocc : Occupancy t false tr)
    (hsd : SameDepth tr) :
    t ^ (heightOf tr + 1) ≤ totalKeys tr + 1 := by
  induction hsd with
  | leaf ks =>
      simp [Occupancy] at hocc
      simp [heightOf, totalKeys_node]
      omega
  | internal ks c0 cs hheights hsd0 hsdcs ih0 ihcs =>
      have hsdNode : SameDepth (node ks (c0 :: cs)) :=
        SameDepth.internal ks c0 cs hheights hsd0 hsdcs
      have hcount : t ≤ (c0 :: cs).length := by
        have hocc' := hocc
        simp [Occupancy] at hocc'
        rcases hocc' with ⟨_, _, ⟨hcount, _⟩, _, _⟩
        exact hcount
      let q := t ^ (heightOf c0 + 1)
      have hpoint :
          ∀ child ∈ c0 :: cs, q ≤ totalKeys child + 1 := by
        intro child hc
        rcases List.mem_cons.mp hc with rfl | hcTail
        · exact ih0
            (childBounded_of_mem hcb (by simp))
            (occupancy_false_of_mem hocc (by simp))
        · have hcMem : child ∈ c0 :: cs := by simp [hcTail]
          simpa [q, heightOf_eq_head_of_mem hsdNode hcMem] using
            (ihcs child hcTail
              (childBounded_of_mem hcb hcMem)
              (occupancy_false_of_mem hocc hcMem))
      have hsum :
          (c0 :: cs).length * q ≤
            ((c0 :: cs).map (fun child => totalKeys child + 1)).sum :=
        length_mul_le_sum_map (c0 :: cs) q
          (fun child => totalKeys child + 1) hpoint
      have hmul : t * q ≤ (c0 :: cs).length * q :=
        Nat.mul_le_mul_right q hcount
      rw [totalKeys_add_one_eq_sum_children hcb]
      calc
        t ^ (heightOf (node ks (c0 :: cs)) + 1) = t * q := by
          rw [heightOf_internal_of_sameDepth hsdNode]
          have hexponent :
              1 + heightOf c0 + 1 = (heightOf c0 + 1) + 1 := by
            omega
          rw [hexponent, Nat.pow_succ]
          exact Nat.mul_comm _ _
        _ ≤ (c0 :: cs).length * q := hmul
        _ ≤ ((c0 :: cs).map (fun child => totalKeys child + 1)).sum := hsum

Root minimum-key and logarithmic-height bounds

A well-formed root is either the legal empty tree or has the CLRS augmented minimum key count for its height.


theorem wellFormed_empty_or_totalKeys_add_one_lower_bound
    (t : Nat) (ht : 2 ≤ t) {tr : BTree}
    (hwf : WellFormed t tr) :
    tr = node [] [] ∨
      2 * t ^ heightOf tr ≤ totalKeys tr + 1 := by
  rcases hwf with ⟨_hsorted, hcb, hocc, hsd⟩
  cases tr with
  | node ks children =>
      cases children with
      | nil =>
          by_cases hks : ks = []
          · left
            simp [hks]
          · right
            simp [Occupancy, hks] at hocc
            simp [heightOf, totalKeys_node]
            omega
      | cons c0 cs =>
          right
          have hcount : 2 ≤ (c0 :: cs).length := by
            have hocc' := hocc
            unfold Occupancy at hocc'
            rcases hocc' with ⟨_, _, hchildren, _⟩
            rcases hchildren with hchildrenEmpty | hchildrenBounds
            · simp at hchildrenEmpty
            · exact hchildrenBounds.1
          let q := t ^ (heightOf c0 + 1)
          have hpoint :
              ∀ child ∈ c0 :: cs, q ≤ totalKeys child + 1 := by
            intro child hc
            simpa [q, heightOf_eq_head_of_mem hsd hc] using
              (nonRoot_totalKeys_add_one_lower_bound t ht
                (childBounded_of_mem hcb hc)
                (occupancy_false_of_mem hocc hc)
                (sameDepth_of_mem hsd hc))
          have hsum :
              (c0 :: cs).length * q ≤
                ((c0 :: cs).map (fun child => totalKeys child + 1)).sum :=
            length_mul_le_sum_map (c0 :: cs) q
              (fun child => totalKeys child + 1) hpoint
          have hmul : 2 * q ≤ (c0 :: cs).length * q :=
            Nat.mul_le_mul_right q hcount
          rw [totalKeys_add_one_eq_sum_children hcb]
          calc
            2 * t ^ heightOf (node ks (c0 :: cs)) = 2 * q := by
              rw [heightOf_internal_of_sameDepth hsd]
              simp [q, Nat.add_comm]
            _ ≤ (c0 :: cs).length * q := hmul
            _ ≤ ((c0 :: cs).map (fun child => totalKeys child + 1)).sum := hsum

A well-formed tree is empty or satisfies the textbook minimum-key expression.

theorem wellFormed_empty_or_minKeys_le_totalKeys
    (t : Nat) (ht : 2 ≤ t) {tr : BTree}
    (hwf : WellFormed t tr) :
    tr = node [] [] ∨ minKeys t (heightOf tr) ≤ totalKeys tr := by
  rcases wellFormed_empty_or_totalKeys_add_one_lower_bound t ht hwf with
    hempty | hbound
  · exact Or.inl hempty
  · right
    unfold minKeys
    omega

Every nonempty well-formed tree satisfies the textbook minimum-key bound.

theorem wellFormed_minKeys_le_totalKeys
    (t : Nat) (ht : 2 ≤ t) {tr : BTree}
    (hwf : WellFormed t tr)
    (hne : tr ≠ node [] []) :
    minKeys t (heightOf tr) ≤ totalKeys tr := by
  rcases wellFormed_empty_or_minKeys_le_totalKeys t ht hwf with
    hempty | hbound
  · exact (hne hempty).elim
  · exact hbound

The height of every well-formed B-tree, including the empty tree, is at most the minimum-degree-base logarithm of its CLRS normalized key count.


theorem wellFormed_height_log_bound
    (t : Nat) (ht : 2 ≤ t) {tr : BTree}
    (hwf : WellFormed t tr) :
    heightOf tr ≤ Nat.log t ((totalKeys tr + 1) / 2) := by
  rcases wellFormed_empty_or_totalKeys_add_one_lower_bound t ht hwf with
    hempty | hbound
  · subst tr
    simp [heightOf, totalKeys, keysOf]
  · have htBase : 1 < t := by omega
    apply Nat.le_log_of_pow_le htBase
    have htwo : 0 < 2 := by omega
    apply (Nat.le_div_iff_mul_le htwo).2
    simpa [Nat.mul_comm] using hbound

              end BTreeend Chapter18end CLRS

CLRSLean.FourthEdition.Chapter_18.Section_18_1_B_Tree_Model.RunningTime

CLRS Chapter 18 - B-tree running time

This module bounds recursive-descent charges that follow the branch structure of the B-tree search, insertion, and deletion definitions. Each selected recursive call contributes one unit; terminal cases also contribute one. Top-level insertion adds one budget unit when the root splits.

These counters do not enumerate literal page reads/writes. In particular, split/borrow/merge accesses, separator scans, max/min predecessor/successor traversals, persistent list copying, and root-normalization work are not charged individually. No constant-factor refinement to complete page I/O is proved here.

Main results:

searchCost_le_height, insertCost_le_height, and deleteCost_le_height: the selected recursive path has at most height + 1 charges.
insertRootCost_le_height: the insertion descent/root-split budget is at most height + 3.
The historical *_le_diskAccessBound theorems bound these same descent counters on well-formed trees with 2 ≤ t.
diskAccessBound_isBigO_log_t: the common mathematical envelope is O(log_t n). The historical name is retained for compatibility; it does not convert the descent counter into a complete disk-access trace.

Functional insertion/deletion structure, key-bag, and search correctness are independent of this accounting boundary and remain available unchanged.

Notation conventions used in this section:

t : B-tree minimum degree (2 ≤ t for every cost theorem)
tr : a BTree
totalKeys tr : the number of represented key slots (the n of CLRS)

              namespace CLRSnamespace Chapter18namespace BTreeopen List

Recursive-descent charges

Number of nodes visited by searchExec for key x: one per level on the separator-selected descent path.

def searchCost (x : Nat) : BTree → Nat
  | node ks cs =>
      if x ∈ ks then 1
      else
        match _hc : cs[findChild ks x]? with
        | some child => 1 + searchCost x child
        | none => 1
termination_by tr => heightOf tr
decreasing_by
  exact heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨findChild ks x, _hc⟩)

Recursive-descent charges for the insertion branch structure. A full-child split changes the selected subtree but adds no separate page-read/write events. This is not a literal count of every node inspected or modified.

def insertCost (t x : Nat) : BTree → Nat
  | node ks cs =>
    if cs.isEmpty then 1
    else
      let i := findChild ks x
      match _hc : cs[i]? with
      | none => 1
      | some c =>
        match _hcc : c with
        | node cKeys cChildren =>
          if cKeys.length = 2 * t - 1 then
            let median := cKeys.getD (t - 1) 0
            if x < median then
              1 + insertCost t x (node (cKeys.take (t - 1)) (cChildren.take t))
            else
              1 + insertCost t x (node (cKeys.drop t) (cChildren.drop t))
          else
            1 + insertCost t x c
termination_by tr => heightOf tr
decreasing_by
  all_goals
    have hmem : node cKeys cChildren ∈ cs := List.mem_iff_getElem?.mpr ⟨i, _hc⟩
    refine lt_of_le_of_lt ?_ (heightOf_mem_lt hmem)
    first
      | exact le_of_eq (congrArg heightOf _hcc)
      | exact heightOf_le_of_children_subset (List.take_subset _ _)
      | exact heightOf_le_of_children_subset (List.drop_subset _ _)

Recursive-descent charges for deletion. Borrow/merge selects the next subtree; max/min chooses a replacement key. The helper traversals and local page operations are not counted by the added unit at each recursive level.


def deleteCost (t : Nat) (x : Nat) : BTree → Nat
  | node ks cs =>
    if cs.isEmpty then 1
    else
      let i := findChild ks x
      if Variable name `hiPos` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hiPos : 0 < i then
        let ki := i - 1
        match Variable name `hk` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hk : ks[ki]? with
        | some k =>
          if Variable name `hkeq` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hkeq : k = x then
            match Variable name `hcl` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hcl : cs[ki]? with
            | some leftChild =>
              match hcr : cs[ki + 1]? with
              | some rightChild =>
                if hla : t ≤ numKeys leftChild then
                  1 + deleteCost t (maxKey leftChild) leftChild
                else if hlb : t ≤ numKeys rightChild then
                  1 + deleteCost t (minKey rightChild) rightChild
                else
                  1 + deleteCost t x (mergeNodes leftChild k rightChild)
              | none => 1
            | none => 1
          else
            match Variable name `hc` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hc : cs[i]? with
            | some child =>
              if hcg : t ≤ numKeys child then
                1 + deleteCost t x child
              else
                match hls : cs[i - 1]? with
                | some leftSib =>
                  if Variable name `hlg` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hlg : t ≤ numKeys leftSib then
                    match hsep : ks[i - 1]? with
                    | some sep =>
                      1 + deleteCost t x (rotateLeft leftSib sep child).2.2
                    | none => 1 + deleteCost t x child
                  else
                    match Variable name `hrs` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hrs : cs[i + 1]? with
                    | some rightSib =>
                      if Variable name `hrg` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hrg : t ≤ numKeys rightSib then
                        match hsep : ks[i]? with
                        | some sep =>
                          1 + deleteCost t x (rotateRight child sep rightSib).1
                        | none => 1 + deleteCost t x child
                      else
                        match hsep : ks[i - 1]? with
                        | some sep =>
                          1 + deleteCost t x (mergeNodes leftSib sep child)
                        | none => 1 + deleteCost t x child
                    | none =>
                      match hsep : ks[i - 1]? with
                      | some sep =>
                        1 + deleteCost t x (mergeNodes leftSib sep child)
                      | none => 1 + deleteCost t x child
                | none => 1 + deleteCost t x child
            | none => 1
        | none =>
          match Variable name `hc` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hc : cs[i]? with
          | some child =>
            if hcg : t ≤ numKeys child then
              1 + deleteCost t x child
            else
              match hls : cs[i - 1]? with
              | some leftSib =>
                if Variable name `hlg` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hlg : t ≤ numKeys leftSib then
                  match hsep : ks[i - 1]? with
                  | some sep =>
                    1 + deleteCost t x (rotateLeft leftSib sep child).2.2
                  | none => 1 + deleteCost t x child
                else
                  match Variable name `hrs` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hrs : cs[i + 1]? with
                  | some rightSib =>
                    if Variable name `hrg` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hrg : t ≤ numKeys rightSib then
                      match hsep : ks[i]? with
                      | some sep =>
                        1 + deleteCost t x (rotateRight child sep rightSib).1
                      | none => 1 + deleteCost t x child
                    else
                      match hsep : ks[i - 1]? with
                      | some sep =>
                        1 + deleteCost t x (mergeNodes leftSib sep child)
                      | none => 1 + deleteCost t x child
                  | none =>
                    match hsep : ks[i - 1]? with
                    | some sep =>
                      1 + deleteCost t x (mergeNodes leftSib sep child)
                    | none => 1 + deleteCost t x child
              | none => 1 + deleteCost t x child
          | none => 1
      else
        match Variable name `hc` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hc : cs[0]? with
        | some child =>
          if hcg : t ≤ numKeys child then
            1 + deleteCost t x child
          else
            match hrs : cs[1]? with
            | some rightSib =>
              if Variable name `hrg` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`hrg : t ≤ numKeys rightSib then
                match hsep : ks[0]? with
                | some sep =>
                  1 + deleteCost t x (rotateRight child sep rightSib).1
                | none => 1 + deleteCost t x child
              else
                match hsep : ks[0]? with
                | some sep =>
                  1 + deleteCost t x (mergeNodes child sep rightSib)
                | none => 1 + deleteCost t x child
            | none => 1 + deleteCost t x child
        | none => 1
termination_by tr => heightOf tr
decreasing_by
  · exact heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨ki, hcl⟩)
  · exact heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨ki + 1, hcr⟩)
  · rw [heightOf_mergeNodes_eq_max]
    have ha : heightOf leftChild < heightOf (node ks cs) :=
      heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨ki, hcl⟩)
    have hb : heightOf rightChild < heightOf (node ks cs) :=
      heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨ki + 1, hcr⟩)
    omega
  all_goals
    first
      | (rw [heightOf_mergeNodes_eq_max]
         first
           | (have ha : heightOf leftSib < heightOf (node ks cs) :=
                heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨_, hls⟩)
              have hb : heightOf child < heightOf (node ks cs) :=
                heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨_, hc⟩)
              omega)
           | (have ha : heightOf child < heightOf (node ks cs) :=
                heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨_, hc⟩)
              have hb : heightOf rightSib < heightOf (node ks cs) :=
                heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨_, hrs⟩)
              omega))
      | exact heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨_, hc⟩)
      | (have hle := heightOf_rotateLeft_right_le leftSib sep child
         have ha : heightOf leftSib < heightOf (node ks cs) :=
           heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨_, hls⟩)
         have hb : heightOf child < heightOf (node ks cs) :=
           heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨_, hc⟩)
         omega)
      | (have hle := heightOf_rotateRight_left_le child sep rightSib
         have ha : heightOf child < heightOf (node ks cs) :=
           heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨_, hc⟩)
         have hb : heightOf rightSib < heightOf (node ks cs) :=
           heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨_, hrs⟩)
         omega)

Height bounds

O(h) search. searchExec descends at most one path, so its number of descent charges is bounded by the tree height plus one.


theorem searchCost_le_height (x : Nat) (tr : BTree) :
    searchCost x tr ≤ heightOf tr + 1 := by
  induction tr using searchCost.induct x with
  | case1 ks cs hxkeys =>
      rw [searchCost, if_pos hxkeys]
      omega
  | case2 ks cs hxkeys child hchild ih =>
      rw [searchCost, if_neg hxkeys]
      split
      · rename_i child' hchild'
        rw [hchild] at hchild'
        cases hchild'
        have hlt : heightOf child < heightOf (node ks cs) :=
          heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨findChild ks x, hchild⟩)
        omega
      · rename_i hnone
        rw [hchild] at hnone
        contradiction
  | case3 ks cs hxkeys hchild =>
      rw [searchCost, if_neg hxkeys]
      split
      · rename_i child hchild'
        rw [hchild] at hchild'
        contradiction
      · omega

O(h) insertion. insertNonFull descends at most one path, so its number of descent charges is bounded by the tree height plus one.


theorem insertCost_le_height (t x : Nat) (tr : BTree) :
    insertCost t x tr ≤ heightOf tr + 1 := by
  induction tr using insertCost.induct (t := t) (x := x) with
  | case1 ks cs hempty =>
      rw [insertCost, if_pos hempty]
      omega
  | case2 ks cs hne i hnone =>
      have hval : insertCost t x (node ks cs) = 1 := by
        rw [insertCost, if_neg hne]
        dsimp only
        split
        · omega
        · rename_i c hc
          rw [hnone] at hc
          simp at hc
      rw [hval]
      omega
  | case3 ks cs hne i cKeys cChildren hsome hfull median hlt hsome2 ih =>
      have hsome' : cs[findChild ks x]? = some (node cKeys cChildren) := hsome
      have hval : insertCost t x (node ks cs)
          = 1 + insertCost t x (node (cKeys.take (t - 1)) (cChildren.take t)) := by
        rw [insertCost, if_neg hne]
        dsimp only
        split
        · rename_i hcnone
          rw [hsome'] at hcnone
          simp at hcnone
        · rename_i c hcsome
          obtain rfl : c = node cKeys cChildren := by
            rw [hsome'] at hcsome; injection hcsome with h; exact h.symm
          dsimp only
          rw [if_pos hfull, if_pos hlt]
      rw [hval]
      have hmem : node cKeys cChildren ∈ cs :=
        List.mem_iff_getElem?.mpr ⟨findChild ks x, hsome'⟩
      have hltH : heightOf (node (cKeys.take (t - 1)) (cChildren.take t)) <
          heightOf (node ks cs) :=
        lt_of_le_of_lt (heightOf_le_of_children_subset (List.take_subset _ _))
          (heightOf_mem_lt hmem)
      omega
  | case4 ks cs hne i cKeys cChildren hsome hfull median hnlt hsome2 ih =>
      have hsome' : cs[findChild ks x]? = some (node cKeys cChildren) := hsome
      have hval : insertCost t x (node ks cs)
          = 1 + insertCost t x (node (cKeys.drop t) (cChildren.drop t)) := by
        rw [insertCost, if_neg hne]
        dsimp only
        split
        · rename_i hcnone
          rw [hsome'] at hcnone
          simp at hcnone
        · rename_i c hcsome
          obtain rfl : c = node cKeys cChildren := by
            rw [hsome'] at hcsome; injection hcsome with h; exact h.symm
          dsimp only
          rw [if_pos hfull, if_neg hnlt]
      rw [hval]
      have hmem : node cKeys cChildren ∈ cs :=
        List.mem_iff_getElem?.mpr ⟨findChild ks x, hsome'⟩
      have hltH : heightOf (node (cKeys.drop t) (cChildren.drop t)) <
          heightOf (node ks cs) :=
        lt_of_le_of_lt (heightOf_le_of_children_subset (List.drop_subset _ _))
          (heightOf_mem_lt hmem)
      omega
  | case5 ks cs hne i cKeys cChildren hsome hnfull hsome2 ih =>
      have hsome' : cs[findChild ks x]? = some (node cKeys cChildren) := hsome
      have hval : insertCost t x (node ks cs)
          = 1 + insertCost t x (node cKeys cChildren) := by
        rw [insertCost, if_neg hne]
        dsimp only
        split
        · rename_i hcnone
          rw [hsome'] at hcnone
          simp at hcnone
        · rename_i c hcsome
          obtain rfl : c = node cKeys cChildren := by
            rw [hsome'] at hcsome; injection hcsome with h; exact h.symm
          dsimp only
          rw [if_neg hnfull]
      rw [hval]
      have hmem : node cKeys cChildren ∈ cs :=
        List.mem_iff_getElem?.mpr ⟨findChild ks x, hsome'⟩
      have hltH : heightOf (node cKeys cChildren) < heightOf (node ks cs) :=
        heightOf_mem_lt hmem
      omega

Deletion height bound

              private lemma child_lt_node (ks : List Nat) {cs : List BTree} {j : Nat} {c : BTree}
    (hc : cs[j]? = some c) : heightOf c < heightOf (node ks cs) :=
  heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨j, hc⟩)

private lemma merge_lt_node (ks : List Nat) {cs : List BTree} {a b : BTree} (s : Nat)
    (ha : a ∈ cs) (hb : b ∈ cs) :
    heightOf (mergeNodes a s b) < heightOf (node ks cs) := by
  rw [heightOf_mergeNodes_eq_max]
  have hha : heightOf a < heightOf (node ks cs) := heightOf_mem_lt ha
  have hhb : heightOf b < heightOf (node ks cs) := heightOf_mem_lt hb
  omegaprivate lemma rotateLeft_target_lt_node (ks : List Nat) {cs : List BTree} {a b : BTree} (s : Nat)
    (ha : a ∈ cs) (hb : b ∈ cs) :
    heightOf (rotateLeft a s b).2.2 < heightOf (node ks cs) := by
  have hle : heightOf (rotateLeft a s b).2.2 ≤ max (heightOf a) (heightOf b) :=
    heightOf_rotateLeft_right_le a s b
  have hha : heightOf a < heightOf (node ks cs) := heightOf_mem_lt ha
  have hhb : heightOf b < heightOf (node ks cs) := heightOf_mem_lt hb
  omegaprivate lemma rotateRight_target_lt_node (ks : List Nat) {cs : List BTree} {a b : BTree} (s : Nat)
    (ha : a ∈ cs) (hb : b ∈ cs) :
    heightOf (rotateRight a s b).1 < heightOf (node ks cs) := by
  have hle : heightOf (rotateRight a s b).1 ≤ max (heightOf a) (heightOf b) :=
    heightOf_rotateRight_left_le a s b
  have hha : heightOf a < heightOf (node ks cs) := heightOf_mem_lt ha
  have hhb : heightOf b < heightOf (node ks cs) := heightOf_mem_lt hb
  omega

O(h) deletion. composedDelete descends at most one path, so its number of descent charges is bounded by the tree height plus one.


theorem deleteCost_le_height (t x : Nat) (tr : BTree) :
    deleteCost t x tr ≤ heightOf tr + 1 := by
  induction x, tr using deleteCost.induct (t := t) with
  | case1 x ks cs hleaf =>
      rw [deleteCost, if_pos hleaf]
      omega
  | case2 ks cs hnonempty sep leftChild rightChild hleftReady i hpos ki hsep hleft hright ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsep hleft hright
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hleft, hright]
      simp [hleftReady]
      have hlt := child_lt_node ks hleft
      omega
  | case3 ks cs hnonempty sep leftChild rightChild hleftNotReady hrightReady i hpos ki hsep hleft hright ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsep hleft hright
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hleft, hright]
      simp [hleftNotReady, hrightReady]
      have hlt := child_lt_node ks hright
      omega
  | case4 ks cs hnonempty sep leftChild rightChild hleftNotReady hrightNotReady i hpos ki hsep hleft hright ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsep hleft hright
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hleft, hright]
      simp [hleftNotReady, hrightNotReady]
      have hlt := merge_lt_node ks sep (List.mem_iff_getElem?.mpr ⟨ki, hleft⟩)
        (List.mem_iff_getElem?.mpr ⟨ki + 1, hright⟩)
      omega
  | case5 ks cs hnonempty sep leftChild i hpos ki hsep hleft hrightNone =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsep hleft hrightNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hleft, hrightNone]
      simp
  | case6 ks cs hnonempty sep i hpos ki hsep hleftNone =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsep hleftNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hleftNone]
      simp
  | case7 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildReady ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsep hchild
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hchild]
      simp [hne, hchildReady]
      have hlt := child_lt_node ks hchild
      omega
  | case8 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildNotReady leftSib hleftSib hleftSibReady sep2 hsep2 ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib hsep2
      simp only [ki, i] at hsep
      have hsepEq : sep = sep2 := Option.some.inj (hsep.symm.trans hsep2)
      subst sep2
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hchild, hleftSib]
      simp [hne, hchildNotReady, hleftSibReady]
      have hlt := rotateLeft_target_lt_node ks sep (List.mem_iff_getElem?.mpr ⟨i - 1, hleftSib⟩)
        (List.mem_iff_getElem?.mpr ⟨i, hchild⟩)
      omega
  | case9 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildNotReady leftSib hleftSib hleftSibReady hsepNone ih =>
      simp only [ki, i] at hsep hsepNone
      rw [hsep] at hsepNone
      cases hsepNone
  | case10 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildNotReady leftSib hleftSib hleftSibNotReady rightSib hrightSib hrightSibReady sep2 hsep2 ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib hrightSib hsep2
      simp only [ki, i] at hsep
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hchild, hleftSib, hrightSib, hsep2]
      simp [hne, hchildNotReady, hleftSibNotReady, hrightSibReady]
      have hlt := rotateRight_target_lt_node ks sep2 (List.mem_iff_getElem?.mpr ⟨i, hchild⟩)
        (List.mem_iff_getElem?.mpr ⟨i + 1, hrightSib⟩)
      omega
  | case11 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildNotReady leftSib hleftSib hleftSibNotReady rightSib hrightSib hrightSibReady hsepNone ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib hrightSib hsepNone
      simp only [ki, i] at hsep
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hchild, hleftSib, hrightSib, hsepNone]
      simp [hne, hchildNotReady, hleftSibNotReady, hrightSibReady]
      have hlt := child_lt_node ks hchild
      omega
  | case12 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildNotReady leftSib hleftSib hleftSibNotReady rightSib hrightSib hrightSibNotReady sep2 hsep2 ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib hrightSib hsep2
      simp only [ki, i] at hsep
      have hsepEq : sep = sep2 := Option.some.inj (hsep.symm.trans hsep2)
      subst sep2
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hchild, hleftSib, hrightSib]
      simp [hne, hchildNotReady, hleftSibNotReady, hrightSibNotReady]
      have hlt := merge_lt_node ks sep (List.mem_iff_getElem?.mpr ⟨i - 1, hleftSib⟩)
        (List.mem_iff_getElem?.mpr ⟨i, hchild⟩)
      omega
  | case13 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildNotReady leftSib hleftSib hleftSibNotReady rightSib hrightSib hrightSibNotReady hsepNone ih =>
      simp only [ki, i] at hsep hsepNone
      rw [hsep] at hsepNone
      cases hsepNone
  | case14 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildNotReady leftSib hleftSib hleftSibNotReady hrightNone sep2 hsep2 ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib hrightNone hsep2
      simp only [ki, i] at hsep
      have hsepEq : sep = sep2 := Option.some.inj (hsep.symm.trans hsep2)
      subst sep2
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hchild, hleftSib, hrightNone]
      simp [hne, hchildNotReady, hleftSibNotReady]
      have hlt := merge_lt_node ks sep (List.mem_iff_getElem?.mpr ⟨i - 1, hleftSib⟩)
        (List.mem_iff_getElem?.mpr ⟨i, hchild⟩)
      omega
  | case15 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildNotReady leftSib hleftSib hleftSibNotReady hrightNone hsepNone ih =>
      simp only [ki, i] at hsep hsepNone
      rw [hsep] at hsepNone
      cases hsepNone
  | case16 x ks cs hnonempty i hpos ki sep hsep hne child hchild hchildNotReady hleftNone ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsep hchild hleftNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hchild, hleftNone]
      simp [hne, hchildNotReady]
      have hlt := child_lt_node ks hchild
      omega
  | case17 x ks cs hnonempty i hpos ki sep hsep hne hchildNone =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsep hchildNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsep, hchildNone]
      simp [hne]
  | case18 x ks cs hnonempty i hpos ki hsepNone child hchild hchildReady ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsepNone hchild
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsepNone, hchild]
      simp [hchildReady]
      have hlt := child_lt_node ks hchild
      omega
  | case19 x ks cs hnonempty i hpos ki hsepNone child hchild hchildNotReady leftSib hleftSib hleftSibReady sep hsep ih =>
      simp only [i] at hsep
      simp only [ki, i] at hsepNone
      rw [hsepNone] at hsep
      cases hsep
  | case20 x ks cs hnonempty i hpos ki hsepNone child hchild hchildNotReady leftSib hleftSib hleftSibReady hsepNone2 ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib
      simp only [ki, i] at hsepNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsepNone, hchild, hleftSib]
      simp [hchildNotReady, hleftSibReady]
      have hlt := child_lt_node ks hchild
      omega
  | case21 x ks cs hnonempty i hpos ki hsepNone child hchild hchildNotReady leftSib hleftSib hleftSibNotReady rightSib hrightSib hrightSibReady sep hsep ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib hrightSib hsep
      simp only [ki, i] at hsepNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsepNone, hchild, hleftSib, hrightSib, hsep]
      simp [hchildNotReady, hleftSibNotReady, hrightSibReady]
      have hlt := rotateRight_target_lt_node ks sep (List.mem_iff_getElem?.mpr ⟨i, hchild⟩)
        (List.mem_iff_getElem?.mpr ⟨i + 1, hrightSib⟩)
      omega
  | case22 x ks cs hnonempty i hpos ki hsepNone child hchild hchildNotReady leftSib hleftSib hleftSibNotReady rightSib hrightSib hrightSibReady hsepNone2 ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib hrightSib hsepNone2
      simp only [ki, i] at hsepNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsepNone, hchild, hleftSib, hrightSib, hsepNone2]
      simp [hchildNotReady, hleftSibNotReady, hrightSibReady]
      have hlt := child_lt_node ks hchild
      omega
  | case23 x ks cs hnonempty i hpos ki hsepNone child hchild hchildNotReady leftSib hleftSib hleftSibNotReady rightSib hrightSib hrightSibNotReady sep hsep ih =>
      simp only [i] at hsep
      simp only [ki, i] at hsepNone
      rw [hsepNone] at hsep
      cases hsep
  | case24 x ks cs hnonempty i hpos ki hsepNone child hchild hchildNotReady leftSib hleftSib hleftSibNotReady rightSib hrightSib hrightSibNotReady hsepNone2 ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib hrightSib
      simp only [ki, i] at hsepNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsepNone, hchild, hleftSib, hrightSib]
      simp [hchildNotReady, hleftSibNotReady, hrightSibNotReady]
      have hlt := child_lt_node ks hchild
      omega
  | case25 x ks cs hnonempty i hpos ki hsepNone child hchild hchildNotReady leftSib hleftSib hleftSibNotReady hrightNone sep hsep ih =>
      simp only [i] at hsep
      simp only [ki, i] at hsepNone
      rw [hsepNone] at hsep
      cases hsep
  | case26 x ks cs hnonempty i hpos ki hsepNone child hchild hchildNotReady leftSib hleftSib hleftSibNotReady hrightNone hsepNone2 ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftSib hrightNone
      simp only [ki, i] at hsepNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsepNone, hchild, hleftSib, hrightNone]
      simp [hchildNotReady, hleftSibNotReady]
      have hlt := child_lt_node ks hchild
      omega
  | case27 x ks cs hnonempty i hpos ki hsepNone child hchild hchildNotReady hleftNone ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos hchild hleftNone
      simp only [ki, i] at hsepNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsepNone, hchild, hleftNone]
      simp [hchildNotReady]
      have hlt := child_lt_node ks hchild
      omega
  | case28 x ks cs hnonempty i hpos ki hsepNone hchildNone =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hpos
      simp only [ki, i] at hsepNone hchildNone
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte, hpos]
      rw [hsepNone, hchildNone]
      simp
  | case29 x ks cs hnonempty i hnotPos child hchild hchildReady ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hnotPos
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte]
      rw [dif_neg hnotPos]
      rw [hchild]
      simp [hchildReady]
      have hlt := child_lt_node ks hchild
      omega
  | case30 x ks cs hnonempty i hnotPos child hchild hchildNotReady rightSib hrightSib hrightSibReady sep hsep ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hnotPos
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte]
      rw [dif_neg hnotPos]
      rw [hchild, hrightSib, hsep]
      simp [hchildNotReady, hrightSibReady]
      have hlt := rotateRight_target_lt_node ks sep (List.mem_iff_getElem?.mpr ⟨0, hchild⟩)
        (List.mem_iff_getElem?.mpr ⟨1, hrightSib⟩)
      omega
  | case31 x ks cs hnonempty i hnotPos child hchild hchildNotReady rightSib hrightSib hrightSibReady hsepNone ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hnotPos
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte]
      rw [dif_neg hnotPos]
      rw [hchild, hrightSib, hsepNone]
      simp [hchildNotReady, hrightSibReady]
      have hlt := child_lt_node ks hchild
      omega
  | case32 x ks cs hnonempty i hnotPos child hchild hchildNotReady rightSib hrightSib hrightSibNotReady sep hsep ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hnotPos
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte]
      rw [dif_neg hnotPos]
      rw [hchild, hrightSib, hsep]
      simp [hchildNotReady, hrightSibNotReady]
      have hlt := merge_lt_node ks sep (List.mem_iff_getElem?.mpr ⟨0, hchild⟩)
        (List.mem_iff_getElem?.mpr ⟨1, hrightSib⟩)
      omega
  | case33 x ks cs hnonempty i hnotPos child hchild hchildNotReady rightSib hrightSib hrightSibNotReady hsepNone ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hnotPos
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte]
      rw [dif_neg hnotPos]
      rw [hchild, hrightSib, hsepNone]
      simp [hchildNotReady, hrightSibNotReady]
      have hlt := child_lt_node ks hchild
      omega
  | case34 x ks cs hnonempty i hnotPos child hchild hchildNotReady hrightNone ih =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hnotPos
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte]
      rw [dif_neg hnotPos]
      rw [hchild, hrightNone]
      simp [hchildNotReady]
      have hlt := child_lt_node ks hchild
      omega
  | case35 x ks cs hnonempty i hnotPos hchildNone =>
      have hnotLeaf : cs.isEmpty = false := Bool.eq_false_of_not_eq_true hnonempty
      simp only [i] at hnotPos
      rw [deleteCost]
      simp only [hnotLeaf, Bool.false_eq_true, ↓reduceIte]
      rw [dif_neg hnotPos]
      rw [hchildNone]
      simp

Top-level insertion cost

Insertion descent budget with one extra charge for the full-root split. The charge is a budget unit, not a literal count of split-page reads/writes.

def insertRootCost (t x : Nat) (tr : BTree) : Nat :=
  if rootKeyCount tr = 2 * t - 1 then insertCost t x (splitRoot t tr) + 1
  else insertCost t x tr

O(h) top-level insertion. Splitting a full root adds exactly one level and then insertNonFull descends at most one path, so the cost is bounded by the tree height plus three.


theorem insertRootCost_le_height (t x : Nat) (ht : 2 ≤ t) {tr : BTree}
    (hwf : WellFormed t tr) :
    insertRootCost t x tr ≤ heightOf tr + 3 := by
  unfold insertRootCost
  by_cases hfull : rootKeyCount tr = 2 * t - 1
  · rw [if_pos hfull]
    have hsplit : heightOf (splitRoot t tr) = heightOf tr + 1 :=
      splitRoot_height t ht hwf hfull
    have hins := insertCost_le_height t x (splitRoot t tr)
    omega
  · rw [if_neg hfull]
    have hins := insertCost_le_height t x tr
    omega

Logarithmic descent-budget bounds

Common logarithmic envelope for the descent budgets. Its historical diskAccessBound name is retained, but a full page-I/O interpretation requires additional accounting not established in this module.

def diskAccessBound (t : Nat) (n : Nat) : Nat := Nat.log t ((n + 1) / 2) + 3

Search has at most log_t n + O(1) descent charges on a well-formed tree.

theorem searchCost_le_diskAccessBound (t : Nat) (ht : 2 ≤ t) {tr : BTree}
    (hwf : WellFormed t tr) (x : Nat) :
    searchCost x tr ≤ diskAccessBound t (totalKeys tr) := by
  have hh : heightOf tr ≤ Nat.log t ((totalKeys tr + 1) / 2) :=
    wellFormed_height_log_bound t ht hwf
  have hc := searchCost_le_height x tr
  unfold diskAccessBound
  omega

Top-level insertion has at most log_t n + O(1) descent/root-split charges on a well-formed tree.

theorem insertRootCost_le_diskAccessBound (t : Nat) (ht : 2 ≤ t) {tr : BTree}
    (hwf : WellFormed t tr) (x : Nat) :
    insertRootCost t x tr ≤ diskAccessBound t (totalKeys tr) := by
  have hh : heightOf tr ≤ Nat.log t ((totalKeys tr + 1) / 2) :=
    wellFormed_height_log_bound t ht hwf
  have hc := insertRootCost_le_height t x ht hwf
  unfold diskAccessBound
  omega

Deletion has at most log_t n + O(1) descent charges on a well-formed tree.

theorem deleteCost_le_diskAccessBound (t : Nat) (ht : 2 ≤ t) {tr : BTree}
    (hwf : WellFormed t tr) (x : Nat) :
    deleteCost t x tr ≤ diskAccessBound t (totalKeys tr) := by
  have hh : heightOf tr ≤ Nat.log t ((totalKeys tr + 1) / 2) :=
    wellFormed_height_log_bound t ht hwf
  have hc := deleteCost_le_height t x tr
  unfold diskAccessBound
  omega

The common descent-budget envelope is O(log_t n). This is an asymptotic theorem about the displayed numeric bound, not an additional operational refinement for page I/O or auxiliary traversals.


theorem diskAccessBound_isBigO_log_t (t : Nat) (ht : 2 ≤ t) :
    CLRS.Chapter03.isBigO (fun n => (diskAccessBound t n : ℝ))
      (fun n => (Nat.log t n : ℝ)) := by
  rw [CLRS.Chapter03.isBigO_iff]
  refine ⟨4, by norm_num, t, ?_⟩
  intro n hn
  have hmono : Nat.log t ((n + 1) / 2) ≤ Nat.log t n := by
    apply Nat.log_mono_right
    omega
  have hlogpos : 0 < Nat.log t n := Nat.log_pos (by omega : 1 < t) (by omega : t ≤ n)
  unfold diskAccessBound
  have h1 : (Nat.log t ((n + 1) / 2) + 3 : ℝ) ≤ 4 * (Nat.log t n : ℝ) := by
    have h2 : (Nat.log t ((n + 1) / 2) : ℝ) ≤ (Nat.log t n : ℝ) := by
      exact_mod_cast hmono
    have h3 : (3 : ℝ) ≤ 3 * (Nat.log t n : ℝ) := by
      have h4 : (1 : ℝ) ≤ (Nat.log t n : ℝ) := by
        exact_mod_cast (Nat.succ_le_of_lt hlogpos)
      nlinarith
    nlinarith
  have h_nonneg_left : 0 ≤ ((Nat.log t ((n + 1) / 2) + 3 : Nat) : ℝ) := by positivity
  have h_nonneg_right : 0 ≤ (Nat.log t n : ℝ) := by positivity
  rw [abs_of_nonneg h_nonneg_left, abs_of_nonneg h_nonneg_right]
  push_cast
  exact h1

              end BTreeend Chapter18end CLRS

CLRSLean.FourthEdition.Chapter_18.Section_18_1_B_Tree_Model.Search

CLRS Section 18.1 - Separator-guided B-tree search

Defines the child-selection function used by B-tree search and insertion, reusable path-localization and height lemmas, and a total executable search that descends through exactly one separator-selected child.

Main results:

findChild_localizes_mem: localizes a non-separator member to the selected child under sorted and child-bounded node invariants.
searchExec: checks the current node and otherwise follows only the separator-selected child.
searchExec_sound: successful executable search implies membership without structural assumptions.
searchExec_complete: sorted, child-bounded trees expose every member along the selected path.
searchExec_true_iff: on sorted, child-bounded trees, characterizes successful executable search by membership.
searchExec_eq_search: on sorted, child-bounded trees, connects executable search to the imported specification oracle search.

The selected-child localization and routing wrappers are used by the proved exact erase-one semantics for executable deletion.

namespace CLRS.Chapter18.BTreeopen List

Child selection

Index of the child that key x descends into: the number of leading keys ≤ x (correct for a sorted key list).

def findChild : List Nat → Nat → Nat
  | [], _ => 0
  | k :: ks, x => if k ≤ x then findChild ks x + 1 else 0

Height lemmas

foldl max never drops below its accumulator.

lemma foldl_max_ge (b : Nat) (l : List Nat) : b ≤ l.foldl max b := by
  induction l generalizing b with
  | nil => simp
  | cons y ys ih =>
    simp only [List.foldl_cons]
    exact le_trans (le_max_left b y) (ih (max b y))

Every element of l is ≤ l.foldl max b.

lemma mem_le_foldl_max : ∀ {l : List Nat} {a b : Nat}, a ∈ l → a ≤ l.foldl max b := by
  intro l
  induction l with
  | nil => intro a b h; simp at h
  | cons y ys ih =>
    intro a b h
    simp only [List.foldl_cons]
    rcases List.mem_cons.mp h with rfl | h
    · exact le_trans (le_max_right b a) (foldl_max_ge (max b a) ys)
    · exact ih h

If every element of l is ≤ M and b ≤ M, then l.foldl max b ≤ M.

lemma foldl_max_le' : ∀ {l : List Nat} {M b : Nat}, b ≤ M → (∀ a ∈ l, a ≤ M) → l.foldl max b ≤ M := by
  intro l
  induction l with
  | nil => intro M b hb _; simpa using hb
  | cons y ys ih =>
    intro M b hb h
    simp only [List.foldl_cons]
    exact ih (max_le hb (h y (by simp))) (fun a ha => h a (by simp [ha]))

Folding max over the heights of a sub-multiset of children is ≤ folding over the full children list.


lemma foldl_max_heightOf_subset {cs' cs : List BTree} (h : cs' ⊆ cs) :
    (cs'.map heightOf).foldl max 0 ≤ (cs.map heightOf).foldl max 0 := by
  apply foldl_max_le' (foldl_max_ge 0 _)
  intro a ha
  rw [List.mem_map] at ha
  obtain ⟨c, hc, rfl⟩ := ha
  exact mem_le_foldl_max (List.mem_map_of_mem (h hc))

A child is strictly shorter than its parent.

lemma heightOf_mem_lt {ks : List Nat} {children : List BTree} {c : BTree}
    (hc : c ∈ children) : heightOf c < heightOf (node ks children) := by
  cases children with
  | nil => simp at hc
  | cons d ds =>
    have hle := mem_le_foldl_max (a := heightOf c) (b := 0) (List.mem_map_of_mem hc)
    simp only [heightOf]
    omega

Replacing the children of a node by a sub-multiset cannot increase the height.

lemma heightOf_le_of_children_subset {a b : List Nat} {cs' cs : List BTree}
    (h : cs' ⊆ cs) : heightOf (node a cs') ≤ heightOf (node b cs) := by
  cases cs' with
  | nil => simp [heightOf]
  | cons d ds =>
    cases cs with
    | nil => exact absurd (h List.mem_cons_self) (by simp)
    | cons e es =>
      have hsub := foldl_max_heightOf_subset (cs' := d :: ds) (cs := e :: es) h
      simp only [heightOf]
      omega

Child-index bounds and range correctness

findChild never exceeds the number of keys, so on a node with children.length = keys.length + 1 it always indexes a real child.

lemma findChild_le (ks : List Nat) (x : Nat) : findChild ks x ≤ ks.length := by
  induction ks with
  | nil => simp [findChild]
  | cons k ks ih =>
    unfold findChild
    split
    · simp only [List.length_cons]; omega
    · omega

Every key before the chosen child index is ≤ x.


lemma findChild_take_le (x : Nat) : ∀ (ks : List Nat), ∀ k ∈ ks.take (findChild ks x), k ≤ x := by
  intro ks
  induction ks with
  | nil => intro k hk; simp at hk
  | cons a as ih =>
    intro k hk
    rw [findChild] at hk
    split at hk
    · rename_i hax
      rw [List.take_succ_cons] at hk
      rcases List.mem_cons.mp hk with rfl | hk
      · exact hax
      · exact ih k hk
    · simp at hk

On a sorted key list, every key from the chosen child index onward is > x.


lemma findChild_drop_gt (x : Nat) : ∀ {ks : List Nat}, List.Pairwise (· ≤ ·) ks →
    ∀ k ∈ ks.drop (findChild ks x), x < k := by
  intro ks
  induction ks with
  | nil => intro _ k hk; simp at hk
  | cons a as ih =>
    intro hs k hk
    have hsa : ∀ b ∈ as, a ≤ b := (List.pairwise_cons.mp hs).1
    have hs' : List.Pairwise (· ≤ ·) as := (List.pairwise_cons.mp hs).2
    rw [findChild] at hk
    split at hk
    · rename_i hax
      rw [List.drop_succ_cons] at hk
      exact ih hs' k hk
    · rename_i hax
      have hxa : x < a := not_le.mp hax
      simp only [List.drop_zero, List.mem_cons] at hk
      rcases hk with rfl | hk
      · exact hxa
      · exact lt_of_lt_of_le hxa (hsa k hk)

The right separator at the chosen child bounds x from above (sorted keys).


lemma findChild_x_hi {ks : List Nat} (hs : List.Pairwise (· ≤ ·) ks) (x : Nat) :
    ∀ hi, ks[findChild ks x]? = some hi → x ≤ hi := by
  intro hi hhi
  have hmem : hi ∈ ks.drop (findChild ks x) := by
    rw [List.mem_iff_getElem?]
    exact ⟨0, by rw [List.getElem?_drop, Nat.add_zero]; exact hhi⟩
  exact le_of_lt (findChild_drop_gt x hs hi hmem)

The left separator at the chosen child bounds x from below.


lemma findChild_x_lo (ks : List Nat) (x : Nat) :
    findChild ks x = 0 ∨ ∀ lo, ks[findChild ks x - 1]? = some lo → lo ≤ x := by
  rcases Nat.eq_zero_or_pos (findChild ks x) with h0 | hpos
  · exact Or.inl h0
  · right
    intro lo hlo
    have hmem : lo ∈ ks.take (findChild ks x) := by
      rw [List.mem_iff_getElem?]
      exact ⟨findChild ks x - 1, by rw [List.getElem?_take_of_lt (by omega)]; exact hlo⟩
    exact findChild_take_le x ks lo hmem

If a key absent from a sorted node's separators occurs in one of its children, that child is exactly the one selected by findChild.


theorem findChild_localizes_mem
    {ks : List Nat} {cs : List BTree} {x j : Nat} {child : BTree}
    (hsorted : List.Pairwise (· ≤ ·) ks)
    (hbounded : ChildBounded (node ks cs))
    (hxkeys : x ∉ ks)
    (hchild : cs[j]? = some child)
    (hxchild : x ∈ keysOf child) :
    j = findChild ks x := by
  have hjcs : j < cs.length :=
    _root_.of_getElem?_eq_some (c := cs) (i := j) hchild
  have hchild_get : cs.get ⟨j, hjcs⟩ = child :=
    (_root_.getElem?_eq_some_iff.mp hchild).choose_spec
  unfold ChildBounded at hbounded
  rcases hbounded with ⟨hshape, hbounds, _⟩
  have hlength : cs.length = ks.length + 1 := by
    rcases hshape with hempty | hlength
    · have : cs.length = 0 := by simpa using hempty
      omega
    · exact hlength
  have hjbounds := hbounds j hjcs
  dsimp only at hjbounds
  rw [hchild_get] at hjbounds
  have hnot_left : ¬j < findChild ks x := by
    intro hjleft
    have hjks : j < ks.length := by
      have := findChild_le ks x
      omega
    have hsep_mem : ks[j] ∈ ks.take (findChild ks x) := by
      rw [List.mem_iff_getElem?]
      refine ⟨j, ?_⟩
      rw [List.getElem?_take_of_lt hjleft, List.getElem?_eq_getElem hjks]
    have hsep_le : ks[j] ≤ x :=
      findChild_take_le x ks ks[j] hsep_mem
    have hkey_le : x ≤ ks[j] := by
      have hupper := hjbounds.2
      simp only [List.getElem?_eq_getElem hjks] at hupper
      exact hupper x hxchild
    apply hxkeys
    rw [show x = ks[j] by omega]
    exact List.getElem_mem hjks
  have hnot_right : ¬findChild ks x < j := by
    intro hjright
    have hjpos : 0 < j := by omega
    have hjpred : j - 1 < ks.length := by omega
    have hsep_mem : ks[j - 1] ∈ ks.drop (findChild ks x) := by
      rw [List.mem_iff_getElem?]
      refine ⟨j - 1 - findChild ks x, ?_⟩
      rw [List.getElem?_drop]
      have hindex :
          findChild ks x + (j - 1 - findChild ks x) = j - 1 := by
        omega
      rw [hindex, List.getElem?_eq_getElem hjpred]
    have hx_lt : x < ks[j - 1] :=
      findChild_drop_gt x hsorted (ks[j - 1]) hsep_mem
    have hsep_le : ks[j - 1] ≤ x := by
      rcases hjbounds.1 with hjzero | hlower
      · omega
      · simp only [List.getElem?_eq_getElem hjpred] at hlower
        exact hlower x hxchild
    omega
  omega

If a key occurs among sorted separators, the selected child index is positive and its predecessor separator is that key.


theorem findChild_pos_and_pred_eq_of_mem
    {ks : List Nat} {x : Nat}
    (hsorted : List.Pairwise (· ≤ ·) ks)
    (hx : x ∈ ks) :
    0 < findChild ks x ∧
      ks[findChild ks x - 1]? = some x := by
  induction ks with
  | nil => simp at hx
  | cons a as ih =>
      have hsortedTail : List.Pairwise (· ≤ ·) as :=
        (List.pairwise_cons.mp hsorted).2
      have ha_le : a ≤ x := by
        rcases List.mem_cons.mp hx with hxa | hxTail
        · omega
        · exact (List.pairwise_cons.mp hsorted).1 x hxTail
      rw [findChild, if_pos ha_le]
      refine ⟨by omega, ?_⟩
      simp only [Nat.add_sub_cancel]
      by_cases hxTail : x ∈ as
      · obtain ⟨hpos, hpred⟩ := ih hsortedTail hxTail
        cases hfind : findChild as x with
        | zero => omega
        | succ j =>
            simp only [hfind, Nat.succ_sub_one] at hpred
            simpa [hfind] using hpred
      · have hxa : x = a :=
          (List.mem_cons.mp hx).resolve_right hxTail
        subst x
        have hzero : findChild as a = 0 := by
          cases as with
          | nil => rfl
          | cons b bs =>
              have hab : a ≤ b :=
                (List.pairwise_cons.mp hsorted).1 b (by simp)
              have hne : b ≠ a := by
                intro hba
                apply hxTail
                simp [hba]
              have hnot : ¬b ≤ a := by omega
              simp [findChild, hnot]
        simp [hzero]

A non-selected child of a sorted, child-bounded node cannot contain a key that is absent from the node's separators.

theorem findChild_not_mem_child_of_ne
    {ks : List Nat} {cs : List BTree} {x j : Nat} {child : BTree}
    (hsorted : List.Pairwise (· ≤ ·) ks)
    (hbounded : ChildBounded (node ks cs))
    (hxkeys : x ∉ ks)
    (hchild : cs[j]? = some child)
    (hne : j ≠ findChild ks x) :
    x ∉ keysOf child := by
  intro hxchild
  exact hne
    (findChild_localizes_mem hsorted hbounded hxkeys hchild hxchild)

If a non-separator key belongs to a sorted, child-bounded node, it belongs to the selected child.


theorem findChild_selected_child_mem
    {ks : List Nat} {cs : List BTree} {x : Nat} {child : BTree}
    (hsorted : List.Pairwise (· ≤ ·) ks)
    (hbounded : ChildBounded (node ks cs))
    (hxkeys : x ∉ ks)
    (hchild : cs[findChild ks x]? = some child)
    (hx : x ∈ keysOf (node ks cs)) :
    x ∈ keysOf child := by
  unfold keysOf at hx
  rw [List.mem_append, List.mem_flatMap] at hx
  rcases hx with hxnode | ⟨descendant, hdescendant, hxdescendant⟩
  · exact (hxkeys hxnode).elim
  · obtain ⟨j, hj⟩ := List.mem_iff_getElem?.mp hdescendant
    have hjfind : j = findChild ks x :=
      findChild_localizes_mem hsorted hbounded hxkeys hj hxdescendant
    rw [hjfind, hchild] at hj
    cases hj
    exact hxdescendant

Executable search

Separator-guided executable B-tree search. The current node is checked first; on a miss, search continues only in the child selected by findChild.

def searchExec (x : Nat) : BTree → Bool
  | node ks cs =>
      if x ∈ ks then
        true
      else
        match _hc : cs[findChild ks x]? with
        | some child => searchExec x child
        | none => false
termination_by tr => heightOf tr
decreasing_by
  exact heightOf_mem_lt (List.mem_iff_getElem?.mpr ⟨findChild ks x, _hc⟩)

Executable search is sound on every B-tree: a successful result witnesses membership in the tree, without requiring structural invariants.


theorem searchExec_sound {x : Nat} {tr : BTree}
    (hsearch : searchExec x tr = true) : mem x tr := by
  revert hsearch
  induction tr using searchExec.induct x with
  | case1 ks cs hxkeys =>
      intro _
      unfold mem keysOf
      exact List.mem_append_left _ hxkeys
  | case2 ks cs hxkeys child hchild ih =>
      intro hsearch
      have hchild_search : searchExec x child = true := by
        rw [searchExec, if_neg hxkeys] at hsearch
        split at hsearch
        · rename_i child' hchild'
          rw [hchild] at hchild'
          cases hchild'
          exact hsearch
        · rename_i hnone
          rw [hchild] at hnone
          contradiction
      have hchild_mem : x ∈ keysOf child := ih hchild_search
      unfold mem keysOf
      rw [List.mem_append, List.mem_flatMap]
      right
      exact ⟨child, List.mem_iff_getElem?.mpr ⟨findChild ks x, hchild⟩, hchild_mem⟩
  | case3 ks cs hxkeys hchild =>
      intro hsearch
      rw [searchExec, if_neg hxkeys] at hsearch
      split at hsearch
      · rename_i child hsome
        rw [hchild] at hsome
        contradiction
      · simp at hsearch

On sorted, child-bounded B-trees, executable search is complete: every member is found by the separator-selected descent path.


theorem searchExec_complete {x : Nat} {tr : BTree}
    (hsorted : Sorted tr) (hbounded : ChildBounded tr)
    (hmem : mem x tr) : searchExec x tr = true := by
  revert hsorted hbounded hmem
  induction tr using searchExec.induct x with
  | case1 ks cs hxkeys =>
      intro _ _ _
      rw [searchExec, if_pos hxkeys]
  | case2 ks cs hxkeys child hchild ih =>
      intro hsorted hbounded hmem
      unfold Sorted at hsorted
      rcases hsorted with ⟨hkeys_sorted, hchildren_sorted⟩
      unfold mem keysOf at hmem
      rw [List.mem_append, List.mem_flatMap] at hmem
      rcases hmem with hxnode | ⟨descendant, hdescendant, hxdescendant⟩
      · exact (hxkeys hxnode).elim
      · obtain ⟨j, hj⟩ := List.mem_iff_getElem?.mp hdescendant
        have hjfind : j = findChild ks x :=
          findChild_localizes_mem hkeys_sorted hbounded hxkeys hj hxdescendant
        subst j
        rw [hchild] at hj
        cases hj
        have hchild_mem : child ∈ cs :=
          List.mem_iff_getElem?.mpr ⟨findChild ks x, hchild⟩
        have hchild_sorted : Sorted child :=
          hchildren_sorted child hchild_mem
        have hchild_bounded : ChildBounded child := by
          unfold ChildBounded at hbounded
          exact hbounded.2.2 child hchild_mem
        have hchild_search : searchExec x child = true :=
          ih hchild_sorted hchild_bounded hxdescendant
        rw [searchExec, if_neg hxkeys]
        split
        · rename_i child' hchild'
          rw [hchild] at hchild'
          cases hchild'
          exact hchild_search
        · rename_i hnone
          rw [hchild] at hnone
          contradiction
  | case3 ks cs hxkeys hchild =>
      intro hsorted hbounded hmem
      unfold Sorted at hsorted
      rcases hsorted with ⟨hkeys_sorted, _⟩
      unfold mem keysOf at hmem
      rw [List.mem_append, List.mem_flatMap] at hmem
      rcases hmem with hxnode | ⟨descendant, hdescendant, hxdescendant⟩
      · exact (hxkeys hxnode).elim
      · obtain ⟨j, hj⟩ := List.mem_iff_getElem?.mp hdescendant
        have hjfind : j = findChild ks x :=
          findChild_localizes_mem hkeys_sorted hbounded hxkeys hj hxdescendant
        rw [hjfind, hchild] at hj
        contradiction

On sorted, child-bounded trees, executable search returns true exactly for members of the tree.

theorem searchExec_true_iff {x : Nat} {tr : BTree}
    (hsorted : Sorted tr) (hbounded : ChildBounded tr) :
    searchExec x tr = true ↔ mem x tr :=
  ⟨searchExec_sound, searchExec_complete hsorted hbounded⟩

On sorted, child-bounded trees, separator-guided executable search agrees with the specification-level membership oracle search.

theorem searchExec_eq_search {x : Nat} {tr : BTree}
    (hsorted : Sorted tr) (hbounded : ChildBounded tr) :
    searchExec x tr = search x tr := by
  apply Bool.eq_iff_iff.mpr
  exact (searchExec_true_iff hsorted hbounded).trans (search_true_iff x tr).symm

end CLRS.Chapter18.BTree