Liangrun Da (Jun 03 2024 at 06:50): Liangrun Da (Jun 03 2024 at 06:50):Hi! I'm working with Collections.Collections.hm and trying to prove the following lemma:
theory hm_test
imports Main "Collections.Collections"
begin
lemma hashmap_eq_iff_impl_eq:
"hm1 = hm2 ⟷ impl_of_RBT_HM hm1 = impl_of_RBT_HM hm2"
by (metis impl_of_RBT_HM_inject)
lemma map_not_equal:
assumes "m1 ≠ m2"
shows "∃k. hm.lookup k m1 ≠ hm.lookup k m2"
sorry
end
However I couldn't prove it. I am wondering if the issue might be because two hashmaps, even if they are not equal, do not necessarily have completely different key-value pairs. For example, two red black trees are structurally different but they actually have the same set of key-value pairs.
Mathias Fleury (Jun 03 2024 at 14:11):It feels like something that you should not have to prove. If you go for refinement, you should use a more abstract representation (mapping) where this would be easy to do
Mathias Fleury (Jun 03 2024 at 14:11):So i am slightly wondering: why do you want that?
Liangrun Da (Jun 03 2024 at 14:22):Mathias Fleury said:
It feels like something that you should not have to prove. If you go for refinement, you should use a more abstract representation (mapping) where this would be easy to do
Thanks for answering. It was a long story, but a simple explanation is: I tried to generate code for a graph structure and I defined an inductive predicate on it. Since the inductive predicate can't be converted to executable code directly, I tried to refine the graph structure with Collections.hm, in which I replace the inductive predicate with a recursively defined function on the hashmap. That's why I ended up with this lemma to be proved.
Mathias Fleury (Jun 03 2024 at 14:43):Maybe, but it still feels like the wrong approach. Iteration over the domain to check for equality seems the more structural approach
Mathias Fleury (Jun 03 2024 at 14:43):at least to me
Last updated: Dec 21 2024 at 16:20 UTC