Email Gateway (Aug 18 2022 at 20:15): Email Gateway (Aug 18 2022 at 20:15):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
When I use the transfer package, I frequently have to prove extra transfer rules
for some operations when tuples are involved. Some examples can be found in
Coinductive_Stream.thy in the AFP entry Coinductive (development version
dd789a56473c). Here's a typical one:
lemma SCons_prod_transfer [transfer_rule]:
"(prod_rel op = op = ===> cr_stream ===> cr_stream) LCons SCons"
unfolding prod_rel_eq by(rule SCons.transfer)
These rules are straightforward to prove (by unfolding prod_rel_eq, fun_rel_eq,
etc. and using existing transfer rules), so I would prefer not having to state
and declare them separately. Is this to due insufficient declarations of mine or
a general limitation of the current implementation?
In case of the former: What do I have to do to avoid these kind of boilerplate
rules?
Andreas
Email Gateway (Aug 18 2022 at 20:15):From: Brian Huffman <huffman@in.tum.de>
This is a limitation of the current implementation -- not of the
transfer method per se, but of the form of transfer rules generated by
the lift_definition command.
When lifting a polymorphic constant, the ideal transfer rule should
have a form that looks just like the constant's type signature, with
relation variables in place of type variables. For quotient types with
type parameters, the transfer relation should ideally also have a
relation parameter too, like this:
SCons_prod.transfer [transfer_rule]:
"(A ===> cr_stream A ===> cr_stream A) LCons SCons"
A slightly less ambitious implementation might just replace
occurrences of "op =" at type 'a with a variable, which is separately
constrained to be an equality relation:
definition "is_equality R = (R = (op =))"
lemma is_equality_intros [transfer_rule]:
"is_equality (op =)"
"is_equality A ==> is_equality B ==> is_equality (fun_rel A B)"
"is_equality A ==> is_equality B ==> is_equality (prod_rel A B)"
SCons_prod.transfer [transfer_rule]:
"is_equality A ==> (A ===> cr_stream ===> cr_stream) LCons SCons"
I tested the latter style of rules on Coinductive_Stream.thy, and
everything seems to work fine with just one transfer rule per
constant. I guess we'll try to make lift_definition generate rules
directly in this format.
Anyway, thanks for the feedback on lifting/transfer!
Email Gateway (Aug 18 2022 at 20:16):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Brian,
Thanks for looking into this.
A slightly less ambitious implementation might just replace
occurrences of "op =" at type 'a with a variable, which is separately
constrained to be an equality relation:definition "is_equality R = (R = (op =))"
lemma is_equality_intros [transfer_rule]:
"is_equality (op =)"
"is_equality A ==> is_equality B ==> is_equality (fun_rel A B)"
"is_equality A ==> is_equality B ==> is_equality (prod_rel A B)"SCons_prod.transfer [transfer_rule]:
"is_equality A ==> (A ===> cr_stream ===> cr_stream) LCons SCons"
This approach looks promising because most of the other rules I have also just
to thread "op =" through.
Anyway, thanks for the feedback on lifting/transfer!
When I'm at it: There's one FIXME comment in Coinductive_Stream. szip_iterates
is actually lzip_iterates from Coinductive_List_Lib lifted over the morphism.
Unfortunately, the transfer method only replaces the left hand side, but not the
right hand side, so I had to prove the equation directly.
If you have time to look into that, it would be great to know why it does not
work here as expected.
Email Gateway (Aug 18 2022 at 20:16):From: Brian Huffman <huffman@in.tum.de>
On Thu, Jun 28, 2012 at 10:23 AM, Andreas Lochbihler
<andreas.lochbihler@kit.edu> wrote:
A slightly less ambitious implementation might just replace
occurrences of "op =" at type 'a with a variable, which is separately
constrained to be an equality relation:definition "is_equality R = (R = (op =))"
lemma is_equality_intros [transfer_rule]:
"is_equality (op =)"
"is_equality A ==> is_equality B ==> is_equality (fun_rel A B)"
"is_equality A ==> is_equality B ==> is_equality (prod_rel A B)"SCons_prod.transfer [transfer_rule]:
"is_equality A ==> (A ===> cr_stream ===> cr_stream) LCons SCons"
[...]
When I'm at it: There's one FIXME comment in Coinductive_Stream.
szip_iterates is actually lzip_iterates from Coinductive_List_Lib lifted
over the morphism. Unfortunately, the transfer method only replaces the left
hand side, but not the right hand side, so I had to prove the equation
directly.If you have time to look into that, it would be great to know why it does
not work here as expected.
It seems that this was an instance of the same kind of problem. After
generalizing the transfer rules, the transfer proof works now. See the
changeset on AFP:
http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/a05edd1f98f8
Last updated: Apr 23 2024 at 08:19 UTC