Proof support for HashMap: where to find lemmas/equalities?

Stream: new members

[Jianlin Li]

Hi everyone,

I have some experience with Rocq and recently started working with Lean. I’m currently mechanizing the denotational semantics of a programming language, but I’m having trouble getting familiar with Lean’s Std library. I’d really appreciate advice on two points:

1. Choosing the right data structure to represent typing contexts and, more importantly, their semantics.
2. Where to find documentation, theories, and use cases for the data structures available in Lean.

To make things concrete, I’ve prepared three small MWEs: STLCList.lean, STLCHashMap.lean, and STLCDHashMap.lean. My language is much more complex than STLC; I am just using STLC and MWEs.

In all three, I use a deep embedding of STLC with nat (and add), variable names as strings, intrinsically typed, with the goal of building its denotational semantics. The difference is in how I represent the typing context Ctx (mapping strings to types) and the semantic domain of Ctx (mapping strings to values of the right type).

• STLCList.lean:
  Ctx is a List (String × Ty), and the environment is a list-like structure. I was able to close the proofs, but this approach ties values to positions in the list. What I’d really like is that values associate values with names (like labeled arguments rather than propositional arguments), with environments supporting out-of-order bindings.
  It only makes sense to have def ρxy : Env Γxy := Env.cons 3 (Env.cons 4 Env.nil) for def Γxy : Ctx := [("x", .nat), ("y", .nat)], but I am looking for something like def ρxy : Env Γxy := [("y", 4), ("x", 3)].

• STLCHashMap.lean:
  abbrev Ctx := HashMap String Ty structure Env (Γ : Ctx) where map : HashMap String (Σ T, 〚T〛) wf0 {x : String} : x ∈ Γ → x ∈ map wf1 {x : String} (h : x ∈ Γ) : (map[x]'(wf0 h)).fst = Γ[x]'h notation "〚" Γ "〛" => Env Γ
  With HashMaps, the order of the values in the environment does not matter anymore, but here I ran into difficulty: I couldn’t close some seemingly trivial proofs because I couldn’t find enough lemmas/theorems about HashMap. In particular, I need equalities that allow rewriting goals. (e.g., (Γ.insert y A)[y] = A).

• **STLCDHashMap.lean**:
  I also tried a dependent hash map for the environment:
  structure Env (Γ : Ctx) where map : DHashMap String (fun x => SemOptionTy Γ[x]?) wf {x : String} : x ∈ Γ → x ∈ map
  But again I’m missing theorems I’d expect, like:
  x ∈ Γ → Σ T, Γ[x]? = some T.

My central issue is:

• What’s the best way to represent typing contexts (Ctx) and their semantic domains (environments) in Lean if I use Lists?
• What’s the best way to represent typing contexts (Ctx) and their semantic domains (environments) in Lean if I prefer not to use Lists?
• If I go with HashMap or DHashMap, where can I find the supporting library lemmas/theorems that make proofs tractable?

Any guidance or references would be greatly appreciated!

[Matt Diamond]

you might want to take a look at the recently started CSLib project... they have an implementation of the simply typed lambda calculus (though it's locally nameless):

https://cs-lean.github.io/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.html

[Matt Diamond]

they implement typing contexts here: http://cs-lean.github.io/Cslib/Computability/LambdaCalculus/LocallyNameless/Context.html

[Johannes Tantow]

Here are the lemmas for HashMaps : https://leanprover-community.github.io/mathlib4_docs/Std/Data/HashMap/Lemmas.html
Many lemmas of these are though also added to simp or grind, so using these tactics will often simplify your goal quite enough.

Below some of your hashmap lemmas:

theorem extend_wf0 {Γ : Ctx} {ρ : Env Γ} {x : String} {A : Ty} {v : 〚A〛} {y : String}:
  y ∈ Γ.insert x A → y ∈ ρ.map.insert x ⟨A, v⟩ := by
  intro hy
  by_cases hxy : y = x
  . subst hxy
    simp
  . simp
    simp at hy
    right
    apply ρ.wf0
    cases hy <;> grind

theorem extend_wf1 {Γ : Ctx} {ρ : Env Γ} {x : String} {A : Ty} {v : 〚A〛} {y : String} (h : y ∈ Γ.insert x A) :
  ((ρ.map.insert x ⟨A, v⟩)[y]'(extend_wf0 h)).fst = (Γ.insert x A)[y]'h := by
  by_cases hxy : y = x
  . subst hxy
    simp
  . have : ¬ x = y := by grind
    simp [HashMap.getElem_insert, this]
    apply ρ.wf1

-- Extend an environment with a fresh binding `x : A` carrying value `v`.
def extend {Γ : Ctx} (ρ : Env Γ) (x : String) (A : Ty) (v : 〚A〛) : Env (Γ.insert x A) :=
by
  refine {
    map := ρ.map.insert x ⟨A, v⟩
    wf0 := extend_wf0
    wf1 := extend_wf1
  }

theorem projection_wf0 {Γ' : Ctx} {Γ : Ctx} {hsub : Γ' ⊆ Γ} {ρ : 〚Γ〛} {y : String} :
  y ∈ Γ' → y ∈ ρ.map.filter (fun k y =>  k ∈ Γ') := by
  simp [HashMap.mem_filter]
  intro h
  constructor
  · apply ρ.wf0
    simp [submap, keysSubset] at hsub
    apply hsub.1 _ h
  · exact h
  -- y ∈ Γ' → y ∈ ρ.map.filter (fun k y => k ∈ Γ')

theorem projection_wf1 {Γ' : Ctx} {Γ : Ctx} {hsub : Γ' ⊆ Γ} {ρ : 〚Γ〛} {y : String} (h : y ∈ Γ'):
  ((ρ.map.filter (fun k _ =>  k ∈ Γ'))[y]'(projection_wf0 (hsub := hsub) h)).fst = Γ'[y]'h := by
  simp
  simp [submap, consistent, keysSubset] at hsub
  rw [ρ.wf1]
  · apply Eq.symm
    apply hsub.2
  · apply hsub.1
    exact h

In general it is risky to use tactics to create objects as reasoning about them afterwards is difficult.

[Robin Arnez]

Which version of Lean are you on? In the most recent version of Lean there are quite a lot of lemmas to your disposal, making extend_wf0:

theorem extend_wf0 {Γ : Ctx} {ρ : Env Γ} {x : String} {A : Ty} {v : 〚A〛} {y : String}:
    y ∈ Γ.insert x A → y ∈ ρ.map.insert x ⟨A, v⟩ := by
  intro hy
  by_cases hxy : x = y
  · simp [hxy]
  · simp_all [ρ.wf0]

[Jianlin Li]

Hi @Robin Arnez, this proof works for me. Thanks a lot. I think I am using lean4:v4.22.0.

└─[$] <git:(master*)> elan show
installed toolchains
--------------------

leanprover/lean4-nightly:nightly-2024-04-24
leanprover/lean4-nightly:nightly-2025-04-23
leanprover/lean4:v4.10.0
leanprover/lean4:v4.15.0
leanprover/lean4:v4.16.0-rc2
leanprover/lean4:v4.17.0
leanprover/lean4:v4.18.0
leanprover/lean4:v4.18.0-rc1
leanprover/lean4:v4.19.0-rc3
leanprover/lean4:v4.22.0 (resolved from default 'leanprover/lean4:stable')
leanprover/lean4:v4.23.0-rc2

active toolchain
----------------

leanprover/lean4:v4.22.0 (directory override for '...')
Lean (version 4.22.0, arm64-apple-darwin23.6.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05, Release)

[Jianlin Li]

@Johannes Tantow Thanks so much for the proof. I think I am starting to know how to proceed with your help.

I got two errors from grind ( I am using lean4:v4.22.0).

theorem extend_wf0 {Γ : Ctx} {ρ : Env Γ} {x : String} {A : Ty} {v : 〚A〛} {y : String}:
  y ∈ Γ.insert x A → y ∈ ρ.map.insert x ⟨A, v⟩ := by
  intro hy
  by_cases hxy : y = x
  . subst hxy
    simp
  . simp
    simp at hy
    right
    apply ρ.wf0
    cases hy <;> grind --[error when printing message: unknown goal [anonymous]]

theorem extend_wf1 {Γ : Ctx} {ρ : Env Γ} {x : String} {A : Ty} {v : 〚A〛} {y : String} (h : y ∈ Γ.insert x A) :
  ((ρ.map.insert x ⟨A, v⟩)[y]'(extend_wf0 h)).fst = (Γ.insert x A)[y]'h := by
  by_cases hxy : y = x
  . subst hxy
    simp
  . have : ¬ x = y := by grind --[error when printing message: unknown goal [anonymous]]
    simp [HashMap.getElem_insert, this]
    apply ρ.wf1

But it works after replacing grind with simp or aesop.

theorem extend_wf0 {Γ : Ctx} {ρ : Env Γ} {x : String} {A : Ty} {v : 〚A〛} {y : String}:
    y ∈ Γ.insert x A → y ∈ ρ.map.insert x ⟨A, v⟩ := by
  intro hy
  by_cases hxy : x = y
  · simp [hxy]
  · simp_all [ρ.wf0]

theorem extend_wf1 {Γ : Ctx} {ρ : Env Γ} {x : String} {A : Ty} {v : 〚A〛} {y : String} (h : y ∈ Γ.insert x A) :
  ((ρ.map.insert x ⟨A, v⟩)[y]'(extend_wf0 h)).fst = (Γ.insert x A)[y]'h := by
  by_cases hxy : y = x
  . simp [hxy]
  . have hxy : ¬ x = y := by aesop
    simp [HashMap.getElem_insert, hxy]
    apply ρ.wf1