feat: add Heap instances for TreeMap and ExtTreeMap #106
Conversation
alok
force-pushed
the
feat/heap-instances-105
branch
from
ddf9987 to
0a27a2f
Compare
alok
force-pushed
the
feat/heap-instances-105
branch
4 times, most recently
from
6bb7a12 to
e9f9512
Compare
|
Nice, thanks for doing this! |
|
thanks @claude |
markusdemedeiros
left a comment
markusdemedeiros
left a comment
There was a problem hiding this comment.
Good start! This might be okay to use in unstable, but the proofs are very redundant and need to be refactored before merging into main. Please review some of the other files in the development to get a better idea of our style.
I have left some high-level comments and will review again after the code is cleaned up.
src/Iris/Std/HeapInstances.lean
Outdated
| | some v => simp [alterFn] | ||
| · rw [Impl.Const.get?_alter! hinit] | ||
| simp only [heq, ↓reduceIte] | ||
| have hfind : List.find? (fun kv => compare kv.1 k == .eq) (hd :: tl) = |
| cases Impl.Const.get? init k <;> rfl | ||
| | cons hd tl ih => | ||
| simp only [List.foldl_cons] | ||
| let alterFn : Option V → Option V := fun |
There was a problem hiding this comment.
Can be simplified using more Option primitives
| (l.foldl (fun acc kv => acc.alter kv.1 fun | ||
| | none => some kv.2 | ||
| | some v1 => some (f kv.1 v1 kv.2)) init)[k]? = | ||
| match init[k]?, l.find? (fun kv => cmp kv.1 k == .eq) with |
There was a problem hiding this comment.
This is just Option.merge f
src/Iris/Std/HeapInstances.lean
Outdated
| cases init[hd.1]? <;> rfl | ||
| · -- hd.1 doesn't match k | ||
| simp only [getElem?_alter, heq, ↓reduceIte] | ||
| have hfind : List.find? (fun kv => cmp kv.1 k == .eq) (hd :: tl) = |
| rw [hfind] | ||
|
|
||
| /-- TreeMap.mergeWith equals list foldl with alter at the getElem? level. -/ | ||
| theorem getElem?_mergeWith_eq_foldl [LawfulEqCmp cmp] {t₁ t₂ : TreeMap K V cmp} |
There was a problem hiding this comment.
This proof is long. Can you break it up and simplify please?
src/Iris/Std/HeapInstances.lean
Outdated
| have hfind : List.find? (fun kv => compare kv.1 k == .eq) (hd :: tl) = | ||
| tl.find? (fun kv => compare kv.1 k == .eq) := by | ||
| simp only [List.find?_cons] | ||
| have hne : (compare hd.1 k == .eq) = false := by simp [beq_eq_false_iff_ne, heq] |
There was a problem hiding this comment.
have+simp can be inlined
src/Iris/Std/HeapInstances.lean
Outdated
| by_cases heq : cmp hd.1 k = .eq | ||
| · -- hd.1 matches k | ||
| simp only [getElem?_alter, getElem?_congr (OrientedCmp.eq_symm heq)] | ||
| have hfind : List.find? (fun kv => cmp kv.1 k == .eq) (hd :: tl) = some hd := by |
There was a problem hiding this comment.
have+rw can be inlined
src/Iris/Std/HeapInstances.lean
Outdated
| have hfind_eq := h_find t₂.inner.inner.toListModel | ||
| rw [← h_toList] at hfind_eq | ||
|
|
||
| cases hres : t₂.inner.inner.toListModel.find? (fun kv => cmp kv.1 k == .eq) with |
There was a problem hiding this comment.
Nearly identical match arms, can you factor out the have+simp somehow?
| @[simp] theorem getElem?_mergeWith' [LawfulEqCmp cmp] {t₁ t₂ : TreeMap K V cmp} | ||
| {f : K → V → V → V} {k : K} : | ||
| (t₁.mergeWith f t₂)[k]? = | ||
| match t₁[k]?, t₂[k]? with |
There was a problem hiding this comment.
This is Option.merge
src/Iris/Std/HeapInstances.lean
Outdated
| -- Use the helper lemma that connects mergeWith to foldl | ||
| have mergeWith_eq := getElem?_mergeWith_eq_foldl (t₁ := t₁) (t₂ := t₂) (f := f) (k := k) | ||
|
|
||
| -- Case split based on t₁[k]? and t₂[k]? |
There was a problem hiding this comment.
Identical match arms
alok
force-pushed
the
feat/heap-instances-105
branch
2 times, most recently
from
f32b896 to
c4b3448
Compare
Implements Heap typeclass instances for Batteries' TreeMap and ExtTreeMap, enabling their use in Iris separation logic proofs. Key additions: - Store instances for TreeMap/ExtTreeMap (insert, alter, erase operations) - Heap instances with disjoint union via mergeWith - Helper lemmas connecting TreeMap operations to list-based specifications - Uses grind tactic for cleaner proofs where applicable
alok
force-pushed
the
feat/heap-instances-105
branch
from
c4b3448 to
8f928e4
Compare
|
Just FYI I think there is a git error here, you seemed to push a bunch of unrelated commits like |
2 participants
Summary
StoreandHeapinstances forTreeMap K V cmpandExtTreeMap K V cmpStore,Heap,RepFunStore, andIsoFunStoreinstances for function typesgetElem?_mergeWith'lemma for both map types with full WF tracking through internal foldl operationsImplementation
The key challenge was proving
getElem?_mergeWith'which requires tracking well-formedness throughStd.DTreeMap.Internal.Imploperations. This was solved by:get?_foldl_alter_impl_sigma,foldl_alter_getElem?) that track WF through foldl with alter operationsordered_iff_pairwise_keysto derive pairwise distinctness from the tree's Ordered propertyTest plan
lake buildpasses with no sorriesCloses #105