Email Gateway (Aug 19 2022 at 09:50): Email Gateway (Aug 19 2022 at 09:50):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
When experimenting with lifting and transfer, I ran into situations
where transfer yields funny goal states. I have distilled two prominent
candidates into the attached theories. The first one seems to me a
result of erroneous backtracking in a tactic behind the transfer method.
For the second one, I am standing in the dark.
Maybe experts on transfer can comment on this.
Cheers,
Florian
Transfer_Report.thy
signature.asc
Email Gateway (Aug 19 2022 at 09:51):From: Peter Lammich <lammich@in.tum.de>
On Do, 2013-01-31 at 10:58 +0100, Florian Haftmann wrote:
When experimenting with lifting and transfer, I ran into situations
where transfer yields funny goal states. I have distilled two prominent
candidates into the attached theories. The first one seems to me a
result of erroneous backtracking in a tactic behind the transfer method.
For the second one, I am standing in the dark
Not being an expert on the impl of transfer, the second one looks like
an artifact of a higher-order unification, where one intended a
first-order matching ...
.
Maybe experts on transfer can comment on this.
Cheers,
Florian
Email Gateway (Aug 19 2022 at 09:51):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Florian,
Example 1:
yes, transfer backtracks: first uses later introduced matching transfer
rules and then it tries earlier introduced rules. So if you do this:
lemma
fixes m n q :: natural
shows "(m + n) * q = m * q + n * q"
apply transfer
back
back
back
back
back
back
back
back
you get:
1. ?a21 (λm. transfer_forall (λn. transfer_forall (λq. (m + n) * q = m
q + n * q)))
The first goal is solved by simplifier by substituting (λa. True) for
?a21 and then you get the second goal to prove. That's the reason it
doesn't fail because the simplifier did some progress.
Example 2:
No surprise. Transfer knows that the abstraction function natural_of_nat
transfers to identity on the raw level (i.e., there is a transfer rule
for this; the rule is proved in setup_lifting) but it doesn't know
anything about of_nat. Thut it transfers natural_of_nat to id and it
doesn't do anything with of_nat. Because the types doesn't match it
cannot transfer equality to equality on the raw level and thus it asks
for a rule saying what equality should be transferred to.
If you prove a transfer rule for of_nat
lemma [transfer_rule]:
"(op= ===> cr_natural) (of_nat::nat=>nat) (of_nat::nat=>natural)"
unfolding of_nat_def[abs_def] by transfer_prover
then you can finish your proof:
lemma natural_of_nat_of_nat [simp]:
"natural_of_nat = of_nat"
by transfer auto
I hope my answer helps.
Ondrej
Email Gateway (Aug 19 2022 at 09:51):From: Ondřej Kunčar <kuncar@in.tum.de>
just a side remark:
The type annotations are not necessary but I think they improve the
readability.
Ondrej
Last updated: Nov 21 2024 at 12:39 UTC