Email Gateway (Aug 19 2022 at 13:03): Email Gateway (Aug 19 2022 at 13:03):From: Daniel Raggi <danielraggi@gmail.com>
Dear transfer/lifting experts,
I've been experimenting with transfer and lifting and there is something
that I just haven't managed to understand.
I didn't have this problem before I upgraded from Isabelle2013 to
Isabelle2013-2 (and I suspect I would have also had it with Isabelle2013-1,
but I never used it)
Things similar to what I'm about to describe happen every time I define a
new type using quotient_type or typedef. I'll give a concrete example with
quotient_type (a type with two elements, as a quotient from integers):
quotient_type bin = int / "(λx y. [x = y] (mod 2))"
<proof>
Then I instantiate bin to the numeral class successfully and prove the
transfer rule that lets one transfer every int numeral to the 'same' bin
numeral:
lemma cr_bin_numeral [transfer_rule]: "cr_bin (numeral x) (numeral x)".
As far as I understand, this should be enough to do:
lemma "2 = (4::bin)"
apply transfer
to get subgoal "[2 = (4::int)] (mod 2)".
However, I get:
Here, the obvious value for ?a5 is the relation "λx y. [x = y] (mod 2)",
and actually this is by default with every quotient type definition, so I
don't understand why the transfer rule was not generated automatically in
the first place when I defined the new type. I thought it was already
automatic in Isabelle2013, and my theories actually broke down once I tried
running them on Isabelle2013-2 because of this issue.
The issue doesn't stop here, because even if I define the transfer rule
(cr_bin ===> cr_bin ===> op =) (λx y. [x = y] (mod 2)) op =
by hand I still get a problem when I try:
lemma "1 = (3::bin)"
apply transfer
What I get is
This is because 1 was actually lifted so that I could instantiate bin in
the numeral class, so it's transfer rule is generated differently. I'm not
familiar with the pcr_ thing. Can anyone explain this?
So, If I wanted to write the transfer rules for equality manually I would
have to make four rules:
(cr_bin ===> cr_bin ===> op =) (λx y. [x = y] (mod 2)) op =
(pcr_bin ===> cr_bin ===> op =) (λx y. [x = y] (mod 2)) op =
(cr_bin ===> pcr_bin ===> op =) (λx y. [x = y] (mod 2)) op =
(pcr_bin ===> pcr_bin ===> op =) (λx y. [x = y] (mod 2)) op =
I keep thinking that there's something essential I'm not understanding, but
maybe it's not me. I would greatly benefit from your feedback. I'm
attaching a test file with this experiment, if anyone wants to have a look.
Best,
Daniel
quot_experiment.thy
Email Gateway (Aug 19 2022 at 13:03):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Daniel,
the pcr_... relations generalise the cr_... relations. For types with type variables, they
allow other relations than equality for the type variables. If there is no type variable
(as in your example), pcr_... and cr_... are logically equivalent (theorem bin.pcr_cr_eq).
But since Isabelle2013-1, the lifting package expects that you use pcr_... in your custom
transfer rules rather than cr_... If you replace cr_... with pcr_... in your theory file,
transfer should work as you expect.
Best,
Andreas
Email Gateway (Aug 19 2022 at 13:03):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Daniel,
sorry for the inconvenience.
There is an easy fix: Rename cr_bin in your user-provided transfer rules
to pcr_bin.
Long answer: The transfer relation that is used in rules that are
generated by the Lifting package is now called pcr_T, which is a
generalization of cr_T and uses cr_T internally. You can prove "pcr_bin
= cr_bin" (thm bin.pcr_cr_eq) for your type bin because bin is not a
polymorphic type. In general pcr_T op= ... op= = cr_t. So what is pcr_T?
It's a relation that allows you to change the polymorphic argument of
your type (if there is one). E.g., consider 'a fset defined in
HOL/Library/FSet. Here cr_fset :: 'a set => 'a fset => bool, whereas
pcr_fset :: ('a => 'b => bool) => 'a set => 'b fset => bool. And
pcr_fset op= = cr_fset.
Btw, you don't have to import HOL/Library/Quotient_List since the
content of this file that is relevant for Lifting and Transfer has been
moved to Main. The syntax for Lifting (===> and --->) is now also local
and can be reintroduced by this trick:
context
begin
interpretation lifting_syntax .
...
end
Hope this helps.
Ondrej
Email Gateway (Aug 19 2022 at 13:03):From: Daniel Raggi <danielraggi@gmail.com>
Thank you, Andreas and Ondřej. It works now! I didn't understand why I was
getting both cr_T and pcr_T in different places. Now I see that cr appeared
because I had introduced it myself with my user defined transfer rules, and
pcr appeared because that's the way the transfer method works now. By
changing cr to pcr things work smoothly. Thanks!
Daniel
Last updated: Apr 19 2024 at 20:15 UTC