## 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: Aug 13 2022 at 06:26 UTC