Discussion:
[isabelle] Usability of lift_bnf/copy_bnf
Lars Hupel
2016-08-01 07:31:10 UTC
Raw Message
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.
Jasmin Blanchette
2016-08-01 08:11:47 UTC
Raw Message
Dear Lars,
Post by Lars Hupel
This is as expected. However, I noticed some problems when working with
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.
Post by Lars Hupel
* 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
Lars Hupel
2016-08-01 08:23:09 UTC
Raw Message
Hi Jasmin,
Post by Jasmin Blanchette
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 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
Dmitriy Traytel
2016-08-01 20:45:02 UTC
Raw Message
Hi Lars,
Post by Lars Hupel
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
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
map_fmap ≡ λf. Abs_fmap ∘ op ∘ (map_option f) ∘ fmlookup
This is as expected. However, I noticed some problems when working with
* The defining equations are not exported. I had to obtain them via
|> 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.
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’.
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
Lars Hupel
2016-08-02 06:34:20 UTC
Raw Message
Hi Dmitriy,
Post by Dmitriy Traytel
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.
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