*To*: OndÅej KunÄar <kuncar at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Parametrized transfer rules with lift_definition*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 24 Jun 2016 16:19:23 +0200*In-reply-to*: <3d182583-8a07-80e8-a7c1-21873b81be1c@in.tum.de>*References*: <575ADD90.5030305@inf.ethz.ch> <dfe427b1-3f6a-384f-5cc0-fdae36ef69e6@in.tum.de> <575FB4D3.60206@inf.ethz.ch> <0aa84570-8251-378d-78f5-a42638f900d9@in.tum.de> <576CF3E7.4050509@inf.ethz.ch> <3d182583-8a07-80e8-a7c1-21873b81be1c@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0

Hi Ondrej, Your understanding is right. So my idea will not work :-(. Andreas On 24/06/16 15:12, OndÅej KunÄar wrote:

I'm a little bit confused. Is my understanding right that you want to get some rules that allows you to infer the following? (fix x A ===> B) <= ((fix x op= ===> op=) OO (A ===> B)) That property doesn't hold :( Ondrej On 06/24/2016 10:48 AM, Andreas Lochbihler wrote:Dear Ondrej, Thanks for the explanations. I am still not sure whether this merging can be used for what I have in mind. Here is some background: For the translator from HOL4 to CakeML, Myreen and Owens came up with a small calculus to automatically prove transfer relations from well-founded function definitions. I would like to adapt their approach for deriving parametricity theorems for "function" definitions. In essence, rather than proving (rel_P A ===> rel_R A) f f for a function f :: 'a P => 'a R, they prove (fix x (rel_P A) ===> rel_R A) f f by induction on x using f.induct where fix x R = (%y z. x = y & R y z) The cases of the induction proofs then look very much like a transfer proof (more like Peter Lammich's transfer prover than your skeleton approach in transfer). However, for all the operators whose congruence rules were used in the function definition, the ordinary parametricity rules for those operators do not suffice. For example, for map, one needs list_all2 A xs ys ==> (!!x. x : set xs ==> (fix x A ===> B) f g) ==> list_all2 B (map f xs) (map g ys) My idea was now to see whether one can derive this rule automatically from the parametricity of map and its congruence rule, namely as the merge of list_all2 op = xs ys ==> (!!x. x : set xs ==> (fix x (op =) ===> op =) f g) ==> list_all2 op = (map f xs) (map g ys) and list_all2 A xs ys ==> (A ===> B) f g ==> list_all2 B (map f xs) (map g xs) because fix distributes nicely over OO: fix x (R OO S) = fix x R OO S Thinking backwards, I want to split the relation about f and g into two, namely fix x op = ===> op = A ===> B Thus, only one of them depends on the x (and this part then simplifies to the congruence rule) and the other corresponds to the transfer rule. As all this happens in a premise, ===> is in a negative position, so neg_fun_distr* come into play. And so far I was not able to find a set of side conditions such that the merging (or splitting) works with "fix x op = ===> op =" on the left-hand side. Can you see whether any of your additional rules for fun_distr would work here? Cheers, Andreas On 20/06/16 23:39, OndÅej KunÄar wrote:I looked at the procedure again and here is a more detailed description: Let say you have a transfer rule of the form "T t f" and a parametric transfer rule of the form "par_R t' t". From that you obtain "(par_R' OO T) t' f". (par_R' is an instance of par_R). Now you want to do some massaging on the relation "par_R' OO T". I call it merging and it is enough if you prove (par_R' OO T) <= desired_T, from which you obtain "desired_T t' f". How to prove "(par_R OO T) <= desired_T"? In principle, you use rules such as list_all R OO list_all S <= list_all (R OO S) (obtained from list_all R OO list_all S = list_all (R OO S)). But before applying that rule, we should not forget that we have to also do merging recursively on R and S by using this rule: R <= R' ==> list_all R <= list_all R' (monotonicity of list_all). As you know, some relators (yes it is ===>) have contra-variant positions and thus R >= R' ==> S <= S' ==> (R ===> S) <= (R' ===> S') Thus, we are suddenly proving the other direction R >= R'. This is how it happens that we need neg_fun_distr1 and and neg_fun_distr2. Yes, they are used for higher-order arguments, if you want. But only for negative positions. When you get to double-negative positions (i.e., positive again) pos_fun_distr is your friend again. Thus, switching the direction also requires rules such as list_all R OO list_all S >= list_all (R OO S). On the topic of side-conditions: in general there might be multiple rules for "distributivity" for one relator and they can have side conditions. The rules are ordered by the time when they were registered. The merging procedure searches for the first one for which it can discharge all the side conditions after the rule is applied. The side conditions are always of the form [right|left|bi][unique|total] and they are simply discharged by the Transfer tool. Overall: for a given relator RR, you obtain all the above-used rules automatically if (RR R1 ... Rn) OO (RR S1 ... Sn) = RR (R1 OO S1) ... (Rn OO Sn) and if you have the monotonicity rule (i.e., all BNFs fall in this category). If this is not the case, you have to do something manually as for the function type. You noticed that there are other variants of neg_fun_distr. Once I proved even more of them (6 or 8, I can't remember) and included only some of them. My quick inspection showed that at higher-order negative positions you are merging only equalities anyway. If you came across different examples, let me know. We can add the other rules as well. Ondrej On 06/14/2016 09:40 AM, Andreas Lochbihler wrote:Dear Ondrej, Thanks for the pointer. The last sentence of this section is what I am wondering about: I implemented a procedure that can do all of those steps automatically. The problem is that the function relator rel_fun does not distribute over relation composition op OO. The comment in Lifting.thy indicates that the theorems pos_fun_distr, neg_fun_distr1, and neg_fun_distr2 take the role of distributivity for functions. It seems as if the latter two are used only for higher-order arguments, but it is not yet clear to me which of the two covers which cases. They have preconditions on the relations like left_unique and right_total. How do you make sure that they can be used for the relations? neg_fun_distr2 only has assumptions about the relations on the right hand side of OO, so this will affect only the correspondence relation, so lift_definition has some control over this. But what about neg_fun_distr1 and its assumptions on relations on the left? Also, one could prove two more rules of the kind of neg_fun_distr1 and neg_fun_distr2. For example, lemma neg_fun_distr3: assumes 1: "left_unique R" "right_total R" and 2: "right_unique S" "left_total S" shows "R OO R' ===> S OO S' â (R ===> S) OO (R' ===> S')" using functional_converse_relation[OF 1] functional_relation[OF 2] unfolding rel_fun_def OO_def apply clarify apply (subst all_comm) apply (subst all_conj_distrib[symmetric]) apply (intro choice) by metis Why are these rules not needed? Best, Andreas On 13/06/16 20:08, OndÅej KunÄar wrote:Hi Andreas, there is a brief description of the algorithm in my thesis in Â4.3. That description should give you a good overview how the procedure works. I can answer additional questions if needed. Bests, Ondrej On 06/10/2016 05:32 PM, Andreas Lochbihler wrote:Dear Lifting experts, I am looking for some documentation on how the Lifting tool derives the parametrised transfer rules from the parametricity theorem. In some cases, lift_definition reports that it was not able to merge certain terms. I'd like to understand how this works and its limitations. I have a different application in mind (strengthening parametricity theorems with congruence rules) and would like to understand whether the same approach could work there. Best, Andreas

**References**:**[isabelle] Parametrized transfer rules with lift_definition***From:*Andreas Lochbihler

**Re: [isabelle] Parametrized transfer rules with lift_definition***From:*OndÅej KunÄar

**Re: [isabelle] Parametrized transfer rules with lift_definition***From:*Andreas Lochbihler

**Re: [isabelle] Parametrized transfer rules with lift_definition***From:*OndÅej KunÄar

**Re: [isabelle] Parametrized transfer rules with lift_definition***From:*Andreas Lochbihler

**Re: [isabelle] Parametrized transfer rules with lift_definition***From:*OndÅej KunÄar

- Previous by Date: Re: [isabelle] Parametrized transfer rules with lift_definition
- Next by Date: [isabelle] Last CfP: JSC Special Issue on Symbolic Computation in Software Science
- Previous by Thread: Re: [isabelle] Parametrized transfer rules with lift_definition
- Next by Thread: [isabelle] Opaque ascription for SML code generation
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list