Email Gateway (Aug 22 2022 at 13:53): Email Gateway (Aug 22 2022 at 13:53):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Lars,
coincidentally, I was using lift_bnf myself last week and run into exactly the same limitations as you did (except for the custom names which work fine as Jasmin pointed out).
I think your way of dealing with those limitations (they also apply to set and rel) are as good as it can get for now. They are on my list of things to improve. Eventually, I’ll report here when this happens.
Thanks for sharing,
Dmitriy
Email Gateway (Aug 22 2022 at 13:53):From: Lars Hupel <hupel@in.tum.de>
Hi Dmitriy,
glad to hear that you're on it :-)
For posterity, here's an improved version of getting transfer to work,
as pointed out by Johannes:
lemma fmmap_lifting[transfer_rule]:
"(op = ===> pcr_fmap op = op = ===> pcr_fmap op = op =)
(λf. op ∘ (map_option f)) fmmap"
The proof is a little bit more complicated, but this avoids introducing
an extraneous constant.
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:54):From: Lars Hupel <hupel@in.tum.de>
Dear BNF experts,
on the weekend I was toying with introducing a new type for finite maps
for my own formalization.¹
typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a ⇀ 'b) set"
morphisms fmlookup Abs_fmap
Luckily enough, registering this as a BNF is very simple:
lift_bnf ('a, 'b) fmap [wits: Map.empty]
by auto
This is very nice – thanks for that facility!
Constants such as 'map_fmap', 'set_fmap', 'rel_fmap' and 'pred_fmap' are
defined using composition of their underlying counterparts and the
abstraction function. For example:
map_fmap ≡ λf. Abs_fmap ∘ op ∘ (map_option f) ∘ fmlookup
This is as expected. However, I noticed some problems when working with
these constants wrt to other Isabelle tools and the BNF package itself:
The defining equations are not exported. I had to obtain them via
BNF_Def.bnf_of @{context} @{type_name fmap}
|> the
|> BNF_Def.map_def_of_bnf
I can't give them a custom name. If I want to rename 'map_fmap' to
'fmmap', I need to explicitly add an abbreviation.
Lifting is not set up for these constants which makes proving lemmas
over e.g. 'map_fmap' and the lifted version of 'op ++' very tedious.
Here's an example:
private lift_definition
fmmap0 :: "('b ⇒ 'c) ⇒ ('a, 'b) fmap ⇒ ('a, 'c) fmap"
is "λf m. map_option f ∘ m"
by simp
lemma fmmap0: "fmmap = fmmap0"
unfolding fmmap0_def (* prove via defining equation of 'fmmap' *)
lemma fmmap_add[simp]: "fmmap f (m ++⇩f n) = fmmap f m ++⇩f fmmap f n"
unfolding fmmap0
by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
I introduced an auxiliary constant which is equivalent to 'map_fmap',
but defined using 'lift_definition' instead of manually. I can use that
equivalence to rewrite propositions to make them amenable for 'transfer'.
Cheers
Lars
¹ Yes, I'm aware of FinFun, Fin_Map and Mapping, but neither of these
fit my purpose.
Email Gateway (Aug 22 2022 at 13:56):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Lars,
This is as expected. However, I noticed some problems when working with
these constants wrt to other Isabelle tools and the BNF package itself:
I will let Dmitriy and/or handle most of your questions, since they're in charge of these parts. But here's some immediate help regarding one of them.
The defining equations are not exported. I had to obtain them via
[...]I can't give them a custom name. If I want to rename 'map_fmap' to
'fmmap', I need to explicitly add an abbreviation.
The "them" in the second point presumably refers to the constants introduced by the command, esp. the map function and the relator.
In this case, I'm not sure where you get this notion from. If you look at "isabelle doc datatypes", you will find a syntactic item called map-rel in the syntax of "lift_bnf" and "copy_bnf". You can use that to specify custom names to the map function and the relator, e.g.
lift_bnf ('a, 'b) fmap [wits: Map.empty] for map: fmmap
by auto
I hope this helps.
Jasmin
Email Gateway (Aug 22 2022 at 13:58):From: Lars Hupel <hupel@in.tum.de>
Hi Jasmin,
I stand corrected. I thought I tried that syntax and it didn't work, but
I must have done something wrong. It works now.
Cheers
Lars
Last updated: Apr 25 2024 at 12:23 UTC