Skip to content

Commit b0cf25d

Browse files
wkrozowskiwkrozowski
committed
chore: rearrange files a bit
1 parent bd4afe1 commit b0cf25d

File tree

4 files changed

+146
-140
lines changed

4 files changed

+146
-140
lines changed

‎src/Std/Data/DTreeMap/Internal/Def.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ def toListModel : Impl α β → List ((a : α) × β a)
8282
Computes the size of the tree. Used for verification of iterators.
8383
-/
8484
def treeSize : Internal.Impl α β → Nat
85-
| .leaf => 0
86-
| .inner _ _ _ l r => 1 + l.treeSize + treeSize r
85+
| .leaf => 0
86+
| .inner _ _ _ l r => 1 + l.treeSize + treeSize r
8787

8888
end Std.DTreeMap.Internal.Impl

‎src/Std/Data/DTreeMap/Internal/Lemmas.lean‎

Lines changed: 0 additions & 112 deletions
Original file line numberDiff line numberDiff line change
@@ -7945,116 +7945,4 @@ end Const
79457945

79467946
end map
79477947

7948-
theorem pruneLE_eq_filter {α β} [Ord α] [TransOrd α] (t : Internal.Impl α β) (ord_t : t.Ordered) (lowerBound : α) :
7949-
(t.pruneLE lowerBound).toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE) := by
7950-
induction t
7951-
case leaf =>
7952-
simp only [pruneLE, toList_eq_toListModel, toListModel_leaf, List.filter_nil]
7953-
case inner _ k v l r l_ih r_ih =>
7954-
simp only [pruneLE, toList_eq_toListModel, toListModel_inner, List.filter_append]
7955-
generalize heq : compare lowerBound k = x
7956-
cases x
7957-
case lt =>
7958-
simp only [toListModel_inner]
7959-
specialize l_ih (Internal.Impl.Ordered.left ord_t)
7960-
rw [toList_eq_toListModel] at l_ih
7961-
simp only [l_ih, toList_eq_toListModel, List.filter, List.append_cancel_left_eq]
7962-
rw [OrientedOrd.eq_swap, Ordering.swap_eq_lt] at heq
7963-
simp only [heq, Ordering.isGE_gt, List.cons.injEq, true_and]
7964-
symm
7965-
apply List.filter_eq_self.2
7966-
intro a mem
7967-
apply Ordering.isGE_of_eq_gt
7968-
apply TransCmp.gt_trans ?_ heq
7969-
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt]
7970-
exact Internal.Impl.Ordered.compare_right ord_t mem
7971-
case eq =>
7972-
simp only [toListModel_inner, toListModel_leaf, List.nil_append, List.filter]
7973-
rw [OrientedCmp.eq_comm] at heq
7974-
simp only [heq, Ordering.isGE_eq]
7975-
suffices new_goal : List.filter (fun e => (compare e.fst lowerBound).isGE) l.toListModel = [] from by
7976-
simp only [new_goal, List.nil_append, List.cons.injEq, true_and]
7977-
symm
7978-
apply List.filter_eq_self.2
7979-
intro a mem
7980-
apply Ordering.isGE_of_eq_gt
7981-
apply TransCmp.gt_of_gt_of_eq ?_ heq
7982-
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt]
7983-
apply Internal.Impl.Ordered.compare_right ord_t mem
7984-
rw [List.filter_eq_nil_iff]
7985-
intro a mem
7986-
simp only [Bool.not_eq_true, Ordering.isGE_eq_false]
7987-
exact TransCmp.lt_of_lt_of_eq (Internal.Impl.Ordered.compare_left ord_t mem) heq
7988-
case gt =>
7989-
simp only [List.filter]
7990-
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt] at heq
7991-
rw [heq]
7992-
simp
7993-
suffices new_goal : List.filter (fun e => (compare e.fst lowerBound).isGE) l.toListModel = [] from by
7994-
simp only [new_goal, List.nil_append]
7995-
simp only [toList_eq_toListModel] at r_ih
7996-
apply r_ih
7997-
exact Internal.Impl.Ordered.right ord_t
7998-
rw [List.filter_eq_nil_iff]
7999-
intro a mem
8000-
simp only [Bool.not_eq_true, Ordering.isGE_eq_false]
8001-
exact TransCmp.lt_trans (Internal.Impl.Ordered.compare_left ord_t mem) heq
8002-
8003-
theorem pruneLT_eq_filter {α β} [Ord α] [TransOrd α] (t : Internal.Impl α β) (ord_t : t.Ordered) (lowerBound : α) :
8004-
(t.pruneLT lowerBound).toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT) := by
8005-
induction t
8006-
case leaf =>
8007-
simp only [pruneLT, toList_eq_toListModel, toListModel_leaf, List.filter_nil]
8008-
case inner _ k v l r l_ih r_ih =>
8009-
simp only [pruneLT, toList_eq_toListModel, toListModel_inner, List.filter_append]
8010-
generalize heq : compare lowerBound k = x
8011-
cases x
8012-
case lt =>
8013-
simp
8014-
specialize l_ih (Internal.Impl.Ordered.left ord_t)
8015-
rw [toList_eq_toListModel] at l_ih
8016-
simp only [l_ih, toList_eq_toListModel, List.filter, List.append_cancel_left_eq]
8017-
rw [OrientedOrd.eq_swap, Ordering.swap_eq_lt] at heq
8018-
simp only [heq, Ordering.isGT_gt, List.cons.injEq, true_and]
8019-
symm
8020-
apply List.filter_eq_self.2
8021-
intro a mem
8022-
rw [Ordering.isGT_iff_eq_gt]
8023-
apply TransCmp.gt_trans ?_ heq
8024-
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt]
8025-
exact Internal.Impl.Ordered.compare_right ord_t mem
8026-
case eq =>
8027-
simp only [List.filter]
8028-
rw [OrientedCmp.eq_comm] at heq
8029-
rw [heq]
8030-
suffices new_goal : List.filter (fun e => (compare e.fst lowerBound).isGT) l.toListModel = [] ∧
8031-
List.filter (fun e => (compare e.fst lowerBound).isGT) r.toListModel = r.toListModel from by
8032-
simp only [new_goal, Ordering.isGT_eq, List.nil_append]
8033-
apply And.intro
8034-
. rw [List.filter_eq_nil_iff]
8035-
intro a mem
8036-
simp only [Ordering.isGT_iff_eq_gt, ← Ordering.isLE_iff_ne_gt]
8037-
apply TransOrd.isLE_trans _ (Ordering.isLE_of_eq_eq heq)
8038-
apply Ordering.isLE_of_eq_lt
8039-
exact Internal.Impl.Ordered.compare_left ord_t mem
8040-
. apply List.filter_eq_self.2
8041-
intro a mem
8042-
rw [Ordering.isGT_iff_eq_gt]
8043-
apply TransCmp.gt_of_gt_of_eq ?_ heq
8044-
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt]
8045-
exact Internal.Impl.Ordered.compare_right ord_t mem
8046-
case gt =>
8047-
simp only [List.filter]
8048-
rw [OrientedOrd.eq_swap] at heq
8049-
rw [Ordering.swap_eq_gt] at heq
8050-
simp only [heq, Ordering.isGT_lt]
8051-
specialize r_ih (Ordered.right ord_t)
8052-
rw [toList_eq_toListModel] at r_ih
8053-
simp only [r_ih, toList_eq_toListModel, List.self_eq_append_left, List.filter_eq_nil_iff,
8054-
Ordering.isGT_iff_eq_gt]
8055-
intro a mem
8056-
rw [← Ordering.isLE_iff_ne_gt]
8057-
apply Ordering.isLE_of_eq_lt
8058-
exact TransCmp.lt_trans (Internal.Impl.Ordered.compare_left ord_t mem) heq
8059-
80607948
end Std.DTreeMap.Internal.Impl

‎src/Std/Data/DTreeMap/Internal/Operations.lean‎

Lines changed: 0 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -516,32 +516,6 @@ def insertMany! [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Imp
516516
## Operations for verification of iterators and slices
517517
-/
518518

519-
/--
520-
Removes all elements with key less than or equal to `lowerBound`.
521-
Does not modify size information stored in the tree.
522-
-/
523-
def pruneLE {α β} [Ord α] (t : Internal.Impl α β) (lowerBound : α) : Internal.Impl α β :=
524-
match t with
525-
| .leaf => .leaf
526-
| .inner sz k v l r =>
527-
match compare lowerBound k with
528-
| .lt => .inner sz k v (l.pruneLE lowerBound) r
529-
| .eq => .inner sz k v .leaf r
530-
| .gt => r.pruneLE lowerBound
531-
532-
/--
533-
Removes all elements with key less than to `lowerBound`.
534-
Does not modify size information stored in the tree.
535-
-/
536-
def pruneLT {α β} [Ord α] (t : Internal.Impl α β) (lowerBound : α) : Internal.Impl α β :=
537-
match t with
538-
| .leaf => .leaf
539-
| .inner sz k v l r =>
540-
match compare lowerBound k with
541-
| .lt => .inner sz k v (l.pruneLT lowerBound) r
542-
| .eq => r
543-
| .gt => r.pruneLT lowerBound
544-
545519
namespace Const
546520

547521
variable {β : Type v}

‎src/Std/Data/DTreeMap/Internal/Zipper.lean‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,150 @@ public import Init.Data.Slice
1111
public import Std.Data.DTreeMap.Internal.Lemmas
1212

1313
namespace Std.DTreeMap.Internal
14+
15+
namespace Impl
16+
/--
17+
Removes all elements with key less than or equal to `lowerBound`.
18+
19+
Does not modify size information stored in the tree.
20+
-/
21+
def pruneLE {α β} [Ord α] (t : Internal.Impl α β) (lowerBound : α) : Internal.Impl α β :=
22+
match t with
23+
| .leaf => .leaf
24+
| .inner sz k v l r =>
25+
match compare lowerBound k with
26+
| .lt => .inner sz k v (l.pruneLE lowerBound) r
27+
| .eq => .inner sz k v .leaf r
28+
| .gt => r.pruneLE lowerBound
29+
30+
/--
31+
Removes all elements with key less than to `lowerBound`.
32+
33+
Does not modify size information stored in the tree.
34+
-/
35+
def pruneLT {α β} [Ord α] (t : Internal.Impl α β) (lowerBound : α) : Internal.Impl α β :=
36+
match t with
37+
| .leaf => .leaf
38+
| .inner sz k v l r =>
39+
match compare lowerBound k with
40+
| .lt => .inner sz k v (l.pruneLT lowerBound) r
41+
| .eq => r
42+
| .gt => r.pruneLT lowerBound
43+
44+
theorem pruneLE_eq_filter {α β} [Ord α] [TransOrd α] (t : Internal.Impl α β) (ord_t : t.Ordered) (lowerBound : α) :
45+
(t.pruneLE lowerBound).toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGE) := by
46+
induction t
47+
case leaf =>
48+
simp only [pruneLE, toList_eq_toListModel, toListModel_leaf, List.filter_nil]
49+
case inner _ k v l r l_ih r_ih =>
50+
simp only [pruneLE, toList_eq_toListModel, toListModel_inner, List.filter_append]
51+
generalize heq : compare lowerBound k = x
52+
cases x
53+
case lt =>
54+
simp only [toListModel_inner]
55+
specialize l_ih (Internal.Impl.Ordered.left ord_t)
56+
rw [toList_eq_toListModel] at l_ih
57+
simp only [l_ih, toList_eq_toListModel, List.filter, List.append_cancel_left_eq]
58+
rw [OrientedOrd.eq_swap, Ordering.swap_eq_lt] at heq
59+
simp only [heq, Ordering.isGE_gt, List.cons.injEq, true_and]
60+
symm
61+
apply List.filter_eq_self.2
62+
intro a mem
63+
apply Ordering.isGE_of_eq_gt
64+
apply TransCmp.gt_trans ?_ heq
65+
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt]
66+
exact Internal.Impl.Ordered.compare_right ord_t mem
67+
case eq =>
68+
simp only [toListModel_inner, toListModel_leaf, List.nil_append, List.filter]
69+
rw [OrientedCmp.eq_comm] at heq
70+
simp only [heq, Ordering.isGE_eq]
71+
suffices new_goal : List.filter (fun e => (compare e.fst lowerBound).isGE) l.toListModel = [] from by
72+
simp only [new_goal, List.nil_append, List.cons.injEq, true_and]
73+
symm
74+
apply List.filter_eq_self.2
75+
intro a mem
76+
apply Ordering.isGE_of_eq_gt
77+
apply TransCmp.gt_of_gt_of_eq ?_ heq
78+
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt]
79+
apply Internal.Impl.Ordered.compare_right ord_t mem
80+
rw [List.filter_eq_nil_iff]
81+
intro a mem
82+
simp only [Bool.not_eq_true, Ordering.isGE_eq_false]
83+
exact TransCmp.lt_of_lt_of_eq (Internal.Impl.Ordered.compare_left ord_t mem) heq
84+
case gt =>
85+
simp only [List.filter]
86+
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt] at heq
87+
rw [heq]
88+
simp
89+
suffices new_goal : List.filter (fun e => (compare e.fst lowerBound).isGE) l.toListModel = [] from by
90+
simp only [new_goal, List.nil_append]
91+
simp only [toList_eq_toListModel] at r_ih
92+
apply r_ih
93+
exact Internal.Impl.Ordered.right ord_t
94+
rw [List.filter_eq_nil_iff]
95+
intro a mem
96+
simp only [Bool.not_eq_true, Ordering.isGE_eq_false]
97+
exact TransCmp.lt_trans (Internal.Impl.Ordered.compare_left ord_t mem) heq
98+
99+
theorem pruneLT_eq_filter {α β} [Ord α] [TransOrd α] (t : Internal.Impl α β) (ord_t : t.Ordered) (lowerBound : α) :
100+
(t.pruneLT lowerBound).toList = t.toList.filter (fun e => (compare e.fst lowerBound).isGT) := by
101+
induction t
102+
case leaf =>
103+
simp only [pruneLT, toList_eq_toListModel, toListModel_leaf, List.filter_nil]
104+
case inner _ k v l r l_ih r_ih =>
105+
simp only [pruneLT, toList_eq_toListModel, toListModel_inner, List.filter_append]
106+
generalize heq : compare lowerBound k = x
107+
cases x
108+
case lt =>
109+
simp
110+
specialize l_ih (Internal.Impl.Ordered.left ord_t)
111+
rw [toList_eq_toListModel] at l_ih
112+
simp only [l_ih, toList_eq_toListModel, List.filter, List.append_cancel_left_eq]
113+
rw [OrientedOrd.eq_swap, Ordering.swap_eq_lt] at heq
114+
simp only [heq, Ordering.isGT_gt, List.cons.injEq, true_and]
115+
symm
116+
apply List.filter_eq_self.2
117+
intro a mem
118+
rw [Ordering.isGT_iff_eq_gt]
119+
apply TransCmp.gt_trans ?_ heq
120+
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt]
121+
exact Internal.Impl.Ordered.compare_right ord_t mem
122+
case eq =>
123+
simp only [List.filter]
124+
rw [OrientedCmp.eq_comm] at heq
125+
rw [heq]
126+
suffices new_goal : List.filter (fun e => (compare e.fst lowerBound).isGT) l.toListModel = [] ∧
127+
List.filter (fun e => (compare e.fst lowerBound).isGT) r.toListModel = r.toListModel from by
128+
simp only [new_goal, Ordering.isGT_eq, List.nil_append]
129+
apply And.intro
130+
. rw [List.filter_eq_nil_iff]
131+
intro a mem
132+
simp only [Ordering.isGT_iff_eq_gt, ← Ordering.isLE_iff_ne_gt]
133+
apply TransOrd.isLE_trans _ (Ordering.isLE_of_eq_eq heq)
134+
apply Ordering.isLE_of_eq_lt
135+
exact Internal.Impl.Ordered.compare_left ord_t mem
136+
. apply List.filter_eq_self.2
137+
intro a mem
138+
rw [Ordering.isGT_iff_eq_gt]
139+
apply TransCmp.gt_of_gt_of_eq ?_ heq
140+
rw [OrientedOrd.eq_swap, Ordering.swap_eq_gt]
141+
exact Internal.Impl.Ordered.compare_right ord_t mem
142+
case gt =>
143+
simp only [List.filter]
144+
rw [OrientedOrd.eq_swap] at heq
145+
rw [Ordering.swap_eq_gt] at heq
146+
simp only [heq, Ordering.isGT_lt]
147+
specialize r_ih (Ordered.right ord_t)
148+
rw [toList_eq_toListModel] at r_ih
149+
simp only [r_ih, toList_eq_toListModel, List.self_eq_append_left, List.filter_eq_nil_iff,
150+
Ordering.isGT_iff_eq_gt]
151+
intro a mem
152+
rw [← Ordering.isLE_iff_ne_gt]
153+
apply Ordering.isLE_of_eq_lt
154+
exact TransCmp.lt_trans (Internal.Impl.Ordered.compare_left ord_t mem) heq
155+
156+
end Impl
157+
14158
open Std.Iterators
15159

16160
section Zipper

0 commit comments

Comments
 (0)