From 8bca9d4477edfb30e2e7ed99aac579b75b5bd0dc Mon Sep 17 00:00:00 2001
From: subfish-zhou <subfishzhou@gmail.com>
Date: Thu, 13 Aug 2026 22:25:11 +0000
Subject: [PATCH] docs: translate the official grind index map tutorial

---
 .../files/grind-index-map/IndexMap.lean       | 397 ++++++++
 .../grind-index-map/LICENSE-Apache-2.0.txt    |  70 ++
 docs/assets/files/grind-index-map/README.txt  |  12 +
 .../grind-index-map-4.34.0-rc1.zip            | Bin 0 -> 3709 bytes
 .../files/grind-index-map/lakefile.toml       |   5 +
 .../files/grind-index-map/lean-toolchain      |   1 +
 docs/projects/grind-index-map.md              | 901 ++++++++++++++++++
 mkdocs.yml                                    |   1 +
 8 files changed, 1387 insertions(+)
 create mode 100644 docs/assets/files/grind-index-map/IndexMap.lean
 create mode 100644 docs/assets/files/grind-index-map/LICENSE-Apache-2.0.txt
 create mode 100644 docs/assets/files/grind-index-map/README.txt
 create mode 100644 docs/assets/files/grind-index-map/grind-index-map-4.34.0-rc1.zip
 create mode 100644 docs/assets/files/grind-index-map/lakefile.toml
 create mode 100644 docs/assets/files/grind-index-map/lean-toolchain
 create mode 100644 docs/projects/grind-index-map.md

diff --git a/docs/assets/files/grind-index-map/IndexMap.lean b/docs/assets/files/grind-index-map/IndexMap.lean
new file mode 100644
index 0000000..2f83662
--- /dev/null
+++ b/docs/assets/files/grind-index-map/IndexMap.lean
@@ -0,0 +1,397 @@
+import Std.Data.HashMap
+
+open Std
+
+structure IndexMap
+    (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+  private indices : HashMap α Nat
+  private keys : Array α
+  private values : Array β
+  private size_keys' : keys.size = values.size := by grind
+  private WF : ∀ (i : Nat) (a : α),
+    keys[i]? = some a ↔ indices[a]? = some i := by grind
+
+namespace IndexMap
+
+variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
+variable {m : IndexMap α β} {a : α} {b : β} {i : Nat}
+
+@[inline] def size (m : IndexMap α β) : Nat :=
+  m.values.size
+
+@[local grind =] private theorem size_keys : m.keys.size = m.size :=
+  m.size_keys'
+
+@[local grind =] private theorem size_values : m.values.size = m.size := rfl
+
+def emptyWithCapacity (capacity := 8) : IndexMap α β where
+  indices := HashMap.emptyWithCapacity capacity
+  keys := Array.emptyWithCapacity capacity
+  values := Array.emptyWithCapacity capacity
+
+@[inline] def contains (m : IndexMap α β)
+    (a : α) : Bool :=
+  m.indices.contains a
+
+instance : Membership α (IndexMap α β) where
+  mem m a := a ∈ m.indices
+
+instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) :=
+  inferInstanceAs (Decidable (a ∈ m.indices))
+
+-- theorem getElem_indices_lt (m : IndexMap α β) (a : α) (h : a ∈ m) :
+--     m.indices[a] < m.size := by
+--   grind
+
+@[local grind _=_] private theorem mem_indices
+    {m : IndexMap α β} {a : α} :
+    a ∈ m.indices ↔ a ∈ m := Iff.rfl
+
+variable [LawfulBEq α] [LawfulHashable α]
+
+attribute [local grind _=_] IndexMap.WF
+
+private theorem getElem_indices_lt {h : a ∈ m} : m.indices[a] < m.size := by
+  have : m.indices[a]? = some m.indices[a] := by grind
+  grind
+
+attribute [local grind] getElem_indices_lt
+
+grind_pattern getElem_indices_lt => m.indices[a]
+
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
+
+attribute [local grind] size
+
+instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem m a h :=
+    m.values[m.indices[a]]
+  getElem? m a :=
+    m.indices[a]?.bind (fun i => (m.values[i]?))
+  getElem! m a :=
+    m.indices[a]?.bind (fun i => (m.values[i]?)) |>.getD default
+
+@[local grind =] private theorem getElem_def
+    (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m[a] = m.values[m.indices[a]'h] :=
+  rfl
+@[local grind =] private theorem getElem?_def
+    (m : IndexMap α β) (a : α) :
+    m[a]? = m.indices[a]?.bind (fun i => (m.values[i]?)) :=
+  rfl
+@[local grind =] private theorem getElem!_def
+    [Inhabited β] (m : IndexMap α β) (a : α) :
+    m[a]! = (m.indices[a]?.bind (m.values[·]?)).getD default :=
+  rfl
+
+instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem?_def := by grind
+  getElem!_def := by grind
+
+@[inline] def insert (m : IndexMap α β) (a : α) (b : β) : IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    { indices := m.indices
+      keys    := m.keys.set i a
+      values  := m.values.set i b }
+  | none =>
+    { indices := m.indices.insert a m.size
+      keys    := m.keys.push a
+      values  := m.values.push b }
+
+-- @[inline] def eraseSwap (m : IndexMap α β) (a : α) : IndexMap α β :=
+--   match h : m.indices[a]? with
+--   | some i =>
+--     if w : i = m.size - 1 then
+--       { indices := m.indices.erase a
+--         keys := m.keys.pop
+--         values := m.values.pop }
+--     else
+--       let lastKey := m.keys.back
+--       let lastValue := m.values.back
+--       { indices := (m.indices.erase a).insert lastKey i
+--         keys := m.keys.pop.set i lastKey
+--         values := m.values.pop.set i lastValue }
+--   | none => m
+
+@[local grind .]
+private theorem WF' (i : Nat) (a : α) (h₁ : i < m.keys.size) (h₂ : a ∈ m) :
+    m.keys[i] = a ↔ m.indices[a] = i := by
+  have := m.WF i a
+  grind
+
+example {m : IndexMap α β} {a : α} {h : a ∈ m} :
+  m.keys[m.indices[a]'h] = a := by grind
+
+@[inline] def eraseSwap (m : IndexMap α β) (a : α) : IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    if w : i = m.size - 1 then
+      { indices := m.indices.erase a
+        keys := m.keys.pop
+        values := m.values.pop }
+    else
+      let lastKey := m.keys.back
+      let lastValue := m.values.back
+      { indices := (m.indices.erase a).insert lastKey i
+        keys := m.keys.pop.set i lastKey
+        values := m.values.pop.set i lastValue }
+  | none => m
+
+@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat :=
+  m.indices[a]?
+
+@[inline] def findIdx (m : IndexMap α β) (a : α)
+    (h : a ∈ m := by get_elem_tactic) : Nat :=
+  m.indices[a]
+
+@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β :=
+  m.values[i]?
+
+@[inline] def getIdx (m : IndexMap α β) (i : Nat)
+    (h : i < m.size := by get_elem_tactic) : β :=
+  m.values[i]
+
+/-! ### Verification theorems (not exhaustive) -/
+
+@[grind =]
+theorem mem_insert (m : IndexMap α β) (a a' : α) (b : β) :
+    a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
+  grind +locals
+
+@[grind =]
+theorem getElem_insert (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
+    (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
+  grind +locals
+
+theorem findIdx_lt (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m.findIdx a h < m.size := by
+  grind +locals
+
+grind_pattern findIdx_lt => m.findIdx a h
+
+@[grind =]
+theorem findIdx_insert_self (m : IndexMap α β) (a : α) (b : β) :
+    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
+  grind +locals
+
+@[grind =]
+theorem findIdx?_eq (m : IndexMap α β) (a : α) :
+    m.findIdx? a = if h : a ∈ m then some (m.findIdx a h) else none := by
+  grind +locals
+
+@[grind =]
+theorem getIdx_findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m.getIdx (m.findIdx a) = m[a] := by grind +locals
+
+omit [LawfulBEq α] [LawfulHashable α] in
+@[grind =]
+theorem getIdx?_eq (m : IndexMap α β) (i : Nat) :
+    m.getIdx? i = if h : i < m.size then some (m.getIdx i h) else none := by
+  grind +locals
+
+private theorem getElem_keys_mem {m : IndexMap α β} {i : Nat} (h : i < m.size) :
+    m.keys[i] ∈ m := by
+  have : m.indices[m.keys[i]]? = some i := by grind
+  grind
+
+local grind_pattern getElem_keys_mem => m.keys[i]
+
+theorem getElem?_eraseSwap (m : IndexMap α β) (a a' : α) :
+    (m.eraseSwap a)[a']? = if a' == a then none else m[a']? := by
+  grind +locals
+
+@[grind =]
+theorem mem_eraseSwap (m : IndexMap α β) (a a' : α) :
+    a' ∈ m.eraseSwap a ↔ a' ≠ a ∧ a' ∈ m := by
+  grind +locals
+
+theorem getElem_eraseSwap (m : IndexMap α β) (a a' : α) (h : a' ∈ m.eraseSwap a) :
+    (m.eraseSwap a)[a'] = m[a'] := by
+  grind +locals
+
+local macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
+
+open Std
+
+structure IndexMap
+    (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+  private indices : HashMap α Nat
+  private keys : Array α
+  private values : Array β
+  private size_keys' : keys.size = values.size := by grind
+  private WF : ∀ (i : Nat) (a : α),
+    keys[i]? = some a ↔ indices[a]? = some i := by grind
+
+namespace IndexMap
+
+variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
+variable {m : IndexMap α β} {a : α} {b : β} {i : Nat}
+
+@[inline] def size (m : IndexMap α β) : Nat :=
+  m.values.size
+
+@[local grind =] private theorem size_keys : m.keys.size = m.size :=
+  m.size_keys'
+
+@[local grind =] private theorem size_values : m.values.size = m.size := rfl
+
+def emptyWithCapacity (capacity := 8) : IndexMap α β where
+  indices := HashMap.emptyWithCapacity capacity
+  keys := Array.emptyWithCapacity capacity
+  values := Array.emptyWithCapacity capacity
+
+instance : EmptyCollection (IndexMap α β) where
+  emptyCollection := emptyWithCapacity
+
+instance : Inhabited (IndexMap α β) where
+  default := ∅
+
+@[inline] def contains (m : IndexMap α β) (a : α) : Bool :=
+  m.indices.contains a
+
+instance : Membership α (IndexMap α β) where
+  mem m a := a ∈ m.indices
+
+instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) :=
+  inferInstanceAs (Decidable (a ∈ m.indices))
+
+@[local grind _=_] private theorem mem_indices
+    {m : IndexMap α β} {a : α} :
+    a ∈ m.indices ↔ a ∈ m := Iff.rfl
+
+@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat :=
+  m.indices[a]?
+
+@[inline] def findIdx (m : IndexMap α β) (a : α)
+    (h : a ∈ m := by get_elem_tactic) : Nat :=
+  m.indices[a]
+
+@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β :=
+  m.values[i]?
+
+@[inline] def getIdx (m : IndexMap α β) (i : Nat)
+    (h : i < m.size := by get_elem_tactic) : β :=
+  m.values[i]
+
+variable [LawfulBEq α] [LawfulHashable α]
+
+attribute [local grind _=_] IndexMap.WF
+
+private theorem getElem_indices_lt
+    {h : a ∈ m} : m.indices[a] < m.size := by
+  have : m.indices[a]? = some m.indices[a] := by grind
+  grind
+
+grind_pattern getElem_indices_lt => m.indices[a]
+
+instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem m a h :=
+    m.values[m.indices[a]]
+  getElem? m a :=
+    m.indices[a]?.bind (fun i => (m.values[i]?))
+  getElem! m a :=
+    m.indices[a]?.bind (fun i => (m.values[i]?)) |>.getD default
+
+@[local grind =] private theorem getElem_def
+    (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m[a] = m.values[m.indices[a]'h] :=
+  rfl
+@[local grind =] private theorem getElem?_def
+    (m : IndexMap α β) (a : α) :
+    m[a]? = m.indices[a]?.bind (fun i => (m.values[i]?)) :=
+  rfl
+@[local grind =] private theorem getElem!_def
+    [Inhabited β] (m : IndexMap α β) (a : α) :
+    m[a]! = (m.indices[a]?.bind (m.values[·]?)).getD default :=
+  rfl
+
+instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem?_def := by grind
+  getElem!_def := by grind
+
+@[inline] def insert (m : IndexMap α β) (a : α) (b : β) : IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    { indices := m.indices
+      keys    := m.keys.set i a
+      values  := m.values.set i b }
+  | none =>
+    { indices := m.indices.insert a m.size
+      keys    := m.keys.push a
+      values  := m.values.push b }
+
+instance : Singleton (α × β) (IndexMap α β) :=
+  ⟨fun ⟨a, b⟩ => (∅ : IndexMap α β).insert a b⟩
+
+instance : Insert (α × β) (IndexMap α β) :=
+  ⟨fun ⟨a, b⟩ s => s.insert a b⟩
+
+instance : LawfulSingleton (α × β) (IndexMap α β) :=
+  ⟨fun _ => rfl⟩
+
+@[local grind .]
+private theorem WF' (i : Nat) (a : α) (h₁ : i < m.keys.size) (h₂ : a ∈ m) :
+    m.keys[i] = a ↔ m.indices[a] = i := by
+  have := m.WF i a
+  grind
+
+/--
+Erase the key-value pair with the given key,
+moving the last pair into its place in the order.
+If the key is not present, the map is unchanged.
+-/
+@[inline] def eraseSwap (m : IndexMap α β) (a : α) : IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    if w : i = m.size - 1 then
+      { indices := m.indices.erase a
+        keys := m.keys.pop
+        values := m.values.pop }
+    else
+      let lastKey := m.keys.back
+      let lastValue := m.values.back
+      { indices := (m.indices.erase a).insert lastKey i
+        keys := m.keys.pop.set i lastKey
+        values := m.values.pop.set i lastValue }
+  | none => m
+
+/-! ### Verification theorems (not exhaustive) -/
+
+@[grind =]
+theorem mem_insert (m : IndexMap α β) (a a' : α) (b : β) :
+    a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
+  grind +locals
+
+@[grind =]
+theorem getElem_insert (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
+    (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
+  grind +locals
+
+theorem findIdx_lt (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m.findIdx a h < m.size := by
+  grind +locals
+
+grind_pattern findIdx_lt => m.findIdx a h
+
+@[grind =]
+theorem findIdx_insert_self (m : IndexMap α β) (a : α) (b : β) :
+    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
+  grind +locals
+
+@[grind =]
+theorem findIdx?_eq (m : IndexMap α β) (a : α) :
+    m.findIdx? a = if h : a ∈ m then some (m.findIdx a h) else none := by
+  grind +locals
+
+@[grind =]
+theorem getIdx_findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m.getIdx (m.findIdx a) = m[a] := by grind +locals
+
+omit [LawfulBEq α] [LawfulHashable α] in
+@[grind =]
+theorem getIdx?_eq (m : IndexMap α β) (i : Nat) :
+    m.getIdx? i = if h : i < m.size then some (m.getIdx i h) else none := by
+  grind +locals
+
+end IndexMap
diff --git a/docs/assets/files/grind-index-map/LICENSE-Apache-2.0.txt b/docs/assets/files/grind-index-map/LICENSE-Apache-2.0.txt
new file mode 100644
index 0000000..4c3f8ab
--- /dev/null
+++ b/docs/assets/files/grind-index-map/LICENSE-Apache-2.0.txt
@@ -0,0 +1,70 @@
+Apache License 2.0 (Apache)
+Apache License
+Version 2.0, January 2004
+http://www.apache.org/licenses/
+
+TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+1. Definitions.
+
+"License" shall mean the terms and conditions for use, reproduction, and distribution as defined by Sections 1 through 9 of this document.
+
+"Licensor" shall mean the copyright owner or entity authorized by the copyright owner that is granting the License.
+
+"Legal Entity" shall mean the union of the acting entity and all other entities that control, are controlled by, or are under common control with that entity. For the purposes of this definition, "control" means (i) the power, direct or indirect, to cause the direction or management of such entity, whether by contract or otherwise, or (ii) ownership of fifty percent (50%) or more of the outstanding shares, or (iii) beneficial ownership of such entity.
+
+"You" (or "Your") shall mean an individual or Legal Entity exercising permissions granted by this License.
+
+"Source" form shall mean the preferred form for making modifications, including but not limited to software source code, documentation source, and configuration files.
+
+"Object" form shall mean any form resulting from mechanical transformation or translation of a Source form, including but not limited to compiled object code, generated documentation, and conversions to other media types.
+
+"Work" shall mean the work of authorship, whether in Source or Object form, made available under the License, as indicated by a copyright notice that is included in or attached to the work (an example is provided in the Appendix below).
+
+"Derivative Works" shall mean any work, whether in Source or Object form, that is based on (or derived from) the Work and for which the editorial revisions, annotations, elaborations, or other modifications represent, as a whole, an original work of authorship. For the purposes of this License, Derivative Works shall not include works that remain separable from, or merely link (or bind by name) to the interfaces of, the Work and Derivative Works thereof.
+
+"Contribution" shall mean any work of authorship, including the original version of the Work and any modifications or additions to that Work or Derivative Works thereof, that is intentionally submitted to Licensor for inclusion in the Work by the copyright owner or by an individual or Legal Entity authorized to submit on behalf of the copyright owner. For the purposes of this definition, "submitted" means any form of electronic, verbal, or written communication sent to the Licensor or its representatives, including but not limited to communication on electronic mailing lists, source code control systems, and issue tracking systems that are managed by, or on behalf of, the Licensor for the purpose of discussing and improving the Work, but excluding communication that is conspicuously marked or otherwise designated in writing by the copyright owner as "Not a Contribution."
+
+"Contributor" shall mean Licensor and any individual or Legal Entity on behalf of whom a Contribution has been received by Licensor and subsequently incorporated within the Work.
+
+2. Grant of Copyright License.
+
+Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable copyright license to reproduce, prepare Derivative Works of, publicly display, publicly perform, sublicense, and distribute the Work and such Derivative Works in Source or Object form.
+
+3. Grant of Patent License.
+
+Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable (except as stated in this section) patent license to make, have made, use, offer to sell, sell, import, and otherwise transfer the Work, where such license applies only to those patent claims licensable by such Contributor that are necessarily infringed by their Contribution(s) alone or by combination of their Contribution(s) with the Work to which such Contribution(s) was submitted. If You institute patent litigation against any entity (including a cross-claim or counterclaim in a lawsuit) alleging that the Work or a Contribution incorporated within the Work constitutes direct or contributory patent infringement, then any patent licenses granted to You under this License for that Work shall terminate as of the date such litigation is filed.
+
+4. Redistribution.
+
+You may reproduce and distribute copies of the Work or Derivative Works thereof in any medium, with or without modifications, and in Source or Object form, provided that You meet the following conditions:
+
+1. You must give any other recipients of the Work or Derivative Works a copy of this License; and
+
+2. You must cause any modified files to carry prominent notices stating that You changed the files; and
+
+3. You must retain, in the Source form of any Derivative Works that You distribute, all copyright, patent, trademark, and attribution notices from the Source form of the Work, excluding those notices that do not pertain to any part of the Derivative Works; and
+
+4. If the Work includes a "NOTICE" text file as part of its distribution, then any Derivative Works that You distribute must include a readable copy of the attribution notices contained within such NOTICE file, excluding those notices that do not pertain to any part of the Derivative Works, in at least one of the following places: within a NOTICE text file distributed as part of the Derivative Works; within the Source form or documentation, if provided along with the Derivative Works; or, within a display generated by the Derivative Works, if and wherever such third-party notices normally appear. The contents of the NOTICE file are for informational purposes only and do not modify the License. You may add Your own attribution notices within Derivative Works that You distribute, alongside or as an addendum to the NOTICE text from the Work, provided that such additional attribution notices cannot be construed as modifying the License.
+
+You may add Your own copyright statement to Your modifications and may provide additional or different license terms and conditions for use, reproduction, or distribution of Your modifications, or for any such Derivative Works as a whole, provided Your use, reproduction, and distribution of the Work otherwise complies with the conditions stated in this License.
+
+5. Submission of Contributions.
+
+Unless You explicitly state otherwise, any Contribution intentionally submitted for inclusion in the Work by You to the Licensor shall be under the terms and conditions of this License, without any additional terms or conditions. Notwithstanding the above, nothing herein shall supersede or modify the terms of any separate license agreement you may have executed with Licensor regarding such Contributions.
+
+6. Trademarks.
+
+This License does not grant permission to use the trade names, trademarks, service marks, or product names of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and reproducing the content of the NOTICE file.
+
+7. Disclaimer of Warranty.
+
+Unless required by applicable law or agreed to in writing, Licensor provides the Work (and each Contributor provides its Contributions) on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied, including, without limitation, any warranties or conditions of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A PARTICULAR PURPOSE. You are solely responsible for determining the appropriateness of using or redistributing the Work and assume any risks associated with Your exercise of permissions under this License.
+
+8. Limitation of Liability.
+
+In no event and under no legal theory, whether in tort (including negligence), contract, or otherwise, unless required by applicable law (such as deliberate and grossly negligent acts) or agreed to in writing, shall any Contributor be liable to You for damages, including any direct, indirect, special, incidental, or consequential damages of any character arising as a result of this License or out of the use or inability to use the Work (including but not limited to damages for loss of goodwill, work stoppage, computer failure or malfunction, or any and all other commercial damages or losses), even if such Contributor has been advised of the possibility of such damages.
+
+9. Accepting Warranty or Additional Liability.
+
+While redistributing the Work or Derivative Works thereof, You may choose to offer, and charge a fee for, acceptance of support, warranty, indemnity, or other liability obligations and/or rights consistent with this License. However, in accepting such obligations, You may act only on Your own behalf and on Your sole responsibility, not on behalf of any other Contributor, and only if You agree to indemnify, defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against, such Contributor by reason of your accepting any such warranty or additional liability.
diff --git a/docs/assets/files/grind-index-map/README.txt b/docs/assets/files/grind-index-map/README.txt
new file mode 100644
index 0000000..0529f50
--- /dev/null
+++ b/docs/assets/files/grind-index-map/README.txt
@@ -0,0 +1,12 @@
+Lean 官方 grind 有序映射教程配套源码
+
+来源：https://lean-lang.org/doc/tutorials/4.34.0-rc1/grind-index-map/
+下载日期：2026-08-13
+版本：Lean 4.34.0-rc1
+上游作者：Leo de Moura、Kim Morrison
+上游版权：Copyright (c) 2025 Lean FRO LLC
+许可证：Apache License 2.0
+
+grind-index-map-4.34.0-rc1.zip 是官方页面所附源码包的原样副本。
+其余三个工程文件从该压缩包中原样解出，便于浏览器直接查看。
+LICENSE-Apache-2.0.txt 是上游适用的 Apache License 2.0 许可证文本。
diff --git a/docs/assets/files/grind-index-map/grind-index-map-4.34.0-rc1.zip b/docs/assets/files/grind-index-map/grind-index-map-4.34.0-rc1.zip
new file mode 100644
index 0000000000000000000000000000000000000000..8e964089763a57a2397b282e8b8666f84299e668
GIT binary patch
literal 3709
zcmZ{nc~q0f`p4hAdGlr=gaiVFu!T)oLJ}k*L9`((CTtBDAR^j;paCg{MXzYpB!Gf~
z1_cEK`ho!iMF}8o)!VRXz^H6mtl9#iMOy1tt=9Jbe)O+<>$!L4e9z3BGxL4U^PDqh
z<|B?mLsS3&aEk(fm&C({okReTZ~(w@alIukGbi15Q5idZKTlP#MSsm=QWdQ1jMSVP
zCSN1lI}XPZjpd7&qRH1n=B*bo%<0(?w(uqzpPy@ef?B=gM3qg8_s%CR+C*i#wUYnn
zK?KI9L^Gn6l*Gp{wpo=YwYHI;%_Zv;Ih#5JT;r8NZM}rk8SK{UX|212c=j;6+!I{<
z*&hD9UYd@gCCWMCYV~Jn_@hUEo{ZF7*%TL-<{`EbwKDxqQ#)+EFW^OI1ADxeJ82Uf
zJuRBw@LdV##WCc@>NA4)7QrscsI@S8;Gr_vX*<_bo(|gauLFM`$E7#i*R`P~tv~=P
z$p5aBJUMr7PP?GF|I~RePG{IsS9j&_mD$rHQKlGQmM}Vk5OKD9usK>WFF~&&ng4S<
znPEYx=?w&}MB7+mKT|Y9<#;M1_z#Hb?kXCCg6!u1tL^b@Ug<5<jbT$%MS@TigT@|L
z!>ulLd<wD)VJrW2>rN;kNQ39SA1>pOzww&7)?d`=?za3J&*iq+o`JA(|J;I#CTlS0
zhf6p}t9nYdePNJJ$i+@caaP%IcOM}<lb4dh=xljnQzhBI<#>AFQZRINk2XHU&F&i5
z-UAd;?o7Pk5(+?1LC6Tdk0e13WYSF>WS7R7f3UBO@=bhcPgy*XXf>ycymi}0WHR|&
zqi^6JQ(dyOe9kz+d;H^%fG>*h<3h-uQ`i-Z%0p(tYWF9oiBr|;ZCN?-S#h}$OQx9S
z+@hJ(qh{qrDKa(ovO~?n${;fAR=fWbUb5Fk?UF66N-Ngr8Cj_EFy_)Sf3|P0(JHIl
zZS+Wuck12Dti0T(3;h$}yRyo*#%ARNO9ED(hPDE#a?~ZzXatrao59bqwHQ$GT6Is_
z2OCQ~blS*LOT`EjPRJ8fT&TDn-EKhCJnZ~(jGzfjL~kdXDARcuZ#b`bOLCo4V8%fH
z-gBR(6((nru6&_XgbZ6V&8d%OBbi=aBhlWNAoGba&TsQ2U+3mFeE_16L^q86=os#F
z8lH_QDIZ+Mz<M4OLu~s>j0>Id3z$_j8u-BR(9pV+6j|Fl5IH{C9L)5lW<L{W&&`g+
zM6*VYu)S}h;QR`KIzp6|C)%86F5LEox6nU~vAVa}eR*e~6|Jt05vrl8JD^qp(jaZX
z6Y$#T)Rt*dZuP3ozkq8A^vsq*!_HV}9ojrCX6H3@keSwwX;F?A=b%~=g&~#|Kle%z
zs-$<7l$YWssJOb(QiJaDvr7LGe&8v)3Y*p|+^ECL1x?ptE#&*nbd!-x%n&83u`m82
zy1J;N9J>IlUz1FNv&2SB5V6KE%?jC}-vxU%psH1Q<gT2qrQ?3MpF;2s_mb5!VcjRG
zGdTy}n$S;Pn~qLWk*#T}CFl*I#a7m;Sm-h+H><OsVXZvpILEDe7kbf(7ZW;SFCS@j
zPc1^z<=99bPzipp4JXhf#_g`7tJ(}U%)QUI@{>ah3jSI&*G`_4lP1c8J-0MPGzxh7
zcsTM~KEYQEfrW;C2f3G&B3>cDN(tYQ0Z>mZJ(X0S3{IZJRUd$sNu2ss?ZS8+roAoB
zc;hzu{FWE%FxtMxScssCq9c(E;2x}HM20wARgcdSuLKlXE17VDLWeq;TqUiir;vzV
zf21B_VYtreG?f_h6`v&41A1#stC%#2qJj(H`<RfVK5`ZQmCRcK6Q=t3KlI-T357av
zgX2C%Hvf1@F)GZdA8rF+SQ3*Jo9kVE2GO9)we^Fumd_=MN0hAe__Vx$);f+Rlbj$f
zio4VF4ybvJ1lQPdRp2xZuElh-t(vS)o<{JvcKSNs!5yVpIQy7YgDqnAz(k{f<$2QO
zgm70E&9_*wVmtGyyKL+aT^q%C3tE9U#6m-EVa<3?6dQw-SW3<H!B7NGOqiNi9l&xf
z0T@-HvilRUpH_r=Wu`v~568>C&CP8|bbn$4+z)<tf1TW%hV0NiHU_BM37RP7+iCB7
z!&unnyTEs4?9Y_0s7fzoUlDr^kf8!R{Q4@2TRe2G*~2gkBeEllaQ5!z(bjyPkOhqM
zfvE2dVQ?HV0AGJj)y)Ui0-^+&hxoOI+H~=RZqQ;9f*C*Y>ku3C!_umws>m6F%W*-K
zU`l?_g#;CneQ&z0$)}HIG<sPZ0_;`Nw`|X0({1!)G*Zp?pV<oz`H<GWv?p+(sRf{g
zBG1FniLr-u<`T_g>F41Ws5%SzQr4G1KFvteWQsct6W-i+%6nD=Ze)Kv4bMd{P=tj*
ztRe7E^-wa4wP!;(CL<%GL_gVVI%k>-)1y^Soh3Nb*JXw8JqT^qc4aL?9<>>Uw1_0<
zIkDoOnDeJDB7~+@%M|_nzs!b}gpDdFoEMdKX8a4l%FPR!Kwv*xy3bXA4XR$t&lQKf
z)NR6);uFDw)uUVa8^|Ae`@%i-yUT|{_|J>zf!dV>hdO?$zC@U#=GoS_OsmJr7LZp&
z>A`emG`P@%;nC+01|uu@wf2)tsJ(9{4-x3|n}%&B8~Pthkk|ZQpp_Q0K{dzn-XPzp
zEbZh^0UdBNl4JY*mqiQEI^u}dxFpp)Nf*pbd30!P{y6Ru&8C}ty?MX$(LEY5)L!yC
z$+FbQQbS8O-k#afwdad0m(e`rec%Q{F5^MOZlrq35p!0cbW(Xkk(=d$6fEmm=|Ai_
z)!>`!1E#*`!9T}Y_<=g>8M<s6y=nm|BR#Zxf2r0(KSm5LvNvQw7Y@CImUPGk`N%4L
zu^PK1J{7~Yr8JUT_?c;HtE+v`B=OcuWW>iw>NF!i!+)4$hL0_dB9mY{fJt{jnO|@m
z4+106j;OQnG(lBiHg7N+&DLa<MyYl&xVBS6WK!@CsTXbPKk$Q*veG<MJCXK1vS7dM
z6i)h<KaL-CHcW@jiy&JG;~(HAKu3-fszPZFcMVi@Jopwh3hDDHO%)zqz=oL1J<1ft
zMc0+2#0Q@&qyV!8Ol&^CU2zG10?A)!W{HY(=t9}+$_=P|m*YzGe*3@z1rHmIUf(F8
zzoj=gf}7nno0NNtZ1$e&2^~eywSXu`_6_Q_TktzsEvO|rp!uPUaDsFxC!68nXp)fa
zJ8}wk;7+E^bp<AAmi_ogeZ52$i#dP9FXE9b7JKr5mMo`8arX$+W0ZmNz?;ziB?VRF
z8eVcpZb^Od^s!j!F$(klfZ^2Dn@Z}`eg2&JOxpZL+1J(`X!&aWSLHus%9hImRAvr3
z+GuTQrrV@Y6)>cDgL6p){>1-8c741ZiPeN7<HQ4P@60iDu!CW!cIdA~n#sL3;JU+i
z5(}bKzbkjlzQUiAp=;qc1dem)&EmP`;=+oD(O?94Q@INo6Qb!A18iwWxc8%`XX|%n
zl4jHdTRm4y{5IXn-J{O|?_f9Z@CDQkm$>MCFa=o7c2zy80xin|FB97Vno;fqwqKWT
z1Rps|_3Ewu=^>?X>3!vQ3~ut5q=^t@2i)x?e4k(Nir716i2n_>_*6kRtCeR48go=<
zQQaz{i~}^l=1YZMVD>7teI@4vV<nC2N_dOaIk?>Qo#r_rPJ+WBQj5qK<6TSQ(xVTd
z#>Goz*AQG}lh6N6d5!mCx3gccx)qi$8)aD@=!uKiHxp!tAKhU|R<`gR<~6?ARC`OK
zxDbbJ2e}6@-NXm$2e(>l;N5j~$F}g@QeV>RYfq3IVC-FgWcBFGQ-cD8U9t?QB1>xC
zktdzN5L**D87JJu-RChnL!cXMsG~HlIc`nSWRnz^tyHEP^=D}5&ha~yP+a+bZQS@C
zs>L!|&2-<Brp>oPRv*!Jes$w9VPSny3O3T}^7O?-Poaqko|fx(1}PAph5J_n)h9oL
ziB5V?`9@ST$G_A4GnXE%w26V8Y`FnhB>BwQwrFjh<`%Z93i%HSwL^wq36pE9lI!b|
zn$b45F|e2T3YX1u^JA}C9)83u5UHr!N@>{lhn?*P!h8nusmRo6n5h|ix)cYj!;V9}
zwD}163_5|3gzKU<Q~M*<5_1{Gq8FBC+&{TN6R0`x9%oGm-CJx{`2fmi1-_kDPrqc#
z0<edt)r*A>CAuEIRRG-M!_0J-!{O$ixPM?Y;Us2n9No#48z6k_mBxW*Y11;lvwej%
zQ7)w7`+-3ds)?bUpq2Ddh<Abn8^5pB&DyBCcMAiE|As8!eDoFmBC3cN_1};sJ9TTu
z=FIF2R>8K<vu`Z^;1l!-;t^An=!`LjDV~iK#Y8c0df`RP$WMK};E`~jLbdxI)zPk$
zl(8{hTUp^tUahFBD~0n=fl2u&^dIetz4nV?9Tw%ZsE=vsFG%t&*tRWulRPyu=Y}Z8
z<l{NQj`AJH`o(la|5_gNE3x3vQS(cSwkVJa{BI0f^!|_bahShB*~eBNm*?L;J&T<8
nvDM#-^|95*>Hgb_W&U5R{+7Hr3IqSOAHCRT7sryt69Dl4Z=8=q

literal 0
HcmV?d00001

diff --git a/docs/assets/files/grind-index-map/lakefile.toml b/docs/assets/files/grind-index-map/lakefile.toml
new file mode 100644
index 0000000..677dd39
--- /dev/null
+++ b/docs/assets/files/grind-index-map/lakefile.toml
@@ -0,0 +1,5 @@
+name = "indexmap"
+defaultTargets = ["IndexMap"]
+
+[[lean_lib]]
+name = "IndexMap"
diff --git a/docs/assets/files/grind-index-map/lean-toolchain b/docs/assets/files/grind-index-map/lean-toolchain
new file mode 100644
index 0000000..17a4672
--- /dev/null
+++ b/docs/assets/files/grind-index-map/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:4.34.0-rc1
diff --git a/docs/projects/grind-index-map.md b/docs/projects/grind-index-map.md
new file mode 100644
index 0000000..7dd7521
--- /dev/null
+++ b/docs/projects/grind-index-map.md
@@ -0,0 +1,901 @@
+# 使用 `grind` 实现有序映射
+
+- 原文：[官方教程页面](https://lean-lang.org/doc/tutorials/4.34.0-rc1/grind-index-map/)；[Verso 源文件](https://github.com/leanprover/reference-manual/blob/v4.34.0-rc1/Tutorial/Grind/IndexMap.lean)
+- 作者：Leo de Moura、Kim Morrison
+- 译者：Lean 中文社区
+- 对应版本：Lean `v4.34.0-rc1`
+- 上游版权：Copyright © 2025 Lean FRO LLC，以 [Apache License 2.0](https://www.apache.org/licenses/LICENSE-2.0) 发布
+- 配套源码：[下载完整工程压缩包](../assets/files/grind-index-map/grind-index-map-4.34.0-rc1.zip)；[直接查看 `IndexMap.lean`](../assets/files/grind-index-map/IndexMap.lean)
+
+本节构造一种新的数据结构及其基本 API，以此说明 [`grind`](https://lean-lang.org/doc/reference/4.34.0-rc1/Tactic-Proofs/Tactic-Reference/#grind) 的用法。示例取材于 Rust 的 [`indexmap`](https://docs.rs/indexmap/latest/indexmap/) 数据结构。
+
+教程展示如何让 `grind` 自动完成一种新数据结构中几乎所有的证明，使 API 兼顾安全性和使用便利。上游 Verso 源在生成本页时设置 `maxHeartbeats 1000000` 和 `maxRecDepth 20000`，分别供 `IndexMap` 示例精译和编译使用；它还启用 `pp.rawOnError true`，以生成后文展示的原始诊断信息。
+
+`IndexMap` 旨在替代 `HashMap`。它同样支持快速的哈希查找，同时允许用户控制元素顺序。这里不会给出完整 API，只建立一些基本函数以及关于它们的定理。
+
+当前要实现的两个主要函数是 `insert` 和 `eraseSwap`：
+
+- `insert k v` 检查映射中是否已有 `k`。如果有，就用 `v` 替换其值，并保持 `k` 在原顺序中的位置；如果没有，就把 `(k, v)` 添加到映射末尾。
+- `eraseSwap k` 删除键为 `k` 的元素，再把原来的最后一个元素移入被删元素留下的槽位；如果 `k` 原本就在末尾，则直接弹出末项；如果映射中没有 `k`，则不做任何操作。这个行为可能出人意料。该函数适用于不关心其余元素顺序、只求高效删除的场合。另一种这里未实现的函数可以保留其余元素的顺序，但运行时间会与被删元素之后的元素数量成正比。
+
+目标如下：
+
+- 完全封装：`IndexMap` 的实现对用户隐藏，关于实现细节的定理也设为私有。
+- 尽可能使用 `grind`：只要可行，就优先添加私有定理，并为它作适当的本地 `grind` 标注，而不是手写较长的证明。
+- 尽可能使用自动参数：理想情况下，证明甚至不会出现在眼前，绝大部分工作由 `grind` 在幕后处理。
+
+第一步是导入所需的数据结构：
+
+```lean
+import Std.Data.HashMap
+```
+
+## 实现骨架
+
+先写出预期实现的骨架，并大量使用 `sorry` 占位所有证明。特别要注意，这个版本完全没有使用 `grind`。
+
+**实现骨架：**
+
+```lean
+import Std.Data.HashMap
+
+open Std
+
+structure IndexMap
+    (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+  indices : HashMap α Nat
+  keys : Array α
+  values : Array β
+  size_keys : keys.size = values.size
+  WF : ∀ (i : Nat) (a : α),
+    keys[i]? = some a ↔ indices[a]? = some i
+
+namespace IndexMap
+
+variable {α : Type u} {β : Type v}
+  [BEq α] [LawfulBEq α] [Hashable α] [LawfulHashable α]
+variable {m : IndexMap α β} {a : α} {b : β} {i : Nat}
+
+@[inline] def size (m : IndexMap α β) : Nat :=
+  m.values.size
+
+def emptyWithCapacity (capacity := 8) : IndexMap α β where
+  indices := HashMap.emptyWithCapacity capacity
+  keys := Array.emptyWithCapacity capacity
+  values := Array.emptyWithCapacity capacity
+  size_keys := sorry
+  WF := sorry
+
+instance : EmptyCollection (IndexMap α β) where
+  emptyCollection := emptyWithCapacity
+
+instance : Inhabited (IndexMap α β) where
+  default := ∅
+
+@[inline] def contains (m : IndexMap α β)
+    (a : α) : Bool :=
+  m.indices.contains a
+
+instance : Membership α (IndexMap α β) where
+  mem m a := a ∈ m.indices
+
+instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) :=
+  inferInstanceAs (Decidable (a ∈ m.indices))
+
+@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat :=
+  m.indices[a]?
+
+@[inline] def findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) : Nat :=
+  m.indices[a]
+
+@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β :=
+  m.values[i]?
+
+@[inline] def getIdx (m : IndexMap α β) (i : Nat)
+    (h : i < m.size := by get_elem_tactic) : β :=
+  m.values[i]
+
+instance :
+    GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem m a h :=
+    m.values[m.indices[a]]'(by sorry)
+  getElem? m a :=
+    m.indices[a]?.bind (m.values[·]?)
+  getElem! m a :=
+    m.indices[a]?.bind (m.values[·]?) |>.getD default
+
+instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem?_def := sorry
+  getElem!_def := sorry
+
+@[inline] def insert (m : IndexMap α β) (a : α) (b : β) :
+    IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    { indices := m.indices
+      keys := m.keys.set i a sorry
+      values := m.values.set i b sorry
+      size_keys := sorry
+      WF := sorry }
+  | none =>
+    { indices := m.indices.insert a m.size
+      keys := m.keys.push a
+      values := m.values.push b
+      size_keys := sorry
+      WF := sorry }
+
+instance : Singleton (α × β) (IndexMap α β) :=
+  ⟨fun ⟨a, b⟩ => (∅ : IndexMap α β).insert a b⟩
+
+instance : Insert (α × β) (IndexMap α β) :=
+  ⟨fun ⟨a, b⟩ s => s.insert a b⟩
+
+instance : LawfulSingleton (α × β) (IndexMap α β) :=
+  ⟨fun _ => rfl⟩
+
+/--
+删除具有给定键的键值对，并把最后一个键值对
+移动到被删除键值对原来的顺序位置。
+如果该键不存在，映射保持不变。
+-/
+@[inline] def eraseSwap (m : IndexMap α β) (a : α) :
+    IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    if w : i = m.size - 1 then
+      { indices := m.indices.erase a
+        keys := m.keys.pop
+        values := m.values.pop
+        size_keys := sorry
+        WF := sorry }
+    else
+      let lastKey := m.keys.back sorry
+      let lastValue := m.values.back sorry
+      { indices := (m.indices.erase a).insert lastKey i
+        keys := m.keys.pop.set i lastKey sorry
+        values := m.values.pop.set i lastValue sorry
+        size_keys := sorry
+        WF := sorry }
+  | none => m
+
+/-! ### 验证定理 -/
+
+theorem getIdx_findIdx (m : IndexMap α β) (a : α)
+    (h : a ∈ m) :
+    m.getIdx (m.findIdx a h) sorry = m[a] :=
+  sorry
+
+theorem mem_insert (m : IndexMap α β) (a a' : α) (b : β) :
+    a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
+  sorry
+
+theorem getElem_insert
+    (m : IndexMap α β) (a a' : α) (b : β)
+    (h : a' ∈ m.insert a b) :
+    (m.insert a b)[a']'h =
+      if h' : a' == a then b else m[a']'sorry := by
+  sorry
+
+theorem findIdx_insert_self
+    (m : IndexMap α β) (a : α) (b : β) :
+    (m.insert a b).findIdx a sorry =
+      if h : a ∈ m then m.findIdx a h else m.size := by
+  sorry
+
+end IndexMap
+```
+
+## 用 `grind` 填充实现骨架
+
+现在正式着手实现。目标是完全不手写证明。第一步是在 `size_keys'` 和 `WF` 字段上安装自动参数；只要 `grind` 能证明它们，构造值时就可以省略这些字段。既然正在修改 `IndexMap` 的定义本身，而且目标是完全封装，也把所有字段都设为私有。
+
+```lean
+open Std
+
+structure IndexMap
+    (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+  private indices : HashMap α Nat
+  private keys : Array α
+  private values : Array β
+  private size_keys' : keys.size = values.size := by grind
+  private WF : ∀ (i : Nat) (a : α),
+    keys[i]? = some a ↔ indices[a]? = some i := by grind
+```
+
+本教程余下部分都在以下命名空间和变量声明下进行：
+
+```lean
+namespace IndexMap
+
+variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
+variable {m : IndexMap α β} {a : α} {b : β} {i : Nat}
+```
+
+### 大小与基本构造
+
+让 `grind` 可以使用 `size` 的定义和私有字段 `size_keys'`：
+
+```lean
+@[inline] def size (m : IndexMap α β) : Nat :=
+  m.values.size
+
+@[local grind =] private theorem size_keys : m.keys.size = m.size :=
+  m.size_keys'
+
+@[local grind =] private theorem size_values : m.values.size = m.size := rfl
+```
+
+草稿版构造 `emptyWithCapacity` 时，最先遇到的 `sorry` 是 `size_keys'` 和 `WF` 字段。这两项显然很简单，`grind` 可以解决，因此直接删去这两个字段：
+
+```lean
+def emptyWithCapacity (capacity := 8) : IndexMap α β where
+  indices := HashMap.emptyWithCapacity capacity
+  keys := Array.emptyWithCapacity capacity
+  values := Array.emptyWithCapacity capacity
+```
+
+还需要定义包含关系。上游将这段标记为 `codeOnly`：网页正文隐藏它，但下载源码和编译上下文需要这些定义。
+
+```lean
+@[inline] def contains (m : IndexMap α β)
+    (a : α) : Bool :=
+  m.indices.contains a
+
+instance : Membership α (IndexMap α β) where
+  mem m a := a ∈ m.indices
+
+instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) :=
+  inferInstanceAs (Decidable (a ∈ m.indices))
+```
+
+### `GetElem?` 与良构性
+
+下一个任务是处理草稿版 `GetElem?` 实例中的 `sorry`：
+
+```lean
+instance :
+    GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem m a h :=
+    m.values[m.indices[a]]'(by sorry)
+  getElem? m a :=
+    m.indices[a]?.bind (m.values[·]?)
+  getElem! m a :=
+    m.indices[a]?.bind (m.values[·]?) |>.getD default
+```
+
+这个 `sorry` 处的目标是：
+
+```text
+m : IndexMap α β
+a : α
+h : a ∈ m
+⊢ m.indices[a] < m.values.size
+```
+
+> 上游维护备注：上述目标展示需要与前一个代码块中的 `sorry` 保持同步。解决办法是为 SubVerso 提取机制添加项级目标支持，做法可仿照现有的普通目标保存功能。
+
+先把它写成独立定理，尝试用 `grind` 证明，看看 `grind` 会卡在哪里。由于已经为 `size` 和 `size_keys` 添加了 `grind` 标注，可以把目标安全地改写为：
+
+```lean
+theorem getElem_indices_lt (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m.indices[a] < m.size := by
+  grind
+```
+
+**预期失败。** 这个证明会失败。从 `grind` 消息的 `Goal diagnostics` 一节看，它几乎没有取得进展：
+
+```text
+`grind` failed
+case grind
+α : Type u
+β : Type v
+inst : BEq α
+inst_1 : Hashable α
+m : IndexMap α β
+a : α
+h : a ∈ m
+h_1 : m.size ≤ m.indices[a]
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] a ∈ m
+    [prop] m.size ≤ m.indices[a]
+  [eqc] True propositions
+  [eqc] Equivalence classes
+  [ematch] E-matching patterns
+  [cutsat] Assignment satisfying linear constraints
+```
+
+这里立刻能看出一个问题：`grind` 还不知道 `a ∈ m` 与 `a ∈ m.indices` 是同一回事。添加这一事实：
+
+```lean
+@[local grind _=_] private theorem mem_indices
+    {m : IndexMap α β} {a : α} :
+    a ∈ m.indices ↔ a ∈ m := Iff.rfl
+```
+
+以下变量声明是上游展示区段的上下文：
+
+```lean
+variable {α : Type u} [BEq α] [Hashable α]
+```
+
+不论最终证明采用什么方式，已经知道以下几点：
+
+- 它必须使用映射的良构性条件。
+- 它必须关联 `m.indices[a]` 和 `m.indices[a]?`，因为后者出现在良构性条件中。
+- 除非映射 `m.indices` 满足 `LawfulGetElem`，预期的对应关系根本不成立。为此，需要 `LawfulBEq α` 和 `LawfulHashable α` 的[类型类实例](https://lean-lang.org/doc/reference/4.34.0-rc1/Type-Classes/#--tech-term-instances)。
+
+> 上游待办：这里希望能链接到 `HashMap` 的 `LawfulGetElem` 实例，以便读者直接看到这些要求。
+
+把这些实例和良构性条件配置给 `grind`：
+
+```lean
+variable [LawfulBEq α] [LawfulHashable α]
+
+attribute [local grind _=_] IndexMap.WF
+```
+
+再给 `grind` 一条手工提示，关联 `m.indices[a]` 与 `m.indices[a]?`：
+
+```lean
+private theorem getElem_indices_lt {h : a ∈ m} : m.indices[a] < m.size := by
+  have : m.indices[a]? = some m.indices[a] := by grind
+  grind
+```
+
+定理证明完成后，还要让 `grind` 能使用它。可以在定理陈述前添加 `@[local grind]`，也可以在陈述后写 `attribute [local grind] getElem_indices_lt`。两种写法都会使用 `grind` 的内置启发式方法，决定用什么模式匹配这条定理。
+
+这里先查看 `grind` 属性生成了哪些模式：
+
+```lean
+attribute [local grind] getElem_indices_lt
+```
+
+**信息输出：**
+
+```text
+Try these:
+  [apply] [grind
+    .] for pattern: [@LE.le `[Nat] `[instLENat] ((@getElem (HashMap #8 `[Nat] #6 #5) _ `[Nat] _ _ (@indices _ #7 _ _ #4) #3 #0) + 1) (@size _ _ _ _ #4)]
+  [apply] [grind →] for pattern: [LawfulBEq #8 #6, LawfulHashable _ _ #5, @Membership.mem _ (IndexMap _ #7 _ _) _ #4 #3]
+```
+
+这些模式没有用。第一个匹配定理的整个结论，而且是规范化后的版本，其中 `x < y` 已被替换为 `x + 1 ≤ y`。第二个过于宽泛：它会匹配任何包含该定理各项假设的项，而完全忽略结论。
+
+所需模式应比整个结论更一般，但又不能忽略结论。希望每当 `grind` 看到 `m.indices[a]` 时就触发这条定理，因此不用属性自动选取模式，而是编写自定义模式：
+
+```lean
+grind_pattern getElem_indices_lt => m.indices[a]
+```
+
+Lean 标准库把 `get_elem_tactic` 用作 `xs[i]` 记法的自动参数。该记法展开为 `GetElem.getElem xs i h`，证明 `h` 由 `get_elem_tactic` 生成。这里不只希望 `grind` 填入这些证明，还希望可以完全省略证明。为此添加：
+
+```lean
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
+```
+
+在之后的 Lean 版本中，这可能会成为内置行为的一部分。
+
+现在可以回到 `GetElem?` 实例的构造。为了使用良构性条件，`grind` 必须能展开 `size`：
+
+```lean
+attribute [local grind] size
+```
+
+其中 `local` 修饰符把这种展开限制在当前文件。配置完成后，可以直接写成：
+
+```lean
+instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem m a h :=
+    m.values[m.indices[a]]
+  getElem? m a :=
+    m.indices[a]?.bind (fun i => (m.values[i]?))
+  getElem! m a :=
+    m.indices[a]?.bind (fun i => (m.values[i]?)) |>.getD default
+```
+
+这里既没有 `sorry`，也没有显式写出的证明。
+
+接下来需要把这些定义的展开等式暴露给本文件内的 `grind`，但不把实现细节加入公开 API：
+
+```lean
+@[local grind =] private theorem getElem_def
+    (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m[a] = m.values[m.indices[a]'h] :=
+  rfl
+@[local grind =] private theorem getElem?_def
+    (m : IndexMap α β) (a : α) :
+    m[a]? = m.indices[a]?.bind (fun i => (m.values[i]?)) :=
+  rfl
+@[local grind =] private theorem getElem!_def
+    [Inhabited β] (m : IndexMap α β) (a : α) :
+    m[a]! = (m.indices[a]?.bind (m.values[·]?)).getD default :=
+  rfl
+```
+
+这里再次采用 `@[local grind =] private theorem` 模式：对外隐藏实现细节，同时允许 `grind` 在本文件内看到这些事实。
+
+然后证明 `LawfulGetElem` 实例，并让 `grind` 填入证明：
+
+```lean
+instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem?_def := by grind
+  getElem!_def := by grind
+```
+
+成功。
+
+### `insert`
+
+继续尝试在不写任何证明的情况下定义 `insert`：
+
+```lean
+@[inline] def insert (m : IndexMap α β) (a : α) (b : β) : IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    { indices := m.indices
+      keys    := m.keys.set i a
+      values  := m.values.set i b }
+  | none =>
+    { indices := m.indices.insert a m.size
+      keys    := m.keys.push a
+      values  := m.values.push b }
+```
+
+两个分支中，`grind` 都自动证明了 `size_keys'` 和 `WF` 字段。另请注意，第一个分支中的 `m.keys.set i a` 和 `m.values.set i b` 调用，其“索引在界内”义务也由 `grind` 通过 `get_elem_tactic` 自动参数填入。
+
+### `eraseSwap` 的失败诊断与修复
+
+接着尝试 `eraseSwap`：
+
+```lean
+@[inline] def eraseSwap (m : IndexMap α β) (a : α) : IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    if w : i = m.size - 1 then
+      { indices := m.indices.erase a
+        keys := m.keys.pop
+        values := m.values.pop }
+    else
+      let lastKey := m.keys.back
+      let lastValue := m.values.back
+      { indices := (m.indices.erase a).insert lastKey i
+        keys := m.keys.pop.set i lastKey
+        values := m.values.pop.set i lastValue }
+  | none => m
+```
+
+**预期失败：**
+
+```text
+could not synthesize default value for field 'WF' of 'IndexMap' using tactics
+```
+
+**预期失败的详细诊断：**
+
+```text
+`grind` failed
+case grind.1.1.2.2.1.1.1
+α : Type u
+β : Type v
+inst : BEq α
+inst_1 : Hashable α
+m_1 : IndexMap α β
+a_1 : α
+b : β
+i_1 : Nat
+inst_2 : LawfulBEq α
+inst_3 : LawfulHashable α
+m : IndexMap α β
+a : α
+i : Nat
+h : m.indices[a]? = some i
+w : ¬i = m.size - 1
+lastKey : α := m.keys.back ⋯
+lastValue : β := m.values.back ⋯
+i_2 : Nat
+a_2 : α
+h_1 : ((m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some a_2) =
+  ¬((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2
+h_2 : -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0
+left : (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some a_2
+right : ¬((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2
+h_4 : ¬i = i_2
+left_1 : ¬m.keys[i_2]? = some a
+right_1 : ¬m.indices[a]? = some i_2
+h_6 : (m.keys.back ⋯ == a_2) = true
+h_7 : i + 1 ≤ m.keys.pop.size
+left_2 : (m.indices.erase a).contains a_2 = true
+right_2 : a_2 ∈ m.indices.erase a
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+  [eqc] True propositions
+  [eqc] False propositions
+  [eqc] Equivalence classes
+  [cases] Case analyses
+  [ematch] E-matching patterns
+  [cutsat] Assignment satisfying linear constraints
+  [ring] Rings
+
+[grind] Diagnostics
+```
+
+失败发生在证明第二个分支的 `WF` 字段时。与往常一样，`grind` 给出了失败状态的详细信息，只是信息多得几乎难以利用。查看 `cutsat` 生成的模型，判断问题所在：
+
+```text
+[cutsat] Assignment satisfying linear constraints
+  [assign] i_1 := 4
+  [assign] i := 0
+  [assign] i_2 := 1
+  [assign] m.keys.pop.size := 2
+  [assign] m.keys.size := 3
+  [assign] m.size := 3
+  [assign] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size := 2
+  [assign] m.values.size := 3
+  [assign] m.indices[a] := 0
+  [assign] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2] := 0
+  [assign] (m.keys.set i (m.keys.back ⋯) ⋯).pop.size := 2
+  [assign] (m.keys.set i (m.keys.back ⋯) ⋯).size := 3
+  [assign] m.indices[a] := 0
+  [assign] m.indices[a_2] := 1
+  [assign] m.indices[m.keys[i_2]] := 1
+  [assign] m.indices[m.keys[i_2]] := 1
+```
+
+上游对该输出的备注：
+
+```text
+FIXME（@kim-em / @leodemoura）：这里有一些重复输出。
+```
+
+这不是一个合法 `IndexMap` 的反例，而是 `cutsat` 在当前线性抽象下允许的一组赋值。它表现得像一个大小为 `3`、键为 `a`、`a_2` 和未单独命名的 `m.keys.back ⋯` 的映射，用来指出当前规则还没有向线性算术求解器传递哪些事实。
+
+赋值中最可疑的是下面这一行：
+
+```text
+((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2] := 0
+```
+
+如果把原 `IndexMap` 的良构性和由此推出的键单射性充分传递进来，这三个位置对应的键互异，因而应当有：
+
+```text
+((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2] =
+  (m.indices.erase a)[a_2] =
+  m.indices[a_2] =
+  1
+```
+
+发现可疑之处后，可以检查 `grind` 找到的等价类。未来会提供检查等价类的搜索工具；目前只能手工通读。许多等价类中包括：
+
+```text
+{a_2,
+  m.keys.back ⋯,
+  ..
+  m.keys[m.keys.size - 1],
+  ..
+  m.keys[i_2], ...}
+```
+
+根据 `keys` 的单射性，这应当推出 `i_2 = m.keys.size - 1`。但这组 `cutsat` 赋值并未反映该等式，说明 `grind` 尚未把由 `WF` 推出的单射性传递给线性算术求解器。
+
+回看良构性条件的表达方式：`∀ (i : Nat) (a : α), keys[i]? = some a ↔ indices[a]? = some i`，出现这种情况或许并不意外。它以 `keys[i]?` 和 `indices[a]?` 表述。添加一个改用 `GetElem.getElem` 而非 `GetElem?.getElem?` 的良构性条件变体：
+
+```lean
+@[local grind .]
+private theorem WF' (i : Nat) (a : α) (h₁ : i < m.keys.size) (h₂ : a ∈ m) :
+    m.keys[i] = a ↔ m.indices[a] = i := by
+  have := m.WF i a
+  grind
+```
+
+有了这个变体，可以验证 `grind` 现在能够证明：
+
+```lean
+example {m : IndexMap α β} {a : α} {h : a ∈ m} :
+  m.keys[m.indices[a]'h] = a := by grind
+```
+
+再次尝试 `eraseSwap`，现在所有内容都顺利通过，不需要手工证明：
+
+```lean
+@[inline] def eraseSwap (m : IndexMap α β) (a : α) : IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    if w : i = m.size - 1 then
+      { indices := m.indices.erase a
+        keys := m.keys.pop
+        values := m.values.pop }
+    else
+      let lastKey := m.keys.back
+      let lastValue := m.values.back
+      { indices := (m.indices.erase a).insert lastKey i
+        keys := m.keys.pop.set i lastKey
+        values := m.values.pop.set i lastValue }
+  | none => m
+```
+
+以下是索引查找和值读取函数。上游同样将这段标记为 `codeOnly`：网页正文隐藏它，但后续证明和下载源码需要这些定义。
+
+```lean
+@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat :=
+  m.indices[a]?
+
+@[inline] def findIdx (m : IndexMap α β) (a : α)
+    (h : a ∈ m := by get_elem_tactic) : Nat :=
+  m.indices[a]
+
+@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β :=
+  m.values[i]?
+
+@[inline] def getIdx (m : IndexMap α β) (i : Nat)
+    (h : i < m.size := by get_elem_tactic) : β :=
+  m.values[i]
+```
+
+### 验证定理与完整原型
+
+最后证明基本操作的验证定理，关联 `getIdx`、`findIdx`、`insert` 和 `eraseSwap`。所有证明都能直接使用带 `+locals` 修饰符的 `grind` 完成；该修饰符把当前文件中的定义加入 `grind` 可用的规则集合，使这些本文件定义的方程能够参与证明：
+
+```lean
+/-! ### 验证定理（并未穷尽） -/
+
+@[grind =]
+theorem mem_insert (m : IndexMap α β) (a a' : α) (b : β) :
+    a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
+  grind +locals
+
+@[grind =]
+theorem getElem_insert (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
+    (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
+  grind +locals
+
+theorem findIdx_lt (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m.findIdx a h < m.size := by
+  grind +locals
+
+grind_pattern findIdx_lt => m.findIdx a h
+
+@[grind =]
+theorem findIdx_insert_self (m : IndexMap α β) (a : α) (b : β) :
+    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
+  grind +locals
+
+@[grind =]
+theorem findIdx?_eq (m : IndexMap α β) (a : α) :
+    m.findIdx? a = if h : a ∈ m then some (m.findIdx a h) else none := by
+  grind +locals
+
+@[grind =]
+theorem getIdx_findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m.getIdx (m.findIdx a) = m[a] := by grind +locals
+
+omit [LawfulBEq α] [LawfulHashable α] in
+@[grind =]
+theorem getIdx?_eq (m : IndexMap α β) (i : Nat) :
+    m.getIdx? i = if h : i < m.size then some (m.getIdx i h) else none := by
+  grind +locals
+
+private theorem getElem_keys_mem {m : IndexMap α β} {i : Nat} (h : i < m.size) :
+    m.keys[i] ∈ m := by
+  have : m.indices[m.keys[i]]? = some i := by grind
+  grind
+
+local grind_pattern getElem_keys_mem => m.keys[i]
+
+theorem getElem?_eraseSwap (m : IndexMap α β) (a a' : α) :
+    (m.eraseSwap a)[a']? = if a' == a then none else m[a']? := by
+  grind +locals
+
+@[grind =]
+theorem mem_eraseSwap (m : IndexMap α β) (a a' : α) :
+    a' ∈ m.eraseSwap a ↔ a' ≠ a ∧ a' ∈ m := by
+  grind +locals
+
+theorem getElem_eraseSwap (m : IndexMap α β) (a a' : α) (h : a' ∈ m.eraseSwap a) :
+    (m.eraseSwap a)[a'] = m[a'] := by
+  grind +locals
+```
+
+其中，希望供模块外的 `grind` 自动使用的 API 定理，需要通过 `@[grind]` 或 `grind_pattern` 注册；普通公开定理不必全部注册。这样，即使用户无法使用本文件内部的 `local grind` 规则，选定的公开事实仍能参与 `grind` 证明。
+
+汇总以上代码，原型 API 得到如下实现。
+
+> 上游待办：应当通过注解从源模块生成这个版本，并丢弃不需要的内容，从而使展示代码与源码保持同步。
+
+```lean
+local macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
+
+open Std
+
+structure IndexMap
+    (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+  private indices : HashMap α Nat
+  private keys : Array α
+  private values : Array β
+  private size_keys' : keys.size = values.size := by grind
+  private WF : ∀ (i : Nat) (a : α),
+    keys[i]? = some a ↔ indices[a]? = some i := by grind
+
+namespace IndexMap
+
+variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
+variable {m : IndexMap α β} {a : α} {b : β} {i : Nat}
+
+@[inline] def size (m : IndexMap α β) : Nat :=
+  m.values.size
+
+@[local grind =] private theorem size_keys : m.keys.size = m.size :=
+  m.size_keys'
+
+@[local grind =] private theorem size_values : m.values.size = m.size := rfl
+
+def emptyWithCapacity (capacity := 8) : IndexMap α β where
+  indices := HashMap.emptyWithCapacity capacity
+  keys := Array.emptyWithCapacity capacity
+  values := Array.emptyWithCapacity capacity
+
+instance : EmptyCollection (IndexMap α β) where
+  emptyCollection := emptyWithCapacity
+
+instance : Inhabited (IndexMap α β) where
+  default := ∅
+
+@[inline] def contains (m : IndexMap α β) (a : α) : Bool :=
+  m.indices.contains a
+
+instance : Membership α (IndexMap α β) where
+  mem m a := a ∈ m.indices
+
+instance {m : IndexMap α β} {a : α} : Decidable (a ∈ m) :=
+  inferInstanceAs (Decidable (a ∈ m.indices))
+
+@[local grind _=_] private theorem mem_indices
+    {m : IndexMap α β} {a : α} :
+    a ∈ m.indices ↔ a ∈ m := Iff.rfl
+
+@[inline] def findIdx? (m : IndexMap α β) (a : α) : Option Nat :=
+  m.indices[a]?
+
+@[inline] def findIdx (m : IndexMap α β) (a : α)
+    (h : a ∈ m := by get_elem_tactic) : Nat :=
+  m.indices[a]
+
+@[inline] def getIdx? (m : IndexMap α β) (i : Nat) : Option β :=
+  m.values[i]?
+
+@[inline] def getIdx (m : IndexMap α β) (i : Nat)
+    (h : i < m.size := by get_elem_tactic) : β :=
+  m.values[i]
+
+variable [LawfulBEq α] [LawfulHashable α]
+
+attribute [local grind _=_] IndexMap.WF
+
+private theorem getElem_indices_lt
+    {h : a ∈ m} : m.indices[a] < m.size := by
+  have : m.indices[a]? = some m.indices[a] := by grind
+  grind
+
+grind_pattern getElem_indices_lt => m.indices[a]
+
+instance : GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem m a h :=
+    m.values[m.indices[a]]
+  getElem? m a :=
+    m.indices[a]?.bind (fun i => (m.values[i]?))
+  getElem! m a :=
+    m.indices[a]?.bind (fun i => (m.values[i]?)) |>.getD default
+
+@[local grind =] private theorem getElem_def
+    (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m[a] = m.values[m.indices[a]'h] :=
+  rfl
+@[local grind =] private theorem getElem?_def
+    (m : IndexMap α β) (a : α) :
+    m[a]? = m.indices[a]?.bind (fun i => (m.values[i]?)) :=
+  rfl
+@[local grind =] private theorem getElem!_def
+    [Inhabited β] (m : IndexMap α β) (a : α) :
+    m[a]! = (m.indices[a]?.bind (m.values[·]?)).getD default :=
+  rfl
+
+instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
+  getElem?_def := by grind
+  getElem!_def := by grind
+
+@[inline] def insert (m : IndexMap α β) (a : α) (b : β) : IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    { indices := m.indices
+      keys    := m.keys.set i a
+      values  := m.values.set i b }
+  | none =>
+    { indices := m.indices.insert a m.size
+      keys    := m.keys.push a
+      values  := m.values.push b }
+
+instance : Singleton (α × β) (IndexMap α β) :=
+  ⟨fun ⟨a, b⟩ => (∅ : IndexMap α β).insert a b⟩
+
+instance : Insert (α × β) (IndexMap α β) :=
+  ⟨fun ⟨a, b⟩ s => s.insert a b⟩
+
+instance : LawfulSingleton (α × β) (IndexMap α β) :=
+  ⟨fun _ => rfl⟩
+
+@[local grind .]
+private theorem WF' (i : Nat) (a : α) (h₁ : i < m.keys.size) (h₂ : a ∈ m) :
+    m.keys[i] = a ↔ m.indices[a] = i := by
+  have := m.WF i a
+  grind
+
+/--
+删除具有给定键的键值对，并把最后一个键值对
+移动到被删除键值对原来的顺序位置。
+如果该键不存在，映射保持不变。
+-/
+@[inline] def eraseSwap (m : IndexMap α β) (a : α) : IndexMap α β :=
+  match h : m.indices[a]? with
+  | some i =>
+    if w : i = m.size - 1 then
+      { indices := m.indices.erase a
+        keys := m.keys.pop
+        values := m.values.pop }
+    else
+      let lastKey := m.keys.back
+      let lastValue := m.values.back
+      { indices := (m.indices.erase a).insert lastKey i
+        keys := m.keys.pop.set i lastKey
+        values := m.values.pop.set i lastValue }
+  | none => m
+
+/-! ### 验证定理（并未穷尽） -/
+
+@[grind =]
+theorem mem_insert (m : IndexMap α β) (a a' : α) (b : β) :
+    a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := by
+  grind +locals
+
+@[grind =]
+theorem getElem_insert (m : IndexMap α β) (a a' : α) (b : β) (h : a' ∈ m.insert a b) :
+    (m.insert a b)[a'] = if h' : a' == a then b else m[a'] := by
+  grind +locals
+
+theorem findIdx_lt (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m.findIdx a h < m.size := by
+  grind +locals
+
+grind_pattern findIdx_lt => m.findIdx a h
+
+@[grind =]
+theorem findIdx_insert_self (m : IndexMap α β) (a : α) (b : β) :
+    (m.insert a b).findIdx a = if h : a ∈ m then m.findIdx a else m.size := by
+  grind +locals
+
+@[grind =]
+theorem findIdx?_eq (m : IndexMap α β) (a : α) :
+    m.findIdx? a = if h : a ∈ m then some (m.findIdx a h) else none := by
+  grind +locals
+
+@[grind =]
+theorem getIdx_findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) :
+    m.getIdx (m.findIdx a) = m[a] := by grind +locals
+
+omit [LawfulBEq α] [LawfulHashable α] in
+@[grind =]
+theorem getIdx?_eq (m : IndexMap α β) (i : Nat) :
+    m.getIdx? i = if h : i < m.size then some (m.getIdx i h) else none := by
+  grind +locals
+
+end IndexMap
+```
+
+现在还为 `eraseSwap` 操作添加了验证定理。有兴趣的读者可以继续扩充，甚至发布一个完整的 `IndexMap` 库。
+
+以上封装设计遵循这些原则：
+
+- `IndexMap` 的所有字段都是私有的，因为它们属于实现细节。
+- 关于这些字段的定理也都是私有的，并标注 `@[local grind]` 而不是 `@[grind]`，因为 API 建立之后不再需要它们。
+- 希望模块外的 `grind` 自动使用的验证定理，通过 `@[grind]` 或 `grind_pattern` 注册；这些定理本身由 `grind` 证明。离开当前模块后，`@[local grind]` 定理不再可用，因此必须把所需的公开事实另行注册。未供自动匹配使用的公开定理不必标注 `@[grind]`。
diff --git a/mkdocs.yml b/mkdocs.yml
index cc273c0..7046188 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -94,6 +94,7 @@ nav:
     - Lean4Game 教程: projects/lean4game.md
     - Verso 教程: projects/verso.md
     - mvcgen 命令式程序验证: projects/mvcgen.md
+    - grind 有序映射验证: projects/grind-index-map.md
   - Mathlib4Help:
     - Mathlib4Help: mathlib4_help/index.md
     - attributes: mathlib4_help/attributes.md