Finite maps?

Stream: Is there code for X?

[Paula Neeley]

I'm looking for finite maps and having trouble finding anything. I've been implementing this myself as a structure with two fields, a Finset of pairs along with a requirement that the pairing is functional. There has to be a better way.

[Ruben Van de Velde]

Your link goes to a disambiguation page

[Paula Neeley]

I'm looking for something that I could use like an associative array

[Adam Topaz]

docs#HashMap

[Ruben Van de Velde]

docs#Std.HashMap ?

[Paula Neeley]

I was kind of looking for something more general than HashMaps? For clarification, I'm formalizing some of the Hoare Type Theory concepts from this paper. On page 6 of the paper they define heaps as sets of pairs, where the first element is a location in memory and the second is a dependent pair of some type and value in memory. These sets must satisfy finite and functional predicates that they define above. But for a lot of the operations defined on page 7, I need things like decidability of membership in the set. So I got rid of the finite predicate and just used finsets. My questions is if there is a nice way to get rid of the functional predicate by using something like a finite map, if that exists in Lean.

[Kim Morrison]

Do you need dependently typed pairs? What generality is missing in HashMap?

[Kyle Miller]

Where do you need decidability? Aren't all these operations ones that you reason about, not evaluate at runtime?

Regarding finite maps, one of the mathlib solutions to that is docs#Finsupp . If your key type is K and your value type is V, then you can use Finsupp K (WithZero V) (or, with finsupp notation, K →₀ WithZero V). This is the find? function for the finite map, using the fact that WithZero V = Option V.

It's not a "runtime" data type. It's more of a specification sort of type, for an abstract finite map. The issue is that all the operations are manipulating these K → WithZero V functions, creating trees of closures.

[Kyle Miller]

Here's a version of page 7 mostly from scratch:

import Mathlib

set_option autoImplicit true

structure Map (K V : Type*) where
  find? : K → Option V
  /-- The set of everything that doesn't map to `none` is finite. -/
  finite : Set.Finite (find? ⁻¹' (Set.univ \ {none}))

def Map.empty : Map K V where
  find? _ := none
  finite := by simp

def Map.insert [DecidableEq K] (m : Map K V) (k : K) (v : V) : Map K V where
  find? := Function.update m.find? k v
  finite := by
    apply (m.finite.insert k).subset
    intro x
    by_cases h : x = k <;> simp [Function.update_apply, h]

def Map.remove [DecidableEq K] (m : Map K V) (k : K) : Map K V where
  find? := Function.update m.find? k none
  finite := by
    apply m.finite.subset
    intro x
    by_cases h : x = k <;> simp [Function.update_apply, h]

def Map.keys (h : Map K V) : Set K := h.find? ⁻¹' (Set.univ \ {none})
instance : Finite (Map.keys h) := h.finite

def Heap := Map Nat ((α : Type) × α)

def Heap.empty : Heap := Map.empty
def Heap.update (h : Heap) (n : Nat) (x : α) : Heap := h.insert n ⟨α, x⟩
def Heap.seleq (h : Heap) (n : Nat) (x : α) : Prop := h.find? n = some ⟨α, x⟩
def Heap.free (h : Heap) (n : Nat) : Heap := h.remove n
def Heap.dom (h : Heap) : Set Nat := h.keys
def Heap.share (h₁ h₂ : Heap) (n : Nat) : Prop := h₁.find? n = h₂.find? n
def Heap.splits (h h₁ h₂ : Heap) : Prop :=
  ∀ n, (n ∉ h₁.dom ∧ Heap.share h h₂ n) ∨ (n ∉ h₂.dom ∧ Heap.share h h₁ n)

def emp : Set Heap := {Heap.empty}
def mapsto (n : Nat) (x : α) : Set Heap := {Heap.empty.update n x}
def hookarrow (n : Nat) (x : α) : Set Heap := {h | h.seleq n x}
def star (H₁ H₂ : Set Heap) : Set Heap := {h | ∃ h₁ ∈ H₁, ∃ h₂ ∈ H₂, h.splits h₁ h₂}
def linestar (H₁ H₂ : Set Heap) : Set Heap := {h | ∀ h₁ h₂, Heap.splits h₂ h₁ h → h ∈ H₁ → h ∈ H₂}
def this (h : Heap) : Set Heap := {h}

[Paula Neeley]

Thank you, everyone, for the suggestions. I think either of these implementation will work, I'm mostly just trying to make design decisions on what will be cleanest to deal with later.

To respond to @Kyle Miller's question,
Where do you need decidability? Aren't all these operations ones that you reason about, not evaluate at runtime?
It says on page 4 of the paper that HTT is supposed to be able to compute with small types as if they were data, and compute with and abstract over assertions as if they were data. So yes I'm planning to reason about these objects, but I'm also trying to formalize this paper as accurately as possible (and probably getting confused by details like this because I'm not a type theorist :smile: )

[Kyle Miller]

I'm not a type theorist, so take what I say with a big grain of salt, but when I was reading the paper earlier, my interpretation of "compute" there is more in the sense of "types are also terms of this language", with reduction rules and normal forms. Their definition of a finite set is not computable in the Finset sense, which is "actual" data that a compiled program is able to compute with.

[Paula Neeley]

I see, that makes sense. Thanks so much for your help and explanations.