Stream: Beginner Questions

Topic: Introductory explanation of lifting and transfer


view this post on Zulip Jakub Kądziołka (Mar 19 2021 at 12:23):

I have ran into uprod - quotient type, something I have no practical experience with. If I understand correctly, the lifting and transfer tools are important facilities for working with quotients, so I'd like to learn something about them. However, I can't seem to find any introductory documentation on them. Looking through the documentation page, I've only been able to find a dry description in isar-ref, with no examples. Is there any more introductory material?

view this post on Zulip Lukas Stevens (Mar 19 2021 at 12:33):

There is src/HOL/ex/Transfer_Int_Nat.thy

view this post on Zulip Jakub Kądziołka (Mar 19 2021 at 21:36):

Hmm, I guess that helps somewhat. Though, I still don't see how I could prove something simple like

lift_definition pair_content :: "'a uprod ⇒ 'a multiset" is
  "λ(a, b). {# a, b #}" by auto

lemma "pair_content (Upair a b) = {# a, b #}"

view this post on Zulip Jakub Kądziołka (Mar 19 2021 at 23:16):

I've managed to prove this with by (simp add: Upair.abs_eq pair_content.abs_eq), is that the canonical approach, or am I going about this in a round-about way?

view this post on Zulip Manuel Eberl (Mar 20 2021 at 12:37):

No, it the idiomatic way would be something like by transfer auto, but it doesn't. I don't really understand why it doesn't work, but I never had a very good understanding of the transfer package.

view this post on Zulip Jakub Kądziołka (Mar 20 2021 at 12:52):

The transfer method leaves some schematic variables in the goals in this case. Is that normal, or could that be the problem?

view this post on Zulip Manuel Eberl (Mar 20 2021 at 12:57):

No, this normally happens when there's a missing transfer rule.

view this post on Zulip Manuel Eberl (Mar 20 2021 at 12:57):

And the first goal tells you what constant the rule is missing for.

view this post on Zulip Manuel Eberl (Mar 20 2021 at 12:57):

But sometimes I don't understand why it happens, and this is one of these cases.

view this post on Zulip Manuel Eberl (Mar 20 2021 at 12:58):

Sometimes transfer' does the trick in those cases, bot not here. I'm not even sure what transfer' does. Ondřej Kunčar told me it's bad and that I shouldn't use it.

view this post on Zulip Jakub Kądziołka (Mar 20 2021 at 13:06):

Hmm, I think it's trying to transfer through both uprod and multiset?

view this post on Zulip Manuel Eberl (Mar 20 2021 at 13:15):

That might be the problem, yes. I never really understood how to get around that.

view this post on Zulip Manuel Eberl (Mar 20 2021 at 13:15):

Maybe ask on the mailing list. I think the probability that someone knowledgeable on lifting and transfer will reply is higher there.

view this post on Zulip Lukas Stevens (Mar 20 2021 at 13:39):

If you haven't seen it already, there is also a file HOL/ex/Transfer_Debug.thy that goes through same cases where transfer fails and how to debug. (I have to add that I didn't find the file too illuminating)

view this post on Zulip Jakub Kądziołka (Mar 20 2021 at 13:55):

Yes, I've just noticed. I managed to craft the following proof with that method:

declare Upair_parametric[transfer_rule del]
lemma [simp]: "pair_content (Upair a b) = {# a, b #}"
  apply transfer_start
          apply (rule Rel_eq_refl)
         apply transfer_step+
  apply transfer_end
  by simp

view this post on Zulip Jakub Kądziołka (Mar 20 2021 at 13:58):

oh, actually, this works:

declare Upair_parametric[transfer_rule del] zero_multiset.transfer[transfer_rule del]
lemma [simp]: "pair_content (Upair a b) = {# a, b #}"
  by transfer simp

view this post on Zulip Lukas Stevens (Mar 20 2021 at 14:09):

What theories did you import? For me, it works without the declare.

view this post on Zulip Lukas Stevens (Mar 20 2021 at 14:11):

(On the development version of Isabelle and Isabelle2020)

view this post on Zulip Jakub Kądziołka (Mar 20 2021 at 14:12):

Oh, so apparently apply transfer by simp doesn't work and by transfer simp does...

view this post on Zulip Manuel Eberl (Mar 20 2021 at 14:39):

Yes, by transfer simp does backtracking.

view this post on Zulip Manuel Eberl (Mar 20 2021 at 14:39):

The other one does not.

view this post on Zulip Manuel Eberl (Mar 20 2021 at 14:39):

Beware though: transfer can cause excessive backtracking sometimes.


Last updated: Mar 28 2024 at 08:18 UTC