Re: [isabelle] Parametrized transfer rules with lift_definition



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








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