Get keys of a `Std.ExtHashMap`

Stream: Is there code for X?

[Pranav cs22b015]

I wish to use Std.ExtHashMap (https://lean-lang.org/doc/reference/4.21.0-rc3//Basic-Types/Maps-and-Sets/#Std___ExtHashMap) to implement a function which takes two Extensional Hashmaps to return a new Extensional HashMap which contains the maximum of the values in each of the input maps for every key. The equivalent for HashMaps is given below.

abbrev concrete_st := Std.HashMap ℕ Int

def sel (s:concrete_st) (k: ℕ) : Int := match (Std.HashMap.get? s k) with
| some n => n
| none => 0

def merge_helper (klist: List ℕ) (a b: concrete_st) : concrete_st :=
match klist with
| [] => {}
| key::keys => Std.HashMap.insert (merge_helper keys a b) key (max (sel a key) (sel b key))

def merge (a b: concrete_st) :=
let keys1 := Std.HashMap.keys a
let keys2 := Std.HashMap.keys b
let keys:= keys1 ∪ keys2
merge_helper keys a b

Is there a way to iterate over / find the keys of the Std.ExtHashMap ? I want to use extensionality to prove certain theorems related to this implementation

[Markus Himmel]

If your keys are natural numbers, then using docs#Std.ExtTreeMap instead of ExtHashMap could be an option, as that oen has a keys function.

[Markus Himmel]

One of the next few releases will contain an ExtDHashMap.mergeWith function that should suit your needs, but it's not done yet.

[Pranav cs22b015]

Is there a way to reason about the keys of such an ExtTreeMap? For example, how should I proceed in proving the following -

abbrev concrete_st := Std.ExtTreeMap ℕ Int

@[simp]
def sel (s : concrete_st) (k : ℕ) : Int := match (Std.ExtTreeMap.get? s k) with
| some n => n
| none => 0

@[simp]
def merge_helper (klist : List ℕ) (a b : concrete_st) : concrete_st :=
match klist with
| [] => {}
| key::keys => Std.ExtTreeMap.insert (merge_helper keys a b) key (max (sel a key) (sel b key))

@[simp]
def merge (a b : concrete_st) : concrete_st :=
let keys1 := Std.ExtTreeMap.keys a
let keys2 := Std.ExtTreeMap.keys b
let keys:= keys1 ∪ keys2
merge_helper keys a b

theorem merge_comm (l: concrete_st) (a: concrete_st) (b: concrete_st) :
eq (merge a b) (merge b a) := by sorry

The merge function basically collects the keys kof each of the maps A and B, and creates a new map with the values corresponding to max(A[k], B[k]). We need to show that this function is commutative.

[Matej Penciak]

You can prove some helper lemmas about merge_helper that would make merge_comm a lot easier. Like when merge_helper contains a key, the value is given by max ... and similarly merge_helper contains a key iff it is in klist.

[Pranav cs22b015]

Is there a direct way to prove this seemingly simpler result?

theorem insert_insert (s: Std.ExtTreeMap ℕ Int) (k1 k2 : ℕ) (v1 v2: Int) :
¬ k1 = k2 → (s.insert k1 v1).insert k2 v2 = (s.insert k2 v2).insert k1 v1 := by

[Pranav cs22b015]

Pranav cs22b015 said:

Is there a direct way to prove this seemingly simpler result?

theorem insert_insert (s: Std.ExtTreeMap ℕ Int) (k1 k2 : ℕ) (v1 v2: Int) :
¬ k1 = k2 → (s.insert k1 v1).insert k2 v2 = (s.insert k2 v2).insert k1 v1 := by

Okay, I got it, I need to use extensionality

[Pranav cs22b015]

How does one show this?

theorem union_same (l : List ℕ) : l ∪ l = l := by

I am also confused on the difference between List.union and ∪ in terms of what theorems simp and grind are aware of about these constructs.

[Chris Henson]

All the simp and grind annotations should be on lemmas using the notation. docs#List.union_def shows how they are equivalent.

[Ruben Van de Velde]

List.Subset.union_eq_right (List.Subset.refl _) works, but I'm surprised this doesn't exist as a simp lemma yet

[Ruben Van de Velde]

Feel free to PR it to Mathlib.Data.List.Lattice

[Ruben Van de Velde]

Or maybe

import Mathlib

@[simp]
lemma List.Subset.union_left {α : Type*} [DecidableEq α] {xs ys : List α} : xs ⊆ xs ∪ ys := by
  simp +contextual [List.subset_def]

@[simp]
lemma List.Subset.union_eq_right_iff {α : Type*} [DecidableEq α] {xs ys : List α} : xs ∪ ys = ys ↔ xs ⊆ ys :=
  ⟨fun h => h ▸ List.Subset.union_left, List.Subset.union_eq_right⟩

protected lemma List.Subset.union_self {α : Type*} [DecidableEq α] {xs : List α} : xs ∪ xs = xs := by simp

[Pranav cs22b015]

Any help for proving this?

theorem merge_idem_prime (s: Std.ExtTreeMap ℕ Int) (k: ℕ) (a: Int):
(merge_helper (Std.ExtTreeMap.keys s ∪ Std.ExtTreeMap.keys s) s s)[k]? = some a
→  s[k]? = some a

where merge_helper is defined as follows:

def sel (s : concrete_st) (k : ℕ) : Int := match (Std.ExtTreeMap.get? s k) with
| some n => n
| none => 0

def merge_helper (klist: List ℕ) (a b: concrete_st) : concrete_st :=
match klist with
| [] => {}
| key::keys => Std.HashMap.insert (merge_helper keys a b) key (max (sel a key) (sel b key))

[Pranav cs22b015]

From a theoretical standpoint, how does an ExtTreeMap behave differently from a TreeMap in terms of reference counting? Also, in the PR introducing ExtTreeMaps, the fact that trees maintain data in order made it possible for building an extensional version with equal representative power. Why is order important here? In other words, why is designing an ExtHashMap with iterability difficult?

[Robin Arnez]

Pranav cs22b015 schrieb:

From a theoretical standpoint, how does an ExtTreeMap behave differently from a TreeMap in terms of reference counting?

Not sure what you mean about theoretical standpoint but ExtTreeMap behaves exactly like TreeMap at runtime.

Pranav cs22b015 schrieb:

Why is order important here? In other words, why is designing an ExtHashMap with iterability difficult?

Order gives you a canonical iteration order. With ExtHashMap this is more difficult: You'll have to either prove that iteration order doesn't matter (some kind of commutativity on the operation) or preprocess the data to put it into a deterministic order (e.g. through sorting). The first one should come eventually though.

[Pranav cs22b015]

From the response, if I understand correctly, Extensionality on a TreeMap comes for free. My question also stems from the fact that in order to have extensionality, you only need to have decidable equality between the elements of the type constructing the keys of the map / set. Therefore, it is still unclear as to why order really matters. Iterability can be gained by attaching a separate iterator to walk through the map / set.

[Robin Arnez]

Pranav cs22b015 schrieb:

My question also stems from the fact that in order to have extensionality, you only need to have decidable equality between the elements of the type constructing the keys of the map / set

How do you come to that conclusion? docs#Std.ExtHashMap.ext_getKey_getElem? doesn't require decidability

[Robin Arnez]

The extensional variants of maps are defined as a quotient by equivalence on the regular map (e.g. docs#Std.DTreeMap.Equiv). Most operations are defined by lifting a function on the regular map to the quotient (e.g. see the equations tab under docs#Std.ExtDHashMap.insert). That however requires a proof that these operations are congruent (see e.g. docs#Std.DHashMap.Equiv.insert), i.e. that equivalent inputs produce equivalent outputs. Lifting docs#Std.DTreeMap.toList is possible because it is congruent under equivalence (docs#Std.DTreeMap.Equiv.toList_eq). This is however not the case for docs#Std.DHashMap since multiple equivalent hash maps may have different ordering of elements in toList.

[Robin Arnez]

And in case you're confused about why congruence matters so much:

import Std

-- both hash sets have different `toList` output
#eval ({1, 17} : Std.HashSet Nat).toList -- [1, 17]
#eval ({17, 1} : Std.HashSet Nat).toList -- [17, 1]

-- both extensional hash sets are equal
theorem th1 : ({1, 17} : Std.ExtHashSet Nat) = ({17, 1} : Std.ExtHashSet Nat) := by
  ext; simp [or_comm]

-- assume a `toList` operation exists
axiom Std.ExtHashSet.toList [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] : Std.ExtHashSet α → List α

-- both extensional hash sets must produce the same `toList` output (but they don't as regular hash sets!)
theorem th2 : ({1, 17} : Std.ExtHashSet Nat).toList = ({17, 1} : Std.ExtHashSet Nat).toList := by
  rw [th1]

-- => extensional hash set `toList` can't just be defined through `toList` on regular hash sets
````