Re: [isabelle] Problems with transfer_prover



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.

--
  Peter


On Fr, 2015-07-17 at 16:48 +0200, 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.