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
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 | 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
|