Skip to content

Commit 2b25785

Browse files
wkrozowskiwkrozowski
authored
feat: add lemmas relating insert/insertIfNew and toList on DTreeMap/DHashMap-derived containers (#11565)
This PR adds lemmas that relate `insert`/`insertIfNew` and `toList` on `DTreeMap`/`DHashMap`-derived containers.
1 parent 1824865 commit 2b25785

File tree

15 files changed

+223
-0
lines changed

15 files changed

+223
-0
lines changed

‎src/Std/Data/DHashMap/Internal/RawLemmas.lean‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -406,6 +406,26 @@ theorem get_insert_self [LawfulBEq α] (h : m.1.WF) {k : α} {v : β k} :
406406
(m.insert k v).get k (contains_insert_self _ h) = v := by
407407
simp_to_model [insert, get] using List.getValueCast_insertEntry_self
408408

409+
theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
410+
(m.insert k v).1.toList.Perm (⟨k, v⟩ :: m.1.toList.filter (¬k == ·.1)) := by
411+
simp_to_model using List.Perm.trans (toListModel_insert _) <| List.insertEntry_perm_filter _ _ _
412+
413+
theorem Const.toList_insert_perm {β : Type v} (m : Raw₀ α (fun _ => β)) [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β} :
414+
(Raw.Const.toList (m.insert k v).1).Perm ((k, v) :: (Raw.Const.toList m.1).filter (¬k == ·.1)) := by
415+
simp_to_model
416+
apply List.Perm.trans <| List.Perm.map _ <| toListModel_insert (by wf_trivial)
417+
apply List.Perm.trans <| List.Const.map_insertEntry_perm_filter_map _ _ (by wf_trivial)
418+
simp
419+
420+
theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
421+
(m.insertIfNew k v).1.keys.Perm (if m.contains k then m.1.keys else k :: m.1.keys) := by
422+
simp_to_model
423+
apply List.Perm.trans
424+
simp only [keys_eq_map]
425+
apply List.Perm.map _ <| toListModel_insertIfNew (by wf_trivial)
426+
simp only [← keys_eq_map]
427+
apply List.keys_insertEntryIfNew_perm
428+
409429
@[simp]
410430
theorem get_erase [LawfulBEq α] (h : m.1.WF) {k a : α} {h'} :
411431
(m.erase k).get a h' = m.get a (contains_of_contains_erase _ h h') := by

‎src/Std/Data/DHashMap/Lemmas.lean‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -384,6 +384,18 @@ theorem get_insert_self [LawfulBEq α] {k : α} {v : β k} :
384384
(m.insert k v).get k mem_insert_self = v :=
385385
Raw₀.get_insert_self ⟨m.1, _⟩ m.2
386386

387+
theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
388+
(m.insert k v).toList.Perm (⟨k, v⟩ :: m.toList.filter (¬k == ·.1)) :=
389+
Raw₀.toList_insert_perm ⟨m.1, _⟩ m.2
390+
391+
theorem Const.toList_insert_perm {β : Type v} {m : DHashMap α (fun _ => β)} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
392+
(Const.toList (m.insert k v)).Perm (⟨k, v⟩ :: (Const.toList m).filter (¬k == ·.1)) :=
393+
Raw₀.Const.toList_insert_perm ⟨m.1, _⟩ m.2
394+
395+
theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
396+
(m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys) :=
397+
Raw₀.keys_insertIfNew_perm ⟨m.1, _⟩ m.2
398+
387399
@[simp, grind =]
388400
theorem get_erase [LawfulBEq α] {k a : α} {h'} :
389401
(m.erase k).get a h' = m.get a (mem_of_mem_erase h') :=

‎src/Std/Data/DHashMap/RawLemmas.lean‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -443,6 +443,19 @@ theorem get_insert_self [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
443443
(m.insert k v).get k (mem_insert_self h) = v := by
444444
simp_to_raw using Raw₀.get_insert_self ⟨m, _⟩
445445

446+
theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
447+
(m.insert k v).toList.Perm (⟨k, v⟩ :: m.toList.filter (¬k == ·.1)) := by
448+
simp_to_raw using Raw₀.toList_insert_perm ⟨m, _⟩
449+
450+
theorem Const.toList_insert_perm {β : Type v} {m : Raw α (fun _ => β)} [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
451+
(Const.toList (m.insert k v)).Perm ((k, v) :: (Const.toList m).filter (¬k == ·.1)) := by
452+
simp_to_raw using Raw₀.Const.toList_insert_perm ⟨m, _⟩
453+
454+
theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β k} :
455+
(m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys) := by
456+
simp only [Membership.mem]
457+
simp_to_raw using Raw₀.keys_insertIfNew_perm ⟨m, _⟩
458+
446459
@[simp, grind =]
447460
theorem get_erase [LawfulBEq α] (h : m.WF) {k a : α} {h'} :
448461
(m.erase a).get k h' = m.get k (mem_of_mem_erase h h') := by

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

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -660,6 +660,42 @@ theorem get_insert! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β
660660
t.get a (contains_of_contains_insert! h h₁ h₂) := by
661661
simpa only [insert_eq_insert!] using get_insert h (h₁ := by simpa [insert_eq_insert!])
662662

663+
theorem toList_insert_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
664+
(t.insert k v h.balanced).1.toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := by
665+
simp_to_model
666+
refine List.Perm.trans (toListModel_insert _ h.ordered) <| List.Perm.trans (List.insertEntry_perm_filter _ _ h.ordered.distinctKeys) ?_
667+
simp
668+
669+
theorem toList_insert!_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
670+
(t.insert! k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := by
671+
simpa only [insert_eq_insert!] using toList_insert_perm h
672+
673+
theorem Const.toList_insert_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} :
674+
(Const.toList (t.insert k v h.balanced).1).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) := by
675+
simp_to_model
676+
apply List.Perm.trans <| List.Perm.map _ <| toListModel_insert _ h.ordered
677+
apply List.Perm.trans <| List.Const.map_insertEntry_perm_filter_map _ _ h.ordered.distinctKeys
678+
simp
679+
680+
theorem Const.toList_insert!_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} :
681+
(Const.toList (t.insert! k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) := by
682+
simpa only [insert_eq_insert!] using Const.toList_insert_perm h
683+
684+
theorem keys_insertIfNew_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
685+
(t.insertIfNew k v h.balanced).1.keys.Perm (if t.contains k then t.keys else k :: t.keys) := by
686+
simp_to_model
687+
apply List.Perm.trans
688+
simp only [List.keys_eq_map]
689+
apply List.Perm.map _ <| toListModel_insertIfNew _ h.ordered
690+
simp only [← List.keys_eq_map]
691+
apply List.Perm.trans
692+
apply List.keys_insertEntryIfNew_perm
693+
simp
694+
695+
theorem keys_insertIfNew!_perm {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
696+
(t.insertIfNew! k v).keys.Perm (if t.contains k then t.keys else k :: t.keys) := by
697+
simpa only [insertIfNew_eq_insertIfNew!] using keys_insertIfNew_perm h
698+
663699
theorem get_insert_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} :
664700
(t.insert k v h.balanced).impl.get k (contains_insert_self h) = v := by
665701
simp_to_model [insert, get] using List.getValueCast_insertEntry_self

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -357,6 +357,17 @@ end Const
357357
t.get a (mem_of_mem_insert h₁ h₂) :=
358358
Impl.get_insert t.wf
359359

360+
theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} :
361+
(t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := Impl.toList_insert_perm t.wf
362+
363+
theorem Const.toList_insert_perm {β : Type v} {t : DTreeMap α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} :
364+
(Const.toList (t.insert k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) :=
365+
Impl.Const.toList_insert_perm t.2
366+
367+
theorem keys_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} :
368+
(t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
369+
Impl.keys_insertIfNew_perm t.2
370+
360371
@[simp]
361372
theorem get_insert_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
362373
(t.insert k v).get k mem_insert_self = v :=

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -350,6 +350,18 @@ theorem get?_congr [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = .eq) :
350350

351351
end Const
352352

353+
theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
354+
(t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) :=
355+
Impl.toList_insert!_perm h
356+
357+
theorem Const.toList_insert_perm {β : Type v} {t : Raw α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β} :
358+
(Const.toList (t.insert k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) :=
359+
Impl.Const.toList_insert!_perm h
360+
361+
theorem keys_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
362+
(t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
363+
Impl.keys_insertIfNew!_perm h
364+
353365
@[grind =] theorem get_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} :
354366
(t.insert k v).get a h₁ =
355367
if h₂ : cmp k a = .eq then

‎src/Std/Data/HashMap/Lemmas.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -314,6 +314,14 @@ theorem getElem?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
314314
if h₂ : k == a then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
315315
DHashMap.Const.get_insert (h₁ := h₁)
316316

317+
theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
318+
(m.insert k v).toList.Perm (⟨k, v⟩ :: m.toList.filter (¬k == ·.1)) :=
319+
DHashMap.Const.toList_insert_perm
320+
321+
theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
322+
(m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys) :=
323+
DHashMap.keys_insertIfNew_perm
324+
317325
@[simp]
318326
theorem getElem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
319327
(m.insert k v)[k]'mem_insert_self = v :=

‎src/Std/Data/HashMap/RawLemmas.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -323,6 +323,14 @@ theorem getElem?_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (
323323
if h₂ : k == a then v else m[a]'(mem_of_mem_insert h h₁ (Bool.eq_false_iff.2 h₂)) :=
324324
DHashMap.Raw.Const.get_insert (h₁ := h₁) h.out
325325

326+
theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
327+
(m.insert k v).toList.Perm (⟨k, v⟩ :: m.toList.filter (¬k == ·.1)) :=
328+
DHashMap.Raw.Const.toList_insert_perm h.out
329+
330+
theorem keys_insertIfNew_perm [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
331+
(m.insertIfNew k v).keys.Perm (if k ∈ m then m.keys else k :: m.keys) :=
332+
DHashMap.Raw.keys_insertIfNew_perm h.out
333+
326334
@[simp]
327335
theorem getElem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
328336
(m.insert k v)[k]'(mem_insert_self h) = v :=

‎src/Std/Data/HashSet/Lemmas.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -288,6 +288,10 @@ theorem get?_eq_some [LawfulBEq α] {k : α} (h : k ∈ m) : m.get? k = some k :
288288
if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h₁ h₂) :=
289289
HashMap.getKey_insertIfNew (h₁ := h₁)
290290

291+
theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] {k : α} :
292+
(m.insert k).toList.Perm (if k ∈ m then m.toList else k :: m.toList) :=
293+
HashMap.keys_insertIfNew_perm
294+
291295
@[simp, grind =]
292296
theorem get_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
293297
(m.erase k).get a h' = m.get a (mem_of_mem_erase h') :=

‎src/Std/Data/HashSet/RawLemmas.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -300,6 +300,10 @@ theorem get?_eq_some [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) :
300300
if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h h₁ h₂) :=
301301
HashMap.Raw.getKey_insertIfNew (h₁ := h₁) h.out
302302

303+
theorem toList_insert_perm [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
304+
(m.insert k).toList.Perm (if k ∈ m then m.toList else k :: m.toList) :=
305+
HashMap.Raw.keys_insertIfNew_perm (v := ()) h.out
306+
303307
@[simp, grind =]
304308
theorem get_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
305309
(m.erase k).get a h' = m.get a (mem_of_mem_erase h h') :=

0 commit comments

Comments
 (0)