feat: RBMap lemmas (#739)

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Batteries/Data/RBMap/Lemmas.lean

@@ -1103,3 +1103,126 @@ theorem lowerBound?_lt {t : RBSet α cmp} [TransCmp cmp]
   lowerBoundP?_lt H hz
 
 end RBSet
+
+namespace RBMap
+
+-- @[simp] -- FIXME: RBSet.val_toList already triggers here, seems bad?
+theorem val_toList {t : RBMap α β cmp} : t.1.toList = t.toList := rfl
+
+@[simp] theorem mkRBSet_eq : mkRBMap α β cmp = ∅ := rfl
+@[simp] theorem empty_eq : @RBMap.empty α β cmp = ∅ := rfl
+@[simp] theorem default_eq : (default : RBMap α β cmp) = ∅ := rfl
+@[simp] theorem empty_toList : toList (∅ : RBMap α β cmp) = [] := rfl
+@[simp] theorem single_toList : toList (single a b : RBMap α β cmp) = [(a, b)] := rfl
+
+theorem mem_toList {t : RBMap α β cmp} : x ∈ toList t ↔ x ∈ t.1 := RBNode.mem_toList
+
+theorem foldl_eq_foldl_toList {t : RBMap α β cmp} :
+    t.foldl f init = t.toList.foldl (fun r p => f r p.1 p.2) init :=
+  RBNode.foldl_eq_foldl_toList
+
+theorem foldr_eq_foldr_toList {t : RBMap α β cmp} :
+    t.foldr f init = t.toList.foldr (fun p r => f p.1 p.2 r) init :=
+  RBNode.foldr_eq_foldr_toList
+
+theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {t : RBMap α β cmp} :
+    t.foldlM (m := m) f init = t.toList.foldlM (fun r p => f r p.1 p.2) init :=
+  RBNode.foldlM_eq_foldlM_toList
+
+theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {t : RBMap α β cmp} :
+    t.forM (m := m) f = t.toList.forM (fun p => f p.1 p.2) :=
+  RBNode.forM_eq_forM_toList
+
+theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] {t : RBMap α β cmp} :
+    forIn (m := m) t init f = forIn t.toList init f := RBNode.forIn_eq_forIn_toList
+
+theorem toStream_eq {t : RBMap α β cmp} : toStream t = t.1.toStream .nil := rfl
+
+@[simp] theorem toStream_toList {t : RBMap α β cmp} : (toStream t).toList = t.toList :=
+  RBSet.toStream_toList
+
+theorem toList_sorted {t : RBMap α β cmp} : t.toList.Pairwise (RBNode.cmpLT (cmp ·.1 ·.1)) :=
+  RBSet.toList_sorted
+
+theorem findEntry?_some_eq_eq {t : RBMap α β cmp} : t.findEntry? x = some (y, v) → cmp x y = .eq :=
+  RBSet.findP?_some_eq_eq
+
+theorem findEntry?_some_mem_toList {t : RBMap α β cmp} (h : t.findEntry? x = some y) :
+    y ∈ toList t := RBSet.findP?_some_mem_toList h
+
+theorem find?_some_mem_toList {t : RBMap α β cmp} (h : t.find? x = some v) :
+    ∃ y, (y, v) ∈ toList t ∧ cmp x y = .eq := by
+  obtain ⟨⟨y, v⟩, h', rfl⟩ := Option.map_eq_some'.1 h
+  exact ⟨_, findEntry?_some_mem_toList h', findEntry?_some_eq_eq h'⟩
+
+theorem mem_toList_unique [@TransCmp α cmp] {t : RBMap α β cmp}
+    (hx : x ∈ toList t) (hy : y ∈ toList t) (e : cmp x.1 y.1 = .eq) : x = y :=
+  RBSet.mem_toList_unique hx hy e
+
+/-- A "representable cut" is one generated by `cmp a` for some `a`. This is always a valid cut. -/
+instance (cmp) (a : α) : IsStrictCut cmp (cmp a) where
+  le_lt_trans h₁ h₂ := TransCmp.lt_le_trans h₂ h₁
+  le_gt_trans h₁ := Decidable.not_imp_not.1 (TransCmp.le_trans · h₁)
+  exact h := (TransCmp.cmp_congr_left h).symm
+
+instance (f : α → β) (cmp) [@TransCmp β cmp] (x : β) :
+    IsStrictCut (Ordering.byKey f cmp) (fun y => cmp x (f y)) where
+  le_lt_trans h₁ h₂ := TransCmp.lt_le_trans h₂ h₁
+  le_gt_trans h₁ := Decidable.not_imp_not.1 (TransCmp.le_trans · h₁)
+  exact h := (TransCmp.cmp_congr_left h).symm
+
+theorem findEntry?_some [@TransCmp α cmp] {t : RBMap α β cmp} :
+    t.findEntry? x = some y ↔ y ∈ toList t ∧ cmp x y.1 = .eq := RBSet.findP?_some
+
+theorem find?_some [@TransCmp α cmp] {t : RBMap α β cmp} :
+    t.find? x = some v ↔ ∃ y, (y, v) ∈ toList t ∧ cmp x y = .eq := by
+  simp only [find?, findEntry?_some, Option.map_eq_some']; constructor
+  · rintro ⟨_, h, rfl⟩; exact ⟨_, h⟩
+  · rintro ⟨b, h⟩; exact ⟨_, h, rfl⟩
+
+theorem contains_iff_findEntry? {t : RBMap α β cmp} :
+    t.contains x ↔ ∃ v, t.findEntry? x = some v := Option.isSome_iff_exists
+
+theorem contains_iff_find? {t : RBMap α β cmp} :
+    t.contains x ↔ ∃ v, t.find? x = some v := by
+  simp [contains_iff_findEntry?, find?, and_comm, exists_comm]
+
+theorem size_eq (t : RBMap α β cmp) : t.size = t.toList.length := RBNode.size_eq
+
+theorem mem_toList_insert_self (v) (t : RBMap α β cmp) : (k, v) ∈ toList (t.insert k v) :=
+  RBSet.mem_toList_insert_self ..
+
+theorem mem_toList_insert_of_mem (v) {t : RBMap α β cmp} (h : y ∈ toList t) :
+    y ∈ toList (t.insert k v) ∨ cmp k y.1 = .eq := RBSet.mem_toList_insert_of_mem _ h
+
+theorem mem_toList_insert [@TransCmp α cmp] {t : RBMap α β cmp} :
+    y ∈ toList (t.insert k v) ↔ (y ∈ toList t ∧ t.findEntry? k ≠ some y) ∨ y = (k, v) :=
+  RBSet.mem_toList_insert
+
+theorem findEntry?_congr [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k₁ k₂ = .eq) :
+    t.findEntry? k₁ = t.findEntry? k₂ := by simp [findEntry?, TransCmp.cmp_congr_left' h]
+
+theorem find?_congr [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k₁ k₂ = .eq) :
+    t.find? k₁ = t.find? k₂ := by simp [find?, findEntry?_congr _ h]
+
+theorem findEntry?_insert_of_eq [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k' k = .eq) :
+    (t.insert k v).findEntry? k' = some (k, v) := RBSet.findP?_insert_of_eq _ h
+
+theorem find?_insert_of_eq [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k' k = .eq) :
+    (t.insert k v).find? k' = some v := by rw [find?, findEntry?_insert_of_eq _ h]; rfl
+
+theorem findEntry?_insert_of_ne [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k' k ≠ .eq) :
+    (t.insert k v).findEntry? k' = t.findEntry? k' := RBSet.findP?_insert_of_ne _ h
+
+theorem find?_insert_of_ne [@TransCmp α cmp] (t : RBMap α β cmp) (h : cmp k' k ≠ .eq) :
+    (t.insert k v).find? k' = t.find? k' := by simp [find?, findEntry?_insert_of_ne _ h]
+
+theorem findEntry?_insert [@TransCmp α cmp] (t : RBMap α β cmp) (k v k') :
+    (t.insert k v).findEntry? k' = if cmp k' k = .eq then some (k, v) else t.findEntry? k' :=
+  RBSet.findP?_insert ..
+
+theorem find?_insert [@TransCmp α cmp] (t : RBMap α β cmp) (k v k') :
+    (t.insert k v).find? k' = if cmp k' k = .eq then some v else t.find? k' := by
+  split <;> [exact find?_insert_of_eq t ‹_›; exact find?_insert_of_ne t ‹_›]
+
+end RBMap