feat: tree map lemmas about empty, isEmpty, insert, contains (#6850)

This PR adds some lemmas about the new tree map. These lemmas are about
the interactions of `empty`, `isEmpty`, `insert`, `contains`. Some
lemmas about the interaction of `contains` with the others will follow
in a later PR.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>

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

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Paul Reichert
+-/
+prelude
+import Std.Data.HashMap.Basic
+import Std.Data.DTreeMap.Internal.WF.Lemmas
+
+/-!
+# Internal lemmas about the tree map
+
+This file contains internal lemmas about `Std.DTreeMap.Internal.Impl`. Users of the tree map should
+not rely on the contents of this file.
+-/
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+open Std.Internal.List
+open Std.Internal
+
+universe u v
+
+namespace Std.DTreeMap.Internal.Impl
+
+variable {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β}
+
+/-- Internal implementation detail of the tree map -/
+scoped macro "wf_trivial" : tactic => `(tactic|
+  repeat (first
+    | apply WF.ordered | apply WF.balanced | apply WF.insert | apply WF.insert!
+    | apply WF.insertIfNew | apply WF.insertIfNew!
+    | apply WF.erase | apply WF.erase!
+    | apply Ordered.distinctKeys
+    | assumption
+    ))
+
+/-- Internal implementation detail of the tree map -/
+scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] } )
+
+open Lean
+
+private def queryNames : Array Name :=
+  #[``isEmpty_eq_isEmpty, ``contains_eq_containsKey, ``size_eq_length]
+
+private def modifyMap : Std.HashMap Name Name :=
+  .ofList
+    [⟨`insert, ``toListModel_insert⟩,
+     ⟨`insert!, ``toListModel_insert!⟩,
+     ⟨`insertIfNew, ``toListModel_insertIfNew⟩,
+     ⟨`insertIfNew!, ``toListModel_insertIfNew!⟩,
+     ⟨`erase, ``toListModel_erase⟩,
+     ⟨`erase!, ``toListModel_erase!⟩]
+
+private def congrNames : MacroM (Array (TSyntax `term)) := do
+  return #[← `(_root_.List.Perm.isEmpty_eq), ← `(containsKey_of_perm),
+    ← `(_root_.List.Perm.length_eq), ← `(getValueCast?_of_perm _),
+    ← `(getValue?_of_perm _), ← `(getValue_of_perm _), ← `(getValueCast_of_perm _),
+    ← `(getValueCast!_of_perm _), ← `(getValueCastD_of_perm _), ← `(getValue!_of_perm _),
+    ← `(getValueD_of_perm _), ← `(getKey?_of_perm _), ← `(getKey_of_perm _), ← `(getKeyD_of_perm _),
+    ← `(getKey!_of_perm _)]
+
+/-- Internal implementation detail of the tree map -/
+scoped syntax "simp_to_model" (" [" (ident,*) "]")? ("using" term)? : tactic
+
+macro_rules
+| `(tactic| simp_to_model $[[$modifyNames,*]]? $[using $using?]?) => do
+  let mut congrModify : Array (TSyntax `term) := #[]
+  if let some modifyNames := modifyNames then
+    for modify in modifyNames.getElems.flatMap
+        (fun n => modifyMap.get? (Lean.Syntax.getId n) |>.toArray) do
+      for congr in (← congrNames) do
+        congrModify := congrModify.push (← `($congr:term ($(mkIdent modify) ..)))
+  `(tactic|
+    (simp (discharger := wf_trivial) only
+      [$[$(Array.map Lean.mkIdent queryNames):term],*, $[$congrModify:term],*]
+     $[apply $(using?.toArray):term];*)
+    <;> wf_trivial)
+
+attribute [local instance] beqOfOrd
+attribute [local instance] equivBEq_of_transOrd
+
+theorem isEmpty_empty : isEmpty (empty : Impl α β) := by
+  simp [Impl.isEmpty_eq_isEmpty]
+
+theorem isEmpty_insert [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v h.balanced).impl.isEmpty = false := by
+  simp_to_model [insert] using List.isEmpty_insertEntry
+
+theorem isEmpty_insert! [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insert! k v).isEmpty = false := by
+  simp_to_model [insert!] using List.isEmpty_insertEntry
+
+theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
+  Iff.rfl
+
+theorem contains_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : compare k k' = .eq) :
+    t.contains k = t.contains k' := by
+  rw [← beq_iff_eq (b := Ordering.eq), ← beq_eq] at hab
+  simp_to_model using List.containsKey_congr
+
+theorem mem_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : compare k k' = .eq) :
+    k ∈ t ↔ k' ∈ t := by
+  simp [mem_iff_contains, contains_congr h hab]
+
+theorem isEmpty_insertIfNew [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).impl.isEmpty = false := by
+  simp_to_model [insertIfNew] using List.isEmpty_insertEntryIfNew
+
+theorem isEmpty_insertIfNew! [TransOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew! k v).isEmpty = false := by
+  simp_to_model [insertIfNew!] using List.isEmpty_insertEntryIfNew
+
+end Std.DTreeMap.Internal.Impl

src/Std/Data/DTreeMap/Lemmas.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Paul Reichert
+-/
+prelude
+import Std.Data.DTreeMap.Internal.Lemmas
+import Std.Data.DTreeMap.Basic
+
+/-!
+# Dependent tree map lemmas
+
+This file contains lemmas about `Std.Data.DTreeMap`. Most of the lemmas require
+`TransCmp cmp` for the comparison function `cmp`.
+-/
+
+open Std.DTreeMap.Internal
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+universe u v
+
+namespace Std.DTreeMap
+
+variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp}
+
+@[simp]
+theorem isEmpty_emptyc : (∅ : DTreeMap α β cmp).isEmpty :=
+  Impl.isEmpty_empty
+
+@[simp]
+theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β k} :
+    (t.insert k v).isEmpty = false :=
+  Impl.isEmpty_insert t.wf
+
+theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
+  Impl.mem_iff_contains
+
+theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
+    t.contains k = t.contains k' :=
+  Impl.contains_congr t.wf hab
+
+theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
+  Impl.mem_congr t.wf hab
+
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β k} :
+    (t.insertIfNew k v).isEmpty = false :=
+  Impl.isEmpty_insertIfNew t.wf
+
+end Std.DTreeMap

src/Std/Data/DTreeMap/RawLemmas.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Paul Reichert
+-/
+prelude
+import Std.Data.DTreeMap.Internal.Lemmas
+import Std.Data.DTreeMap.Raw
+
+/-!
+# Dependent tree map lemmas
+
+This file contains lemmas about `Std.Data.DTreeMap.Raw`. Most of the lemmas require
+`TransCmp cmp` for the comparison function `cmp`.
+-/
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+open Std.DTreeMap.Internal
+
+universe u v
+
+namespace Std.DTreeMap.Raw
+
+variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap.Raw α β cmp}
+
+@[simp]
+theorem isEmpty_emptyc : (∅ : DTreeMap.Raw α β cmp).isEmpty :=
+  Impl.isEmpty_empty
+
+@[simp]
+theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v).isEmpty = false :=
+  Impl.isEmpty_insert! h
+
+theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
+  Impl.mem_iff_contains
+
+theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) :
+    t.contains k = t.contains k' :=
+  Impl.contains_congr h hab
+
+theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
+  Impl.mem_congr h hab
+
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v).isEmpty = false :=
+  Impl.isEmpty_insertIfNew! h
+
+end Std.DTreeMap.Raw

src/Std/Data/HashSet/RawLemmas.lean

@@ -133,7 +133,7 @@ theorem contains_of_contains_insert' [EquivBEq α] [LawfulHashable α] (h : m.WF
   HashMap.Raw.contains_of_contains_insertIfNew' h.out
 
 /-- This is a restatement of `mem_insert` that is written to exactly match the proof obligation
-in the statement of `get_insertIfNew`. -/
+in the statement of `get_insert`. -/
 theorem mem_of_mem_insert' [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     a ∈ m.insert k → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
   HashMap.Raw.mem_of_mem_insertIfNew' h.out

src/Std/Data/TreeMap/Lemmas.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Paul Reichert
+-/
+prelude
+import Std.Data.DTreeMap.Lemmas
+import Std.Data.TreeMap.Basic
+
+/-!
+# Tree map lemmas
+
+This file contains lemmas about `Std.Data.TreeMap`. Most of the lemmas require
+`TransCmp cmp` for the comparison function `cmp`.
+-/
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+universe u v
+
+namespace Std.TreeMap
+
+variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap α β cmp}
+
+@[simp]
+theorem isEmpty_emptyc : (∅ : TreeMap α β cmp).isEmpty :=
+  DTreeMap.isEmpty_emptyc
+
+@[simp]
+theorem isEmpty_insert [TransCmp cmp] {k : α} {v : β} :
+    (t.insert k v).isEmpty = false :=
+  DTreeMap.isEmpty_insert
+
+theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
+  DTreeMap.mem_iff_contains
+
+theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
+    t.contains k = t.contains k' :=
+  DTreeMap.contains_congr hab
+
+theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
+  DTreeMap.mem_congr hab
+
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] {k : α} {v : β} :
+    (t.insertIfNew k v).isEmpty = false :=
+  DTreeMap.isEmpty_insertIfNew
+
+end Std.TreeMap

src/Std/Data/TreeMap/RawLemmas.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Paul Reichert
+-/
+prelude
+import Std.Data.DTreeMap.RawLemmas
+import Std.Data.TreeMap.Raw
+
+/-!
+# Tree map lemmas
+
+This file contains lemmas about `Std.Data.TreeMap.Raw`. Most of the lemmas require
+`TransCmp cmp` for the comparison function `cmp`.
+-/
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+universe u v
+
+namespace Std.TreeMap.Raw
+
+variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeMap.Raw α β cmp}
+
+@[simp]
+theorem isEmpty_emptyc : (∅ : TreeMap.Raw α β cmp).isEmpty :=
+  DTreeMap.Raw.isEmpty_emptyc
+
+@[simp]
+theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insert k v).isEmpty = false :=
+  DTreeMap.Raw.isEmpty_insert h
+
+theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
+  DTreeMap.Raw.mem_iff_contains
+
+theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) :
+    t.contains k = t.contains k' :=
+  DTreeMap.Raw.contains_congr h hab
+
+theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
+  DTreeMap.Raw.mem_congr h hab
+
+@[simp]
+theorem isEmpty_insertIfNew [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insertIfNew k v).isEmpty = false :=
+  DTreeMap.Raw.isEmpty_insertIfNew h
+
+end Std.TreeMap.Raw

src/Std/Data/TreeSet/Lemmas.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Paul Reichert
+-/
+prelude
+import Std.Data.TreeMap.Lemmas
+import Std.Data.TreeSet.Basic
+
+/-!
+# Tree set lemmas
+
+This file contains lemmas about `Std.Data.TreeSet`. Most of the lemmas require
+`TransCmp cmp` for the comparison function `cmp`.
+-/
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+universe u v
+
+namespace Std.TreeSet
+
+variable {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp}
+
+@[simp]
+theorem isEmpty_emptyc : (∅ : TreeSet α cmp).isEmpty :=
+  TreeMap.isEmpty_emptyc
+
+@[simp]
+theorem isEmpty_insert [TransCmp cmp] {k : α} :
+    (t.insert k).isEmpty = false :=
+  TreeMap.isEmpty_insertIfNew
+
+theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
+  TreeMap.mem_iff_contains
+
+theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
+    t.contains k = t.contains k' :=
+  TreeMap.contains_congr hab
+
+theorem mem_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
+  TreeMap.mem_congr hab
+
+end Std.TreeSet

src/Std/Data/TreeSet/RawLemmas.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Paul Reichert
+-/
+prelude
+import Std.Data.TreeMap.RawLemmas
+import Std.Data.TreeSet.Raw
+
+/-!
+# Tree set lemmas
+
+This file contains lemmas about `Std.Data.TreeSet.Raw`. Most of the lemmas require
+`TransCmp cmp` for the comparison function `cmp`.
+-/
+
+set_option linter.missingDocs true
+set_option autoImplicit false
+
+universe u v
+
+namespace Std.TreeSet.Raw
+
+variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : TreeSet.Raw α cmp}
+
+@[simp]
+theorem isEmpty_emptyc : (∅ : Raw α cmp).isEmpty :=
+  TreeMap.Raw.isEmpty_emptyc
+
+@[simp]
+theorem isEmpty_insert [TransCmp cmp] (h : t.WF) {k : α} :
+    (t.insert k).isEmpty = false :=
+  TreeMap.Raw.isEmpty_insertIfNew h
+
+theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k :=
+  TreeMap.Raw.mem_iff_contains
+
+theorem contains_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) :
+    t.contains k = t.contains k' :=
+  TreeMap.Raw.contains_congr h hab
+
+theorem mem_congr [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = .eq) : k ∈ t ↔ k' ∈ t :=
+  TreeMap.Raw.mem_congr h hab
+
+end Std.TreeSet.Raw