Skip to content

Commit aeafc3e

Browse files
leodemouraleodemoura
committed
test:
1 parent bc8bdc8 commit aeafc3e

File tree

1 file changed

+328
-0
lines changed

1 file changed

+328
-0
lines changed

‎tests/lean/run/grind_indexmap_trace.lean‎

Lines changed: 328 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,328 @@
1+
import Std.Data.HashMap
2+
3+
macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
4+
5+
open Std
6+
7+
structure IndexMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
8+
private indices : HashMap α Nat
9+
private keys : Array α
10+
private values : Array β
11+
private size_keys' : keys.size = values.size := by grind
12+
private WF : ∀ (i : Nat) (a : α), keys[i]? = some a ↔ indices[a]? = some i := by grind
13+
14+
namespace IndexMap
15+
16+
variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
17+
variable {m : IndexMap α β} {a : α} {b : β} {i : Nat}
18+
19+
@[inline] def size (m : IndexMap α β) : Nat :=
20+
m.values.size
21+
22+
@[local grind =] private theorem size_keys : m.keys.size = m.size := m.size_keys'
23+
24+
def emptyWithCapacity (capacity := 8) : IndexMap α β where
25+
indices := HashMap.emptyWithCapacity capacity
26+
keys := Array.emptyWithCapacity capacity
27+
values := Array.emptyWithCapacity capacity
28+
29+
instance : EmptyCollection (IndexMap α β) where
30+
emptyCollection := emptyWithCapacity
31+
32+
instance : Inhabited (IndexMap α β) where
33+
default := ∅
34+
35+
@[inline] def contains (m : IndexMap α β)
36+
(a : α) : Bool :=
37+
m.indices.contains a
38+
39+
instance : Membership α (IndexMap α β) where
40+
mem m a := a ∈ m.indices
41+
42+
instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) :=
43+
inferInstanceAs (Decidable (a ∈ m.indices))
44+
45+
@[local grind =] private theorem mem_indices_of_mem {m : IndexMap α β} {a : α} :
46+
a ∈ m ↔ a ∈ m.indices := Iff.rfl
47+
48+
@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat := m.indices[a]?
49+
50+
@[inline] def findIdx (m : IndexMap α β) (a : α) (h : a ∈ m := by get_elem_tactic) : Nat := m.indices[a]
51+
52+
@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β := m.values[i]?
53+
54+
@[inline] def getIdx (m : IndexMap α β) (i : Nat) (h : i < m.size := by get_elem_tactic) : β :=
55+
m.values[i]
56+
57+
variable [LawfulBEq α] [LawfulHashable α]
58+
59+
attribute [local grind _=_] IndexMap.WF
60+
61+
private theorem getElem_indices_lt {h : a ∈ m} : m.indices[a] < m.size := by
62+
have : m.indices[a]? = some m.indices[a] := by grind
63+
grind
64+
65+
grind_pattern getElem_indices_lt => m.indices[a]
66+
67+
attribute [local grind] size
68+
69+
instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
70+
getElem m a h := m.values[m.indices[a]'h]
71+
getElem? m a := m.indices[a]?.bind (fun i => (m.values[i]?))
72+
getElem! m a := m.indices[a]?.bind (fun i => (m.values[i]?)) |>.getD default
73+
74+
@[local grind =] private theorem getElem_def (m : IndexMap α β) (a : α) (h : a ∈ m) : m[a] = m.values[m.indices[a]'h] := rfl
75+
@[local grind =] private theorem getElem?_def (m : IndexMap α β) (a : α) :
76+
m[a]? = m.indices[a]?.bind (fun i => (m.values[i]?)) := rfl
77+
@[local grind =] private theorem getElem!_def [Inhabited β] (m : IndexMap α β) (a : α) :
78+
m[a]! = (m.indices[a]?.bind (fun i => (m.values[i]?))).getD default := rfl
79+
80+
instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
81+
getElem?_def := by grind
82+
getElem!_def := by grind
83+
84+
@[inline] def insert [LawfulBEq α] (m : IndexMap α β) (a : α) (b : β) :
85+
IndexMap α β :=
86+
match h : m.indices[a]? with
87+
| some i =>
88+
{ indices := m.indices
89+
keys := m.keys.set i a
90+
values := m.values.set i b }
91+
| none =>
92+
{ indices := m.indices.insert a m.size
93+
keys := m.keys.push a
94+
values := m.values.push b }
95+
96+
instance [LawfulBEq α] : Singleton (α × β) (IndexMap α β) :=
97+
⟨fun ⟨a, b⟩ => (∅ : IndexMap α β).insert a b⟩
98+
99+
instance [LawfulBEq α] : Insert (α × β) (IndexMap α β) :=
100+
⟨fun ⟨a, b⟩ s => s.insert a b⟩
101+
102+
instance [LawfulBEq α] : LawfulSingleton (α × β) (IndexMap α β) :=
103+
⟨fun _ => rfl⟩
104+
105+
@[local grind .] private theorem WF' (i : Nat) (a : α) (h₁ : i < m.keys.size) (h₂ : a ∈ m) :
106+
m.keys[i] = a ↔ m.indices[a] = i := by
107+
have := m.WF i a
108+
grind
109+
110+
/--
111+
Erase the key-value pair with the given key, moving the last pair into its place in the order.
112+
If the key is not present, the map is unchanged.
113+
-/
114+
@[inline] def eraseSwap (m : IndexMap α β) (a : α) : IndexMap α β :=
115+
match h : m.indices[a]? with
116+
| some i =>
117+
if w : i = m.size - 1 then
118+
{ indices := m.indices.erase a
119+
keys := m.keys.pop
120+
values := m.values.pop }
121+
else
122+
let lastKey := m.keys.back
123+
let lastValue := m.values.back
124+
{ indices := (m.indices.erase a).insert lastKey i
125+
keys := m.keys.pop.set i lastKey
126+
values := m.values.pop.set i lastValue }
127+
| none => m
128+
129+
/-! ### Verification theorems -/
130+
131+
attribute [local grind] getIdx findIdx insert
132+
133+
/--
134+
info: Try this:
135+
[apply] instantiate only [getIdx, findIdx, = getElem_def]
136+
-/
137+
#guard_msgs in
138+
example (m : IndexMap α β) (a : α) (h : a ∈ m) :
139+
m.getIdx (m.findIdx a) = m[a] := by
140+
grind => finish?
141+
142+
example (m : IndexMap α β) (a : α) (h : a ∈ m) :
143+
m.getIdx (m.findIdx a) = m[a] := by
144+
grind => instantiate only [getIdx, findIdx, = getElem_def]
145+
146+
/--
147+
info: Try this:
148+
[apply] ⏎
149+
instantiate only [= mem_indices_of_mem, insert]
150+
instantiate only [= getElem?_neg, = getElem?_pos, =_ HashMap.contains_iff_mem]
151+
instantiate only [=_ HashMap.contains_iff_mem]
152+
cases #4ed2
153+
next =>
154+
cases #ffdf
155+
next => instantiate only
156+
next =>
157+
instantiate only
158+
instantiate only [= HashMap.contains_insert]
159+
next =>
160+
cases #95a0
161+
next =>
162+
cases #2688
163+
next => instantiate only
164+
next =>
165+
instantiate only
166+
instantiate only [= HashMap.contains_insert]
167+
next =>
168+
cases #ffdf
169+
next => instantiate only
170+
next =>
171+
instantiate only
172+
instantiate only [= HashMap.contains_insert]
173+
-/
174+
#guard_msgs in
175+
example (m : IndexMap α β) (a a' : α) (b : β) :
176+
a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
177+
grind => finish?
178+
179+
-- **TODO**: Investigate whey the following `finish?` has one fewer step.
180+
/--
181+
info: Try this:
182+
[apply] ⏎
183+
instantiate only [= mem_indices_of_mem, insert]
184+
instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
185+
cases #4ed2
186+
next =>
187+
cases #ffdf
188+
next => instantiate only
189+
next =>
190+
instantiate only
191+
instantiate only [= HashMap.contains_insert]
192+
next =>
193+
cases #95a0
194+
next =>
195+
cases #2688
196+
next => instantiate only
197+
next =>
198+
instantiate only
199+
instantiate only [= HashMap.contains_insert]
200+
next =>
201+
cases #ffdf
202+
next => instantiate only
203+
next =>
204+
instantiate only
205+
instantiate only [= HashMap.contains_insert]
206+
-/
207+
#guard_msgs in
208+
example (m : IndexMap α β) (a a' : α) (b : β) :
209+
a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
210+
grind => finish?
211+
212+
example (m : IndexMap α β) (a a' : α) (b : β) :
213+
a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
214+
grind =>
215+
instantiate only [= mem_indices_of_mem, insert]
216+
instantiate only [=_ HashMap.contains_iff_mem, = getElem?_neg, = getElem?_pos]
217+
cases #4ed2
218+
next =>
219+
cases #ffdf
220+
next => instantiate only
221+
next =>
222+
instantiate only
223+
instantiate only [= HashMap.contains_insert]
224+
next =>
225+
cases #95a0
226+
next =>
227+
cases #2688
228+
next => instantiate only
229+
next =>
230+
instantiate only
231+
instantiate only [= HashMap.contains_insert]
232+
next =>
233+
cases #ffdf
234+
next => instantiate only
235+
next =>
236+
instantiate only
237+
instantiate only [= HashMap.contains_insert]
238+
239+
/--
240+
info: Try this:
241+
[apply] ⏎
242+
instantiate only [= getElem_def, insert]
243+
instantiate only [= getElem?_neg, = getElem?_pos]
244+
cases #f590
245+
next =>
246+
cases #ffdf
247+
next =>
248+
instantiate only
249+
instantiate only [= Array.getElem_set]
250+
next =>
251+
instantiate only
252+
instantiate approx [= HashMap.getElem_insert, = Array.size_push, size, = Array.getElem_push,
253+
= HashMap.contains_insert, = HashMap.mem_insert, = Array.size_push]
254+
next =>
255+
instantiate only [= getElem_def, = mem_indices_of_mem]
256+
instantiate only [usr getElem_indices_lt]
257+
instantiate only [size]
258+
cases #ffdf
259+
next =>
260+
instantiate only [=_ WF]
261+
instantiate only [= Array.getElem_set, = getElem?_neg, = getElem?_pos]
262+
instantiate only [WF']
263+
next =>
264+
instantiate only
265+
instantiate only [= Array.getElem_push, = HashMap.mem_insert, = HashMap.getElem_insert]
266+
-/
267+
#guard_msgs in
268+
example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
269+
(m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
270+
grind => finish?
271+
272+
example (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
273+
(m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
274+
grind =>
275+
instantiate only [= getElem_def, insert]
276+
instantiate only [= getElem?_neg, = getElem?_pos]
277+
cases #f590
278+
next =>
279+
cases #ffdf
280+
next =>
281+
instantiate only
282+
instantiate only [= Array.getElem_set]
283+
next =>
284+
instantiate only
285+
-- **TODO**: Investigate why we need `approx` here
286+
instantiate approx [= HashMap.getElem_insert, = Array.size_push, size, = Array.getElem_push,
287+
= HashMap.contains_insert, = HashMap.mem_insert, = Array.size_push]
288+
next =>
289+
instantiate only [= getElem_def, = mem_indices_of_mem]
290+
instantiate only [usr getElem_indices_lt]
291+
instantiate only [size]
292+
cases #ffdf
293+
next =>
294+
instantiate only [=_ WF]
295+
instantiate only [= Array.getElem_set, = getElem?_neg, = getElem?_pos]
296+
instantiate only [WF']
297+
next =>
298+
instantiate only
299+
instantiate only [= Array.getElem_push, = HashMap.mem_insert, = HashMap.getElem_insert]
300+
301+
/--
302+
info: Try this:
303+
[apply] ⏎
304+
instantiate only [insert, = mem_indices_of_mem, findIdx]
305+
instantiate only [= getElem?_pos, = getElem?_neg]
306+
cases #1bba
307+
next => instantiate only [findIdx]
308+
next =>
309+
instantiate only
310+
instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
311+
-/
312+
#guard_msgs in
313+
example (m : IndexMap α β) (a : α) (b : β) :
314+
(m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
315+
grind => finish?
316+
317+
example (m : IndexMap α β) (a : α) (b : β) :
318+
(m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
319+
grind =>
320+
instantiate only [insert, = mem_indices_of_mem, findIdx]
321+
instantiate only [= getElem?_pos, = getElem?_neg]
322+
cases #1bba
323+
next => instantiate only [findIdx]
324+
next =>
325+
instantiate only
326+
instantiate only [= HashMap.mem_insert, = HashMap.getElem_insert]
327+
328+
end IndexMap

0 commit comments

Comments
 (0)