Red-black tree in Lean 4 prover.

I proved all needed properties, for example that resulting tree is sorted.

I implemented one operation only: insertion. And I "cheat" by assuming that original tree is always black. My goal was not implementing everything, I just wanted to implement one simple operation and prove really everything about it.

Proof of sorting (insert_sorted) turned out to be rather big. If someone knows how to make it smaller (possibly using mathlib), then, please, tell me that.

Askar Safin
https://types.pl/@safinaskar
[email protected]
https://lobste.rs/~safinaskar

namespace simple

mutual
  inductive Black where
    | null : Black
    | some (left : Node) (val : Nat) (right : Node) : Black
  inductive Node where
    | black : Black -> Node
    | red (left : Black) (val : Nat) (right : Black) : Node
end

def join (n11 : Node) (n12 : Nat) (n13 : Black) (n2 : Nat) (n3 : Node) : Node := match n11 with
  | .black n11 => .black (.some (.red n11 n12 n13) n2 n3)
  | .red _ _ _ => match n3 with
    | .black n3 => .black (.some n11 n12 (.red n13 n2 n3))
    | .red n31 n32 n33 => .red (.some n11 n12 (.black n13)) n2 (.some (.black n31) n32 (.black n33))

def insert (new : Nat) (node : Black) : Node := match node with
  | .null => .red .null new .null
  | .some n1 n2 n3 => if new <= n2 then
    match n1 with
      | .black n1 => .black (.some (insert new n1) n2 n3)
      | .red n11 n12 n13 => if new <= n12 then
        join (insert new n11) n12 n13 n2 n3
      else
        match insert new n13 with
          | .black n13 => .black (.some (.red n11 n12 n13) n2 n3)
          | n13@(.red n131 n132 n133) => match n3 with
            | .black n3 => .black (.some (.red n11 n12 n131) n132 (.red n133 n2 n3))
            | .red n31 n32 n33 => .red (.some (.black n11) n12 n13) n2 (.some (.black n31) n32 (.black n33))
  else
    match n3 with
      | .black n3 => .black (.some n1 n2 (insert new n3))
      | .red n31 n32 n33 => if new <= n32 then
        match insert new n31 with
          | .black n31 => .black (.some n1 n2 (.red n31 n32 n33))
          | n31@(.red n311 n312 n313) => match n1 with
            | .black n1 => .black (.some (.red n1 n2 n311) n312 (.red n313 n32 n33))
            | .red n11 n12 n13 => .red (.some (.black n11) n12 (.black n13)) n2 (.some n31 n32 (.black n33))
      else
        join n1 n2 n31 n32 (insert new n33)

end simple

namespace peano

mutual
  inductive Black : Nat -> Type where
    | null : Black 0
    | some (left : Node h) (val : Nat) (right : Node h) : Black (.succ h)
  inductive Node : Nat -> Type where
    | black : Black h -> Node h
    | red (left : Black h) (val : Nat) (right : Black h) : Node h
end

def join {h : Nat} (n11 : Node h) (n12 : Nat) (n13 : Black h) (n2 : Nat) (n3 : Node h) : Node (.succ h) := match n11 with
  | .black n11 => .black (.some (.red n11 n12 n13) n2 n3)
  | .red _ _ _ => match n3 with
    | .black n3 => .black (.some n11 n12 (.red n13 n2 n3))
    | .red n31 n32 n33 => .red (.some n11 n12 (.black n13)) n2 (.some (.black n31) n32 (.black n33))

def insert {h : Nat} (new : Nat) (node : Black h) : Node h := match node with
  | .null => .red .null new .null
  | .some n1 n2 n3 => if new <= n2 then
    match n1 with
      | .black n1 => .black (.some (insert new n1) n2 n3)
      | .red n11 n12 n13 => if new <= n12 then
        join (insert new n11) n12 n13 n2 n3
      else
        match insert new n13 with
          | .black n13 => .black (.some (.red n11 n12 n13) n2 n3)
          | n13@(.red n131 n132 n133) => match n3 with
            | .black n3 => .black (.some (.red n11 n12 n131) n132 (.red n133 n2 n3))
            | .red n31 n32 n33 => .red (.some (.black n11) n12 n13) n2 (.some (.black n31) n32 (.black n33))
  else
    match n3 with
      | .black n3 => .black (.some n1 n2 (insert new n3))
      | .red n31 n32 n33 => if new <= n32 then
        match insert new n31 with
          | .black n31 => .black (.some n1 n2 (.red n31 n32 n33))
          | n31@(.red n311 n312 n313) => match n1 with
            | .black n1 => .black (.some (.red n1 n2 n311) n312 (.red n313 n32 n33))
            | .red n11 n12 n13 => .red (.some (.black n11) n12 (.black n13)) n2 (.some n31 n32 (.black n33))
      else
        join n1 n2 n31 n32 (insert new n33)

mutual
  def list {h : Nat} (node : Node h) : List Nat := match node with
    | .black node => list_black node
    | .red a b c => list_black a ++ [b] ++ list_black c

  def list_black {h : Nat} (node : Black h) : List Nat := match node with
    | .null => []
    | .some a b c => list a ++ [b] ++ list c
end

-- lemma
theorem list_join (h : Nat) (n11 : Node h) (n12 : Nat) (n13 : Black h) (n2 : Nat) (n3 : Node h) : list (join n11 n12 n13 n2 n3) = list n11 ++ [n12] ++ list_black n13 ++ [n2] ++ list n3 := by
  fun_cases join with grind +locals

-- result is permutation of original
theorem insert_perm (h : Nat) (new : Nat) (node : Black h) : List.Perm (list_black node ++ [new]) (list (insert new node)) := by
  fun_induction insert
  all_goals
    try rewrite [list_join]
    simp_all!
    try grind

-- lemma
theorem sorted_insert_lemma (height : Nat) (a : Black height) (c : List Nat) (mid : Nat) (new : Nat) : List.Pairwise (· <= ·) (list_black a ++ [mid] ++ c) -> List.Pairwise (· <= ·) (list (insert new a)) -> new <= mid -> List.Pairwise (· <= ·) (list (insert new a) ++ [mid] ++ c) := by
  have _ := insert_perm
  grind

-- lemma
theorem sorted_insert_lemma2 (height : Nat) (a : List Nat) (c : Black height) (mid : Nat) (new : Nat) : List.Pairwise (· <= ·) (a ++ [mid] ++ list_black c) -> List.Pairwise (· <= ·) (list (insert new c)) -> new >= mid -> List.Pairwise (· <= ·) (a ++ [mid] ++ list (insert new c)) := by
  have _ := insert_perm
  grind

-- lemma
theorem sorted_insert_lemma3 (height : Nat) (a : List Nat) (b : Nat) (c : Black height) (d : Nat) (e : List Nat) (new : Nat) : List.Pairwise (· <= ·) (a ++ [b] ++ list_black c ++ [d] ++ e) -> List.Pairwise (· <= ·) (list (insert new c)) -> b <= new -> new <= d -> List.Pairwise (· <= ·) (a ++ [b] ++ list (insert new c) ++ [d] ++ e) := by
  have _ := insert_perm
  intros
  have _ : List.Pairwise (· <= ·) (a ++ [b] ++ list (insert new c)) := by grind
  grind

-- if original is sorted, then result is sorted
theorem insert_sorted (h : Nat) (new : Nat) (node : Black h) : List.Pairwise (· <= ·) (list_black node) -> List.Pairwise (· <= ·) (list (insert new node)) := by
  fun_induction insert with
    | case1 => simp_all!
    | case2 =>
      have _ := sorted_insert_lemma
      simp_all!
      grind
    | case3 =>
      rewrite [list_join]
      have _ := sorted_insert_lemma
      simp_all!
      grind
    | case4 _ d e _ a b c _ c2 =>
      intro
      have _ : List.Pairwise (· <= ·) (list_black a ++ [b] ++ list (insert new c) ++ [d] ++ list e) := by
        apply sorted_insert_lemma3
        all_goals
          simp_all!
          try grind
      simp_all!
    | case5 _ d _ a b c _ _ _ _ _ e =>
      intro
      have _ : List.Pairwise (· <= ·) (list_black a ++ [b] ++ list (insert new c) ++ [d] ++ list_black e) := by
        apply sorted_insert_lemma3
        all_goals
          simp_all!
          try grind
      simp_all!
    | case6 _ d _ a b c _ _ _ _ _ e1 e2 e3 =>
      intro
      have _ : List.Pairwise (· <= ·) (list_black a ++ [b] ++ list (insert new c) ++ [d] ++ (list_black e1 ++ [e2] ++ list_black e3)) := by
        apply sorted_insert_lemma3
        all_goals
          simp_all!
          try grind
      simp_all!
    | case7 =>
      have _ := sorted_insert_lemma2
      simp_all!
      grind
    | case8 _ a b _ c d e _ c2 =>
      intro
      have _ : List.Pairwise (· <= ·) (list a ++ [b] ++ list (insert new c) ++ [d] ++ list_black e) := by
        apply sorted_insert_lemma3
        all_goals
          simp_all!
          try grind
      simp_all!
    | case9 _ b _ c d e _ _ _ _ _ a =>
      intro
      have _ : List.Pairwise (· <= ·) (list_black a ++ [b] ++ list (insert new c) ++ [d] ++ list_black e) := by
        apply sorted_insert_lemma3
        all_goals
          simp_all!
          try grind
      simp_all!
    | case10 _ b _ c d e _ _ _ _ _ a1 a2 a3 =>
      intro
      have _ : List.Pairwise (· <= ·) ((list_black a1 ++ [a2] ++ list_black a3) ++ [b] ++ list (insert new c) ++ [d] ++ list_black e) := by
        apply sorted_insert_lemma3
        all_goals
          simp_all!
          try grind
      simp_all!
    | case11 =>
      rewrite [list_join]
      have _ := sorted_insert_lemma2
      simp_all!
      grind

end peano
Edit

Pub: 01 Apr 2026 08:57 UTC

Views: 677