Email Gateway (Aug 22 2022 at 10:37): Email Gateway (Aug 22 2022 at 10:37):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of parametricity and the transfer package,
I am struggling to prove parametricity of a big function defined by primitive recursion
over a largish tree datatype. I thought I'd use the transfer prover from the transfer
package. Unfortunately, it is driving me almost crazy as it appears as completely
non-deterministic to me when it is able to prove the parametricity statement and when not
(even if parametricity rules for all constants have been declared as [transfer_rule]).
Here are two minimised examples which I do not understand. They are also in the attached
theory (tested with Isabelle2015 and Isabelle/c1b7793c23a3). Why does transfer_prover fail
to prove the rules? And what can I do to make transfer_prover work?
interpretation lifting_syntax .
consts f :: "nat ⇒ nat"
lemma
"(op = ===> B ===> rel_option (rel_prod op = B))
(λx y. Option.bind x (λx. Some (f x, y)))
(λx y. Option.bind x (λx. Some (f x, y)))"
by transfer_prover (* fails *)
lemma (* same lemma, but the first "op =" is expanded to "rel_option op =" *)
"(rel_option op = ===> B ===> rel_option (rel_prod op = B))
(λx y. Option.bind x (λx. Some (f x, y)))
(λx y. Option.bind x (λx. Some (f x, y)))"
by transfer_prover (* succeeds *)
datatype nonce = PNonce nat | ANonce "bool list"
datatype ('a, 'b, dead 'c) gpv = Done 'a
lemma case_nonce_transfer [transfer_rule]:
"((op = ===> A) ===> (op = ===> A) ===> op = ===> A) case_nonce case_nonce"
by(auto simp add: rel_fun_def split: nonce.split)
consts pnonce :: "nat ⇒ 's ⇒ nat ⇒ (bool list × 's, 'call, 'ret) gpv"
consts η :: nat
lemma pnonce_transfer [transfer_rule]: "(op = ===> S ===> op = ===> rel_gpv (rel_prod op =
S) C) pnonce pnonce" sorry
lemma "(op = ===> S ===> rel_gpv (rel_prod op = S) C)
(λnonce s. case nonce of PNonce x ⇒ pnonce η s x | ANonce bs ⇒ Done (bs, s))
(λnonce s. case nonce of PNonce x ⇒ pnonce η s x | ANonce bs ⇒ Done (bs, s))"
apply transfer_prover
apply(rule rel_funI)+
apply(rule case_nonce_transfer[THEN rel_funD, THEN rel_funD, THEN rel_funD])
apply(rule pnonce_transfer[THEN rel_funD, THEN rel_funD])
apply(rule refl)
apply assumption
apply(rule rel_funI)
apply(rule gpv.ctr_transfer[THEN rel_funD])
apply(erule (1) Pair_transfer[THEN rel_funD, THEN rel_funD])
apply assumption
done
Best,
Andreas
Transfer_Prover_Problem.thy
Email Gateway (Aug 22 2022 at 10:37):From: Peter Lammich <lammich@in.tum.de>
The first problem looks familiar to me.
The type of option.bind is
"'a option => ('a => 'b option) => 'b option"
and its transfer rule is accordingly.
However, in the first term, you specify just "op =" as relator, but bind
wants something of the form "rel_option A".
One workaround is to expand the "op =" - relators, based on their type,
as much as possible, e.g., by simplification rules.
Another workaround would be a custom "relator unification" procedure
built into transfer, which is able to handle those cases ... I tried
something similar for Autoref, but quickly gave up on it.
Email Gateway (Aug 22 2022 at 10:37):From: Ondřej Kunčar <kuncar@in.tum.de>
The problem2 is the same as the problem1.
If you write
"(op = ===> S ===> rel_gpv (rel_prod (list_all2 op=) S) C)
for the relation, transfer_prover works.
Funnily enough, Jasmin Blanchette sent me the same bug report two weeks ago.
The transfer_prover should work for your examples. You shouldn't be
forced to expand op= in the statements of your theorems. I put some code
in transfer_prover to support this some time ago. Apparently, I made it
wrong.
Since I'm at the (terminal) stage of writing my PhD thesis, it might
take some time before I get to fix this.
Ondrej
Email Gateway (Aug 22 2022 at 10:37):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Ondřej and Peter,
Thanks for your quick replies. For the time being, I will expand the relator-equality
theorems manually before I invoke transfer_prover. Given your replies I assume that this
is a safe operation.
Best,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC