Finite Maps

lake-manifest.json

@@ -1,11 +1,21 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/quote4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "509ad12ac4efd70d96418b481521296f9619bcf0",
+   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.27.0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "bf4cd323a0d088f361a94fcadb8db5cf1e9f3768",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "stable",

lakefile.toml

@@ -7,6 +7,11 @@ name = "Qq"
 scope = "leanprover-community"
 version = "git#stable"
 
+[[require]]
+name = "batteries"
+scope = "leanprover-community"
+rev = "v4.27.0"
+
 [[lean_lib]]
 name = "Iris"
 

src/Iris/Std/FromMathlib.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Zongyuan Liu, Markus de Medeiros. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+-/
+
+namespace FromMathlib
+
+/-- NB. Copied from Mathlib -/
+theorem List.Nodup.of_map (f : α → β) {l : List α} : List.Nodup (List.map f l) → List.Nodup l := by
+  refine (List.Pairwise.of_map f) fun _ _ => mt <| fun a => (congrArg f ∘ fun _ => a) α
+
+/-- NB. Copied from Mathlib -/
+theorem Pairwise.forall {l : List α} {R : α → α → Prop} (hR : ∀ {a b}, R a b ↔ a ≠ b)
+    (hl : l.Pairwise (· ≠ ·)) : ∀ ⦃a⦄, a ∈ l → ∀ ⦃b⦄, b ∈ l → a ≠ b → R a b := by
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [List.mem_cons]
+    rintro x (rfl | hx) y (rfl | hy)
+    · simp
+    · exact fun a => hR.mpr a
+    · exact fun a => hR.mpr a
+    · refine ih (List.Pairwise.of_cons hl) hx hy
+
+/-- NB. Copied from Mathlib -/
+theorem inj_on_of_nodup_map {f : α → β} {l : List α} (d : List.Nodup (List.map f l)) :
+    ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → f x = f y → x = y := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.map, List.nodup_cons, List.mem_map, not_exists, not_and, ← Ne.eq_def] at d
+    simp only [List.mem_cons]
+    rintro _ (rfl | h₁) _ (rfl | h₂) h₃
+    · rfl
+    · apply (d.1 _ h₂ h₃.symm).elim
+    · apply (d.1 _ h₁ h₃).elim
+    · apply ih d.2 h₁ h₂ h₃
+
+/-- NB. Copied from Mathlib -/
+theorem Nodup.map_on {f : α → β} (H : ∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y) (d : List.Nodup l) :
+    (List.map f l).Nodup :=
+  List.Pairwise.map _ (fun a b ⟨ma, mb, n⟩ e => n (H a ma b mb e)) (List.Pairwise.and_mem.1 d)
+
+/-- NB. Copied from Mathlib -/
+ theorem Nodup.filterMap {f : α → Option β} (h : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') :
+    List.Nodup l → List.Nodup (List.filterMap f l) :=
+  (List.Pairwise.filterMap f) @fun a a' n b bm b' bm' e => n <| h a a' b' (by rw [← e]; exact bm) bm'
+
+/-- NB. Copied from Mathlib -/
+theorem Nodup.filter (p : α → Bool) {l} : List.Nodup l → List.Nodup (List.filter p l) := by
+  simpa using List.Pairwise.filter p
+
+end FromMathlib

src/Iris/Std/HeapInstances.lean

@@ -392,6 +392,32 @@ instance : LawfulPartialMap (TreeMap K · compare) K where
   get?_bindAlter := by simp [Iris.Std.get?, Iris.Std.bindAlter]
   get?_merge := getElem?_mergeWith'
 
+instance : FiniteMap (TreeMap K · compare) K where
+  toList t := t.toList
+
+instance : LawfulFiniteMap (TreeMap K · compare) K where
+  toList_empty := rfl
+  toList_noDupKeys := by
+    intro V m
+    have h' : Pairwise (fun a b => ¬compare a b = eq) (m.toList.map (·.1)) := by
+      refine pairwise_map.mpr ?_
+      refine (distinct_keys_toList (t := m)).imp ?_
+      intro _ _ hab
+      exact hab
+    refine h'.imp ?_
+    intro a b hab
+    rw [compare_eq_iff_eq] at hab
+    exact hab
+  toList_get := by
+    intro V m k v
+    constructor
+    · intro h
+      exact getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList.mpr ⟨k, compare_self, h⟩
+    · intro h
+      obtain ⟨_, hcmp, hmem⟩ := getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList.mp h
+      rw [compare_eq_iff_eq.mp hcmp]
+      exact hmem
+
 end HeapInstance
 
 end Std.TreeMap