From 5d7cf08260f125b40f8324b46555ffe45f8c5bf3 Mon Sep 17 00:00:00 2001
From: Paul Reichert <datokrat@users.noreply.github.com>
Date: Mon, 17 Feb 2025 09:44:52 +0100
Subject: [PATCH] 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 | 115 +++++++++++++++++++++
 src/Std/Data/DTreeMap/Lemmas.lean          |  52 ++++++++++
 src/Std/Data/DTreeMap/RawLemmas.lean       |  52 ++++++++++
 src/Std/Data/HashSet/RawLemmas.lean        |   2 +-
 src/Std/Data/TreeMap/Lemmas.lean           |  50 +++++++++
 src/Std/Data/TreeMap/RawLemmas.lean        |  50 +++++++++
 src/Std/Data/TreeSet/Lemmas.lean           |  45 ++++++++
 src/Std/Data/TreeSet/RawLemmas.lean        |  45 ++++++++
 8 files changed, 410 insertions(+), 1 deletion(-)
 create mode 100644 src/Std/Data/DTreeMap/Internal/Lemmas.lean
 create mode 100644 src/Std/Data/DTreeMap/Lemmas.lean
 create mode 100644 src/Std/Data/DTreeMap/RawLemmas.lean
 create mode 100644 src/Std/Data/TreeMap/Lemmas.lean
 create mode 100644 src/Std/Data/TreeMap/RawLemmas.lean
 create mode 100644 src/Std/Data/TreeSet/Lemmas.lean
 create mode 100644 src/Std/Data/TreeSet/RawLemmas.lean

diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
new file mode 100644
index 0000000000..9c3b376c57
--- /dev/null
+++ b/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
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
new file mode 100644
index 0000000000..3fa06679cc
--- /dev/null
+++ b/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
diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean
new file mode 100644
index 0000000000..ec860a1fb5
--- /dev/null
+++ b/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
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index 344cd8e266..a32e4d3ef4 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/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
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
new file mode 100644
index 0000000000..5c44e12f00
--- /dev/null
+++ b/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
diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean
new file mode 100644
index 0000000000..c14cfb766d
--- /dev/null
+++ b/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
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
new file mode 100644
index 0000000000..2294b92d6c
--- /dev/null
+++ b/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
diff --git a/src/Std/Data/TreeSet/RawLemmas.lean b/src/Std/Data/TreeSet/RawLemmas.lean
new file mode 100644
index 0000000000..2184fd8a5c
--- /dev/null
+++ b/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