Re: [isabelle] Parametrized transfer rules with lift_definition

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 :(


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)


  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,

  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?


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

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
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.


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

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?


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.


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
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
a different application in mind (strengthening parametricity theorems
with congruence rules) and would like to understand whether the same
approach could work there.


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