Email Gateway (Aug 22 2022 at 13:28): Email Gateway (Aug 22 2022 at 13:28):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 13:28):From: Ondřej Kunčar <kuncar@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:28):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Ondrej,
Your understanding is right. So my idea will not work :-(.
Andreas
Email Gateway (Aug 22 2022 at 13:35):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 13:35):From: Ondřej Kunčar <kuncar@in.tum.de>
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
Email Gateway (Aug 22 2022 at 13:35):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 13:38):From: Ondřej Kunčar <kuncar@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC