Re: [isabelle] Problems with transfer_prover



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

On 18/07/15 14:31, OndÅej KunÄar wrote:
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

On 07/17/2015 04:48 PM, Andreas Lochbihler wrote:
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?

1. The problem seems to be related to how "op =" is treated as a relation.

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 *)



2. Transfer prover is not able to prove the parametricity rule at all,
even though all rules are available (as the manual proof shows).

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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.