Email Gateway (Aug 22 2022 at 14:17): Email Gateway (Aug 22 2022 at 14:17):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of the transfer package,
I have a problem with the transfer method (theory attached, Isabelle2016). In the lemma,
transfer is supposed to replace the function f2 with the function f1 using the
parametricity theorem for the operator foo (and thereby replace the natural number i with
an integer i in the domain of cr).
However, the proof does not go through, because the expected transfer relation for foo
(second goal after transfer_start) has a too specific type. In detail, the relation ?Rg12
has type "bool ⇒ (nat ⇒ bool) ⇒ bool", but it should be something like "(nat ⇒ bool) ⇒
(nat ⇒ bool) ⇒ bool" or "?'a ⇒ (nat ⇒ bool) ⇒ bool".
Where does this restricted type come from? And how can I make transfer work for this example?
Thanks,
Andreas
Scratch.thy
Email Gateway (Aug 22 2022 at 14:17):From: Ondřej Kunčar <kuncar@in.tum.de>
Hi Andreas,
this is a bug in the procedure that tries to preinstantiate some of the
schematic variables to cut down the search space. The procedure got
confused because part of your term got eta contracted after transfer
internally universally quantified over the free variables.
A possible workaround:
Quantify explicitly over n: "∀n. foo c (f2 i) n".
Ondrej
Email Gateway (Aug 22 2022 at 14:17):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Ondrej,
Thanks for digging into this. I'll live with the workaround until the bug is resolved.
Best,
Andreas
Last updated: Apr 25 2024 at 16:19 UTC