Skip to content

Commit 947152f

Browse files
nomeatanomeata
committed
And another one (already fixed
1 parent 481b821 commit 947152f

File tree

1 file changed

+136
-0
lines changed

1 file changed

+136
-0
lines changed

‎tests/lean/run/issue6592.lean‎

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
/--
2+
Colors of red black tree nodes.
3+
-/
4+
inductive Color where
5+
| black
6+
| red
7+
8+
/--
9+
The basic red black tree data structure without any invariant etc. attached.
10+
-/
11+
inductive Raw (α : Type u) where
12+
/--
13+
The empty tree.
14+
-/
15+
| nil : Raw α
16+
/--
17+
A node with left and right successor, its color and a piece of data
18+
-/
19+
| node (left : Raw α) (data : α) (color : Color) (right : Raw α) : Raw α
20+
21+
namespace Raw
22+
23+
/--
24+
Paint the color of the root of `t` to given color `c`.
25+
-/
26+
@[inline]
27+
def paintColor (c : Color) (t : Raw α) : Raw α :=
28+
match t with
29+
| .nil => .nil
30+
| .node l d _ r => .node l d c r
31+
32+
-- Balanced insert into the left child, fixing red on red sequences on the way.
33+
@[inline]
34+
def baliL (d : α) : Raw α → Raw α → Raw α
35+
| .node (.node t₁ data₁ .red t₂) data₂ .red t₃, right
36+
| .node t₁ data₁ .red (.node t₂ data₂ .red t₃), right =>
37+
.node (.node t₁ data₁ .black t₂) data₂ .red (.node t₃ d .black right)
38+
| left, right => .node left d .black right
39+
40+
-- Balanced insert into the right child, fixing red on red sequences on the way.
41+
@[inline]
42+
def baliR (d : α) : Raw α → Raw α → Raw α
43+
| left, .node t₁ data₁ .red (.node t₂ data₂ .red t₃)
44+
| left, .node (.node t₁ data₁ .red t₂) data₂ .red t₃ =>
45+
.node (.node left d .black t₁) data₁ .red (.node t₂ data₂ .black t₃)
46+
| left, right => .node left d .black right
47+
48+
-- Balance a tree on the way up from deletion, prioritizing the left side.
49+
def baldL (d : α) : Raw α → Raw α → Raw α
50+
| .node t₁ data .red t₂, right =>
51+
.node (.node t₁ data .black t₂) d .red right
52+
| left, .node t₁ data .black t₂ =>
53+
baliR d left (.node t₁ data .red t₂)
54+
| left, .node (.node t₁ data₁ .black t₂) data₂ .red t₃ =>
55+
.node (.node left d .black t₁) data₁ .red (baliR data₂ t₂ (paintColor .red t₃))
56+
| left, right => .node left d .red right
57+
58+
-- Balance a tree on the way up from deletion, prioritizing the right side.
59+
def baldR (d : α) : Raw α → Raw α → Raw α
60+
| left, .node t₁ data .red t₂ =>
61+
.node left d .red (.node t₁ data .black t₂)
62+
| .node t₁ data .black t₂, right =>
63+
baliL d (.node t₁ data .red t₂) right
64+
| .node t₁ data₁ .red (.node t₂ data₂ .black t₃), right =>
65+
.node (baliL data₁ (paintColor .red t₁) t₂) data₁ .red (.node t₃ data₂ .black right)
66+
| left, right => .node left d .red right
67+
68+
-- Appends one tree to another while painting the correct color
69+
def appendTrees : Raw α → Raw α → Raw α
70+
| .nil, t => t
71+
| t, .nil => t
72+
| .node left₁ data₁ .red right₁, .node left₂ data₂ .red right₂ =>
73+
match appendTrees right₁ left₂ with
74+
| .node left₃ data₃ .red right₃ =>
75+
.node (.node left₁ data₁ .red left₃) data₃ .red (.node right₃ data₂ .red right₂)
76+
| t => .node left₁ data₁ .red (.node t data₂ .red right₂)
77+
| .node left₁ data₁ .black right₁, .node left₂ data₂ .black right₂ =>
78+
match appendTrees right₁ left₂ with
79+
| .node left₃ data₃ .red right₃ =>
80+
.node (node left₁ data₁ .black left₃) data₃ .red (node right₃ data₂ .black right₂)
81+
| t => baldL data₁ left₁ (node t data₂ .black right₂)
82+
| t, .node left data .red right => node (appendTrees t left) data .red right
83+
| .node left data .red right, t => .node left data .red (appendTrees right t)
84+
85+
def del [Ord α] (d : α) : Raw α → Raw α
86+
| .nil => .nil
87+
| .node left data _ right =>
88+
match compare d data with
89+
| .lt =>
90+
match left with
91+
| .node _ _ .black _ => baldL data (del d left) right
92+
| _ => .node (del d left) data .red right
93+
| .eq => appendTrees left right
94+
| .gt =>
95+
match right with
96+
| .node _ _ .black _ => baldR data left (del d right)
97+
| _ => .node left data .red (del d right)
98+
99+
100+
/--
101+
info: equations:
102+
@[defeq] theorem Raw.del.eq_1.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α), del d nil = nil
103+
@[defeq] theorem Raw.del.eq_2.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d d_1 : α) (color : Color) (left_1 : Raw α)
104+
(data : α) (right left_3 : Raw α) (data_1 : α) (right_1 : Raw α),
105+
del d ((left_1.node data Color.black right).node d_1 color (left_3.node data_1 Color.black right_1)) =
106+
match compare d d_1 with
107+
| Ordering.lt => baldL d_1 (del d (left_1.node data Color.black right)) (left_3.node data_1 Color.black right_1)
108+
| Ordering.eq => (left_1.node data Color.black right).appendTrees (left_3.node data_1 Color.black right_1)
109+
| Ordering.gt => baldR d_1 (left_1.node data Color.black right) (del d (left_3.node data_1 Color.black right_1))
110+
theorem Raw.del.eq_3.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d d_1 : α) (color : Color) (r left_1 : Raw α) (data : α)
111+
(right : Raw α),
112+
(∀ (left : Raw α) (data : α) (right : Raw α), r = left.node data Color.black right → False) →
113+
del d ((left_1.node data Color.black right).node d_1 color r) =
114+
match compare d d_1 with
115+
| Ordering.lt => baldL d_1 (del d (left_1.node data Color.black right)) r
116+
| Ordering.eq => (left_1.node data Color.black right).appendTrees r
117+
| Ordering.gt => (left_1.node data Color.black right).node d_1 Color.red (del d r)
118+
theorem Raw.del.eq_4.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α) (l : Raw α) (d_1 : α) (color : Color)
119+
(left_2 : Raw α) (data : α) (right : Raw α),
120+
(∀ (left : Raw α) (data : α) (right : Raw α), l = left.node data Color.black right → False) →
121+
del d (l.node d_1 color (left_2.node data Color.black right)) =
122+
match compare d d_1 with
123+
| Ordering.lt => (del d l).node d_1 Color.red (left_2.node data Color.black right)
124+
| Ordering.eq => l.appendTrees (left_2.node data Color.black right)
125+
| Ordering.gt => baldR d_1 l (del d (left_2.node data Color.black right))
126+
theorem Raw.del.eq_5.{u_1} : ∀ {α : Type u_1} [inst : Ord α] (d : α) (l : Raw α) (d_1 : α) (color : Color) (r : Raw α),
127+
(∀ (left : Raw α) (data : α) (right : Raw α), l = left.node data Color.black right → False) →
128+
(∀ (left : Raw α) (data : α) (right : Raw α), r = left.node data Color.black right → False) →
129+
del d (l.node d_1 color r) =
130+
match compare d d_1 with
131+
| Ordering.lt => (del d l).node d_1 Color.red r
132+
| Ordering.eq => l.appendTrees r
133+
| Ordering.gt => l.node d_1 Color.red (del d r)
134+
-/
135+
#guard_msgs in
136+
#print equations del

0 commit comments

Comments
 (0)