Hernán Rajchert (Feb 24 2023 at 16:16): Hernán Rajchert (Feb 24 2023 at 16:16):Hi! I'm refactoring some proofs I have in a language interpreter that uses associative-list as a concrete representation for Maps.
The current version is thought with performance in mind, so the insert, delete and lookup assumes that the keys are distinct and sorted. This is useful when comparing two associative-list, as two AssocMap are equal if the list is equal, but they are troublesome when proving other stuff as I need to combine list induction with linorder_cases.
The partially refactored version (presented below) makes some tests easier, but now I can't just use equality, as two AssocMap with different sorting are different. This is made obvious in the insert_swap lemma, for which nitpick finds a counter-example.
I was able to express an equivalence relationship, and the insert_swap is proved automatically. But I fear that the simplifier won't be able to use this lemma as it is. I think the solution involves congruence rules, so I read the corresponding sections in the tutorial and in isar-ref, but I wasn't able to express a [cong] rule.
theory AssocMap
imports Main
begin
fun unique_keys :: "('k × 'v) list ⇒ bool" where
"unique_keys m = distinct (map fst m)"
lemma filterOfUniqueIsUnique :
assumes "unique_keys m"
shows "unique_keys (filter P m)"
using assms proof (induction m)
case Nil
then show ?case by simp
next
case (Cons head tail)
then show ?case
using Cons.prems distinct_map_filter unique_keys.simps by blast
qed
typedef
('k, 'v) AssocMap = "{m :: ('k × 'v) list. unique_keys m}"
by (rule_tac x = "[]" in exI) auto
setup_lifting type_definition_AssocMap
lift_definition empty :: "('k, 'v) AssocMap"
is "[]"
by simp
fun delete' :: "'k ⇒ ('k × 'v) list ⇒ ('k × 'v) list" where
"delete' k m = filter (λ(mK, mV). mK ≠ k) m"
lift_definition
delete :: "'k ⇒ ('k, 'v) AssocMap ⇒ ('k, 'v) AssocMap"
is delete'
by (simp add: distinct_map_filter)
lift_definition
insert :: "'k ⇒ 'v ⇒ ('k, 'v) AssocMap ⇒ ('k, 'v) AssocMap"
is "λk v m. (k, v) # (delete' k m)"
using distinct_map_filter by auto
lemma insert_swap :
"k1 ≠ k2 ⟹ insert k1 v1 (insert k2 v2 m) = insert k2 v2 (insert k1 v1 m)"
(* nitpick finds the following counter-example, and it makes sense,
they are not equal, they are equivalent.
k1 = a⇩1
k2 = a⇩2
m = «[(a⇩2, b⇩1)]»
v1 = b⇩2
v2 = b⇩1
*)
oops
lift_definition assocMapEquiv :: "('k, 'v) AssocMap ⇒ ('k, 'v) AssocMap ⇒ bool" (infix "≡⇩a" 50)
is
"λa b. (∀e. e ∈ set a ⟷ e ∈ set b)" .
lemma insert_swap :
"k1 ≠ k2 ⟹ insert k1 v1 (insert k2 v2 m) ≡⇩a insert k2 v2 (insert k1 v1 m)"
by transfer auto
(* How can I define a congruence rule so that the simplifier is able to make the swap? *)
My initial attempt was to refactor the current theory, which requires manual passing of the valid_map assumption, into a typedef, but as I mentioned before some proofs are harder than need to because of the sorting.
theory AssocMap
imports Main
begin
section "Associative Map"
fun unique_keys :: "('k × 'v) list ⇒ bool" where
"unique_keys m = distinct (map fst m)"
fun sorted_keys :: "('k::linorder × 'v) list ⇒ bool" where
"sorted_keys m = sorted (map fst m)"
lemma sorted_keys_cons :
assumes "sorted_keys (tail)"
and "⋀tK tV. (tK, tV) ∈ set tail ⟹ hK < tK"
shows "sorted_keys ((hK, hV) # tail)"
proof -
have "⋀tK tV. (tK, tV) ∈ set tail ⟹ hK ≤ tK"
by (simp add: assms(2) dual_order.order_iff_strict)
then show ?thesis
using assms by auto
qed
typedef (overloaded)
('k::linorder, 'v) AssocMap (*<*) = "{m :: ('k × 'v) list.
(unique_keys m ∧ sorted_keys m)
}"
by (rule_tac x = "[]" in exI) auto
setup_lifting type_definition_AssocMap
lift_definition empty :: "('k::linorder, 'v) AssocMap"
is "[]"
by simp
fun insert' :: "'k::linorder ⇒ 'v ⇒ ('k × 'v) list ⇒ ('k × 'v) list" where
"insert' k v [] = [(k, v)]"
| "insert' k v ((hK, hV) # tail) =
(if k < hK then (k, v) # [(hK, hV)] @ tail
else if k = hK then (k, v) # tail
else (hK, hV) # insert' k v tail
)"
lemma pInsert_union : "set (map fst (insert' k v m)) = set [k] ∪ set (map fst m)"
proof (induction m)
case Nil
then show ?case by simp
next
case (Cons head tail)
then obtain hK hV where "head = (hK, hV)"
by fastforce
then show ?case
using list.simps(9) local.Cons set_append sup.left_idem sup_left_commute by force
qed
lift_definition insert :: "'k::linorder ⇒ 'v ⇒ ('k, 'v) AssocMap ⇒ ('k, 'v) AssocMap"
is insert'
subgoal for k v m
proof (induction m)
case Nil
then show ?case
by simp
next
case (Cons head tail)
then obtain hK hV where pHead: "head = (hK, hV)"
by fastforce
then show ?case
proof (cases rule: linorder_cases[of k hK])
assume "k < hK"
then show ?thesis
using pHead Cons.prems by auto
next
assume "k = hK"
then show ?thesis
using pHead Cons.prems by force
next
assume "k > hK"
moreover note Cons.IH Cons.prems pHead
moreover have "⋀tK tV. (tK, tV) ∈ set (insert' k v tail) ⟹ hK ≤ tK"
using calculation by (metis (no_types, opaque_lifting) append_Cons append_Nil fst_conv insert_iff list.set_map list.simps(15) list.simps(9) map_of_eq_None_iff option.distinct(1) order_less_imp_le pInsert_union set_append sorted_keys.elims(2) sorted_simps(2) weak_map_of_SomeI)
moreover have "sorted_keys (insert' k v tail)"
using calculation by force
moreover have "sorted_keys ((hK, hV) # insert' k v tail)"
using calculation by auto
moreover have "unique_keys ((hK, hV) # insert' k v tail)"
apply auto
using calculation apply (metis (no_types, lifting) UnE empty_iff fst_conv list.set(1) list.set_map list.simps(9) map_of_eq_None_iff not_less_iff_gr_or_eq option.distinct(1) pInsert_union set_ConsD sorted_keys.elims(2) strict_sorted_iff strict_sorted_simps(2) unique_keys.elims(2) weak_map_of_SomeI)
using calculation by simp
ultimately show ?thesis
by (metis insert'.simps(2) order_less_imp_not_less)
qed
qed
done
end
As a bonus question, if I define the two versions of AssocMap (performant and not performant), I should be able to prove that insert, lookup and delete are equivalent, but can I interchange them? Maybe to be able to prove stuff using the not performant representation but to use code equations to the performant implementation when I'm generating Haskell code.
Last updated: Dec 21 2024 at 16:20 UTC