Imports

import CLRSLean.FourthEdition.Chapter_13.Section_13_2_Rotations.Refinement

13.2. Rotations

The functional tree layer proves preservation of inorder keys and BST ordering. The indexed pointer layer implements both rotations, reconnecting the old parent's appropriate child or the store root and reparenting a non-NIL middle child. Missing nodes or pivot children leave the store unchanged.

StoreReprAt tracks an expected parent and a finite owned footprint: nonempty nodes are non-NIL, children have disjoint footprints, the root and external parent are excluded from descendant footprints, and parent links are consistent. StoreRepr additionally requires an absent sentinel; Represents fixes the root's parent to NIL. Both public representation predicates are functional: one store address cannot represent two trees.

rotateLeftP_refines_subtree and rotateRightP_refines_subtree prove the actual pointer operations implement the functional rotations and preserve the owned footprint. Their RotationResult contract states the precise outside-node frame, including the former parent's updated child link. The root refinement theorems cover whole stores. RotationContext and rotateLeftP_refines_context / rotateRightP_refines_context lift an interior rotation through represented ancestors, preserving siblings and reconstructing the enclosing whole-store representation.

The store is a sparse functional model of pointer assignments. The returned rotateCost = 6 is a uniform upper assignment budget, comprising five required assignments and an optional middle-parent assignment; it is not an exact instrumented count or a runtime bound for immutable node-table evaluation. Rotations alone preserve BST ordering, not red-black color balance. The insertion/deletion analysis in the following sections is a separate boundary.

Definitions and proofs

CLRSLean.FourthEdition.Chapter_13.Section_13_2_Rotations.Refinement

              namespace CLRS.Chapter13open RBStore (nil)namespace StoreReprAt

Change only a represented root's parent; all its descendant records agree.


theorem reparent {s s' p q i t F} (h : StoreReprAt s p i t F) (hq : q ∉ F)
    (heq : ∀ j ∈ F, s'.get j =
      if j = i then (s.get j).map (fun n => { n with parent := q }) else s.get j) :
    StoreReprAt s' q i t F := by
  cases h with
  | empty => exact .empty _
  | @node p i n l r L R hn hg hp hL hR hnL hnR hd hpo =>
      apply StoreReprAt.node (n := { n with parent := q }) hn
      · simpa [hg] using heq i (by simp)
      · rfl
      · apply hL.of_agree
        intro j hj
        have hji : j ≠ i := by rintro rfl; exact hnL hj
        simpa [hji] using heq j (by simp [hj])
      · apply hR.of_agree
        intro j hj
        have hji : j ≠ i := by rintro rfl; exact hnR hj
        simpa [hji] using heq j (by simp [hj])
      · exact hnL
      · exact hnR
      · exact hd
      · exact hq

end StoreReprAt

Complete subtree replacement contract, including the outside parent link. Only the old parent's appropriate child field may change outside the footprint.

structure RotationResult (s s' : RBStore) (p oldRoot newRoot : Nat)
    (t : RBTree) (F : Finset Nat) : Prop where
  repr : StoreReprAt s' p newRoot t F
  root : s'.root = if p = nil then newRoot else s.root
  outside : ∀ j, j ∉ F → s'.get j =
    if j = p ∧ p ≠ nil then (s.get j).map (reconnectNode oldRoot newRoot) else s.get j

private theorem disjoint_parts {L R : Finset Nat} (h : Disjoint L R) :
    ∀ j, j ∈ L → j ∈ R → False := Finset.disjoint_left.mp h

A successful left rotation refines the functional rotation at any subtree, including its old parent's link; the footprint is preserved.


theorem rotateLeftP_refines_subtree {s p x c A k d B m C F}
    (h : StoreReprAt s p x (.node c A k (.node d B m C)) F) :
    ∃ y, RotationResult s (rotateLeftP s x).1 p x y
      (.node d (.node c A k B) m C) F := by
  cases h with
  | @node p x nx A right L R hx hg hp hA hR hxL hxR hLR hpF =>
    generalize hydef : nx.right = y at *
    cases hR with
    | @node _ _ ny B C M N hy hgy hpy hB hC hyM hyN hMN hxY =>
      have hxy : x ≠ y := by intro he; apply hxR; simp [he]
      have hxM : x ∉ M := by intro hm; apply hxR; simp [hm]
      have hxN : x ∉ N := by intro hn; apply hxR; simp [hn]
      have hyL : y ∉ L := by
        intro hl
        exact disjoint_parts hLR y hl (by simp)
      have hLM : Disjoint L M := by
        apply Finset.disjoint_left.mpr
        intro j hj hm
        exact disjoint_parts hLR j hj (by simp [hm])
      have hLN : Disjoint L N := by
        apply Finset.disjoint_left.mpr
        intro j hj hn
        exact disjoint_parts hLR j hj (by simp [hn])
      have hpx : p ≠ x := by intro he; apply hpF; simp [he]
      have hpy' : p ≠ y := by intro he; apply hpF; simp [he]
      have hpL : p ∉ L := by intro hj; apply hpF; simp [hj]
      have hpM : p ∉ M := by intro hj; apply hpF; simp [hj]
      have hpN : p ∉ N := by intro hj; apply hpF; simp [hj]
      have hbx : ny.left ≠ x := by
        intro he
        have hh := hB.root_mem (by simpa [he] using hx)
        rw [he] at hh
        exact hxM hh
      have hby : ny.left ≠ y := by
        intro he
        have hh := hB.root_mem (by simpa [he] using hy)
        rw [he] at hh
        exact hyM hh
      let s' := rotationPatch s x y ny.left p
        { nx with right := ny.left, parent := y } { ny with left := x, parent := p }
      have hex : (rotateLeftP s x).1 = s' := by
        simp [rotateLeftP, hg, hydef, hgy, hp, s']
      have hframe (j : Nat) (hjx : j ≠ x) (hjy : j ≠ y)
          (hjb : j ≠ ny.left) (hjp : j ≠ p) : s'.get j = s.get j := by
        simp [s', rotationPatch, RBStore.get, hjx, hjy, hjb, hjp]
      have hA' : StoreReprAt s' x nx.left A L := by
        apply hA.of_agree
        intro j hj
        apply hframe
        · rintro rfl; exact hxL hj
        · rintro rfl; exact hyL hj
        · intro he
          have hb0 : ny.left ≠ nil := by
            intro hb0
            rw [he, hb0] at hj
            exact hA.nil_not_mem hj
          exact disjoint_parts hLM j hj (he ▸ hB.root_mem hb0)
        · rintro rfl; exact hpL hj
      have hC' : StoreReprAt s' y ny.right C N := by
        apply hC.of_agree
        intro j hj
        apply hframe
        · rintro rfl; exact hxN hj
        · rintro rfl; exact hyN hj
        · intro he
          have hb0 : ny.left ≠ nil := by
            intro hb0
            rw [he, hb0] at hj
            exact hC.nil_not_mem hj
          exact disjoint_parts hMN j (he ▸ hB.root_mem hb0) hj
        · rintro rfl; exact hpN hj
      have hB' : StoreReprAt s' x ny.left B M := by
        apply hB.reparent hxM
        intro j hj
        have hjx : j ≠ x := by rintro rfl; exact hxM hj
        have hjy : j ≠ y := by rintro rfl; exact hyM hj
        have hjp : j ≠ p := by rintro rfl; exact hpM hj
        have hj0 : j ≠ nil := by rintro rfl; exact hB.nil_not_mem hj
        by_cases hjb : j = ny.left
        · have hb0 : ny.left ≠ nil := by simpa [← hjb] using hj0
          simp [s', rotationPatch, RBStore.get, hjb, hb0, hbx, hby]
        · simp [s', rotationPatch, RBStore.get, hjx, hjy, hjp, hjb]
      have hx' : s'.get x = some { nx with right := ny.left, parent := y } := by
        simp [s', rotationPatch, RBStore.get]
      have hy' : s'.get y = some { ny with left := x, parent := p } := by
        simp [s', rotationPatch, RBStore.get, Ne.symm hxy]
      have hnewX : StoreReprAt s' y x (.node nx.color A nx.key B) (insert x (L ∪ M)) := by
        apply StoreReprAt.node hx hx' rfl hA' hB' hxL hxM hLM
        simp [Ne.symm hxy, hyL, hyM]
      have hnewY : StoreReprAt s' p y
          (.node ny.color (.node nx.color A nx.key B) ny.key C)
          (insert y (insert x (L ∪ M) ∪ N)) := by
        apply StoreReprAt.node hy hy' rfl hnewX hC'
        · simp [Ne.symm hxy, hyL, hyM]
        · exact hyN
        · simp [Finset.disjoint_insert_left, hxN, Finset.disjoint_union_left, hLN, hMN]
        · simp [hpx, hpy', hpL, hpM, hpN]
      refine ⟨y, ?_⟩
      rw [hex]
      constructor
      · convert hnewY using 1
        ext j
        simp [or_left_comm]
      · simp [s', rotationPatch]
      · intro j hj
        have hjx : j ≠ x := by intro he; apply hj; simp [he]
        have hjy : j ≠ y := by intro he; apply hj; simp [he]
        have hjb : j ≠ ny.left ∨ ny.left = nil := by
          by_cases hb : ny.left = nil
          · exact Or.inr hb
          · left
            intro he
            apply hj
            have hh := hB.root_mem hb
            simp [he, hh]
        rcases hjb with hjb | hb
        · simp [s', rotationPatch, RBStore.get, hjx, hjy, hjb]
        · simp [s', rotationPatch, RBStore.get, hjx, hjy, hb]

The symmetric right-rotation subtree refinement, including reconnection to an external parent and preservation of all other external records.


theorem rotateRightP_refines_subtree {s p x c A k d B m C F}
    (h : StoreReprAt s p x (.node c (.node d A m B) k C) F) :
    ∃ y, RotationResult s (rotateRightP s x).1 p x y
      (.node d A m (.node c B k C)) F := by
  cases h with
  | @node p x nx left C R L hx hg hp hR hA hxR hxL hRL hpF =>
    have hLR := hRL.symm
    generalize hydef : nx.left = y at *
    cases hR with
    | @node _ _ ny A B N M hy hgy hpy hC hB hyN hyM hNM hxY =>
      have hMN := hNM.symm
      have hxy : x ≠ y := by intro he; apply hxR; simp [he]
      have hxM : x ∉ M := by intro hm; apply hxR; simp [hm]
      have hxN : x ∉ N := by intro hn; apply hxR; simp [hn]
      have hyL : y ∉ L := by
        intro hl
        exact disjoint_parts hLR y hl (by simp)
      have hLM : Disjoint L M := by
        apply Finset.disjoint_left.mpr
        intro j hj hm
        exact disjoint_parts hLR j hj (by simp [hm])
      have hLN : Disjoint L N := by
        apply Finset.disjoint_left.mpr
        intro j hj hn
        exact disjoint_parts hLR j hj (by simp [hn])
      have hpx : p ≠ x := by intro he; apply hpF; simp [he]
      have hpy' : p ≠ y := by intro he; apply hpF; simp [he]
      have hpL : p ∉ L := by intro hj; apply hpF; simp [hj]
      have hpM : p ∉ M := by intro hj; apply hpF; simp [hj]
      have hpN : p ∉ N := by intro hj; apply hpF; simp [hj]
      have hbx : ny.right ≠ x := by
        intro he
        have hh := hB.root_mem (by simpa [he] using hx)
        rw [he] at hh
        exact hxM hh
      have hby : ny.right ≠ y := by
        intro he
        have hh := hB.root_mem (by simpa [he] using hy)
        rw [he] at hh
        exact hyM hh
      let s' := rotationPatch s x y ny.right p
        { nx with left := ny.right, parent := y } { ny with right := x, parent := p }
      have hex : (rotateRightP s x).1 = s' := by
        simp [rotateRightP, hg, hydef, hgy, hp, s']
      have hframe (j : Nat) (hjx : j ≠ x) (hjy : j ≠ y)
          (hjb : j ≠ ny.right) (hjp : j ≠ p) : s'.get j = s.get j := by
        simp [s', rotationPatch, RBStore.get, hjx, hjy, hjb, hjp]
      have hA' : StoreReprAt s' x nx.right C L := by
        apply hA.of_agree
        intro j hj
        apply hframe
        · rintro rfl; exact hxL hj
        · rintro rfl; exact hyL hj
        · intro he
          have hb0 : ny.right ≠ nil := by
            intro hb0
            rw [he, hb0] at hj
            exact hA.nil_not_mem hj
          exact disjoint_parts hLM j hj (he ▸ hB.root_mem hb0)
        · rintro rfl; exact hpL hj
      have hC' : StoreReprAt s' y ny.left A N := by
        apply hC.of_agree
        intro j hj
        apply hframe
        · rintro rfl; exact hxN hj
        · rintro rfl; exact hyN hj
        · intro he
          have hb0 : ny.right ≠ nil := by
            intro hb0
            rw [he, hb0] at hj
            exact hC.nil_not_mem hj
          exact disjoint_parts hMN j (he ▸ hB.root_mem hb0) hj
        · rintro rfl; exact hpN hj
      have hB' : StoreReprAt s' x ny.right B M := by
        apply hB.reparent hxM
        intro j hj
        have hjx : j ≠ x := by rintro rfl; exact hxM hj
        have hjy : j ≠ y := by rintro rfl; exact hyM hj
        have hjp : j ≠ p := by rintro rfl; exact hpM hj
        have hj0 : j ≠ nil := by rintro rfl; exact hB.nil_not_mem hj
        by_cases hjb : j = ny.right
        · have hb0 : ny.right ≠ nil := by simpa [← hjb] using hj0
          simp [s', rotationPatch, RBStore.get, hjb, hb0, hbx, hby]
        · simp [s', rotationPatch, RBStore.get, hjx, hjy, hjp, hjb]
      have hx' : s'.get x = some { nx with left := ny.right, parent := y } := by
        simp [s', rotationPatch, RBStore.get]
      have hy' : s'.get y = some { ny with right := x, parent := p } := by
        simp [s', rotationPatch, RBStore.get, Ne.symm hxy]
      have hnewX : StoreReprAt s' y x (.node nx.color B nx.key C) (insert x (M ∪ L)) := by
        apply StoreReprAt.node hx hx' rfl hB' hA' hxM hxL hLM.symm
        simp [Ne.symm hxy, hyL, hyM]
      have hnewY : StoreReprAt s' p y
          (.node ny.color A ny.key (.node nx.color B nx.key C))
          (insert y (N ∪ insert x (M ∪ L))) := by
        apply StoreReprAt.node hy hy' rfl hC' hnewX
        · exact hyN
        · simp [Ne.symm hxy, hyL, hyM]
        · simp [Finset.disjoint_insert_right, hxN, Finset.disjoint_union_right, hLN.symm, hMN.symm]
        · simp [hpx, hpy', hpL, hpM, hpN]
      refine ⟨y, ?_⟩
      rw [hex]
      constructor
      · convert hnewY using 1
        ext j
        simp [or_left_comm, or_comm]
      · simp [s', rotationPatch]
      · intro j hj
        have hjx : j ≠ x := by intro he; apply hj; simp [he]
        have hjy : j ≠ y := by intro he; apply hj; simp [he]
        have hjb : j ≠ ny.right ∨ ny.right = nil := by
          by_cases hb : ny.right = nil
          · exact Or.inr hb
          · left
            intro he
            apply hj
            have hh := hB.root_mem hb
            simp [he, hh]
        rcases hjb with hjb | hb
        · simp [s', rotationPatch, RBStore.get, hjx, hjy, hjb]
        · simp [s', rotationPatch, RBStore.get, hjx, hjy, hb]

A replacement never writes the sentinel record.


theorem RotationResult.sentinel {s s' p i j t F}
    (h : RotationResult s s' p i j t F) : s'.get nil = s.get nil := by
  have hf := h.outside nil h.repr.nil_not_mem
  have hn : ¬ (nil = p ∧ p ≠ nil) := by rintro ⟨rfl, hp⟩; exact hp rfl
  simpa [hn] using hf

A replacement at root level is a whole-store representation refinement.


theorem RotationResult.represents {s s' i j t F}
    (h : RotationResult s s' nil i j t F) (hs : s.get nil = none) : Represents s' t := by
  refine ⟨h.sentinel.trans hs, F, ?_⟩
  have hr : s'.root = j := by simpa using h.root
  simpa [hr] using h.repr

Actual left rotation at the store root refines the functional rotation.

theorem rotateLeftP_refines_root {s c A k d B m C}
    (h : Represents s (.node c A k (.node d B m C))) :
    Represents (rotateLeftP s s.root).1 (.node d (.node c A k B) m C) := by
  obtain ⟨hs, F, ht⟩ := h
  obtain ⟨y, hres⟩ := rotateLeftP_refines_subtree ht
  exact hres.represents hs

Actual right rotation at the store root refines the functional rotation.

theorem rotateRightP_refines_root {s c A k d B m C}
    (h : Represents s (.node c (.node d A m B) k C)) :
    Represents (rotateRightP s s.root).1 (.node d A m (.node c B k C)) := by
  obtain ⟨hs, F, ht⟩ := h
  obtain ⟨y, hres⟩ := rotateRightP_refines_subtree ht
  exact hres.represents hs

@[simp] theorem reconnectNode_self (i : Nat) (n : RBNode) : reconnectNode i i n = n := by
  unfold reconnectNode
  split
  · rename_i h
    cases n
    simp_all
  · split
    · rename_i h
      cases n
      simp_all
    · rfl

@[simp] theorem reconnectNode_self_fun (i : Nat) : reconnectNode i i = id :=
  funext (reconnectNode_self i)

Lift a subtree replacement through a left-child context. This theorem checks the actual updated parent record and frames the sibling subtree.


theorem RotationResult.lift_left {s s' p i n l r L R j l'}
    (hi : i ≠ nil) (hg : s.get i = some n) (hp : n.parent = p)
    (hl : StoreReprAt s i n.left l L) (hr : StoreReprAt s i n.right r R)
    (hiL : i ∉ L) (hiR : i ∉ R) (hd : Disjoint L R)
    (hpF : p ∉ insert i (L ∪ R)) (hroot : p = nil → s.root = i)
    (h : RotationResult s s' i n.left j l' L) :
    RotationResult s s' p i i (.node n.color l' n.key r) (insert i (L ∪ R)) := by
  have hget : s'.get i = some { n with left := j } := by
    simpa [hi, hg, reconnectNode] using h.outside i hiL
  have hr' : StoreReprAt s' i n.right r R := by
    apply hr.of_agree
    intro k hk
    have hkL : k ∉ L := fun hkl => disjoint_parts hd k hkl hk
    have hki : k ≠ i := by rintro rfl; exact hiR hk
    simpa [hki] using h.outside k hkL
  constructor
  · exact StoreReprAt.node (n := { n with left := j }) hi hget hp h.repr hr' hiL hiR hd hpF
  · have hsroot : s'.root = s.root := by simpa [hi] using h.root
    rw [hsroot]
    split
    · exact hroot ‹p = nil›
    · rfl
  · intro k hk
    have hkL : k ∉ L := by intro hkl; apply hk; simp [hkl]
    have hki : k ≠ i := by intro he; apply hk; simp [he]
    simpa [hki, reconnectNode_self] using h.outside k hkL

Lift a subtree replacement through a right-child context. The non-NIL child condition covers every context on a path to a rotated node.


theorem RotationResult.lift_right {s s' p i n l r L R j r'}
    (hi : i ≠ nil) (hg : s.get i = some n) (hp : n.parent = p)
    (hl : StoreReprAt s i n.left l L) (hr : StoreReprAt s i n.right r R)
    (hr0 : n.right ≠ nil)
    (hiL : i ∉ L) (hiR : i ∉ R) (hd : Disjoint L R)
    (hpF : p ∉ insert i (L ∪ R)) (hroot : p = nil → s.root = i)
    (h : RotationResult s s' i n.right j r' R) :
    RotationResult s s' p i i (.node n.color l n.key r') (insert i (L ∪ R)) := by
  have hne : n.left ≠ n.right := by
    intro he
    have hmL := hl.root_mem (by simpa [he] using hr0)
    rw [he] at hmL
    exact disjoint_parts hd n.right hmL (hr.root_mem hr0)
  have hget : s'.get i = some { n with right := j } := by
    simpa [hi, hg, reconnectNode, hne] using h.outside i hiR
  have hl' : StoreReprAt s' i n.left l L := by
    apply hl.of_agree
    intro k hk
    have hkR : k ∉ R := fun hkr => disjoint_parts hd k hk hkr
    have hki : k ≠ i := by rintro rfl; exact hiL hk
    simpa [hki] using h.outside k hkR
  constructor
  · exact StoreReprAt.node (n := { n with right := j }) hi hget hp hl' h.repr hiL hiR hd hpF
  · have hsroot : s'.root = s.root := by simpa [hi] using h.root
    rw [hsroot]
    split
    · exact hroot ‹p = nil›
    · rfl
  · intro k hk
    have hkR : k ∉ R := by intro hkr; apply hk; simp [hkr]
    have hki : k ≠ i := by intro he; apply hk; simp [he]
    simpa [hki, reconnectNode_self] using h.outside k hkR

A represented path from a subtree to its enclosing tree. Each frame owns its sibling footprint and validates the actual parent record.

inductive RotationContext (s : RBStore) :
    Nat → Nat → Finset Nat → Nat → Nat → Finset Nat → (RBTree → RBTree) → Prop where
  | hole (p i : Nat) (F : Finset Nat) (hroot : p = nil → s.root = i) :
      RotationContext s p i F p i F id
  | left {p x F q i n l r L R plug}
      (inner : RotationContext s p x F i n.left L plug)
      (hi : i ≠ nil) (hg : s.get i = some n) (hp : n.parent = q)
      (hl : StoreReprAt s i n.left l L) (hr : StoreReprAt s i n.right r R)
      (hiL : i ∉ L) (hiR : i ∉ R) (hd : Disjoint L R)
      (hqF : q ∉ insert i (L ∪ R)) (hroot : q = nil → s.root = i) :
      RotationContext s p x F q i (insert i (L ∪ R))
        (fun t => .node n.color (plug t) n.key r)
  | right {p x F q i n l r L R plug}
      (inner : RotationContext s p x F i n.right R plug)
      (hi : i ≠ nil) (hg : s.get i = some n) (hp : n.parent = q)
      (hl : StoreReprAt s i n.left l L) (hr : StoreReprAt s i n.right r R)
      (hr0 : n.right ≠ nil)
      (hiL : i ∉ L) (hiR : i ∉ R) (hd : Disjoint L R)
      (hqF : q ∉ insert i (L ∪ R)) (hroot : q = nil → s.root = i) :
      RotationContext s p x F q i (insert i (L ∪ R))
        (fun t => .node n.color l n.key (plug t))

Lift an actual rotation through any represented ancestor path. The result retains the whole enclosing footprint and its outside-node frame contract.

theorem RotationResult.lift_context {s s' p x j t F q z G plug}
    (h : RotationResult s s' p x j t F)
    (ctx : RotationContext s p x F q z G plug) :
    ∃ z', RotationResult s s' q z z' (plug t) G := by
  induction ctx with
  | hole => exact ⟨j, h⟩
  | left inner hi hg hp hl hr hiL hiR hd hqF hroot ih =>
    obtain ⟨j', hj⟩ := ih
    exact ⟨_, hj.lift_left hi hg hp hl hr hiL hiR hd hqF hroot⟩
  | right inner hi hg hp hl hr hr0 hiL hiR hd hqF hroot ih =>
    obtain ⟨j', hj⟩ := ih
    exact ⟨_, hj.lift_right hi hg hp hl hr hr0 hiL hiR hd hqF hroot⟩

Left rotation at an arbitrary represented interior position refines the functional rotation plugged back through its enclosing path.

theorem rotateLeftP_refines_context {s p x F z G plug c A k d B m C}
    (hs : s.get nil = none)
    (h : StoreReprAt s p x (.node c A k (.node d B m C)) F)
    (ctx : RotationContext s p x F nil z G plug) :
    Represents (rotateLeftP s x).1 (plug (.node d (.node c A k B) m C)) := by
  obtain ⟨y, hy⟩ := rotateLeftP_refines_subtree h
  obtain ⟨z', hz⟩ := hy.lift_context ctx
  exact hz.represents hs

Right rotation at an arbitrary represented interior position refines the functional rotation plugged back through its enclosing path.

theorem rotateRightP_refines_context {s p x F z G plug c A k d B m C}
    (hs : s.get nil = none)
    (h : StoreReprAt s p x (.node c (.node d A m B) k C) F)
    (ctx : RotationContext s p x F nil z G plug) :
    Represents (rotateRightP s x).1 (plug (.node d A m (.node c B k C))) := by
  obtain ⟨y, hy⟩ := rotateRightP_refines_subtree h
  obtain ⟨z', hz⟩ := hy.lift_context ctx
  exact hz.represents hs

Missing rotation roots leave the whole store unchanged.

theorem rotateLeftP_missing (s : RBStore) (i : Nat) (h : s.get i = none) :
    rotateLeftP s i = (s, 0) := by simp [rotateLeftP, h]

Missing rotation roots leave the whole store unchanged.

theorem rotateRightP_missing (s : RBStore) (i : Nat) (h : s.get i = none) :
    rotateRightP s i = (s, 0) := by simp [rotateRightP, h]

A missing right child makes left rotation a no-op.

theorem rotateLeftP_missing_child (s : RBStore) (i : Nat) (n : RBNode)
    (hi : s.get i = some n) (hc : s.get n.right = none) :
    rotateLeftP s i = (s, 0) := by simp [rotateLeftP, hi, hc]

A missing left child makes right rotation a no-op.

theorem rotateRightP_missing_child (s : RBStore) (i : Nat) (n : RBNode)
    (hi : s.get i = some n) (hc : s.get n.left = none) :
    rotateRightP s i = (s, 0) := by simp [rotateRightP, hi, hc]

end CLRS.Chapter13

CLRSLean.FourthEdition.Chapter_13.Section_13_2_Rotations.Basic

Pointer rotation primitives and functional ordering

The indexed store models CLRS child and parent pointers with address zero reserved for NIL. Rotations update the two participating records, the non-NIL middle child's parent, and the former parent's appropriate child or the store root. The store update is a sparse functional description of those pointer assignments; it does not model the cost of evaluating an immutable node table.

Successful rotations return the uniform upper assignment budget six: five required pointer assignments and the optional middle-parent assignment. This is not an instrumented exact execution count. Representation, ownership, frame, and actual root/interior refinement theorems are in the sibling modules. Functional rotations preserve inorder keys and the BST ordering predicate; they need not preserve red-black color balance without a surrounding fixup.

namespace CLRSnamespace Chapter13

Pointer/sentinel store (CLRS `T.nil` model)

A single heap node of the pointer-based red-black tree: a key, a color, and the indices of its left, right, and parent pointers. The sentinel index is 0 (CLRS T.nil).

structure RBNode where
  key : Nat
  color : Color
  left : Nat
  right : Nat
  parent : Nat
  deriving Repr, DecidableEq

A pointer-based red-black tree store: a partial node table addressed by natural indices (index 0 is the sentinel T.nil) plus the root index.

structure RBStore where
  node : Nat → Option RBNode
  root : Nat

namespace RBStore

The sentinel index (CLRS T.nil).

def nil : Nat := 0

Read the node table at index i. A valid representation requires the sentinel to be absent; raw stores do not enforce that condition.

def get (s : RBStore) (i : Nat) : Option RBNode := s.node i

Write node n at index i, leaving every other index unchanged.

def set (s : RBStore) (i : Nat) (n : RBNode) : RBStore :=
  { s with node := fun j => if j = i then some n else s.node j }

              @[simp] theorem get_set_eq {s : RBStore} {i : Nat} {n : RBNode} :
    (s.set i n).get i = some n := by
  simp [set, get]@[simp] theorem get_set_ne {s : RBStore} {i j : Nat} {n : RBNode} (h : j ≠ i) :
    (s.set i n).get j = s.get j := by
  simp [set, get, h]end RBStoreopen RBStore (nil)

Inorder key list and BST preservation under rotation

namespace RBTree

The inorder key list of a colored tree.

def keys : RBTree → List Nat
  | .empty => []
  | .node _ l k r => keys l ++ [k] ++ keys r

Left rotation preserves the inorder key list.

theorem keys_rotateLeft (t : RBTree) : keys (rotateLeft t) = keys t := by
  cases t with
  | empty => rfl
  | node c a x r =>
    cases r with
    | empty => rfl
    | node rc b y d =>
      simp [rotateLeft, keys, List.append_assoc]

Right rotation preserves the inorder key list.

theorem keys_rotateRight (t : RBTree) : keys (rotateRight t) = keys t := by
  cases t with
  | empty => rfl
  | node c l y r =>
    cases l with
    | empty => rfl
    | node lc a x b =>
      simp [rotateRight, keys, List.append_assoc]

Root recoloring preserves the inorder key list.

theorem keys_repaintRoot (c : Color) (t : RBTree) :
    keys (repaintRoot c t) = keys t := by
  cases t <;> simp [repaintRoot, keys]

Left rotation preserves the BST ordering invariant.

theorem bst_rotateLeft {t : RBTree} (h : BST t) : BST (rotateLeft t) := by
  cases t with
  | empty => simp [rotateLeft, BST]
  | node c a x r =>
    cases r with
    | empty => simpa [rotateLeft] using h
    | node rc b y d =>
      simp only [rotateLeft]
      change BST a ∧ BST (node rc b y d) ∧ (∀ z, InTree z a → z < x) ∧ (∀ z, z = y ∨ InTree z b ∨ InTree z d → x < z) at h
      rcases h with ⟨hA, hR, hAx, hxR⟩
      change BST b ∧ BST d ∧ (∀ z, InTree z b → z < y) ∧ (∀ z, InTree z d → y < z) at hR
      rcases hR with ⟨hB, hD, hBy, hyD⟩
      change BST (node c a x b) ∧ BST d ∧ (∀ z, z = x ∨ InTree z a ∨ InTree z b → z < y) ∧ (∀ z, InTree z d → y < z)
      constructor
      · constructor
        · exact hA
        constructor
        · exact hB
        constructor
        · intro z hza; exact hAx z hza
        · intro z hzb; exact hxR z (Or.inr (Or.inl hzb))
      · constructor
        · exact hD
        constructor
        · intro z hz
          rcases hz with hzx | hza | hzb
          · subst z; exact hxR y (Or.inl rfl)
          · exact lt_trans (hAx z hza) (hxR y (Or.inl rfl))
          · exact hBy z hzb
        · intro z hzd; exact hyD z hzd

Right rotation preserves the BST ordering invariant.

theorem bst_rotateRight {t : RBTree} (h : BST t) : BST (rotateRight t) := by
  cases t with
  | empty => simp [rotateRight, BST]
  | node c l y r =>
    cases l with
    | empty => simpa [rotateRight] using h
    | node lc a x b =>
      simp only [rotateRight]
      change BST (node lc a x b) ∧ BST r ∧ (∀ z, z = x ∨ InTree z a ∨ InTree z b → z < y) ∧ (∀ z, InTree z r → y < z) at h
      rcases h with ⟨hL, hD, hLtY, hxR⟩
      change BST a ∧ BST b ∧ (∀ z, InTree z a → z < x) ∧ (∀ z, InTree z b → x < z) at hL
      rcases hL with ⟨hA, hB, hAx, hxb⟩
      change BST a ∧ BST (node c b y r) ∧ (∀ z, InTree z a → z < x) ∧ (∀ z, z = y ∨ InTree z b ∨ InTree z r → x < z)
      constructor
      · exact hA
      · constructor
        · change BST b ∧ BST r ∧ (∀ z, InTree z b → z < y) ∧ (∀ z, InTree z r → y < z)
          constructor
          · exact hB
          constructor
          · exact hD
          constructor
          · intro z hzb; exact hLtY z (Or.inr (Or.inr hzb))
          · intro z hzr; exact hxR z hzr
        constructor
        · intro z hza; exact hAx z hza
        · intro z hz
          rcases hz with hzy | hzb | hzr
          · subst z; exact hLtY x (Or.inl rfl)
          · exact hxb z hzb
          · exact lt_trans (hLtY x (Or.inl rfl)) (hxR z hzr)

Root recoloring preserves the BST ordering invariant.

theorem bst_repaintRoot {c : Color} {t : RBTree} (h : BST t) :
    BST (repaintRoot c t) := by
  cases t with
  | empty => simp [repaintRoot, BST]
  | node _ l k r =>
      simp [repaintRoot, BST] at h ⊢
      exact h

end RBTree

Pointer-level rotation and recolor primitives

Uniform assignment budget: five pointer fields (including the old-parent or store-root link), plus the middle child's parent when that child is non-NIL. This budget is not an exact count of executed assignments.

def rotateCost : Nat := 6

Replace the old subtree link in one parent record, preserving its other child and all non-child fields.

def reconnectNode (oldRoot newRoot : Nat) (n : RBNode) : RBNode :=
  if n.left = oldRoot then { n with left := newRoot }
  else if n.right = oldRoot then { n with right := newRoot } else n

The sparse simultaneous update performed by a rotation. On a valid tree, the two rotated nodes, non-NIL middle root, and non-NIL former parent are distinct, so these updates affect independent records.

def rotationPatch (s : RBStore) (oldRoot newRoot middle parent : Nat)
    (oldNode newNode : RBNode) : RBStore where
  root := if parent = nil then newRoot else s.root
  node j :=
    if j = oldRoot then some oldNode
    else if j = newRoot then some newNode
    else if j = middle ∧ middle ≠ nil then
      (s.get j).map (fun n => { n with parent := oldRoot })
    else if j = parent ∧ parent ≠ nil then
      (s.get j).map (reconnectNode oldRoot newRoot)
    else s.get j

Left rotation rewires both participating nodes, the non-NIL middle child's parent, and either the old parent's child link or the store root.

def rotateLeftP (s : RBStore) (x : Nat) : RBStore × Nat :=
  match s.get x with
  | none => (s, 0)
  | some nx =>
      match s.get nx.right with
      | none => (s, 0)
      | some ny =>
          (rotationPatch s x nx.right ny.left nx.parent
            { nx with right := ny.left, parent := nx.right }
            { ny with left := x, parent := nx.parent }, rotateCost)

Right rotation is the symmetric sparse pointer update.

def rotateRightP (s : RBStore) (y : Nat) : RBStore × Nat :=
  match s.get y with
  | none => (s, 0)
  | some ny =>
      match s.get ny.left with
      | none => (s, 0)
      | some nx =>
          (rotationPatch s y ny.left nx.right ny.parent
            { ny with left := nx.right, parent := ny.left }
            { nx with right := y, parent := ny.parent }, rotateCost)

Pointer-level recoloring of node i to color c, at constant cost.

def recolorP (s : RBStore) (i : Nat) (c : Color) : RBStore × Nat :=
  match s.get i with
  | none => (s, 0)
  | some n => (s.set i { n with color := c }, 1)

The assignment budget returned by a left rotation is the constant rotateCost.

theorem rotateLeftP_cost (s : RBStore) (x : Nat) (nx ny : RBNode)
    (hx : s.get x = some nx) (hy : s.get nx.right = some ny) :
    (rotateLeftP s x).2 = rotateCost := by
  unfold rotateLeftP
  simp [hx, hy]

The assignment budget returned by a right rotation is the constant rotateCost.

theorem rotateRightP_cost (s : RBStore) (y : Nat) (ny nx : RBNode)
    (hy : s.get y = some ny) (hx : s.get ny.left = some nx) :
    (rotateRightP s y).2 = rotateCost := by
  unfold rotateRightP
  simp [hy, hx]

A single set write at index i leaves every other index j ≠ i unchanged: the frame property of a single indexed-store write.

theorem set_frame {s : RBStore} {i j : Nat} {n : RBNode} (h : j ≠ i) :
    (s.set i n).get j = s.get j :=
  RBStore.get_set_ne h

Pointer recoloring updates exactly the target node's color at cost 1.

theorem recolorP_spec (s : RBStore) (i : Nat) (c : Color) (n : RBNode)
    (hi : s.get i = some n) :
    (recolorP s i c).2 = 1 ∧ (recolorP s i c).1.get i = some { n with color := c } := by
  simp [recolorP, hi]

end Chapter13end CLRS

CLRSLean.FourthEdition.Chapter_13.Section_13_2_Rotations.Representation

Owned pointer-tree representation

Each represented nonempty node is allocated away from NIL, has the expected parent, and owns a footprint disjoint from both children. The expected parent is outside the subtree. The public wrappers additionally require an absent sentinel, and whole-store representation fixes the root parent to NIL.

namespace CLRS.Chapter13open RBStore (nil)

A finite, uniquely owned subtree with consistent parent links.

inductive StoreReprAt (s : RBStore) : Nat → Nat → RBTree → Finset Nat → Prop where
  | empty (p : Nat) : StoreReprAt s p nil .empty ∅
  | node {p i : Nat} {n : RBNode} {l r : RBTree} {L R : Finset Nat}
      (nonzero : i ≠ nil) (read : s.get i = some n) (parent : n.parent = p)
      (left : StoreReprAt s i n.left l L) (right : StoreReprAt s i n.right r R)
      (not_left : i ∉ L) (not_right : i ∉ R) (disjoint : Disjoint L R)
      (parent_out : p ∉ insert i (L ∪ R)) :
      StoreReprAt s p i (.node n.color l n.key r) (insert i (L ∪ R))

Public subtree representation retains its historical three arguments. The expected parent and owned footprint are existential witnesses.

def StoreRepr (s : RBStore) (i : Nat) (t : RBTree) : Prop :=
  s.get nil = none ∧ ∃ p F, StoreReprAt s p i t F

Whole-store representation requires the root's parent to be NIL.

def Represents (s : RBStore) (t : RBTree) : Prop :=
  s.get nil = none ∧ ∃ F, StoreReprAt s nil s.root t F

namespace StoreReprAt

NIL cannot occur in an owned footprint.

theorem nil_not_mem {s p i t F} (h : StoreReprAt s p i t F) : nil ∉ F := by
  induction h with
  | empty => simp
  | node hn _ _ _ _ _ _ _ _ ihL ihR =>
      simp only [Finset.mem_insert, Finset.mem_union, not_or]
      exact ⟨Ne.symm hn, ihL, ihR⟩

Every represented nonempty root belongs to its footprint.

theorem root_mem {s p i t F} (h : StoreReprAt s p i t F) (hi : i ≠ nil) : i ∈ F := by
  cases h with
  | empty => exact (hi rfl).elim
  | node => simp

The external parent does not belong to the represented subtree.

theorem parent_not_mem {s p i t F} (h : StoreReprAt s p i t F) : p ∉ F := by
  cases h with
  | empty => simp
  | node _ _ _ _ _ _ _ _ hp => exact hp

A represented node cannot point to itself as either child.

theorem no_self_child {s p i t F n} (h : StoreReprAt s p i t F)
    (hi : i ≠ nil) (hg : s.get i = some n) : n.left ≠ i ∧ n.right ≠ i := by
  cases h with
  | empty => exact (hi rfl).elim
  | node hn hg' hp hL hR hnL hnR hd hpo =>
    have he := Option.some.inj (hg.symm.trans hg')
    cases he
    constructor
    · intro he
      apply hnL
      simpa [he] using hL.root_mem (by simpa [he] using hi)
    · intro he
      apply hnR
      simpa [he] using hR.root_mem (by simpa [he] using hi)

Non-NIL children cannot share the same owned root.

theorem children_distinct {s p i t F n} (h : StoreReprAt s p i t F)
    (hi : i ≠ nil) (hg : s.get i = some n) (hl : n.left ≠ nil) : n.left ≠ n.right := by
  cases h with
  | empty => exact (hi rfl).elim
  | node hn hg' hp hL hR hnL hnR hd hpo =>
    have he := Option.some.inj (hg.symm.trans hg')
    cases he
    intro he
    exact Finset.disjoint_left.mp hd (hL.root_mem hl)
      (by simpa [he] using hR.root_mem (by simpa [← he] using hl))

Every occupied address has a stored record.

theorem mem_allocated {s p i t F} (h : StoreReprAt s p i t F)
    {j : Nat} (hj : j ∈ F) : ∃ n, s.get j = some n := by
  induction h with
  | empty => simp at hj
  | @node p i n l r L R hn hg hp hL hR hnL hnR hd hpo ihL ihR =>
      simp only [Finset.mem_insert, Finset.mem_union] at hj
      rcases hj with rfl | hj | hj
      · exact ⟨n, hg⟩
      · exact ihL hj
      · exact ihR hj

Agreement on the owned nodes transports a representation to another store.

theorem of_agree {s s' p i t F} (h : StoreReprAt s p i t F)
    (heq : ∀ j ∈ F, s'.get j = s.get j) : StoreReprAt s' p i t F := by
  induction h with
  | empty => exact .empty _
  | @node p i n l r L R hn hg hp hL hR hnL hnR hd hpo ihL ihR =>
      apply StoreReprAt.node hn ((heq i (by simp)).trans hg) hp
      · apply ihL
        intro j hj
        exact heq j (by simp [hj])
      · apply ihR
        intro j hj
        exact heq j (by simp [hj])
      · exact hnL
      · exact hnR
      · exact hd
      · exact hpo

Writes outside a subtree leave its representation unchanged.

theorem set_frame {s p i t F j n} (h : StoreReprAt s p i t F) (hj : j ∉ F) :
    StoreReprAt (s.set j n) p i t F := by
  apply h.of_agree
  intro k hk
  exact RBStore.get_set_ne (by rintro rfl; exact hj hk)

A root address represents at most one finite tree and one footprint.

theorem unique {s p i t F} (h : StoreReprAt s p i t F) :
    ∀ {p' t' F'}, StoreReprAt s p' i t' F' → t = t' ∧ F = F' := by
  induction h with
  | empty p =>
      intro p' t' F' h'
      cases h' with
      | empty => exact ⟨rfl, rfl⟩
      | node hn => exact (hn rfl).elim
  | @node p i n l r L R hn hg hp hL hR hnL hnR hd hpo ihL ihR =>
      intro p' t' F' h'
      cases h' with
      | empty => exact (hn rfl).elim
      | @node _ _ n' l' r' L' R' hn' hg' hp' hL' hR' hnL' hnR' hd' hpo' =>
          have he : n = n' := Option.some.inj (hg.symm.trans hg')
          cases he
          obtain ⟨rfl, rfl⟩ := ihL hL'
          obtain ⟨rfl, rfl⟩ := ihR hR'
          exact ⟨rfl, rfl⟩