Using `grind` for Ordered Maps

In this section we'll build an example of a new data structure and basic API for it, illustrating the use of grind. The example will be derived from Rust's indexmap data structure.

IndexMap is intended as a replacement for HashMap (in particular, it has fast hash-based lookup), but allowing the user to maintain control of the order of the elements. We won't give a complete API, just set up some basic functions and theorems about them.

The two main functions we'll implement for now are insert and eraseSwap:

insert k v checks if k is already in the map. If so, it replaces the value with v, keeping k in the same position in the ordering. If it is not already in the map, insert adds (k, v) to the end of the map.
eraseSwap k removes the element with key k from the map, and swaps it with the last element of the map (or does nothing if k is not in the map). (This behavior may be surprising: this function exists because it is an efficient way to an erase element when you don't care about the order of the remaining elements. Another function, not implemented here, would preserve the order of the remaining elements, but at the cost of running in time proportional to the number of elements after the erased element.)

Our goals will be:

Complete encapsulation: The implementation of IndexMap is hidden from the users, and the theorems about the implementation details are private.
Use grind as much as possible: We'll prefer adding a private theorem and annotating it with @[grind] over writing a longer proof whenever practical.
Use auto-parameters as much as possible: Ideally, we don't even need to see the proofs; they should mostly be handled invisibly by grind.

The first step is to import the necessary data structures:

import Std.Data.HashMap

Skeleton

To begin with, we'll write out a skeleton of what we want to achieve, liberally using sorry as a placeholder for all proofs. In particular, this version makes no use of grind.

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 declaration uses 'sorry'declaration uses 'sorry'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]

declaration uses 'sorry'instance :
    GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
  getElem m a h :=
    m.values[m.indices[a]]'(byα:Type uβ:Type vinst✝³:BEq αinst✝²:LawfulBEq αinst✝¹:Hashable αinst✝:LawfulHashable αm✝:IndexMap α βa✝:αb:βi:Natm:IndexMap α βa:αh:a ∈ m⊢ m.indices[a] < m.values.size sorryAll goals completed! 🐙)
  getElem? m a :=
    m.indices[a]?.bind (m.values[·]?)
  getElem! m a :=
    m.indices[a]?.bind (m.values[·]?) |>.getD default

declaration uses 'sorry'instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
  getElem?_def := sorry
  getElem!_def := sorry

@[inline] def declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'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⟩

/--
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 declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'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

/-! ### Verification theorems -/

theorem declaration uses 'sorry'getIdx_findIdx (m : IndexMap α β) (a : α)
    (h : a ∈ m) :
    m.getIdx (m.findIdx a h) sorry = m[a] :=
  sorry

theorem declaration uses 'sorry'mem_insert (m : IndexMap α β) (a a' : α) (b : β) :
    a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := byα:Type uβ:Type vinst✝³:BEq αinst✝²:LawfulBEq αinst✝¹:Hashable αinst✝:LawfulHashable αm:IndexMap α βa:αa':αb:β⊢ a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'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α:Type uβ:Type vinst✝³:BEq αinst✝²:LawfulBEq αinst✝¹:Hashable αinst✝:LawfulHashable αm:IndexMap α βa:αa':αb:βh:a' ∈ m.insert a b⊢ (m.insert a b)[a'] = if h' : (a' == a) = true then b else m[a']
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'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α:Type uβ:Type vinst✝³:BEq αinst✝²:LawfulBEq αinst✝¹:Hashable αinst✝:LawfulHashable αm:IndexMap α βa:αb:β⊢ (m.insert a b).findIdx a ⋯ = if h : a ∈ m then m.findIdx a h else m.size
  sorryAll goals completed! 🐙

end IndexMap

Header 2

Let's get started. We'll aspire to never writing a proof by hand, and the first step of that is to install auto-parameters for the size_keys and WF field, so we can omit these fields whenever grind can prove them. While we're modifying the definition of IndexMap itself, let's make all the fields private, since we're planning on having complete encapsulation.

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

For the rest of this tutorial, the following namespace and variable declarations are in effect:

namespace IndexMap

variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
variable {m : IndexMap α β} {a : α} {b : β} {i : Nat}

Let's give grind access to the definition of size, and size_keys private field:

@[inline] def size (m : IndexMap α β) : Nat :=
  m.values.size

@[local grind =] private theorem size_keys : m.keys.size = m.size :=
  m.size_keys'

Our first sorrys in the draft version are the size_keys and WF fields in our construction of def emptyWithCapacity. Surely these are trivial, and solvable by grind, so we simply delete those fields:

def emptyWithCapacity (capacity := 8) : IndexMap α β where
  indices := HashMap.emptyWithCapacity capacity
  keys := Array.emptyWithCapacity capacity
  values := Array.emptyWithCapacity capacity

Our next task is to deal with the sorry in our construction of the original GetElem? instance:

declaration uses 'sorry'instance :
    GetElem? (IndexMap α β) α β (fun m a => a ∈ m) where
  getElem m a h :=
    m.values[m.indices[a]]'(byα:Type uβ:Type vinst✝³:BEq αinst✝²:LawfulBEq αinst✝¹:Hashable αinst✝:LawfulHashable αm✝:IndexMap α βa✝:αb:βi:Natm:IndexMap α βa:αh:a ∈ m⊢ m.indices[a] < m.values.size sorryAll goals completed! 🐙)
  getElem? m a :=
    m.indices[a]?.bind (m.values[·]?)
  getElem! m a :=
    m.indices[a]?.bind (m.values[·]?) |>.getD default

The goal at this sorry is

m : IndexMap α β
a : α
h : a ∈ m
⊢ m.indices[a] < m.values.size

Let's try proving this as a stand-alone theorem, via grind, and see where grind gets stuck. Because we've added grind annotations for size and size_keys already, we can safely reformulate the goal as:

theorem getElem_indices_lt (m : IndexMap α β) (a : α) (h : a ∈ m) :
    m.indices[a] < m.size := byα:Type uβ:Type vinst✝¹:BEq αinst✝:Hashable αm:IndexMap α βa:αh:a ∈ m⊢ m.indices[a] < m.size
  `grind` failed
grindα:Type uβ:Type vinst:BEq αinst_1:Hashable αm:IndexMap α βa:αh:a ∈ mh_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
[prop] m.size ≤ m.indices[a]
[prop] a ∈ m
[eqc] Equivalence classes
[eqc] {Membership.mem, fun m a => a ∈ m}
[ematch] E-matching patterns
[thm] HashMap.contains_iff_mem: [@Membership.mem #5 (HashMap _ #4 #3 #2) _ #1 #0]
[cutsat] Assignment satisfying linear constraints
[assign] m.size := 0
[assign] m.indices[a] := 0grindAll goals completed! 🐙

This fails, and looking at the Goal diagnostics section of the message from grind we see that it hasn't done much:

`grind` failed
grindα:Type uβ:Type vinst:BEq αinst_1:Hashable αm:IndexMap α βa:αh:a ∈ mh_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
[prop] m.size ≤ m.indices[a]
[prop] a ∈ m
[eqc] Equivalence classes
[eqc] {Membership.mem, fun m a => a ∈ m}
[ematch] E-matching patterns
[thm] HashMap.contains_iff_mem: [@Membership.mem #5 (HashMap _ #4 #3 #2) _ #1 #0]
[cutsat] Assignment satisfying linear constraints
[assign] m.size := 0
[assign] m.indices[a] := 0

An immediate problem we can see here is that grind does not yet know that a ∈ m is the same as a ∈ m.indices. Let's add this fact:

@[local grind =] private theorem mem_indices_of_mem
    {m : IndexMap α β} {a : α} :
    a ∈ m ↔ a ∈ m.indices := Iff.rfl

However this proof is going to work, we know the following:

It must use the well-formedness condition of the map.
It can't do so without relating m.indices[a] and m.indices[a]? (because the later is what appears in the well-formedness condition).
The expected relationship there doesn't even hold unless the map m.indices satisfies LawfulGetElem, for which we need instances of LawfulBEq α and LawfulHashable α.

Let's configure things so that those are available:

variable [LawfulBEq α] [LawfulHashable α]

attribute [local grind _=_] IndexMap.WF

and then give grind one manual hint, to relate m.indices[a] and m.indices[a]?:

private theorem getElem_indices_lt {h : a ∈ m} : m.indices[a] < m.size := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βa:αinst✝¹:LawfulBEq αinst✝:LawfulHashable αh:a ∈ m⊢ m.indices[a] < m.size
  have : m.indices[a]? = some m.indices[a] := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βa:αinst✝¹:LawfulBEq αinst✝:LawfulHashable αh:a ∈ m⊢ m.indices[a] < m.size grindAll goals completed! 🐙
  grindAll goals completed! 🐙

With that theorem proved, we want to make it accessible to grind. We could either add @[grind] before the theorem statement, or write attribute [local grind] getElem_indices_lt after the theorem statement. These will use grind's built-in heuristics for deciding a pattern to match the theorem on.

In this case, let's see which patterns the grind attribute generates:

attribute [local 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]grind] getElem_indices_lt

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]

These patterns are not useful. The first is matching on the entire conclusion of the theorem (in fact, a normalized version of it, in which x < y has been replaced by x + 1 ≤ y). The second is too general: it will match any term that includes the theorem's assumptions, ignoring the conclusion.

We want something more general than the entire conclusion, the conclusion should not be ignored. We'd like this theorem to fire whenever grind sees m.indices[a], and so instead of using the attribute we write a custom pattern:

grind_pattern getElem_indices_lt => m.indices[a]

The Lean standard library uses the get_elem_tactic tactic as an auto-parameter for the xs[i] notation (which desugars to GetElem.getElem xs i h, with the proof h generated by get_elem_tactic). We'd like to not only have grind fill in these proofs, but even to be able to omit these proofs. To achieve this, we add the line

macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)

(In later versions of Lean this may be part of the built-in behavior.)

We can now return to constructing our GetElem? instance. In order to use the well-formedness condition, grind must be able to unfold size:

attribute [local grind] size

The local modifier restricts this unfolding to the current file. With this in place, we can simply write:

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

with neither any sorrys, nor any explicitly written proofs.

Next, we want to expose the content of these definitions, but only locally in this file:

@[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

Again we're using the @[local grind =] private theorem pattern to hide these implementation details, but allow grind to see these facts locally.

Next, we want to prove the LawfulGetElem instance, and hope that grind can fill in the proofs:

instance : LawfulGetElem (IndexMap α β) α β (fun m a => a ∈ m) where
  getElem?_def := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βa:αb:βi:Natinst✝¹:LawfulBEq αinst✝:LawfulHashable α⊢ ∀ (c : IndexMap α β) (i : α) [inst : Decidable (i ∈ c)], c[i]? = if h : i ∈ c then some c[i] else none grindAll goals completed! 🐙
  getElem!_def := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βa:αb:βi:Natinst✝¹:LawfulBEq αinst✝:LawfulHashable α⊢ ∀ [inst : Inhabited β] (c : IndexMap α β) (i : α),
  c[i]! =
    match c[i]? with
    | some e => e
    | none => default grindAll goals completed! 🐙

Success!

Let's press onward, and see if we can define insert without having to write any proofs:

@[inline] def insert [LawfulBEq α] (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 }

In both branches, grind is automatically proving both the size_keys' and WF fields! Note also in the first branch the set calls m.keys.set i a and m.values.set i b are having their “in-bounds” obligations automatically filled in by grind via the get_elem_tactic auto-parameter.

Next let's try eraseSwap:

@[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
      could not synthesize default value for field 'WF' of 'IndexMap' using tactics`grind` failed
grind.1.1.2.2.1.1.1α:Type uβ:Type vinst:BEq αinst_1:Hashable αm_1:IndexMap α βa_1:αb:βi_1:Natinst_2:LawfulBEq αinst_3:LawfulHashable αm:IndexMap α βa:αi:Nath:m.indices[a]? = some iw:¬i = m.size - 1lastKey:α := m.keys.back ⋯lastValue:β := m.values.back ⋯i_2:Nata_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_2h_2:-1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0left:(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some a_2right:¬((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2h_4:¬i = i_2left_1:¬m.keys[i_2]? = some aright_1:¬m.indices[a]? = some i_2h_6:(m.keys.back ⋯ == a_2) = trueh_7:i + 1 ≤ m.keys.pop.sizeleft_2:a_2 ∈ m.indices.erase aleft_3:(a == a_2) = falseright_3:a_2 ∈ m.indices⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] LawfulBEq α
[prop] LawfulHashable α
[prop] m.indices[a]? = some i
[prop] ¬i = m.size - 1
[prop] ↑(m.size - 1) = if -1 * ↑m.size + 1 ≤ 0 then ↑m.size + -1 else 0
[prop] ((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
[prop] ¬a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i → ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = none
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] ¬a ∈ m.indices → m.indices[a]? = none
[prop] ∀ (h_9 : a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i),
      ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]
[prop] ∀ (h_9 : i_2 + 1 ≤ (m.keys.pop.set i (m.keys.back ⋯) ⋯).size),
      (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] ∀ (h : a ∈ m.indices), m.indices[a]? = some m.indices[a]
[prop] (m.keys[i]? = some a) = (m.indices[a]? = some i)
[prop] (m.keys[i_2]? = some a) = (m.indices[a]? = some i_2)
[prop] m.size = m.values.size
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = if i = i_2 then some (m.keys.back ⋯) else m.keys.pop[i_2]?
[prop] m.keys.pop.set i (m.keys.back ⋯) ⋯ = (m.keys.set i (m.keys.back ⋯) ⋯).pop
[prop] m.keys.back ⋯ = m.keys[m.keys.size - 1]
[prop] ↑(m.keys.size - 1) = if -1 * ↑m.keys.size + 1 ≤ 0 then ↑m.keys.size + -1 else 0
[prop] m.keys.size = m.size
[prop] m.keys.pop.size = m.keys.size - 1
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? =
      if (m.keys.back ⋯ == a_2) = true then some i else (m.indices.erase a)[a_2]?
[prop] m.keys.size ≤ i_2 → m.keys[i_2]? = none
[prop] m.keys.size ≤ i → m.keys[i]? = none
[prop] ∀ (h : i_2 + 1 ≤ m.keys.size), m.keys[i_2]? = some m.keys[i_2]
[prop] ∀ (h : i + 1 ≤ m.keys.size), m.keys[i]? = some m.keys[i]
[prop] (m.indices.contains a = true) = (a ∈ m.indices)
[prop] (((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true) =
      (a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i)
[prop] (m.keys[m.indices[a]]? = some a) = (m.indices[a]? = some m.indices[a])
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).pop[i_2]? =
      if i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size - 1 then (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? else none
[prop] ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) =
      if -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0 then ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1 else 0
[prop] ∀ (h_9 : i + 1 ≤ m.keys.pop.size), m.keys.pop.set i (m.keys.back ⋯) ⋯ = (m.keys.set i (m.keys.back ⋯) ⋯).pop
[prop] (m.keys[i_2]? = some a_2) = (m.indices[a_2]? = some i_2)
[prop] (m.keys[i]? = some a_2) = (m.indices[a_2]? = some i)
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] m.keys.size ≤ i_2 → m.keys[i_2]? = none
[prop] m.keys.size ≤ i → m.keys[i]? = none
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).pop.size = (m.keys.set i (m.keys.back ⋯) ⋯).size - 1
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size = m.keys.pop.size
[prop] (a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i) = (m.keys.back ⋯ = a_2 ∨ a_2 ∈ m.indices.erase a)
[prop] ∀ (h : a ∈ m), m.indices[a] + 1 ≤ m.size
[prop] ¬a_2 ∈ m.indices → m.indices[a_2]? = none
[prop] ∀ (h : a_2 ∈ m.indices), m.indices[a_2]? = some m.indices[a_2]
[prop] ((m.indices.erase a).contains a_2 = true) = (a_2 ∈ m.indices.erase a)
[prop] (m.keys[m.indices[a]]? = some a_2) = (m.indices[a_2]? = some m.indices[a])
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size = m.keys.size
[prop] (a_2 ∈ m.indices.erase a) = ((a == a_2) = false ∧ a_2 ∈ m.indices)
[prop] (((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true) =
      (m.keys.back ⋯ = a_2 ∨ (m.indices.erase a).contains a_2 = true)
[prop] (a ∈ m) = (a ∈ m.indices)
[prop] (m.indices.contains a_2 = true) = (a_2 ∈ m.indices)
[facts] 40 more entries...
[prop] (m.keys[i]? = some m.keys[i]) = (m.indices[m.keys[i]]? = some i)
[prop] (m.keys[i_2]? = some m.keys[i]) = (m.indices[m.keys[i]]? = some i_2)
[prop] ((m.indices.erase a).contains a_2 = true) = ((!a == a_2) = true ∧ m.indices.contains a_2 = true)
[prop] -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some a_2
[prop] ¬((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] ∀ (h_9 : i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size),
      (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = if i = i_2 then some (m.keys.back ⋯) else m.keys[i_2]?
[prop] (m.keys[i]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]) =
      (m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i)
[prop] (m.keys[i]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some i)
[prop] (m.keys[i_2]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some i_2)
[prop] (m.keys[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]) =
      (m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i_2)
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2] = if i = i_2 then m.keys.back ⋯ else m.keys.pop[i_2]
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).pop[i_2] = (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] ¬m.keys[i_2] ∈ m.indices → m.indices[m.keys[i_2]]? = none
[prop] ∀ (h_9 : m.keys[i_2] ∈ m.indices), m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]]
[prop] (m.keys[m.indices[a]]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some m.indices[a])
[prop] (m.keys.set i (m.keys.back ⋯) ⋯)[i_2] = if i = i_2 then m.keys.back ⋯ else m.keys[i_2]
[prop] (m.indices.contains m.keys[i_2] = true) = (m.keys[i_2] ∈ m.indices)
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]])
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some a_2) = (m.indices[a_2]? = some m.indices[m.keys[i_2]])
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some a) = (m.indices[a]? = some m.indices[m.keys[i_2]])
[prop] ∀ (h_9 : m.keys[i_2] ∈ m), m.indices[m.keys[i_2]] + 1 ≤ m.size
[prop] (m.keys[i_2] ∈ m) = (m.keys[i_2] ∈ m.indices)
[prop] ¬i = i_2
[prop] m.keys.pop.size ≤ i_2 → m.keys.pop[i_2]? = none
[prop] ∀ (h : i_2 + 1 ≤ m.keys.pop.size), m.keys.pop[i_2]? = some m.keys.pop[i_2]
[prop] m.keys.pop[i_2]? = if i_2 + 1 ≤ m.keys.size - 1 then m.keys[i_2]? else none
[prop] m.keys.pop.size ≤ i_2 → m.keys.pop[i_2]? = none
[prop] m.keys.pop[i_2] = m.keys[i_2]
[prop] ¬m.keys[i_2]? = some a
[prop] ¬m.indices[a]? = some i_2
[prop] (m.keys.back ⋯ == a_2) = true
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2] =
      if h₂ : (m.keys.back ⋯ == a_2) = true then i else (m.indices.erase a)[a_2]
[prop] i + 1 ≤ m.keys.pop.size
[prop] a_2 ∈ m.indices.erase a
[prop] (a == a_2) = false
[prop] a_2 ∈ m.indices
[eqc] True propositions
[prop] ¬((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2
[prop] LawfulBEq α
[prop] ((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
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some a_2
[prop] LawfulHashable α
[prop] -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0
[prop] -1 * ↑m.keys.size + 1 ≤ 0
[prop] -1 * ↑m.size + 1 ≤ 0
[prop] i < m.keys.pop.size
[prop] 0 < m.keys.size
[prop] (m.keys[i]? = some a) = (m.indices[a]? = some i)
[prop] (m.keys[i_2]? = some a) = (m.indices[a]? = some i_2)
[prop] (m.keys.back ⋯ == a_2) = true
[prop] m.indices[a]? = some i
[prop] m.indices[a]? = some m.indices[a]
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] m.keys[i]? = some a
[prop] i_2 + 1 ≤ (m.keys.pop.set i (m.keys.back ⋯) ⋯).size
[prop] i < m.keys.size
[prop] i_2 < (m.keys.pop.set i (m.keys.back ⋯) ⋯).size
[prop] m.keys.size - 1 < m.keys.size
[prop] a ∈ m.indices
[prop] a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i
[prop] ¬a ∈ m.indices → m.indices[a]? = none
[prop] ¬a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i → ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = none
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] ∀ (h_9 : i_2 + 1 ≤ (m.keys.pop.set i (m.keys.back ⋯) ⋯).size),
      (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] ∀ (h : a ∈ m.indices), m.indices[a]? = some m.indices[a]
[prop] ∀ (h_9 : a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i),
      ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]
[prop] m.keys.back ⋯ = a_2 ∨ a_2 ∈ m.indices.erase a
[prop] (m.indices.contains a = true) = (a ∈ m.indices)
[prop] (((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true) =
      (a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i)
[prop] (m.keys[i]? = some a_2) = (m.indices[a_2]? = some i)
[prop] (m.keys[i]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]) =
      (m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i)
[prop] (m.keys[i_2]? = some a_2) = (m.indices[a_2]? = some i_2)
[prop] (m.keys[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]) =
      (m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i_2)
[prop] (m.keys[m.indices[a]]? = some a) = (m.indices[a]? = some m.indices[a])
[prop] (a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i) = (m.keys.back ⋯ = a_2 ∨ a_2 ∈ m.indices.erase a)
[prop] m.indices.contains a = true
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true
[prop] m.indices[a_2]? = some i_2
[prop] m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i_2
[prop] m.keys.back ⋯ = a_2
[prop] m.keys.pop.set i (m.keys.back ⋯) ⋯ = (m.keys.set i (m.keys.back ⋯) ⋯).pop
[prop] m.keys.pop[i_2]? = some m.keys.pop[i_2]
[prop] m.keys[i]? = some m.keys[i]
[prop] m.keys[i_2]? = some a_2
[prop] m.keys[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] m.keys[i_2]? = some m.keys[i_2]
[eqc] 67 more entries...
[prop] m.keys[m.indices[a]]? = some a
[prop] i + 1 ≤ m.keys.pop.size
[prop] i + 1 ≤ m.keys.size
[prop] i_2 + 1 ≤ m.keys.pop.size
[prop] i_2 + 1 ≤ m.keys.size
[prop] i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size - 1
[prop] i_2 + 1 ≤ m.keys.size - 1
[prop] m.indices[a] + 1 ≤ m.size
[prop] i_2 < (m.keys.set i (m.keys.back ⋯) ⋯).pop.size
[prop] i_2 < m.keys.pop.size
[prop] i_2 < m.keys.size
[prop] a_2 ∈ m.indices.erase a
[prop] a ∈ m
[prop] m.keys.pop.size ≤ i_2 → m.keys.pop[i_2]? = none
[prop] m.keys.size ≤ i → m.keys[i]? = none
[prop] m.keys.size ≤ i_2 → m.keys[i_2]? = none
[prop] ∀ (h_9 : i + 1 ≤ m.keys.pop.size), m.keys.pop.set i (m.keys.back ⋯) ⋯ = (m.keys.set i (m.keys.back ⋯) ⋯).pop
[prop] ∀ (h : i + 1 ≤ m.keys.size), m.keys[i]? = some m.keys[i]
[prop] ∀ (h : i_2 + 1 ≤ m.keys.pop.size), m.keys.pop[i_2]? = some m.keys.pop[i_2]
[prop] ∀ (h : i_2 + 1 ≤ m.keys.size), m.keys[i_2]? = some m.keys[i_2]
[prop] ∀ (h : a ∈ m), m.indices[a] + 1 ≤ m.size
[prop] (a == a_2) = false ∧ a_2 ∈ m.indices
[prop] m.keys.back ⋯ = a_2 ∨ (m.indices.erase a).contains a_2 = true
[prop] ((m.indices.erase a).contains a_2 = true) = (a_2 ∈ m.indices.erase a)
[prop] (((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true) =
      (m.keys.back ⋯ = a_2 ∨ (m.indices.erase a).contains a_2 = true)
[prop] (m.keys[i]? = some m.keys[i]) = (m.indices[m.keys[i]]? = some i)
[prop] (m.keys[i]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some i)
[prop] (m.keys[i_2]? = some m.keys[i]) = (m.indices[m.keys[i]]? = some i_2)
[prop] (m.keys[i_2]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some i_2)
[prop] (m.keys[m.indices[a]]? = some a_2) = (m.indices[a_2]? = some m.indices[a])
[prop] (a_2 ∈ m.indices.erase a) = ((a == a_2) = false ∧ a_2 ∈ m.indices)
[prop] (a ∈ m) = (a ∈ m.indices)
[prop] (a == a_2) = false
[prop] (m.indices.erase a).contains a_2 = true
[prop] m.indices[a_2]? = some m.indices[a_2]
[prop] m.indices[m.keys[i]]? = some i
[prop] m.indices[m.keys[i_2]]? = some i_2
[prop] (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size
[prop] i_2 < (m.keys.set i (m.keys.back ⋯) ⋯).size
[prop] a_2 ∈ m.indices
[prop] ¬a_2 ∈ m.indices → m.indices[a_2]? = none
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] ∀ (h_9 : i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size),
      (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] ∀ (h : a_2 ∈ m.indices), m.indices[a_2]? = some m.indices[a_2]
[prop] (!a == a_2) = true ∧ m.indices.contains a_2 = true
[prop] (m.indices.contains a_2 = true) = (a_2 ∈ m.indices)
[prop] ((m.indices.erase a).contains a_2 = true) = ((!a == a_2) = true ∧ m.indices.contains a_2 = true)
[prop] (m.keys[m.indices[a]]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some m.indices[a])
[prop] (!a == a_2) = true
[eqc] 17 more entries...
[prop] m.indices.contains a_2 = true
[prop] m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]]
[prop] m.keys[i_2] ∈ m.indices
[prop] ¬m.keys[i_2] ∈ m.indices → m.indices[m.keys[i_2]]? = none
[prop] ∀ (h_9 : m.keys[i_2] ∈ m.indices), m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]]
[prop] (m.indices.contains m.keys[i_2] = true) = (m.keys[i_2] ∈ m.indices)
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some a) = (m.indices[a]? = some m.indices[m.keys[i_2]])
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some a_2) = (m.indices[a_2]? = some m.indices[m.keys[i_2]])
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]])
[prop] m.indices.contains m.keys[i_2] = true
[prop] m.indices[a_2]? = some m.indices[m.keys[i_2]]
[prop] m.keys[m.indices[m.keys[i_2]]]? = some a_2
[prop] m.keys[m.indices[m.keys[i_2]]]? = some m.keys[i_2]
[prop] m.indices[m.keys[i_2]] + 1 ≤ m.size
[prop] m.keys[i_2] ∈ m
[prop] ∀ (h_9 : m.keys[i_2] ∈ m), m.indices[m.keys[i_2]] + 1 ≤ m.size
[prop] (m.keys[i_2] ∈ m) = (m.keys[i_2] ∈ m.indices)
[eqc] False propositions
[prop] i = m.size - 1
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2
[prop] a = a_2
[prop] ¬a ∈ m.indices
[prop] ¬a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i
[prop] i = i_2
[prop] m.indices[a]? = none
[prop] m.indices[a]? = some i_2
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = none
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] m.keys[i_2]? = some a
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size ≤ i_2
[prop] m.indices[a_2]? = some i
[prop] m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i
[prop] m.keys.pop[i_2]? = none
[prop] m.keys[i]? = none
[prop] m.keys[i]? = some a_2
[prop] m.keys[i]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] m.keys[i_2]? = none
[prop] m.keys.pop.size ≤ i_2
[prop] m.keys.size ≤ i
[prop] m.keys.size ≤ i_2
[prop] ¬a_2 ∈ m.indices
[prop] m.indices[a_2]? = none
[prop] m.indices[a_2]? = some m.indices[a]
[prop] m.indices[m.keys[i]]? = some i_2
[prop] m.indices[m.keys[i_2]]? = some i
[prop] (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] m.keys[i]? = some m.keys[i_2]
[prop] m.keys[i_2]? = some m.keys[i]
[prop] m.keys[m.indices[a]]? = some a_2
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size ≤ i_2
[prop] ¬m.keys[i_2] ∈ m.indices
[prop] m.indices[m.keys[i_2]]? = none
[prop] m.indices[m.keys[i_2]]? = some m.indices[a]
[prop] m.keys[m.indices[a]]? = some m.keys[i_2]
[prop] m.indices[a]? = some m.indices[m.keys[i_2]]
[prop] m.keys[m.indices[m.keys[i_2]]]? = some a
[eqc] Equivalence classes
[eqc] {a, m.keys[i]}
[eqc] {i, m.indices[a], ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2], m.indices[a]}
[eqc] {if h₂ : (m.keys.back ⋯ == a_2) = true then i else (m.indices.erase a)[a_2]}
[eqc] {i_2, m.indices[a_2], m.indices[m.keys[i_2]], m.indices[m.keys[i_2]]}
[eqc] {a_2,
    m.keys.back ⋯,
    (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2],
    m.keys[m.keys.size - 1],
    (m.keys.set i (m.keys.back ⋯) ⋯).pop[i_2],
    m.keys.pop[i_2],
    m.keys[i_2],
    (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]}
[eqc] {if i = i_2 then m.keys.back ⋯ else m.keys.pop[i_2], if i = i_2 then m.keys.back ⋯ else m.keys[i_2]}
[eqc] {false, a == a_2}
[eqc] {true,
    m.keys.back ⋯ == a_2,
    m.indices.contains a,
    ((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2,
    (m.indices.erase a).contains a_2,
    !a == a_2,
    m.indices.contains a_2,
    m.indices.contains m.keys[i_2]}
[eqc] {m.keys.pop.size,
    m.size - 1,
    (m.keys.pop.set i (m.keys.back ⋯) ⋯).size,
    m.keys.size - 1,
    (m.keys.set i (m.keys.back ⋯) ⋯).pop.size,
    (m.keys.set i (m.keys.back ⋯) ⋯).size - 1}
[eqc] {m.keys.size, m.size, m.values.size, (m.keys.set i (m.keys.back ⋯) ⋯).size}
[eqc] {some i,
    m.indices[a]?,
    ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]?,
    some m.indices[a],
    some ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2],
    m.indices[m.keys[i]]?}
[eqc] {if (m.keys.back ⋯ == a_2) = true then some i else (m.indices.erase a)[a_2]?}
[eqc] {some i_2,
    m.indices[a_2]?,
    m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]?,
    some m.indices[a_2],
    m.indices[m.keys[i_2]]?,
    some m.indices[m.keys[i_2]]}
[eqc] {some a_2,
    (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]?,
    some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2],
    m.keys.pop[i_2]?,
    m.keys[i_2]?,
    some m.keys.pop[i_2],
    some m.keys[i_2],
    (m.keys.set i (m.keys.back ⋯) ⋯).pop[i_2]?,
    (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]?,
    some (m.keys.set i (m.keys.back ⋯) ⋯)[i_2],
    m.keys[m.indices[m.keys[i_2]]]?}
[eqc] {if i = i_2 then some (m.keys.back ⋯) else m.keys.pop[i_2]?,
    if i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size - 1 then (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? else none,
    if i_2 + 1 ≤ m.keys.size - 1 then m.keys[i_2]? else none,
    if i = i_2 then some (m.keys.back ⋯) else m.keys[i_2]?}
[eqc] {Membership.mem, fun m a => a ∈ m}
[eqc] {m.keys.pop.set i (m.keys.back ⋯) ⋯, (m.keys.set i (m.keys.back ⋯) ⋯).pop}
[eqc] {some a, m.keys[i]?, some m.keys[i], m.keys[m.indices[a]]?}
[eqc] {i_2 + 1, m.indices[m.keys[i_2]] + 1}
[eqc] {i + 1, m.indices[a] + 1}
[eqc] others
[eqc] {↑(m.size - 1), ↑(m.keys.size - 1), ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1)}
[eqc] {↑i, ↑m.indices[a]}
[eqc] {↑i_2, ↑m.indices[m.keys[i_2]]}
[eqc] {↑m.keys.pop.size,
    ↑(m.keys.pop.set i (m.keys.back ⋯) ⋯).size,
    ↑(m.size - 1),
    if -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0 then ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1 else 0,
    if -1 * ↑m.keys.size + 1 ≤ 0 then ↑m.keys.size + -1 else 0,
    if -1 * ↑m.size + 1 ≤ 0 then ↑m.size + -1 else 0,
    ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1,
    ↑m.keys.size + -1,
    ↑m.size + -1,
    ↑(m.keys.size - 1),
    ↑(m.keys.set i (m.keys.back ⋯) ⋯).pop.size,
    ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1)}
[eqc] {↑(m.keys.set i (m.keys.back ⋯) ⋯).size, ↑m.keys.size, ↑m.size}
[eqc] {-1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1, -1 * ↑m.keys.size + 1, -1 * ↑m.size + 1}
[eqc] {-1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size, -1 * ↑m.keys.size, -1 * ↑m.size}
[cases] Case analyses
[cases] [1/2]: if -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0 then ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1 else 0
[cases] source: E-matching `Array.getElem?_pop`
[cases] [1/2]: ((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
[cases] source: Initial goal
[cases] [2/2]: if i = i_2 then some (m.keys.back ⋯) else m.keys.pop[i_2]?
[cases] source: E-matching `Array.getElem?_set`
[cases] [2/2]: (m.keys[i_2]? = some a) = (m.indices[a]? = some i_2)
[cases] source: E-matching `WF`
[cases] [1/2]: if (m.keys.back ⋯ == a_2) = true then some i else (m.indices.erase a)[a_2]?
[cases] source: E-matching `HashMap.getElem?_insert`
[cases] [1/2]: i + 1 ≤ m.keys.pop.size
[cases] source: E-matching `Array.set_pop`
[cases] [1/2]: (a_2 ∈ m.indices.erase a) = ((a == a_2) = false ∧ a_2 ∈ m.indices)
[cases] source: E-matching `HashMap.mem_erase`
[ematch] E-matching patterns
[thm] getElem?_neg: [@getElem? #8 #7 #6 #5 #4 #2 #1]
[thm] getElem?_pos: [@getElem? #8 #7 #6 #5 #4 #2 #1]
[thm] HashMap.contains_iff_mem: [@Membership.mem #5 (HashMap _ #4 #3 #2) _ #1 #0]
[thm] WF: [@getElem? (HashMap #6 `[Nat] #4 #3) _ `[Nat] _ _ (@indices _ #5 _ _ #2) #0, @some `[Nat] #1]
[thm] size.eq_1: [@size #4 #3 #2 #1 #0]
[thm] Option.some_le_some: [@LE.le (Option #3) _ (@some _ #1) (@some _ #0)]
[thm] Option.mem_some: [@Membership.mem #2 (Option _) _ (@some _ #0) #1]
[thm] Array.getElem?_set: [@getElem? (Array #5) `[Nat] _ _ _ (@Array.set _ #4 #3 #1 #2) #0]
[thm] Array.mem_or_eq_of_mem_set: [@Membership.mem #6 (Array _) _ (@Array.set _ #5 #4 #2 _) #3]
[thm] Array.set_pop: [@Array.set #4 (@Array.pop _ #3) #1 #2 #0]
[thm] Array.getElem?_pop: [@getElem? (Array #2) `[Nat] _ _ _ (@Array.pop _ #1) #0]
[thm] Array.set_pop: [@Array.pop #4 (@Array.set _ #3 #1 #2 _)]
[thm] WF: [@getElem? (Array #6) `[Nat] _ _ _ (@keys _ #5 #4 #3 #2) #1, @some _ #0]
[thm] Array.back_eq_getElem: [@Array.back #2 #1 #0]
[thm] Option.some_lt_some: [@LT.lt (Option #3) _ (@some _ #1) (@some _ #0)]
[thm] Array.size_pos_of_mem: [@Membership.mem #3 (Array _) _ #1 #2, @Array.size _ #1]
[thm] size_keys: [@Array.size #4 (@keys _ #3 #2 #1 #0)]
[thm] Array.getElem?_eq_none: [@Array.size #3 #1, @getElem? (Array _) `[Nat] _ _ _ #1 #2]
[thm] Array.size_pop: [@Array.size #1 (@Array.pop _ #0)]
[thm] Array.size_set: [@Array.size #4 (@Array.set _ #3 #2 #1 #0)]
[thm] HashMap.mem_insert: [@Membership.mem #9 (HashMap _ #8 #7 #6) _ (@HashMap.insert _ _ #7 #6 #5 #2 #0) #1]
[thm] HashMap.getElem?_insert: [@getElem? (HashMap #9 #8 #7 #6) _ _ _ _ (@HashMap.insert _ _ #7 #6 #5 #2 #0) #1]
[thm] HashMap.mem_erase: [@Membership.mem #8 (HashMap _ #7 #6 #5) _ (@HashMap.erase _ _ #6 #5 #4 #1) #0]
[thm] HashMap.getElem?_erase: [@getElem? (HashMap #8 #7 #6 #5) _ _ _ _ (@HashMap.erase _ _ #6 #5 #4 #1) #0]
[thm] Option.not_lt_none: [@LT.lt (Option #2) _ #0 (@none _)]
[thm] Option.none_lt_some: [@LT.lt (Option #2) _ (@none _) (@some _ #0)]
[thm] Option.not_mem_none: [@Membership.mem #1 (Option _) _ (@none _) #0]
[thm] Option.not_some_le_none: [@LE.le (Option #2) _ (@some _ #0) (@none _)]
[thm] Option.none_le: [@LE.le (Option #2) _ (@none _) #0]
[thm] Array.getElem_mem: [@Membership.mem #3 (Array _) _ #2 (@getElem (Array _) `[Nat] _ _ _ #2 #1 _)]
[thm] getElem_indices_lt: [@getElem (HashMap #8 `[Nat] #6 #5) _ `[Nat] _ _ (@indices _ #7 _ _ #4) #3 _]
[thm] HashMap.getElem_erase: [@getElem (HashMap #9 #8 #7 #6) _ _ _ _ (@HashMap.erase _ _ #7 #6 #5 #2) #1 #0]
[thm] HashMap.getElem_insert: [@getElem (HashMap #10 #9 #8 #7) _ _ _ _ (@HashMap.insert _ _ #8 #7 #6 #3 #1) #2 #0]
[thm] Array.getElem_set: [@getElem (Array #6) `[Nat] _ _ _ (@Array.set _ #5 #4 #2 #3) #1 #0]
[thm] Array.getElem_pop: [@getElem (Array #3) `[Nat] _ _ _ (@Array.pop _ #2) #1 #0]
[thm] Option.some_beq_some: [@BEq.beq (Option #3) _ (@some _ #1) (@some _ #0)]
[thm] Option.some_beq_none: [@BEq.beq (Option #2) _ (@some _ #0) (@none _)]
[thm] Option.none_beq_some: [@BEq.beq (Option #2) _ (@none _) (@some _ #0)]
[thm] Option.none_beq_none: [@BEq.beq (Option #1) _ (@none _) (@none _)]
[thm] HashMap.contains_erase: [@HashMap.contains #8 #7 #6 #5 (@HashMap.erase _ _ #6 #5 #4 #1) #0]
[thm] HashMap.contains_insert: [@HashMap.contains #9 #8 #7 #6 (@HashMap.insert _ _ #7 #6 #5 #2 #0) #1]
[thm] HashMap.contains_iff_mem: [@HashMap.contains #5 #4 #3 #2 #1 #0, true]
[thm] getElem_def: [@getElem (IndexMap #8 #7 #6 #5) _ _ _ _ #2 #1 #0]
[thm] mem_indices_of_mem: [@Membership.mem #5 (IndexMap _ #4 #3 #2) _ #1 #0]
[thm] getElem?_def: [@getElem? (IndexMap #7 #6 #5 #4) _ _ _ _ #1 #0]
[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
[ring] Rings
[ring] Ring `Int`
[basis] Basis
[_] ↑m.size + -1 * ↑m.keys.size = 0
[_] ↑m.keys.size + -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size = 0
[_] ↑i + -1 * ↑m.indices[a] = 0
[_] ↑m.keys.pop.size + -1 * ↑(m.keys.size - 1) = 0
[_] ↑(m.keys.pop.set i (m.keys.back ⋯) ⋯).size + -1 * ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) = 0
[_] ↑i_2 + -1 * ↑m.indices[m.keys[i_2]] = 0
[_] ↑(m.keys.size - 1) + -1 * ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) = 0
[_] ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) + -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 = 0
[_] ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).pop.size + -1 = 0
[ring] Ring `Lean.Grind.Ring.OfSemiring.Q Nat`
[basis] Basis
[_] ↑(m.keys.size - 1) + -1 * ↑(m.size - 1) = 0
[_] ↑(m.size - 1) + -1 * ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) = 0

[grind] Diagnostics
[thm] E-Matching instances
[thm] WF ↦ 16
[thm] getElem?_neg ↦ 9
[thm] getElem?_pos ↦ 9
[thm] Array.getElem?_eq_none ↦ 5
[thm] HashMap.contains_iff_mem ↦ 5
[thm] Array.getElem?_pop ↦ 2
[thm] Array.getElem?_set ↦ 2
[thm] Array.getElem_pop ↦ 2
[thm] Array.getElem_set ↦ 2
[thm] Array.set_pop ↦ 2
[thm] Array.size_pop ↦ 2
[thm] Array.size_set ↦ 2
[thm] getElem_indices_lt ↦ 2
[thm] mem_indices_of_mem ↦ 2
[thm] Array.back_eq_getElem ↦ 1
[thm] size_keys ↦ 1
[thm] size.eq_1 ↦ 1
[thm] HashMap.contains_erase ↦ 1
[thm] HashMap.contains_insert ↦ 1
[thm] HashMap.getElem?_insert ↦ 1
[thm] HashMap.getElem_insert ↦ 1
[thm] HashMap.mem_erase ↦ 1
[thm] HashMap.mem_insert ↦ 1{ 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` failed
grind.1.1.2.2.1.1.1α:Type uβ:Type vinst:BEq αinst_1:Hashable αm_1:IndexMap α βa_1:αb:βi_1:Natinst_2:LawfulBEq αinst_3:LawfulHashable αm:IndexMap α βa:αi:Nath:m.indices[a]? = some iw:¬i = m.size - 1lastKey:α := m.keys.back ⋯lastValue:β := m.values.back ⋯i_2:Nata_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_2h_2:-1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0left:(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some a_2right:¬((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2h_4:¬i = i_2left_1:¬m.keys[i_2]? = some aright_1:¬m.indices[a]? = some i_2h_6:(m.keys.back ⋯ == a_2) = trueh_7:i + 1 ≤ m.keys.pop.sizeleft_2:a_2 ∈ m.indices.erase aleft_3:(a == a_2) = falseright_3:a_2 ∈ m.indices⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] LawfulBEq α
[prop] LawfulHashable α
[prop] m.indices[a]? = some i
[prop] ¬i = m.size - 1
[prop] ↑(m.size - 1) = if -1 * ↑m.size + 1 ≤ 0 then ↑m.size + -1 else 0
[prop] ((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
[prop] ¬a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i → ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = none
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] ¬a ∈ m.indices → m.indices[a]? = none
[prop] ∀ (h_9 : a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i),
      ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]
[prop] ∀ (h_9 : i_2 + 1 ≤ (m.keys.pop.set i (m.keys.back ⋯) ⋯).size),
      (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] ∀ (h : a ∈ m.indices), m.indices[a]? = some m.indices[a]
[prop] (m.keys[i]? = some a) = (m.indices[a]? = some i)
[prop] (m.keys[i_2]? = some a) = (m.indices[a]? = some i_2)
[prop] m.size = m.values.size
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = if i = i_2 then some (m.keys.back ⋯) else m.keys.pop[i_2]?
[prop] m.keys.pop.set i (m.keys.back ⋯) ⋯ = (m.keys.set i (m.keys.back ⋯) ⋯).pop
[prop] m.keys.back ⋯ = m.keys[m.keys.size - 1]
[prop] ↑(m.keys.size - 1) = if -1 * ↑m.keys.size + 1 ≤ 0 then ↑m.keys.size + -1 else 0
[prop] m.keys.size = m.size
[prop] m.keys.pop.size = m.keys.size - 1
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? =
      if (m.keys.back ⋯ == a_2) = true then some i else (m.indices.erase a)[a_2]?
[prop] m.keys.size ≤ i_2 → m.keys[i_2]? = none
[prop] m.keys.size ≤ i → m.keys[i]? = none
[prop] ∀ (h : i_2 + 1 ≤ m.keys.size), m.keys[i_2]? = some m.keys[i_2]
[prop] ∀ (h : i + 1 ≤ m.keys.size), m.keys[i]? = some m.keys[i]
[prop] (m.indices.contains a = true) = (a ∈ m.indices)
[prop] (((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true) =
      (a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i)
[prop] (m.keys[m.indices[a]]? = some a) = (m.indices[a]? = some m.indices[a])
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).pop[i_2]? =
      if i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size - 1 then (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? else none
[prop] ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) =
      if -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0 then ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1 else 0
[prop] ∀ (h_9 : i + 1 ≤ m.keys.pop.size), m.keys.pop.set i (m.keys.back ⋯) ⋯ = (m.keys.set i (m.keys.back ⋯) ⋯).pop
[prop] (m.keys[i_2]? = some a_2) = (m.indices[a_2]? = some i_2)
[prop] (m.keys[i]? = some a_2) = (m.indices[a_2]? = some i)
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] m.keys.size ≤ i_2 → m.keys[i_2]? = none
[prop] m.keys.size ≤ i → m.keys[i]? = none
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).pop.size = (m.keys.set i (m.keys.back ⋯) ⋯).size - 1
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size = m.keys.pop.size
[prop] (a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i) = (m.keys.back ⋯ = a_2 ∨ a_2 ∈ m.indices.erase a)
[prop] ∀ (h : a ∈ m), m.indices[a] + 1 ≤ m.size
[prop] ¬a_2 ∈ m.indices → m.indices[a_2]? = none
[prop] ∀ (h : a_2 ∈ m.indices), m.indices[a_2]? = some m.indices[a_2]
[prop] ((m.indices.erase a).contains a_2 = true) = (a_2 ∈ m.indices.erase a)
[prop] (m.keys[m.indices[a]]? = some a_2) = (m.indices[a_2]? = some m.indices[a])
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size = m.keys.size
[prop] (a_2 ∈ m.indices.erase a) = ((a == a_2) = false ∧ a_2 ∈ m.indices)
[prop] (((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true) =
      (m.keys.back ⋯ = a_2 ∨ (m.indices.erase a).contains a_2 = true)
[prop] (a ∈ m) = (a ∈ m.indices)
[prop] (m.indices.contains a_2 = true) = (a_2 ∈ m.indices)
[facts] 40 more entries...
[prop] (m.keys[i]? = some m.keys[i]) = (m.indices[m.keys[i]]? = some i)
[prop] (m.keys[i_2]? = some m.keys[i]) = (m.indices[m.keys[i]]? = some i_2)
[prop] ((m.indices.erase a).contains a_2 = true) = ((!a == a_2) = true ∧ m.indices.contains a_2 = true)
[prop] -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some a_2
[prop] ¬((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] ∀ (h_9 : i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size),
      (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = if i = i_2 then some (m.keys.back ⋯) else m.keys[i_2]?
[prop] (m.keys[i]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]) =
      (m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i)
[prop] (m.keys[i]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some i)
[prop] (m.keys[i_2]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some i_2)
[prop] (m.keys[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]) =
      (m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i_2)
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2] = if i = i_2 then m.keys.back ⋯ else m.keys.pop[i_2]
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).pop[i_2] = (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] ¬m.keys[i_2] ∈ m.indices → m.indices[m.keys[i_2]]? = none
[prop] ∀ (h_9 : m.keys[i_2] ∈ m.indices), m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]]
[prop] (m.keys[m.indices[a]]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some m.indices[a])
[prop] (m.keys.set i (m.keys.back ⋯) ⋯)[i_2] = if i = i_2 then m.keys.back ⋯ else m.keys[i_2]
[prop] (m.indices.contains m.keys[i_2] = true) = (m.keys[i_2] ∈ m.indices)
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]])
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some a_2) = (m.indices[a_2]? = some m.indices[m.keys[i_2]])
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some a) = (m.indices[a]? = some m.indices[m.keys[i_2]])
[prop] ∀ (h_9 : m.keys[i_2] ∈ m), m.indices[m.keys[i_2]] + 1 ≤ m.size
[prop] (m.keys[i_2] ∈ m) = (m.keys[i_2] ∈ m.indices)
[prop] ¬i = i_2
[prop] m.keys.pop.size ≤ i_2 → m.keys.pop[i_2]? = none
[prop] ∀ (h : i_2 + 1 ≤ m.keys.pop.size), m.keys.pop[i_2]? = some m.keys.pop[i_2]
[prop] m.keys.pop[i_2]? = if i_2 + 1 ≤ m.keys.size - 1 then m.keys[i_2]? else none
[prop] m.keys.pop.size ≤ i_2 → m.keys.pop[i_2]? = none
[prop] m.keys.pop[i_2] = m.keys[i_2]
[prop] ¬m.keys[i_2]? = some a
[prop] ¬m.indices[a]? = some i_2
[prop] (m.keys.back ⋯ == a_2) = true
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2] =
      if h₂ : (m.keys.back ⋯ == a_2) = true then i else (m.indices.erase a)[a_2]
[prop] i + 1 ≤ m.keys.pop.size
[prop] a_2 ∈ m.indices.erase a
[prop] (a == a_2) = false
[prop] a_2 ∈ m.indices
[eqc] True propositions
[prop] ¬((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2
[prop] LawfulBEq α
[prop] ((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
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some a_2
[prop] LawfulHashable α
[prop] -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0
[prop] -1 * ↑m.keys.size + 1 ≤ 0
[prop] -1 * ↑m.size + 1 ≤ 0
[prop] i < m.keys.pop.size
[prop] 0 < m.keys.size
[prop] (m.keys[i]? = some a) = (m.indices[a]? = some i)
[prop] (m.keys[i_2]? = some a) = (m.indices[a]? = some i_2)
[prop] (m.keys.back ⋯ == a_2) = true
[prop] m.indices[a]? = some i
[prop] m.indices[a]? = some m.indices[a]
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] m.keys[i]? = some a
[prop] i_2 + 1 ≤ (m.keys.pop.set i (m.keys.back ⋯) ⋯).size
[prop] i < m.keys.size
[prop] i_2 < (m.keys.pop.set i (m.keys.back ⋯) ⋯).size
[prop] m.keys.size - 1 < m.keys.size
[prop] a ∈ m.indices
[prop] a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i
[prop] ¬a ∈ m.indices → m.indices[a]? = none
[prop] ¬a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i → ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = none
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] ∀ (h_9 : i_2 + 1 ≤ (m.keys.pop.set i (m.keys.back ⋯) ⋯).size),
      (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] ∀ (h : a ∈ m.indices), m.indices[a]? = some m.indices[a]
[prop] ∀ (h_9 : a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i),
      ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]
[prop] m.keys.back ⋯ = a_2 ∨ a_2 ∈ m.indices.erase a
[prop] (m.indices.contains a = true) = (a ∈ m.indices)
[prop] (((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true) =
      (a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i)
[prop] (m.keys[i]? = some a_2) = (m.indices[a_2]? = some i)
[prop] (m.keys[i]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]) =
      (m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i)
[prop] (m.keys[i_2]? = some a_2) = (m.indices[a_2]? = some i_2)
[prop] (m.keys[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]) =
      (m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i_2)
[prop] (m.keys[m.indices[a]]? = some a) = (m.indices[a]? = some m.indices[a])
[prop] (a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i) = (m.keys.back ⋯ = a_2 ∨ a_2 ∈ m.indices.erase a)
[prop] m.indices.contains a = true
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true
[prop] m.indices[a_2]? = some i_2
[prop] m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i_2
[prop] m.keys.back ⋯ = a_2
[prop] m.keys.pop.set i (m.keys.back ⋯) ⋯ = (m.keys.set i (m.keys.back ⋯) ⋯).pop
[prop] m.keys.pop[i_2]? = some m.keys.pop[i_2]
[prop] m.keys[i]? = some m.keys[i]
[prop] m.keys[i_2]? = some a_2
[prop] m.keys[i_2]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] m.keys[i_2]? = some m.keys[i_2]
[eqc] 67 more entries...
[prop] m.keys[m.indices[a]]? = some a
[prop] i + 1 ≤ m.keys.pop.size
[prop] i + 1 ≤ m.keys.size
[prop] i_2 + 1 ≤ m.keys.pop.size
[prop] i_2 + 1 ≤ m.keys.size
[prop] i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size - 1
[prop] i_2 + 1 ≤ m.keys.size - 1
[prop] m.indices[a] + 1 ≤ m.size
[prop] i_2 < (m.keys.set i (m.keys.back ⋯) ⋯).pop.size
[prop] i_2 < m.keys.pop.size
[prop] i_2 < m.keys.size
[prop] a_2 ∈ m.indices.erase a
[prop] a ∈ m
[prop] m.keys.pop.size ≤ i_2 → m.keys.pop[i_2]? = none
[prop] m.keys.size ≤ i → m.keys[i]? = none
[prop] m.keys.size ≤ i_2 → m.keys[i_2]? = none
[prop] ∀ (h_9 : i + 1 ≤ m.keys.pop.size), m.keys.pop.set i (m.keys.back ⋯) ⋯ = (m.keys.set i (m.keys.back ⋯) ⋯).pop
[prop] ∀ (h : i + 1 ≤ m.keys.size), m.keys[i]? = some m.keys[i]
[prop] ∀ (h : i_2 + 1 ≤ m.keys.pop.size), m.keys.pop[i_2]? = some m.keys.pop[i_2]
[prop] ∀ (h : i_2 + 1 ≤ m.keys.size), m.keys[i_2]? = some m.keys[i_2]
[prop] ∀ (h : a ∈ m), m.indices[a] + 1 ≤ m.size
[prop] (a == a_2) = false ∧ a_2 ∈ m.indices
[prop] m.keys.back ⋯ = a_2 ∨ (m.indices.erase a).contains a_2 = true
[prop] ((m.indices.erase a).contains a_2 = true) = (a_2 ∈ m.indices.erase a)
[prop] (((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2 = true) =
      (m.keys.back ⋯ = a_2 ∨ (m.indices.erase a).contains a_2 = true)
[prop] (m.keys[i]? = some m.keys[i]) = (m.indices[m.keys[i]]? = some i)
[prop] (m.keys[i]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some i)
[prop] (m.keys[i_2]? = some m.keys[i]) = (m.indices[m.keys[i]]? = some i_2)
[prop] (m.keys[i_2]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some i_2)
[prop] (m.keys[m.indices[a]]? = some a_2) = (m.indices[a_2]? = some m.indices[a])
[prop] (a_2 ∈ m.indices.erase a) = ((a == a_2) = false ∧ a_2 ∈ m.indices)
[prop] (a ∈ m) = (a ∈ m.indices)
[prop] (a == a_2) = false
[prop] (m.indices.erase a).contains a_2 = true
[prop] m.indices[a_2]? = some m.indices[a_2]
[prop] m.indices[m.keys[i]]? = some i
[prop] m.indices[m.keys[i_2]]? = some i_2
[prop] (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size
[prop] i_2 < (m.keys.set i (m.keys.back ⋯) ⋯).size
[prop] a_2 ∈ m.indices
[prop] ¬a_2 ∈ m.indices → m.indices[a_2]? = none
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size ≤ i_2 → (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] ∀ (h_9 : i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size),
      (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = some (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] ∀ (h : a_2 ∈ m.indices), m.indices[a_2]? = some m.indices[a_2]
[prop] (!a == a_2) = true ∧ m.indices.contains a_2 = true
[prop] (m.indices.contains a_2 = true) = (a_2 ∈ m.indices)
[prop] ((m.indices.erase a).contains a_2 = true) = ((!a == a_2) = true ∧ m.indices.contains a_2 = true)
[prop] (m.keys[m.indices[a]]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some m.indices[a])
[prop] (!a == a_2) = true
[eqc] 17 more entries...
[prop] m.indices.contains a_2 = true
[prop] m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]]
[prop] m.keys[i_2] ∈ m.indices
[prop] ¬m.keys[i_2] ∈ m.indices → m.indices[m.keys[i_2]]? = none
[prop] ∀ (h_9 : m.keys[i_2] ∈ m.indices), m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]]
[prop] (m.indices.contains m.keys[i_2] = true) = (m.keys[i_2] ∈ m.indices)
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some a) = (m.indices[a]? = some m.indices[m.keys[i_2]])
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some a_2) = (m.indices[a_2]? = some m.indices[m.keys[i_2]])
[prop] (m.keys[m.indices[m.keys[i_2]]]? = some m.keys[i_2]) = (m.indices[m.keys[i_2]]? = some m.indices[m.keys[i_2]])
[prop] m.indices.contains m.keys[i_2] = true
[prop] m.indices[a_2]? = some m.indices[m.keys[i_2]]
[prop] m.keys[m.indices[m.keys[i_2]]]? = some a_2
[prop] m.keys[m.indices[m.keys[i_2]]]? = some m.keys[i_2]
[prop] m.indices[m.keys[i_2]] + 1 ≤ m.size
[prop] m.keys[i_2] ∈ m
[prop] ∀ (h_9 : m.keys[i_2] ∈ m), m.indices[m.keys[i_2]] + 1 ≤ m.size
[prop] (m.keys[i_2] ∈ m) = (m.keys[i_2] ∈ m.indices)
[eqc] False propositions
[prop] i = m.size - 1
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = some i_2
[prop] a = a_2
[prop] ¬a ∈ m.indices
[prop] ¬a_2 ∈ (m.indices.erase a).insert (m.keys.back ⋯) i
[prop] i = i_2
[prop] m.indices[a]? = none
[prop] m.indices[a]? = some i_2
[prop] ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]? = none
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] m.keys[i_2]? = some a
[prop] (m.keys.pop.set i (m.keys.back ⋯) ⋯).size ≤ i_2
[prop] m.indices[a_2]? = some i
[prop] m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]? = some i
[prop] m.keys.pop[i_2]? = none
[prop] m.keys[i]? = none
[prop] m.keys[i]? = some a_2
[prop] m.keys[i]? = some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]
[prop] m.keys[i_2]? = none
[prop] m.keys.pop.size ≤ i_2
[prop] m.keys.size ≤ i
[prop] m.keys.size ≤ i_2
[prop] ¬a_2 ∈ m.indices
[prop] m.indices[a_2]? = none
[prop] m.indices[a_2]? = some m.indices[a]
[prop] m.indices[m.keys[i]]? = some i_2
[prop] m.indices[m.keys[i_2]]? = some i
[prop] (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? = none
[prop] m.keys[i]? = some m.keys[i_2]
[prop] m.keys[i_2]? = some m.keys[i]
[prop] m.keys[m.indices[a]]? = some a_2
[prop] (m.keys.set i (m.keys.back ⋯) ⋯).size ≤ i_2
[prop] ¬m.keys[i_2] ∈ m.indices
[prop] m.indices[m.keys[i_2]]? = none
[prop] m.indices[m.keys[i_2]]? = some m.indices[a]
[prop] m.keys[m.indices[a]]? = some m.keys[i_2]
[prop] m.indices[a]? = some m.indices[m.keys[i_2]]
[prop] m.keys[m.indices[m.keys[i_2]]]? = some a
[eqc] Equivalence classes
[eqc] {a, m.keys[i]}
[eqc] {i, m.indices[a], ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2], m.indices[a]}
[eqc] {if h₂ : (m.keys.back ⋯ == a_2) = true then i else (m.indices.erase a)[a_2]}
[eqc] {i_2, m.indices[a_2], m.indices[m.keys[i_2]], m.indices[m.keys[i_2]]}
[eqc] {a_2,
    m.keys.back ⋯,
    (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2],
    m.keys[m.keys.size - 1],
    (m.keys.set i (m.keys.back ⋯) ⋯).pop[i_2],
    m.keys.pop[i_2],
    m.keys[i_2],
    (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]}
[eqc] {if i = i_2 then m.keys.back ⋯ else m.keys.pop[i_2], if i = i_2 then m.keys.back ⋯ else m.keys[i_2]}
[eqc] {false, a == a_2}
[eqc] {true,
    m.keys.back ⋯ == a_2,
    m.indices.contains a,
    ((m.indices.erase a).insert (m.keys.back ⋯) i).contains a_2,
    (m.indices.erase a).contains a_2,
    !a == a_2,
    m.indices.contains a_2,
    m.indices.contains m.keys[i_2]}
[eqc] {m.keys.pop.size,
    m.size - 1,
    (m.keys.pop.set i (m.keys.back ⋯) ⋯).size,
    m.keys.size - 1,
    (m.keys.set i (m.keys.back ⋯) ⋯).pop.size,
    (m.keys.set i (m.keys.back ⋯) ⋯).size - 1}
[eqc] {m.keys.size, m.size, m.values.size, (m.keys.set i (m.keys.back ⋯) ⋯).size}
[eqc] {some i,
    m.indices[a]?,
    ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2]?,
    some m.indices[a],
    some ((m.indices.erase a).insert (m.keys.back ⋯) i)[a_2],
    m.indices[m.keys[i]]?}
[eqc] {if (m.keys.back ⋯ == a_2) = true then some i else (m.indices.erase a)[a_2]?}
[eqc] {some i_2,
    m.indices[a_2]?,
    m.indices[(m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]]?,
    some m.indices[a_2],
    m.indices[m.keys[i_2]]?,
    some m.indices[m.keys[i_2]]}
[eqc] {some a_2,
    (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2]?,
    some (m.keys.pop.set i (m.keys.back ⋯) ⋯)[i_2],
    m.keys.pop[i_2]?,
    m.keys[i_2]?,
    some m.keys.pop[i_2],
    some m.keys[i_2],
    (m.keys.set i (m.keys.back ⋯) ⋯).pop[i_2]?,
    (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]?,
    some (m.keys.set i (m.keys.back ⋯) ⋯)[i_2],
    m.keys[m.indices[m.keys[i_2]]]?}
[eqc] {if i = i_2 then some (m.keys.back ⋯) else m.keys.pop[i_2]?,
    if i_2 + 1 ≤ (m.keys.set i (m.keys.back ⋯) ⋯).size - 1 then (m.keys.set i (m.keys.back ⋯) ⋯)[i_2]? else none,
    if i_2 + 1 ≤ m.keys.size - 1 then m.keys[i_2]? else none,
    if i = i_2 then some (m.keys.back ⋯) else m.keys[i_2]?}
[eqc] {Membership.mem, fun m a => a ∈ m}
[eqc] {m.keys.pop.set i (m.keys.back ⋯) ⋯, (m.keys.set i (m.keys.back ⋯) ⋯).pop}
[eqc] {some a, m.keys[i]?, some m.keys[i], m.keys[m.indices[a]]?}
[eqc] {i_2 + 1, m.indices[m.keys[i_2]] + 1}
[eqc] {i + 1, m.indices[a] + 1}
[eqc] others
[eqc] {↑(m.size - 1), ↑(m.keys.size - 1), ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1)}
[eqc] {↑i, ↑m.indices[a]}
[eqc] {↑i_2, ↑m.indices[m.keys[i_2]]}
[eqc] {↑m.keys.pop.size,
    ↑(m.keys.pop.set i (m.keys.back ⋯) ⋯).size,
    ↑(m.size - 1),
    if -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0 then ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1 else 0,
    if -1 * ↑m.keys.size + 1 ≤ 0 then ↑m.keys.size + -1 else 0,
    if -1 * ↑m.size + 1 ≤ 0 then ↑m.size + -1 else 0,
    ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1,
    ↑m.keys.size + -1,
    ↑m.size + -1,
    ↑(m.keys.size - 1),
    ↑(m.keys.set i (m.keys.back ⋯) ⋯).pop.size,
    ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1)}
[eqc] {↑(m.keys.set i (m.keys.back ⋯) ⋯).size, ↑m.keys.size, ↑m.size}
[eqc] {-1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1, -1 * ↑m.keys.size + 1, -1 * ↑m.size + 1}
[eqc] {-1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size, -1 * ↑m.keys.size, -1 * ↑m.size}
[cases] Case analyses
[cases] [1/2]: if -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 ≤ 0 then ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1 else 0
[cases] source: E-matching `Array.getElem?_pop`
[cases] [1/2]: ((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
[cases] source: Initial goal
[cases] [2/2]: if i = i_2 then some (m.keys.back ⋯) else m.keys.pop[i_2]?
[cases] source: E-matching `Array.getElem?_set`
[cases] [2/2]: (m.keys[i_2]? = some a) = (m.indices[a]? = some i_2)
[cases] source: E-matching `WF`
[cases] [1/2]: if (m.keys.back ⋯ == a_2) = true then some i else (m.indices.erase a)[a_2]?
[cases] source: E-matching `HashMap.getElem?_insert`
[cases] [1/2]: i + 1 ≤ m.keys.pop.size
[cases] source: E-matching `Array.set_pop`
[cases] [1/2]: (a_2 ∈ m.indices.erase a) = ((a == a_2) = false ∧ a_2 ∈ m.indices)
[cases] source: E-matching `HashMap.mem_erase`
[ematch] E-matching patterns
[thm] getElem?_neg: [@getElem? #8 #7 #6 #5 #4 #2 #1]
[thm] getElem?_pos: [@getElem? #8 #7 #6 #5 #4 #2 #1]
[thm] HashMap.contains_iff_mem: [@Membership.mem #5 (HashMap _ #4 #3 #2) _ #1 #0]
[thm] WF: [@getElem? (HashMap #6 `[Nat] #4 #3) _ `[Nat] _ _ (@indices _ #5 _ _ #2) #0, @some `[Nat] #1]
[thm] size.eq_1: [@size #4 #3 #2 #1 #0]
[thm] Option.some_le_some: [@LE.le (Option #3) _ (@some _ #1) (@some _ #0)]
[thm] Option.mem_some: [@Membership.mem #2 (Option _) _ (@some _ #0) #1]
[thm] Array.getElem?_set: [@getElem? (Array #5) `[Nat] _ _ _ (@Array.set _ #4 #3 #1 #2) #0]
[thm] Array.mem_or_eq_of_mem_set: [@Membership.mem #6 (Array _) _ (@Array.set _ #5 #4 #2 _) #3]
[thm] Array.set_pop: [@Array.set #4 (@Array.pop _ #3) #1 #2 #0]
[thm] Array.getElem?_pop: [@getElem? (Array #2) `[Nat] _ _ _ (@Array.pop _ #1) #0]
[thm] Array.set_pop: [@Array.pop #4 (@Array.set _ #3 #1 #2 _)]
[thm] WF: [@getElem? (Array #6) `[Nat] _ _ _ (@keys _ #5 #4 #3 #2) #1, @some _ #0]
[thm] Array.back_eq_getElem: [@Array.back #2 #1 #0]
[thm] Option.some_lt_some: [@LT.lt (Option #3) _ (@some _ #1) (@some _ #0)]
[thm] Array.size_pos_of_mem: [@Membership.mem #3 (Array _) _ #1 #2, @Array.size _ #1]
[thm] size_keys: [@Array.size #4 (@keys _ #3 #2 #1 #0)]
[thm] Array.getElem?_eq_none: [@Array.size #3 #1, @getElem? (Array _) `[Nat] _ _ _ #1 #2]
[thm] Array.size_pop: [@Array.size #1 (@Array.pop _ #0)]
[thm] Array.size_set: [@Array.size #4 (@Array.set _ #3 #2 #1 #0)]
[thm] HashMap.mem_insert: [@Membership.mem #9 (HashMap _ #8 #7 #6) _ (@HashMap.insert _ _ #7 #6 #5 #2 #0) #1]
[thm] HashMap.getElem?_insert: [@getElem? (HashMap #9 #8 #7 #6) _ _ _ _ (@HashMap.insert _ _ #7 #6 #5 #2 #0) #1]
[thm] HashMap.mem_erase: [@Membership.mem #8 (HashMap _ #7 #6 #5) _ (@HashMap.erase _ _ #6 #5 #4 #1) #0]
[thm] HashMap.getElem?_erase: [@getElem? (HashMap #8 #7 #6 #5) _ _ _ _ (@HashMap.erase _ _ #6 #5 #4 #1) #0]
[thm] Option.not_lt_none: [@LT.lt (Option #2) _ #0 (@none _)]
[thm] Option.none_lt_some: [@LT.lt (Option #2) _ (@none _) (@some _ #0)]
[thm] Option.not_mem_none: [@Membership.mem #1 (Option _) _ (@none _) #0]
[thm] Option.not_some_le_none: [@LE.le (Option #2) _ (@some _ #0) (@none _)]
[thm] Option.none_le: [@LE.le (Option #2) _ (@none _) #0]
[thm] Array.getElem_mem: [@Membership.mem #3 (Array _) _ #2 (@getElem (Array _) `[Nat] _ _ _ #2 #1 _)]
[thm] getElem_indices_lt: [@getElem (HashMap #8 `[Nat] #6 #5) _ `[Nat] _ _ (@indices _ #7 _ _ #4) #3 _]
[thm] HashMap.getElem_erase: [@getElem (HashMap #9 #8 #7 #6) _ _ _ _ (@HashMap.erase _ _ #7 #6 #5 #2) #1 #0]
[thm] HashMap.getElem_insert: [@getElem (HashMap #10 #9 #8 #7) _ _ _ _ (@HashMap.insert _ _ #8 #7 #6 #3 #1) #2 #0]
[thm] Array.getElem_set: [@getElem (Array #6) `[Nat] _ _ _ (@Array.set _ #5 #4 #2 #3) #1 #0]
[thm] Array.getElem_pop: [@getElem (Array #3) `[Nat] _ _ _ (@Array.pop _ #2) #1 #0]
[thm] Option.some_beq_some: [@BEq.beq (Option #3) _ (@some _ #1) (@some _ #0)]
[thm] Option.some_beq_none: [@BEq.beq (Option #2) _ (@some _ #0) (@none _)]
[thm] Option.none_beq_some: [@BEq.beq (Option #2) _ (@none _) (@some _ #0)]
[thm] Option.none_beq_none: [@BEq.beq (Option #1) _ (@none _) (@none _)]
[thm] HashMap.contains_erase: [@HashMap.contains #8 #7 #6 #5 (@HashMap.erase _ _ #6 #5 #4 #1) #0]
[thm] HashMap.contains_insert: [@HashMap.contains #9 #8 #7 #6 (@HashMap.insert _ _ #7 #6 #5 #2 #0) #1]
[thm] HashMap.contains_iff_mem: [@HashMap.contains #5 #4 #3 #2 #1 #0, true]
[thm] getElem_def: [@getElem (IndexMap #8 #7 #6 #5) _ _ _ _ #2 #1 #0]
[thm] mem_indices_of_mem: [@Membership.mem #5 (IndexMap _ #4 #3 #2) _ #1 #0]
[thm] getElem?_def: [@getElem? (IndexMap #7 #6 #5 #4) _ _ _ _ #1 #0]
[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
[ring] Rings
[ring] Ring `Int`
[basis] Basis
[_] ↑m.size + -1 * ↑m.keys.size = 0
[_] ↑m.keys.size + -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size = 0
[_] ↑i + -1 * ↑m.indices[a] = 0
[_] ↑m.keys.pop.size + -1 * ↑(m.keys.size - 1) = 0
[_] ↑(m.keys.pop.set i (m.keys.back ⋯) ⋯).size + -1 * ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) = 0
[_] ↑i_2 + -1 * ↑m.indices[m.keys[i_2]] = 0
[_] ↑(m.keys.size - 1) + -1 * ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) = 0
[_] ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) + -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + 1 = 0
[_] ↑(m.keys.set i (m.keys.back ⋯) ⋯).size + -1 * ↑(m.keys.set i (m.keys.back ⋯) ⋯).pop.size + -1 = 0
[ring] Ring `Lean.Grind.Ring.OfSemiring.Q Nat`
[basis] Basis
[_] ↑(m.keys.size - 1) + -1 * ↑(m.size - 1) = 0
[_] ↑(m.size - 1) + -1 * ↑((m.keys.set i (m.keys.back ⋯) ⋯).size - 1) = 0

[grind] Diagnostics
[thm] E-Matching instances
[thm] WF ↦ 16
[thm] getElem?_neg ↦ 9
[thm] getElem?_pos ↦ 9
[thm] Array.getElem?_eq_none ↦ 5
[thm] HashMap.contains_iff_mem ↦ 5
[thm] Array.getElem?_pop ↦ 2
[thm] Array.getElem?_set ↦ 2
[thm] Array.getElem_pop ↦ 2
[thm] Array.getElem_set ↦ 2
[thm] Array.set_pop ↦ 2
[thm] Array.size_pop ↦ 2
[thm] Array.size_set ↦ 2
[thm] getElem_indices_lt ↦ 2
[thm] mem_indices_of_mem ↦ 2
[thm] Array.back_eq_getElem ↦ 1
[thm] size_keys ↦ 1
[thm] size.eq_1 ↦ 1
[thm] HashMap.contains_erase ↦ 1
[thm] HashMap.contains_insert ↦ 1
[thm] HashMap.getElem?_insert ↦ 1
[thm] HashMap.getElem_insert ↦ 1
[thm] HashMap.mem_erase ↦ 1
[thm] HashMap.mem_insert ↦ 1

This fails while attempting to prove the WF field in the second branch. As usual, there is detailed information from grind about its failure state, but almost too much to be helpful! Let's look at the model produced by cutsat and see if we can see what's going on:

[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

This model consists of an IndexMap of size 3, with keys a_1, a_2 and the otherwise unnamed (keys m_1).back ⋯.

Everything looks fine, except the line:

(((indices m_1).erase a_1).insert ((keys m_1).back ⋯) i_1)[a_2] := 0

This shouldn't be possible! Since the three keys are distinct, we should have

(((indices m_1).erase a_1).insert ((keys m_1).back ⋯) i_1)[a_2] =
  ((indices m_1).erase a_1)[a_2] =
  (indices m_1)[a_2] =
  1

Now that we've found something suspicious, we can look through the equivalence classes identified by grind. (In the future we'll be providing search tools for inspecting equivalence classes, but for now you need to read through manually.) We find amongst many others:

{a_2,
  (keys m_1).back ⋯,
  (keys m_1)[(keys m_1).size - 1],
  (keys m_1)[i_2], ...}

This should imply, by the injectivity of keys, that i_2 = (keys m_1).size - 1. Since this identity wasn't reflected by the cutsat model, we suspect that grind is not managing to use the injectivity of keys.

Thinking about the way that we've provided the well-formedness condition, as ∀ (i : Nat) (a : α), keys[i]? = some a ↔ indices[a]? = some i, this perhaps isn't surprising: it's expressed in terms of keys[i]? and indices[a]?. Let's add a variant version of the well-formedness condition using getElem instead of getElem?:

@[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α:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βinst✝¹:LawfulBEq αinst✝:LawfulHashable αi:Nata:αh₁:i < m.keys.sizeh₂:a ∈ m⊢ m.keys[i] = a ↔ m.indices[a] = i
  have := m.WF i aα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βinst✝¹:LawfulBEq αinst✝:LawfulHashable αi:Nata:αh₁:i < m.keys.sizeh₂:a ∈ mthis:m.keys[i]? = some a ↔ m.indices[a]? = some i := WF m i a⊢ m.keys[i] = a ↔ m.indices[a] = i
  grindAll goals completed! 🐙

We can verify that with this available, grind can now prove:

example {m : IndexMap α β} {a : α} {h : a ∈ m} :
  m.keys[m.indices[a]'h] = a := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm✝:IndexMap α βa✝:αb:βi:Natinst✝¹:LawfulBEq αinst✝:LawfulHashable αm:IndexMap α βa:αh:a ∈ m⊢ m.keys[m.indices[a]] = a grindAll goals completed! 🐙

Trying again with eraseSwap, everything goes through cleanly now, with no manual proofs:

@[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

Finally we turn to the verification theorems about the basic operations, relating getIdx, findIdx, and insert. By adding a local grind annotation allowing grind to unfold the definitions of these operations, the proofs all go through effortlessly:

/-! ### Verification theorems -/

attribute [local grind] getIdx findIdx insert

@[grind _=_] theorem getIdx_findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) :
    m.getIdx (m.findIdx a) = m[a] := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αinst✝¹:LawfulBEq αinst✝:LawfulHashable αm:IndexMap α βa:αh:a ∈ m⊢ m.getIdx (m.findIdx a h) ⋯ = m[a] grindAll goals completed! 🐙

@[grind =] theorem mem_insert (m : IndexMap α β) (a a' : α) (b : β) :
    a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αinst✝¹:LawfulBEq αinst✝:LawfulHashable αm:IndexMap α βa:αa':αb:β⊢ a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m
  grindAll goals completed! 🐙

@[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α:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αinst✝¹:LawfulBEq αinst✝:LawfulHashable αm:IndexMap α βa:αa':αb:βh:a' ∈ m.insert a b⊢ (m.insert a b)[a'] = if h' : (a' == a) = true then b else m[a']
  grindAll goals completed! 🐙

@[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α:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αinst✝¹:LawfulBEq αinst✝:LawfulHashable αm:IndexMap α βa:αb:β⊢ (m.insert a b).findIdx a ⋯ = if h : a ∈ m then m.findIdx a h else m.size
  grindAll goals completed! 🐙

Note that these are part of the public API of IndexMap, so we need to mark them as @[grind], so that users without our internal local grind annotations can still use them in grind proofs.

Putting this all together, our prototype API has reached the following state:

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'

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 Try these:
  [apply] [grind =] for pattern: [@Membership.mem #5 (IndexMap _ #4 #3 #2) _ #1 #0]
  [apply] [grind =_] for pattern: [@Membership.mem #5 (HashMap _ `[Nat] #3 #2) _ (@indices _ #4 _ _ #1) #0]grind] private theorem mem_indices_of_mem
    {m : IndexMap α β} {a : α} :
    a ∈ m ↔ a ∈ m.indices := 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α:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βa:αinst✝¹:LawfulBEq αinst✝:LawfulHashable αh:a ∈ m⊢ m.indices[a] < m.size
  have : m.indices[a]? = some m.indices[a] := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βa:αinst✝¹:LawfulBEq αinst✝:LawfulHashable αh:a ∈ m⊢ m.indices[a] < m.size grindAll goals completed! 🐙
  grindAll goals completed! 🐙

grind_pattern getElem_indices_lt => m.indices[a]

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 Try these:
  [apply] [grind =] for pattern: [@getElem (IndexMap #8 #7 #6 #5) _ _ _ _ #2 #1 #0]
  [apply] [grind
    =_] for pattern: [@getElem (Array #7) `[Nat] _ _ _ (@values #8 _ #6 #5 #2) (@getElem (HashMap _ `[Nat] _ _) _ `[Nat] _ _ (@indices _ _ _ _ #2) #1 #0) _]
  [apply] [grind →] for pattern: [LawfulBEq #8 #6, LawfulHashable _ _ #5, @Membership.mem _ (IndexMap _ #7 _ _) _ #2 #1]grind] private theorem getElem_def
    (m : IndexMap α β) (a : α) (h : a ∈ m) :
    m[a] = m.values[m.indices[a]'h] :=
  rfl
@[local Try these:
  [apply] [grind =] for pattern: [@getElem? (IndexMap #7 #6 #5 #4) _ _ _ _ #1 #0]
  [apply] [grind
    =_] for pattern: [@Option.bind `[Nat] #6 (@getElem? (HashMap #7 `[Nat] #5 #4) _ `[Nat] _ _ (@indices _ _ _ _ #1) #0) _]
  [apply] [grind =>] for pattern: [LawfulBEq #7 #5, LawfulHashable _ _ #4, @getElem? (IndexMap _ #6 _ _) _ _ _ _ #1 #0]grind] private theorem getElem?_def
    (m : IndexMap α β) (a : α) :
    m[a]? = m.indices[a]?.bind (fun i => (m.values[i]?)) :=
  rfl
@[local Try these:
  [apply] [grind =] for pattern: [@getElem! (IndexMap #8 #7 #6 #5) _ _ _ _ #2 #1 #0]
  [apply] [grind
    =_] for pattern: [@Option.getD #7 (@Option.bind `[Nat] _ (@getElem? (HashMap #8 `[Nat] #6 #5) _ `[Nat] _ _ (@indices _ _ _ _ #1) #0) _) (@default _ #2)]
  [apply] [grind =>] for pattern: [LawfulBEq #8 #6, LawfulHashable _ _ #5, @getElem! (IndexMap _ #7 _ _) _ _ _ _ #2 #1 #0]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α:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βa:αb:βi:Natinst✝¹:LawfulBEq αinst✝:LawfulHashable α⊢ ∀ (c : IndexMap α β) (i : α) [inst : Decidable (i ∈ c)], c[i]? = if h : i ∈ c then some c[i] else none grindAll goals completed! 🐙
  getElem!_def := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βa:αb:βi:Natinst✝¹:LawfulBEq αinst✝:LawfulHashable α⊢ ∀ [inst : Inhabited β] (c : IndexMap α β) (i : α),
  c[i]! =
    match c[i]? with
    | some e => e
    | none => default grindAll goals completed! 🐙

@[inline] def insert [LawfulBEq α] (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 [LawfulBEq α] : Singleton (α × β) (IndexMap α β) :=
    ⟨fun ⟨a, b⟩ => (∅ : IndexMap α β).insert a b⟩

instance [LawfulBEq α] : Insert (α × β) (IndexMap α β) :=
    ⟨fun ⟨a, b⟩ s => s.insert a b⟩

instance [LawfulBEq α] : LawfulSingleton (α × β) (IndexMap α β) :=
    ⟨fun _ => rfl⟩

@[local Try these:
  [apply] [grind
    .] for pattern: [@getElem (Array #10) `[Nat] _ _ _ (@keys _ #9 #8 #7 #6) #3 #1, @getElem (HashMap _ `[Nat] _ _) _ `[Nat] _ _ (@indices _ _ _ _ #6) #2 #0]
  [apply] [grind
    →] for pattern: [LawfulBEq #10 #8, LawfulHashable _ _ #7, @LE.le `[Nat] `[instLENat] (#3 + 1) (@Array.size _ (@keys _ #9 _ _ #6)), @Membership.mem _ (IndexMap _ _ _ _) _ #6 #2]grind] private theorem WF'
    (i : Nat) (a : α) (h₁ : i < m.keys.size) (h₂ : a ∈ m) :
    m.keys[i] = a ↔ m.indices[a] = i := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βinst✝¹:LawfulBEq αinst✝:LawfulHashable αi:Nata:αh₁:i < m.keys.sizeh₂:a ∈ m⊢ m.keys[i] = a ↔ m.indices[a] = i
  have := m.WF i aα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αm:IndexMap α βinst✝¹:LawfulBEq αinst✝:LawfulHashable αi:Nata:αh₁:i < m.keys.sizeh₂:a ∈ mthis:m.keys[i]? = some a ↔ m.indices[a]? = some i := WF m i a⊢ m.keys[i] = a ↔ m.indices[a] = i
  grindAll goals completed! 🐙

/--
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 -/

attribute [local grind] getIdx findIdx insert

@[Try these:
  [apply] [grind =] for pattern: [@getIdx #8 #7 #6 #5 #2 (@findIdx _ _ _ _ #2 #1 #0) _]
  [apply] [grind =_] for pattern: [@getElem (IndexMap #8 #7 #6 #5) _ _ _ _ #2 #1 #0]
  [apply] [grind →] for pattern: [LawfulBEq #8 #6, LawfulHashable _ _ #5, @Membership.mem _ (IndexMap _ #7 _ _) _ #2 #1]
  [apply] [grind! .] for pattern: [@findIdx #8 #7 #6 #5 #2 #1 #0]grind] theorem getIdx_findIdx (m : IndexMap α β) (a : α) (h : a ∈ m) :
    m.getIdx (m.findIdx a) = m[a] := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αinst✝¹:LawfulBEq αinst✝:LawfulHashable αm:IndexMap α βa:αh:a ∈ m⊢ m.getIdx (m.findIdx a h) ⋯ = m[a] grindAll goals completed! 🐙

@[Try these:
  [apply] [grind =] for pattern: [@Membership.mem #9 (IndexMap _ #8 #7 #6) _ (@insert _ _ _ _ #4 #5 #3 #2 #0) #1]
  [apply] [grind
    =>] for pattern: [LawfulBEq #9 #7, LawfulHashable _ _ #6, @Membership.mem _ (IndexMap _ #8 _ _) _ (@insert _ _ _ _ #4 #5 #3 #2 #0) #1]grind] theorem mem_insert (m : IndexMap α β) (a a' : α) (b : β) :
    a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m := byα:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αinst✝¹:LawfulBEq αinst✝:LawfulHashable αm:IndexMap α βa:αa':αb:β⊢ a' ∈ m.insert a b ↔ a' = a ∨ a' ∈ m
  grindAll goals completed! 🐙

@[Try these:
  [apply] [grind =] for pattern: [@getElem (IndexMap #10 #9 #8 #7) _ _ _ _ (@insert _ _ _ _ #5 #6 #4 #3 #1) #2 #0]
  [apply] [grind
    →] for pattern: [LawfulBEq #10 #8, LawfulHashable _ _ #7, @Membership.mem _ (IndexMap _ #9 _ _) _ (@insert _ _ _ _ #5 #6 #4 #3 #1) #2]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α:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αinst✝¹:LawfulBEq αinst✝:LawfulHashable αm:IndexMap α βa:αa':αb:βh:a' ∈ m.insert a b⊢ (m.insert a b)[a'] = if h' : (a' == a) = true then b else m[a']
  grindAll goals completed! 🐙

@[Try these:
  [apply] [grind =] for pattern: [@findIdx #8 #7 #6 #5 (@insert _ _ _ _ #3 #4 #2 #1 #0) #1 _]
  [apply] [grind
    =>] for pattern: [LawfulBEq #8 #6, LawfulHashable _ _ #5, @findIdx _ #7 _ _ (@insert _ _ _ _ #3 #4 #2 #1 #0) #1 _]
  [apply] [grind! .] for pattern: [@insert #8 #7 #6 #5 #3 #4 #2 #1 #0]
  [apply] [grind! =>] for pattern: [LawfulBEq #8 #6, LawfulHashable _ _ #5, @insert _ #7 _ _ #3 #4 #2 #1 #0]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α:Type uβ:Type vinst✝³:BEq αinst✝²:Hashable αinst✝¹:LawfulBEq αinst✝:LawfulHashable αm:IndexMap α βa:αb:β⊢ (m.insert a b).findIdx a ⋯ = if h : a ∈ m then m.findIdx a h else m.size
  grindAll goals completed! 🐙

end IndexMap

We haven't yet proved all the theorems we would want about these operations (or indeed any theorems about eraseSwap); the interested reader is encouraged to try proving more, and perhaps even releasing a complete IndexMap library!

Summarizing the design principles discussed above about encapsulation:

the fields of IndexMap are all private, as these are implementation details.
the theorems about these fields are all private, and marked as @[grind], rather than @[grind], as they won't be needed after we've set up the API.
the verification theorems are both marked as @[grind], and proved by grind: the annotation is necessary because we want grind to be able to prove these facts even once we're outside the current module, and the @[grind] theorems are no longer available.

Using grind for Ordered Maps

Skeleton

Header 2

Using `grind` for Ordered Maps