feat: equivalence of tree maps (leanprover#8210)

This PR adds an equivalence relation to tree maps akin to the existing
one for hash maps. In order to get many congruence lemmas to eventually
use for defining functions on extensional tree maps, almost all of the
remaining tree map functions have also been given lemmas to relate them
to list functions, although these aren't currently used to prove lemmas
other than congruence lemmas.

Author: Rob23oba

src/Init/Data/Array/Lemmas.lean

@@ -3621,8 +3621,8 @@ We can prove that two folds over the same array are related (by some arbitrary r
 if we know that the initial elements are related and the folding function, for each element of the array,
 preserves the relation.
 -/
-theorem foldl_rel {xs : Array α} {f g : β → α → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
+theorem foldl_rel {xs : Array α} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) :
     r (xs.foldl (fun acc a => f acc a) a) (xs.foldl (fun acc a => g acc a) b) := by
   rcases xs with ⟨xs⟩
   simpa using List.foldl_rel h (by simpa using h')
@@ -3632,8 +3632,8 @@ We can prove that two folds over the same array are related (by some arbitrary r
 if we know that the initial elements are related and the folding function, for each element of the array,
 preserves the relation.
 -/
-theorem foldr_rel {xs : Array α} {f g : α → β → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
+theorem foldr_rel {xs : Array α} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) :
     r (xs.foldr (fun a acc => f a acc) a) (xs.foldr (fun a acc => g a acc) b) := by
   rcases xs with ⟨xs⟩
   simpa using List.foldr_rel h (by simpa using h')

src/Init/Data/List/Lemmas.lean

@@ -2778,8 +2778,8 @@ We can prove that two folds over the same list are related (by some arbitrary re
 if we know that the initial elements are related and the folding function, for each element of the list,
 preserves the relation.
 -/
-theorem foldl_rel {l : List α} {f g : β → α → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
+theorem foldl_rel {l : List α} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) :
     r (l.foldl (fun acc a => f acc a) a) (l.foldl (fun acc a => g acc a) b) := by
   induction l generalizing a b with
   | nil => simp_all
@@ -2794,8 +2794,8 @@ We can prove that two folds over the same list are related (by some arbitrary re
 if we know that the initial elements are related and the folding function, for each element of the list,
 preserves the relation.
 -/
-theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
+theorem foldr_rel {l : List α} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ l → ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) :
     r (l.foldr (fun a acc => f a acc) a) (l.foldr (fun a acc => g a acc) b) := by
   induction l generalizing a b with
   | nil => simp_all

src/Init/Data/Vector/Lemmas.lean

@@ -2538,23 +2538,23 @@ theorem foldr_hom (f : β₁ → β₂) {g₁ : α → β₁ → β₁} {g₂ :
   rw [Array.foldr_hom _ H]
 
 /--
-We can prove that two folds over the same array are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the array,
-preserves the relation.
+We can prove that two folds over the same vector are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the
+vector, preserves the relation.
 -/
-theorem foldl_rel {xs : Vector α n} {f g : β → α → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f c a) (g c' a)) :
+theorem foldl_rel {xs : Vector α n} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) :
     r (xs.foldl (fun acc a => f acc a) a) (xs.foldl (fun acc a => g acc a) b) := by
   rcases xs with ⟨xs, rfl⟩
   simpa using Array.foldl_rel h (by simpa using h')
 
 /--
-We can prove that two folds over the same array are related (by some arbitrary relation)
-if we know that the initial elements are related and the folding function, for each element of the array,
-preserves the relation.
+We can prove that two folds over the same vector are related (by some arbitrary relation)
+if we know that the initial elements are related and the folding function, for each element of the
+vector, preserves the relation.
 -/
-theorem foldr_rel {xs : Vector α n} {f g : α → β → β} {a b : β} {r : β → β → Prop}
-    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c c' : β), r c c' → r (f a c) (g a c')) :
+theorem foldr_rel {xs : Vector α n} {f : α → β → β} {g : α → γ → γ} {a : β} {b : γ} {r : β → γ → Prop}
+    (h : r a b) (h' : ∀ (a : α), a ∈ xs → ∀ (c : β) (c' : γ), r c c' → r (f a c) (g a c')) :
     r (xs.foldr (fun a acc => f a acc) a) (xs.foldr (fun a acc => g a acc) b) := by
   rcases xs with ⟨xs, rfl⟩
   simpa using Array.foldr_rel h (by simpa using h')

src/Std/Data/DTreeMap/AdditionalOperations.lean

@@ -66,7 +66,7 @@ def getEntryLE [TransCmp cmp] (t : DTreeMap α β cmp) (k : α) (h : ∃ a ∈ t
   letI : Ord α := ⟨cmp⟩; Impl.getEntryLE k t.inner t.wf.ordered h
 
 /--
-Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
+Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
 less than the given key.
 -/
 @[inline]
@@ -99,7 +99,7 @@ def getKeyLE [TransCmp cmp] (t : DTreeMap α β cmp) (k : α) (h : ∃ a ∈ t,
   letI : Ord α := ⟨cmp⟩; Impl.getKeyLE k t.inner t.wf.ordered h
 
 /--
-Given a proof that such a mapping exists, retrieves the smallest key that is
+Given a proof that such a mapping exists, retrieves the largest key that is
 less than the given key.
 -/
 @[inline]
@@ -138,7 +138,7 @@ def getEntryLE [TransCmp cmp] (t : DTreeMap α β cmp) (k : α) (h : ∃ a ∈ t
   letI : Ord α := ⟨cmp⟩; Impl.Const.getEntryLE k t.inner t.wf.ordered h
 
 /--
-Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
+Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
 less than the given key.
 -/
 @[inline]

src/Std/Data/DTreeMap/Basic.lean

@@ -83,6 +83,13 @@ instance : EmptyCollection (DTreeMap α β cmp) where
 instance : Inhabited (DTreeMap α β cmp) where
   default := ∅
 
+@[inherit_doc Impl.Equiv]
+structure Equiv (m₁ m₂ : DTreeMap α β cmp) where
+  /-- Internal implementation detail of the tree map -/
+  inner : m₁.1.Equiv m₂.1
+
+@[inherit_doc] scoped infix:50 " ~m " => Equiv
+
 @[simp]
 theorem empty_eq_emptyc : (empty : DTreeMap α β cmp) = ∅ :=
   rfl
@@ -500,7 +507,7 @@ def getEntryLE? (t : DTreeMap α β cmp) (k : α) : Option ((a : α) × β a) :=
   letI : Ord α := ⟨cmp⟩; Impl.getEntryLE? k t.inner
 
 /--
-Tries to retrieve the key-value pair with the smallest key that is less than the given key,
+Tries to retrieve the key-value pair with the largest key that is less than the given key,
 returning `none` if no such pair exists.
 -/
 @[inline]
@@ -537,7 +544,7 @@ def getEntryLE! [Inhabited (Sigma β)] (t : DTreeMap α β cmp) (k : α) : (a :
   letI : Ord α := ⟨cmp⟩; Impl.getEntryLE! k t.inner
 
 /--
-Tries to retrieve the key-value pair with the smallest key that is less than the given key,
+Tries to retrieve the key-value pair with the largest key that is less than the given key,
 panicking if no such pair exists.
 -/
 @[inline]
@@ -569,7 +576,7 @@ def getEntryLED (t : DTreeMap α β cmp) (k : α) (fallback : Sigma β) : (a : 
   letI : Ord α := ⟨cmp⟩; Impl.getEntryLED k t.inner fallback
 
 /--
-Tries to retrieve the key-value pair with the smallest key that is less than the given key,
+Tries to retrieve the key-value pair with the largest key that is less than the given key,
 returning `fallback` if no such pair exists.
 -/
 @[inline]
@@ -601,7 +608,7 @@ def getKeyLE? (t : DTreeMap α β cmp) (k : α) : Option α :=
   letI : Ord α := ⟨cmp⟩; t.inner.getKeyLE? k
 
 /--
-Tries to retrieve the smallest key that is less than the given key,
+Tries to retrieve the largest key that is less than the given key,
 returning `none` if no such key exists.
 -/
 @[inline]
@@ -638,7 +645,7 @@ def getKeyLE! [Inhabited α] (t : DTreeMap α β cmp) (k : α) : α :=
   letI : Ord α := ⟨cmp⟩; Impl.getKeyLE! k t.inner
 
 /--
-Tries to retrieve the smallest key that is less than the given key,
+Tries to retrieve the largest key that is less than the given key,
 panicking if no such key exists.
 -/
 @[inline]
@@ -670,7 +677,7 @@ def getKeyLED (t : DTreeMap α β cmp) (k : α) (fallback : α) : α :=
   letI : Ord α := ⟨cmp⟩; Impl.getKeyLED k t.inner fallback
 
 /--
-Tries to retrieve the smallest key that is less than the given key,
+Tries to retrieve the largest key that is less than the given key,
 returning `fallback` if no such key exists.
 -/
 @[inline]