Proof support for HashMap.union

Stream: new members

[Jianlin Li]

Hi all,

I’m looking for theorems about HashMap.union (or possibly Union.union), for example a lemma of the form
k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂.

I checked Std.Data.HashMap.Lemmas but couldn’t find anything like this. Does this mean I need to prove it (seemingly by induction on fold) myself, or are such theorems provided through a different interface that isn’t exposed in Std.Data.HashMap.Lemmas?

MEW

import Std
import Aesop

open Std

@[simp]
def xyz : HashMap String Nat := HashMap.ofList [("x", 1), ("y", 2), ("z", 3)]
@[simp]
def xy  : HashMap String Nat := HashMap.ofList [("x", 1), ("y", 2)]
@[simp]
def yz  : HashMap String Nat := HashMap.ofList [("y", 2), ("z", 3)]

theorem fold_induction  {α β} [BEq α] [Hashable α] {γ : Type w} {P : γ → Prop}
  {f : γ → α → β → γ} {init : γ} {m : HashMap α β}
  : P init → (∀ acc x y, P acc → (hmem : x ∈ m) → m[x]'hmem = y → P (f acc x y)) → P (HashMap.fold f init m) :=
  sorry

@[simp]
theorem mem_union {α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulBEq α] [LawfulHashable α] (m₁ m₂ : HashMap α β) (k : α)
  : k ∈ m₁ ∪ m₂ → k ∈ m₁ ∨ k ∈ m₂ := by
  intro h
  simp [Union.union, HashMap.union] at h
  let P (m : HashMap α β) : Prop := k ∈ m → k ∈ m₁ ∨ k ∈ m₂
  have P0 : P m₁ := by aesop
  have PS : ∀ acc x y, P acc  → (hmem : x ∈ m₂) → m₂[x]'hmem = y → P (acc.insert x y) := by
    intro acc x y IH hmem hy h
    simp_all [P]
    cases h with
    | inl h =>
      have hxk : x = k := by simp_all
      simp [hxk] at hmem
      right
      exact hmem
    | inr h =>
      apply IH h
  apply fold_induction (α := α) (β := β) (γ := HashMap α β) (P := P) P0 PS
  apply h

theorem mem_union' {α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulBEq α] [LawfulHashable α] (m₁ m₂ : HashMap α β) (k : α)
  : k ∈ m₁ ∨ k ∈ m₂ → k ∈ m₁ ∪ m₂  := by
  intro h
  cases h with
  | inl h =>
    sorry
  | inr h =>
    sorry


example :HashMap.union xy yz = xyz := by
  simp_all
  sorry

example :  k ∈ xy ∪ yz → k ∈ xyz := by
  intro h
  have g : k ∈ xy ∨ k ∈ yz := by
    apply mem_union
    exact h
  simp_all [xyz, xy, yz]
  aesop

example :  k ∈ xyz → k ∈ xy ∪ yz := by
  intro h
  apply mem_union'
  aesop

[Robin Arnez]

lean4#7823 but there hasn't been much progress lately