Stream: Beginner Questions

Topic: Introductory explanation of lifting and transfer

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?

Lukas Stevens (Mar 19 2021 at 12:33):

There is src/HOL/ex/Transfer_Int_Nat.thy

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 #}"

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?

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.

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?

Manuel Eberl (Mar 20 2021 at 12:57):

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

Manuel Eberl (Mar 20 2021 at 12:57):

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

Manuel Eberl (Mar 20 2021 at 12:57):

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

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.

Jakub Kądziołka (Mar 20 2021 at 13:06):

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

Manuel Eberl (Mar 20 2021 at 13:15):

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

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.

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)

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

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

Lukas Stevens (Mar 20 2021 at 14:09):

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

Lukas Stevens (Mar 20 2021 at 14:11):

(On the development version of Isabelle and Isabelle2020)

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...

Manuel Eberl (Mar 20 2021 at 14:39):

Yes, by transfer simp does backtracking.

Manuel Eberl (Mar 20 2021 at 14:39):

The other one does not.

Manuel Eberl (Mar 20 2021 at 14:39):

Beware though: transfer can cause excessive backtracking sometimes.

Last updated: Dec 21 2024 at 16:20 UTC