Email Gateway (Aug 22 2022 at 18:53): Email Gateway (Aug 22 2022 at 18:53):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to ask a technical question with regard to the
best-recommended practices for using the lifting/transfer capabilities of
Isabelle/HOL in one particular scenario.
Suppose there exist 4 distinct types: AS, AT, BQ, BT. The type AS is a
subtype of the type AT and the type BQ is a quotient type of the type BT
(the specific relationships between the pairs “AS and AT” and “BQ and BT”
are of secondary importance). Furthermore, suppose that the types AS and BQ
are isomorphic. Suppose, for a certain application, it would be useful to
transfer results/definitions from BQ to AS. I would like to understand what
is the best practice for performing the transfer.
At the moment, I use the following solution:
1. I provide functions BQ_of_AS (“representation”) and AS_of_BQ
(“abstraction”) that allow for conversion between the types and show that
these functions are bijective and are inverses of each other.
2. I provide all lemmas similar to those that are automatically
generated during the definition of a type copy, e.g. BQ_of_AS_cases,
BQ_of_AS_induct, …, type_definition_BQ_AS, etc
3. I use “setup_lifting type_definition_BQ_AS” to automatically generate
further lemmas.
4. For each pair of functions (of interest) of BQ and AS, I provide
transfer rules explicitly.
This approach seems to work well for my application. However, I have
concerns about whether or not this approach is considered to be a good
practice and whether or not it is optimal for the application. In
particular, I would like to ask the following questions:
1. In step 2 in my solution, is it necessary to provide the lemmas
explicitly, i.e. is it possible to, somehow, automate the process of the
generation of the lemmas?
2. In step 3 in my solution, is it considered to be a good practice to
use setup_lifting, given that AS was not ‘derived’ from BQ? Could this
cause conflicts if setup_lifting has already been used for the type AS in a
different context?
3. In relation to step 4, is it possible to automate the process of
transfer further, i.e. beyond proving each transfer relation explicitly,
given that there exists a bijective transformation between the types?
Any other comments with regard to my solution and proposals for better
alternatives will be appreciated.
I provide an example that is closely related to my application. In the
example, the type AS is the type fmap from HOL-Library, the type AT is the
type map from HOL, the type BQ is my own type fmaplist and the type BT is
the type alist from HOL-Library. The subsections that are named <Step N> in
the code correspond to the steps in the outline of my solution above.
theory ml_example
imports
Complex_Main
"HOL-Library.Finite_Map"
"HOL-Library.DAList"
"HOL-Library.Permutation"
begin
subsection ‹Auxiliary›
abbreviation "dmf ≡ distinct ∘ map fst"
lift_definition aperm ::
"('key, 'val) alist ⇒ ('key, 'val) alist ⇒ bool" ("_ <~~>a _" [50, 50]
50)
is Permutation.perm .
lemma aperm_trans [intro]: "xs <>a ys ⟹ ys <>a zs ⟹ xs <~~>a zs"
by transfer auto
lemma aperm_sym: "xs <>a ys ⟹ ys <>a xs"
by transfer (rule perm_sym)
lemma map_of_eq_mset:
assumes "dmf xs" and "dmf ys"
shows "map_of xs = map_of ys ⟷ mset xs = mset ys"
apply(insert assms, rule)
apply(simp add: distinct_map map_of_inject_set
set_eq_iff_mset_eq_distinct)
using map_of_inject_set mset_eq_setD by fastforce
lemma map_of_eq_perm:
assumes "dmf xs" and "dmf ys"
shows "map_of xs = map_of ys ⟷ xs <~~> ys"
using assms map_of_eq_mset mset_eq_perm by auto
lemma perm_eq_fmap_of_list:
assumes "dmf xs" and "dmf ys"
shows "xs <~~> ys ⟷ fmap_of_list xs = fmap_of_list ys"
proof
assume "xs <~~> ys"
with assms have "map_of xs = map_of ys"
by (simp add: map_of_inject_set perm_set_eq)
then have "fmlookup (fmap_of_list xs) = fmlookup (fmap_of_list ys)"
by (simp add: fmlookup_of_list)
thus "fmap_of_list xs = fmap_of_list ys" by (rule fmlookup_inject[THEN
iffD1])
next
assume "fmap_of_list xs = fmap_of_list ys"
then have "fmlookup (fmap_of_list xs) = fmlookup (fmap_of_list ys)" by
simp
then have "map_of xs = map_of ys" by (simp add: fmlookup_of_list)
with assms show "xs <~~> ys" by (rule map_of_eq_perm[THEN iffD1])
qed
lemma exists_distinct_fst_fmap_of_list:
"∃xa. (distinct ∘ list.map fst) xa ∧ fmap_of_list xa = m"
including fmap.lifting
by transfer (metis comp_def distinct_clearjunk exists_map_of
map_of_clearjunk)
subsection ‹Type Definition›
quotient_type ('a, 'b) fmaplist = "('a, 'b) alist" / "aperm"
morphisms impl_of FMapList
proof(rule equivpI)
show "reflp aperm" by (simp add: aperm.rep_eq reflp_def)
show "symp aperm" unfolding symp_def using aperm_sym by blast
show "transp aperm" by (metis aperm_trans transpI)
qed
lift_definition fml_lookup :: "('key, 'val) fmaplist ⇒ 'key ⇒ 'val option"
is DAList.lookup
by transfer (simp add: map_of_inject_set perm_set_eq)
(* ... *)
subsection ‹Step 1›
subsubsection ‹Step 1.1 - Auxiliary›
lift_definition fmap_of_alist :: "('a, 'b) alist ⇒ ('a, 'b) fmap"
is fmap_of_list .
lemma perm_eq_fmap_of_alist:
"xs <~~>a ys ⟷ fmap_of_alist xs = fmap_of_alist ys"
by transfer (rule perm_eq_fmap_of_list)
lemma exists_distinct_fst_fmap_of_alist: "∃xs. fmap_of_alist xs = m"
by transfer (insert exists_distinct_fst_fmap_of_list, auto)
lemma surj_fmap_of_alist: "surj fmap_of_alist"
unfolding image_def by (auto, metis exists_distinct_fst_fmap_of_alist)
subsubsection ‹Step 1.2 - Definitions›
lift_definition fmap_of_fmaplist :: "('a, 'b) fmaplist ⇒ ('a, 'b) fmap"
is fmap_of_alist
by (rule perm_eq_fmap_of_alist[THEN iffD1])
definition fmaplist_of_fmap :: "('a, 'b) fmap ⇒ ('a, 'b) fmaplist" where
"fmaplist_of_fmap = the_inv_into UNIV fmap_of_fmaplist"
lemma inj_fmap_of_fmaplist: "inj fmap_of_fmaplist"
by (rule, simp, transfer) (simp add: perm_eq_fmap_of_alist)
lemma surj_fmap_of_fmaplist: "surj fmap_of_fmaplist"
by transfer (auto simp add: surj_fmap_of_alist)
lemma bij_fmap_of_fmaplist: "bij fmap_of_fmaplist"
by (insert inj_fmap_of_fmaplist surj_fmap_of_fmaplist, rule bijI)
lemma bij_fmaplist_of_fmap: "bij fmaplist_of_fmap"
unfolding fmaplist_of_fmap_def using bij_fmap_of_fmaplist
by (simp add: bij_fmap_of_fmaplist bij_betw_the_inv_into)
lemma inj_fmaplist_of_fmap: "inj fmaplist_of_fmap"
using bij_betw_def bij_fmaplist_of_fmap by auto
lemma surj_fmaplist_of_fmap: "surj fmaplist_of_fmap"
by (simp add: bij_fmaplist_of_fmap bij_betw_imp_surj_on)
subsection ‹Step 2›
lemma fmap_of_fmaplist_cases:
"(⋀y. x = fmap_of_fmaplist y ⟹ y ∈ UNIV ⟹ P) ⟹ P"
by (metis UNIV_I bij_fmap_of_fmaplist f_the_inv_into_f_bij_betw)
lemma fmap_of_fmaplist_induct:
"(⋀y. y ∈ UNIV ⟹ P (fmap_of_fmaplist y)) ⟹ P x"
by (metis fmap_of_fmaplist_cases iso_tuple_UNIV_I)
lemma fmap_of_fmaplist_inject:
"x ∈ UNIV ⟹
y ∈ UNIV ⟹
(fmap_of_fmaplist x = fmap_of_fmaplist y) = (x = y)"
by (meson inj_fmap_of_fmaplist inj_onD)
lemma fmap_of_fmaplist_inverse:
"y ∈ UNIV ⟹ fmaplist_of_fmap (fmap_of_fmaplist y) = y"
by (simp add: fmaplist_of_fmap_def inj_fmap_of_fmaplist the_inv_f_f)
lemma fmaplist_of_fmap: "fmaplist_of_fmap x ∈ UNIV" ..
lemma fmaplist_of_fmap_cases:
"y ∈ UNIV ⟹ (⋀x. y = fmaplist_of_fmap x ⟹ P) ⟹ P"
by (metis fmap_of_fmaplist_inverse)
lemma fmaplist_of_fmap_induct:
"y ∈ UNIV ⟹ (⋀x. P (fmaplist_of_fmap x)) ⟹ P y"
by (metis fmap_of_fmaplist_inverse)
lemma fmaplist_of_fmap_inject:
"(fmaplist_of_fmap x = fmaplist_of_fmap y) = (x = y)"
by (meson injD inj_fmaplist_of_fmap)
lemma fmaplist_of_fmap_inverse: "fmap_of_fmaplist (fmaplist_of_fmap x) = x"
using fmap_of_fmaplist_inverse fmaplist_of_fmap_inject by auto
lemma type_definition_fmaplist_fmap:
"type_definition fmaplist_of_fmap fmap_of_fmaplist UNIV"
unfolding type_definition_def
by (simp add: fmap_of_fmaplist_inverse fmaplist_of_fmap_inverse)
subsection ‹Step 3›
setup_lifting type_definition_fmaplist_fmap
subsection ‹Step 4›
context includes lifting_syntax
begin
lemma fmlookup_fml_lookup_transfer_1:
"((λ m ml. m = fmap_of_fmaplist ml) ===> (=) ===> (=)) fmlookup
fml_lookup"
unfolding rel_fun_def by (transfer, auto, transfer, simp add:
fmlookup_of_list)
lemma fmlookup_fml_lookup_transfer_2 [transfer_rule]:
"((λ m ml. cr_fmap ml m) ===> (=) ===> (=)) fmlookup fml_lookup"
unfolding rel_fun_def cr_fmap_def
by auto
(metis (mono_tags, lifting)
fmaplist_of_fmap_inverse
fmlookup_fml_lookup_transfer_1
rel_funD)
lemma fml_lookup_fmlookup_transfer_2 [transfer_rule]:
"((λ ml m. cr_fmap ml m) ===> (=) ===> (=)) fml_lookup fmlookup"
unfolding rel_fun_def cr_fmap_def
by auto
(metis (mono_tags, lifting)
fmaplist_of_fmap_inverse
fmlookup_fml_lookup_transfer_1
rel_funD)
lemma fml_fm_transfer_forall_transfer [transfer_rule]:
"((cr_fmap ===> (=)) ===> (=)) transfer_forall transfer_forall"
unfolding transfer_forall_def rel_fun_def cr_fmap_def
using fmaplist_of_fmap_induct by auto
(* ... *)
end
end
Email Gateway (Aug 22 2022 at 18:53):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi there,
Your approach looks sensible. There is nothing wrong with manually providing transfer
rules. But you should be careful with which rules are declared as [transfer_rule] at a
given point in time. The transfer proof method (and its friends) can easily get confused
when you have several rules for the same constant. Often, transfer just tries all
combinations until it finds a suitable one, but this can quickly exceed one's patience for
larger goals. One way to do so is to prove all rules between the isomorphic types'
constants in a locale (without parameters) and locally "interpret" the locale whenever
these rules are needed. Example:
locale AS_BQ begin
lemma fml_lookup_fmlookup_transfer_2 [transfer_rule]: ...
end
context begin
interpretation AS_BQ ..
lemma ...
by transfer ... (* uses the isomorphism rules *)
end
lemma ...
by transfer ... (* does not use the isomorphism rules *)
Moreover, I think that you can simplify things a bit by eliminating one of the isomorphic
types AS or BQ completely. In your example, you do not seem to exploit anything from the
quotient package. Rather, you simply prove that the quotiented definition of alist
correspond to the definitions on fmap. You should be able to prove this refinement
directly between the operations on alist and fmap.
That is, manually define a representation function corresponding to the abstraction
function fmap_of_alist and prove the Quotient theorem that quotient_type generates under
the name Quotient_fmaplist. Then, declare a locale to collect all the transfer rules
between fmap and alist:
locale fmap_as_alist begin
setup_lifting Quotient_fmaplist
In this locale, you can prove all the transfer rules that the various lift_definitions for
fmaplist generate, but for the functions on fmap. When you need the quotient view on fmap,
then you can interpret fmap_as_alist in a local context as shown above and use it.
Now to your remaining questions:
Once you have proven the type_definition theorems, then the other theorems that you'd
get from a typedef can be obtained by interpreting the locale type_definition.
For quotients, there is unfortunately no such locale. But once you've proven the
Quotient theorem, you can get the desired theorems by instantiating the abstract theorems
from theory Quotient (lemma Quotient_abs_rep and below), e.g.
lemmas fmaplist_abs_rep = Quotient_abs_rep[OF Quotient_fmaplist]
and fmaplist_rep_reflp = Quotient_rep_reflp[OF Quotient_fmaplist]
and ...
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 18:53):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Andreas Lochbihler,
Thank you for your reply. Indeed, I found your advice very helpful.
In fact, you have also answered a question that I was going to include in
my email, but for some reason forgotten about after I started writing the
email. Indeed, I was not entirely certain how to ensure that the most
relevant transfer rules are applied upon calling the transfer proof method.
Thank you
Last updated: Nov 21 2024 at 12:39 UTC