feat: HashMap.toList_insert_perm_of_not_mem

[kim-em]

WIP, this is stacked on top of #6232, and may not make sense at all if that requires substantial revisions.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-12-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-12-04 11:27:40)

[TwoFX]

Here is how I had envisioned this working: you prove

private theorem perm_of_perm {l₁ l₂ l₃ : List α} (h : List.Perm l₁ l₂) :
    List.Perm l₁ l₃ ↔ List.Perm l₂ l₃ :=
  ⟨h.symm.trans, h.trans⟩

and add ← `(perm_of_perm) to congrNames. Then this lemma is proved like this:

Suggested change

	open _root_.List in
	theorem toList_insert_perm_of_not_contains [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
	(k : α) (v : β k) (h' : m.contains k = false) :
	(m.insert k v).1.toList ~ ⟨k, v⟩ :: m.1.toList := by
	revert h'
	simp_to_model
	intro h'
	exact Perm.trans (toListModel_insert (Raw.WF.out h)) (by simp [insertEntry, h'])
	open _root_.List in
	theorem toList_insert_perm_of_not_contains [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
	(k : α) (v : β k) : m.contains k = false →
	(m.insert k v).1.toList ~ ⟨k, v⟩ :: m.1.toList := by
	simp_to_model using Perm.of_eq ∘ insertEntry_of_containsKey_eq_false

To spell it out explicitly: after simp_to_model, it should always be possible to generalize toListModel m.1.buckets = l so that m is then no longer present in the goal.

[TwoFX]

The way this is supposed to work is that you prove Const.toList_insert_perm_of_not_contains in Internal/RawLemmas.lean and DHashMap/(Raw)Lemmas.lean and then just apply that here. toList_inner and insert_inner should not exist.

To give more details:

• I think you should drop Const.toListModel and change the statement of Const.toList_eq_toListModel to Raw.Const.toList m = (toListModel m.buckets).map (fun ⟨k, v⟩ => (k, v)).
• Then you should add Raw.Const.toList_eq_toListModel to queryNames in Internal/RawLemmas.lean. Then you can add ← `(perm_of_perm ∘ List.Perm.map _) to congrNames (in addition to what was already added in my previous comment). This will allow you to put

namespace Const

variable {β : Type v} (m : Raw₀ α (fun _ => β))

open _root_.List in
theorem Const.toList_insert_perm_of_not_contains [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β} :
    m.contains k = false → Raw.Const.toList (m.insert k v).1 ~ (k, v) :: (Raw.Const.toList m.1) := by
  simp_to_model
  exact fun h => by simp [insertEntry_of_containsKey_eq_false h]

end Const

in the bottom of Internal/RawLemmas.lean, from which the statements about (D)HashMap.toList follow imediately.

I should add that this still isn't perfect; it would be even better to prove containsKey k l = false → List.map (fun x => (x.fst, x.snd)) (insertEntry k v l) = (k, v) :: List.map (fun x => (x.fst, x.snd)) l in List/Associative.lean (perhaps as part of the theory of a "toListOfPairs" function) instead of inlining the proof.