From f2c939c3986ee3a6480b3811588a11ee008ab3b2 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 17 Aug 2024 00:50:34 +0200 Subject: [PATCH] feat: RBMap lemmas (#739) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: François G. Dorais --- Batteries/Data/RBMap/Lemmas.lean | 123 +++++++++++++++++++++++++++++++ 1 file changed, 123 insertions(+) diff --git a/Batteries/Data/RBMap/Lemmas.lean b/Batteries/Data/RBMap/Lemmas.lean index 5577b3a1a7..43d31af8f7 100644 --- a/Batteries/Data/RBMap/Lemmas.lean +++ b/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