feat: Finite Maps (#160)

Co-authored-by: Zongyuan Liu <zy.liu@cs.au.dk>

Author: markusdemedeiros

lake-manifest.json

@@ -1,7 +1,17 @@
 {"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": "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",

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

@@ -290,13 +290,13 @@ private theorem get?_foldl_alter_impl_sigma {l : List ((_ : K) × V)}
         ((l.find? (fun x => (compare x.1 k).isEq)).map (fun kv => (kv.1, kv.2))) := by
   induction l generalizing init with
   | nil =>
-    simp [foldl_nil]
+    simp [List.foldl_nil]
   | cons hd tl IH =>
-    rw [foldl_cons, IH (WF.constAlter! hinit) (hl.tail), Const.get?_alter! hinit]
+    rw [List.foldl_cons, IH (WF.constAlter! hinit) (hl.tail), Const.get?_alter! hinit]
     by_cases h : compare hd.1 k = .eq <;> simp [h]
     rw [← Const.get?_congr hinit h]
     have hhead_none : tl.find? (fun x => (compare x.1 k).isEq) = none := by
-      refine find?_eq_none.mpr fun _ hkv He => rel_of_pairwise_cons hl hkv ?_
+      refine List.find?_eq_none.mpr fun _ hkv He => List.rel_of_pairwise_cons hl hkv ?_
       refine isEq_iff_eq_eq.mpr <| compare_eq_iff_eq.mpr ?_
       rw [eq_of_compare h, compare_eq_iff_eq.mp <| isEq_iff_eq_eq.mp He]
     rw [hhead_none, map_none, pairMerge_none_right]
@@ -309,11 +309,11 @@ private theorem getElem?_foldl_alter {l : List (K × V)} {init : TreeMap K V com
   | nil =>
     simp
   | cons hd tl ih =>
-    rw [foldl_cons, ih (hl.tail)]
+    rw [List.foldl_cons, ih (hl.tail)]
     by_cases heq : compare hd.1 k = .eq
     · have htl : tl.find? (fun kv => (compare kv.1 k).isEq) = none := by
-        refine find?_eq_none.mpr fun kv hkv h => ?_
-        refine rel_of_pairwise_cons hl hkv (eq_trans heq ?_)
+        refine List.find?_eq_none.mpr fun kv hkv h => ?_
+        refine List.rel_of_pairwise_cons hl hkv (eq_trans heq ?_)
         rw [compare_eq_iff_eq.mp <| isEq_iff_eq_eq.mp h]
         exact compare_self
       simp [getElem?_congr (eq_symm heq), htl, heq]
@@ -346,7 +346,7 @@ private theorem getElem?_mergeWith_eq_foldl {t₁ t₂ : TreeMap K V compare}
     fun l => by induction l with grind [isEq]
   rw [hfind_map]
   refine get?_foldl_alter_impl_sigma t₁.inner.wf ?_
-  refine (pairwise_map.mp <|
+  refine (List.pairwise_map.mp <|
     SameKeys.ordered_iff_pairwise_keys.mp t₂.inner.wf.ordered).imp ?_
   rintro hlt heq H
   simp [H]
@@ -373,11 +373,11 @@ theorem getElem?_mergeWith' {t₁ t₂ : TreeMap K V compare} {f : K → V → V
       getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList.mp h
     have hpred : (compare k' k).isEq = true := by simp [eq_symm hcmp]
     obtain ⟨kv, hfind⟩ := isSome_iff_exists.mp <|
-      find?_isSome (p := fun kv => (compare kv.1 k).isEq) |>.mpr ⟨(k', v), hmem, hpred⟩
+      List.find?_isSome (p := fun kv => (compare kv.1 k).isEq) |>.mpr ⟨(k', v), hmem, hpred⟩
     have hkv_cmp : compare kv.1 k = .eq := by
       simpa [beq_iff_eq] using List.find?_some hfind
     have hval : kv.2 = v := by grind
-    have hfind : find? (fun kv => (compare kv.fst k).isEq) t₂.toList =
+    have hfind : List.find? (fun kv => (compare kv.fst k).isEq) t₂.toList =
         some (kv.fst, v) := by
       simp [← hval, ← hfind]
     simp [← hval, hfind]
@@ -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' : List.Pairwise (fun a b => ¬compare a b = eq) (m.toList.map (·.1)) := by
+      refine List.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