Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Questions about "transfer"


view this post on Zulip Email Gateway (Jan 05 2021 at 12:41):

From: Manuel Eberl <eberlm@in.tum.de>
Hello,

I recently did some experiments with the "transfer" command, but there
are a few things that I don't quite understand, so here are a few questions:

  1. It seems to me that "transfer" always transfers theorems
    "left-to-right". For the "transferred" attribute, there is
    "untransferred" – is there a similar thing for "transfer" as well?

  2. Relatedly, is there an easy idiomatic way to use "flipped" relators?
    The following does not work:

lemma
assumes [transfer_rule]: "rel_set r X Y"
shows "rel_set (λy x. r x y) Y X"
by transfer_prover

  1. Sometimes, it is more convenient to prove transfer rules for
    functions following the pattern

lemma
assumes [transfer_rule]: "r1 a b" "r2 c d"
shows "r3 (f a c) (f' b d)"

but if I declare that lemmas as a transfer_rule, it is not used. I have
to explicitly prove "(r1 ===> r2 ===> r3) f f'" from this for it to be
used. Is there some way around this?

  1. There is currently no relator for measures. I came up with the
    following one, which works well for my purposes, but I think it is not a
    good relator because it only makes sense for bi-unique relators on the
    values.

definition rel_measure :: "('a ⇒ 'b ⇒ bool) ⇒ ('a measure ⇒ 'b measure ⇒
bool)" where
"rel_measure r M1 M2 ⟷
rel_set r (space M1) (space M2) ∧
rel_set (rel_set r) (sets M1) (sets M2) ∧
(rel_set r ===> (=)) (emeasure M1) (emeasure M2)"

The definition of rel_pmf suggests something involving product measures
would be the right way to go.

On a related note: suppose I defined my simple relator and then later on
someone else defines another relator for measures. Would the rules then
clash? Would one have to remove all the rules for my relator for things
to still work smoothly?

  1. Is there any trick for proving transfer rules for constants defined
    by "inductive" or "fun" that I am unaware of? Doing the induction proofs
    manually is very tedious.

  2. The constant "has_derivative" is not parametric (I think) because
    e.g. for "(f has_derivative D) at_top" you get "Lim (λx. x)", which
    equal to "THE x. False". However, in practice, F is always of the form
    "at x within A" and then has_derivative is parametric. But if I prove
    the transfer rule

    (r ===> r) ===> (r ===> r) ===> r ===> rel_set r ===> (=))
    (λf D x A. (f has_derivative D) (at x within A))
    (λf D x A. (f has_derivative D) (at x within A))

for some suitable relator r, it does not get used. The transfer package
insists on a relator for "has_derivative". Of course, if I do an
auxiliary definition for this and fold it before applying transfer, it
works, but then I have a useless auxiliary function cluttering the
namespace.

  1. In measure theory, there is the definition

    nn_integral :: 'a measure ⇒ ('a ⇒ ennreal) ⇒ ennreal
    nn_integral M f =
    Sup (simple_integral M `
    {g. simple_function M g ∧ g ≤ f})

I was able to prove

lemma transfer_nn_integral [transfer_rule]:
assumes [transfer_rule]: "bi_unique r"
shows "(rel_measure r ===> (r ===> (=)) ===> (=))
nn_integral nn_integral"

but I needed some trickery to avoid "bi_total r" due to the use of
"Collect". The reason why it works is that "simple_integral" only
evaluates the function on values from "space M", so we can replace the
set in question by

{g. simple_function M g ∧ (∀x. x ∉ space M ⟶ f x = 0) ∧
∀x∈space M. g x ≤ f x}

which can be shown (with quite a bit of pain!) to be parametric.

Is there some trick to make any of this easier?

  1. Is there any way of telling the transfer package that some rules have
    higher priority than others?

Cheers,

Manuel
smime.p7s

view this post on Zulip Email Gateway (Jan 05 2021 at 23:21):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Manuel Eberl/All,

I will allow myself to provide a few remarks as a regular user of the
transfer infrastructure. Certainly, my own understanding of the framework
is still somewhat limited. However, hopefully, my advice will help to get
rid of the questions that are less difficult.

  1. It seems to me that "transfer" always transfers theorems
    "left-to-right". For the "transferred" attribute, there is
    "untransferred" – is there a similar thing for "transfer" as well?

Similar questions have been asked before and the answer seems to be
negative (
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2019-July/msg00013.html
).

  1. Sometimes, it is more convenient to prove transfer rules for
    functions following the pattern
    lemma
    assumes [transfer_rule]: "r1 a b" "r2 c d"
    shows "r3 (f a c) (f' b d)"
    but if I declare that lemmas as a transfer_rule, it is not used. I have
    to explicitly prove "(r1 ===> r2 ===> r3) f f'" from this for it to be
    used. Is there some way around this?

In certain circumstances, the rules stated in a similar format can be used.
For example,

context
includes lifting_syntax
fixes r1 r2 r3 :: "'a ⇒ 'b ⇒ bool"
and f :: "'a ⇒ 'a ⇒ 'a" and f' :: "'b ⇒ 'b ⇒ 'b"
assumes [transfer_rule]: "bi_unique r3"
and [transfer_rule]: "r1 a b ⟹ r2 c d ⟹ r3 (f a c) (f' b d)"
begin

lemma
assumes [transfer_rule]: "r1 a b" "r2 c d"
shows "f' b d = f' b d"
by transfer (rule refl)

end

In this case, "r1 a b" and "r2 c d" are treated as side conditions, and the
transfer infrastructure has some limited support for such unconventional
side conditions (however, I am not certain as to what is the extent of such
support).

If it is more convenient to prove a transfer rule in the form that you have
stated, then you can always use (intro rel_funI) to perform the conversion,
e.g.

lemma
includes lifting_syntax
shows "(r1 ===> r2 ===> r3) f f'"
apply(intro rel_funI)
(⋀x y xa ya. r1 x y ⟹ r2 xa ya ⟹ r3 (f x xa) (f' y ya))

  1. Is there any trick for proving transfer rules for constants defined
    by "inductive" or "fun" that I am unaware of? Doing the induction proofs
    manually is very tedious.

Yes, there is: see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-January/msg00072.html.
I would like to add to the suggestion in the post that, technically, there
is little that is stopping one from recovering the original definitional
axiom in Isabelle/ML using Thm.axiom (e.g. see the implementation of UD in
https://gitlab.com/user9716869/Isabelle-Complement-Library, but keep in
mind that it is still in a reasonably rough experimental state) instead of
using the collection of theorems associated with nitpick. Providing further
automation for this is on my own "to do" list, but it has a very low
priority. If you decide to make an attempt to generalize/automate this
idea, I would highly appreciate it if you could let me know about this to
avoid possible duplication of efforts.

  1. In measure theory, there is the definition
    nn_integral :: 'a measure ⇒ ('a ⇒ ennreal) ⇒ ennreal
    nn_integral M f =
    Sup (simple_integral M `
    {g. simple_function M g ∧ g ≤ f})
    I was able to prove
    lemma transfer_nn_integral [transfer_rule]:
    assumes [transfer_rule]: "bi_unique r"
    shows "(rel_measure r ===> (r ===> (=)) ===> (=))
    nn_integral nn_integral"
    but I needed some trickery to avoid "bi_total r" due to the use of
    "Collect". The reason why it works is that "simple_integral" only
    evaluates the function on values from "space M", so we can replace the
    set in question by
    {g. simple_function M g ∧ (∀x. x ∉ space M ⟶ f x = 0) ∧
    ∀x∈space M. g x ≤ f x}
    which can be shown (with quite a bit of pain!) to be parametric.
    Is there some trick to make any of this easier?

I cannot be certain, but it appears that a pattern similar to the one that
you suggest was used in published work by those whom I would consider to be
well-versed in the functionality of transfer (e.g. see the code associated
with [1]). Thus, it is likely that the problem does not have a generic
solution. However, I would be happy to be wrong about this, as my own work
would benefit from having such a solution.

In this context, I wonder if the types of algorithms used in the work of
Peter Lammich (e.g. [2] and other related articles) would handle this
scenario. I would certainly appreciate any comments from him.

  1. Is there any way of telling the transfer package that some rules have
    higher priority than others?

A slightly hacky way would be to simply rearrange the transfer_raw
programmatically, as you need. Practically, in most circumstances, this
should not be needed. One can always write lemmas [transfer_rule] =
(relevant rules that need to have a higher priority). The duplicates will
not be produced: the theorems in transfer_raw will simply be rearranged
with the restated rules at the top of the list.

Kind Regards,
Mikhail Chekhov

[1]. Immler F, Zhan B. Smooth Manifolds and Types to Sets for Linear
Algebra in Isabelle/HOL. In: 8th ACM SIGPLAN International Conference on
Certified Programs and Proofs. New York: ACM; 2019. p. 65–77. (CPP 2019).
[2]. Lammich P. Automatic Data Refinement. In: Blazy S, Paulin-Mohring C,
Pichardie D, editors. Interactive Theorem Proving. Heidelberg: Springer;
2013. p. 84–99.

view this post on Zulip Email Gateway (Jan 06 2021 at 20:46):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Hi Manuel,

  1. It seems to me that "transfer" always transfers theorems
    "left-to-right". For the "transferred" attribute, there is
    "untransferred" – is there a similar thing for "transfer" as well?

Not that I know of. Going from right to left is problematic with rules that have compound
terms on the right-hand side (see below).

  1. Relatedly, is there an easy idiomatic way to use "flipped" relators?
    No. The capabilities of "transfer" are very much tailored to the needs of the lifting
    package. And there, you normally just go one way.
  1. Sometimes, it is more convenient to prove transfer rules for
    functions following the pattern

lemma
assumes [transfer_rule]: "r1 a b" "r2 c d"
shows "r3 (f a c) (f' b d)"

but if I declare that lemmas as a transfer_rule, it is not used. I have
to explicitly prove "(r1 ===> r2 ===> r3) f f'" from this for it to be
used. Is there some way around this?

Again, nothing that I'm aware of. But it shouldn't be too hard to write an attribute that
does the preprocessing.

  1. There is currently no relator for measures. I came up with the
    following one, which works well for my purposes, but I think it is not a
    good relator because it only makes sense for bi-unique relators on the
    values.

definition rel_measure :: "('a ⇒ 'b ⇒ bool) ⇒ ('a measure ⇒ 'b measure ⇒
bool)" where
"rel_measure r M1 M2 ⟷
rel_set r (space M1) (space M2) ∧
rel_set (rel_set r) (sets M1) (sets M2) ∧
(rel_set r ===> (=)) (emeasure M1) (emeasure M2)"

The definition of rel_pmf suggests something involving product measures
would be the right way to go.

Yours doesn't look right. The relators coming out of the BNF package are all defined via
the product, namely find a value z over pairs whose projections are the original two
values x and y to be related such that the elements in z are contained in the relation r.
While these definitions are canonical, they are hardly intuitive for custom type
constructors and usually unwieldy to work with. For probability spaces, this product is
commonly called a probabilistic coupling and I believe this would also be the right
relator definition for general measures.

For rel_pmf, you find the characterization theorem in the AFP in
MFMC_Countable.Rel_PMF_Characterization. Essentially, it says that rel_pmf R p q iff
measure p A <= measure q (R `` A) for all A. I'm pretty sure that such a characterization
can be generalized to arbitrary measures. Strassen has proven a number of theorems in that
direction (https://www.jstor.org/stable/2238148).

On a related note: suppose I defined my simple relator and then later on
someone else defines another relator for measures. Would the rules then
clash? Would one have to remove all the rules for my relator for things
to still work smoothly?

You'd get a clash for some things. In general, you want to register a few theorems for a
relator (e.g., [relator_eq], [relator_mono], [quot_map]) and some of these attributes
allow only one theorem per type constructor. So you can't register theorems for both
relators. The plain transfer machinery can cope with several relators for the same type
constructor (except for the function type) and I've used that occasionally. However, you
have to be very careful to not end up with an exponentially large search space for transfer.

  1. Is there any trick for proving transfer rules for constants defined
    by "inductive" or "fun" that I am unaware of? Doing the induction proofs
    manually is very tedious.

I have looked into this previously. For inductive, I had a few ideas but eventually
realized that it doesn't play well together with the current architecture of transfer. The
problem is that like for the predicate compiler, an inductive definition may have
different computational interpretations (modes in logic programming speak) and those
interpretations lead to different relators in the resulting transfer rule (predicates vs.
sets). While it's possible to convert between predicates and sets, this requires
additional assumptions about the relations (typically bi_totality). However, as transfer
does not really support multiple relators for the same type constructor, such a solution
would be problematic. Moreover, there may be exponentially many transfer rules for an
inductive predicate, in particular if you do a higher-order mode analysis similar to
Lukas' work for the predicate compiler, so we'd end up creating an exponential number of
transfer rules.

  1. The constant "has_derivative" is not parametric (I think) because
    e.g. for "(f has_derivative D) at_top" you get "Lim (λx. x)", which
    equal to "THE x. False". However, in practice, F is always of the form
    "at x within A" and then has_derivative is parametric. But if I prove
    the transfer rule

    (r ===> r) ===> (r ===> r) ===> r ===> rel_set r ===> (=))
    (λf D x A. (f has_derivative D) (at x within A))
    (λf D x A. (f has_derivative D) (at x within A))

for some suitable relator r, it does not get used. The transfer package
insists on a relator for "has_derivative". Of course, if I do an
auxiliary definition for this and fold it before applying transfer, it
works, but then I have a useless auxiliary function cluttering the
namespace.

The transfer package's algorithm assumes that the transferred term preserves function
applications and abstractions, i.e., those are always transferred with rel_funI and
rel_funD. Therefore, you cannot have a compound term on the left-hand side of a transfer
rule; it will virtually never trigger. (The exception is if you have a constant on the
right-hand side and use the untransferred attribute.) So your only chance here is to
introduce an auxiliary constant and fold the definition before applying transfer.

There are other algorithms that one could use to support such compound terms. For example,
Peter Lammich's Autoref tool supports compound terms in transfer rules, but that's not
integrated with transfer.

  1. In measure theory, there is the definition

    nn_integral :: 'a measure ⇒ ('a ⇒ ennreal) ⇒ ennreal
    nn_integral M f =
    Sup (simple_integral M `
    {g. simple_function M g ∧ g ≤ f})

I was able to prove

lemma transfer_nn_integral [transfer_rule]:
assumes [transfer_rule]: "bi_unique r"
shows "(rel_measure r ===> (r ===> (=)) ===> (=))
nn_integral nn_integral"

but I needed some trickery to avoid "bi_total r" due to the use of
"Collect". The reason why it works is that "simple_integral" only
evaluates the function on values from "space M", so we can replace the
set in question by

{g. simple_function M g ∧ (∀x. x ∉ space M ⟶ f x = 0) ∧
∀x∈space M. g x ≤ f x}

which can be shown (with quite a bit of pain!) to be parametric.

Is there some trick to make any of this easier?

I don't think so. These complications are very typical of proving transfer rules. More
precisely, they just show how many shortcuts we're taking in our definitions in HOL
because HOL is a logic of total functions. In ordinary mathematics, we'd say that f and
g are only defined on space M. So the universal quantifier that's implicit in the
original definition's g <= f would range only over space M anyway.

  1. Is there any way of telling the transfer package that some rules have
    higher priority than others?

Finally something that I can answer positively. "transfer" uses the [transfer_rule]s in
inverse order, i.e., theorems that are declared as [transfer_rule] later have higher priority.

Hope this helps,
Andreas

view this post on Zulip Email Gateway (Jan 06 2021 at 23:31):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

I would like to thank Andreas Lochbihler for providing a more elaborate
answer in the following post:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-January/msg00038.html.
I believe that there is one notable difference in our answers. More
specifically, the answer that was given by Andreas Lochbihler to question 5

Is there any trick for proving transfer rules for constants defined
by "inductive" or "fun" that I am unaware of? Doing the induction proofs
manually is very tedious.

is as follows:

I have looked into this previously. For inductive, I had a few ideas but
eventually
realized that it doesn't play well together with the current architecture
of transfer. The
problem is that like for the predicate compiler, an inductive definition
may have
different computational interpretations (modes in logic programming speak)
and those
interpretations lead to different relators in the resulting transfer rule
(predicates vs.
sets). While it's possible to convert between predicates and sets, this
requires
additional assumptions about the relations (typically bi_totality).
However, as transfer
does not really support multiple relators for the same type constructor,
such a solution
would be problematic. Moreover, there may be exponentially many transfer
rules for an
inductive predicate, in particular if you do a higher-order mode analysis
similar to
Lukas' work for the predicate compiler, so we'd end up creating an
exponential number of
transfer rules.

My own answer is also provided for reference:

Yes, there is: see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-January/msg00072.html.
I would like to add to the suggestion in the post that, technically, there
is little that is stopping one from recovering the original definitional
axiom in Isabelle/ML using Thm.axiom (e.g. see the implementation of UD in
https://gitlab.com/user9716869/Isabelle-Complement-Library, but keep in
mind that it is still in a reasonably rough experimental state) instead of
using the collection of theorems associated with nitpick. Providing further
automation for this is on my own "to do" list, but it has a very low
priority. If you decide to make an attempt to generalize/automate this
idea, I would highly appreciate it if you could let me know about this to
avoid possible duplication of efforts.

I would like to make an attempt to resolve any confusion that this
discrepancy may have caused. The scope of my answer was significantly more
narrow. More specifically, my answer assumes that, given a constant c
(defined as an inductive predicate), there is a term t (normally, also
defined with the help of an inductive predicate), a parametricity relation
R for the type of c, constructed under the assumption that the relators for
every non-nullary type constructor are known in advance and some side
conditions on the involved relations, also known in advance. Then, if the
transfer rule R t c exists under the aforementioned side conditions, then
its proof can often be automated using the transfer prover, assuming the
existence of the transfer rules for the constant lfp under compatible side
conditions, as showcased in
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-January/msg00072.html.
The transfer rules for the lfp can often cover a significant number of
similar applications, possibly allowing for some degree of proof
automation. However, of course, as can be inferred from the answer given by
Andreas Lochbihler, it is hardly a fundamental solution. After all, the OP
asked for a 'trick' that could help to reduce the size of the proof, and I
tried to oblige by providing a trick :-).

Kind Regards,
Mikhail Chekhov

On Wed, Jan 6, 2021 at 1:20 AM Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
wrote:

Dear Manuel Eberl/All,

I will allow myself to provide a few remarks as a regular user of the
transfer infrastructure. Certainly, my own understanding of the framework
is still somewhat limited. However, hopefully, my advice will help to get
rid of the questions that are less difficult.

  1. It seems to me that "transfer" always transfers theorems
    "left-to-right". For the "transferred" attribute, there is
    "untransferred" – is there a similar thing for "transfer" as well?

Similar questions have been asked before and the answer seems to be
negative (
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2019-July/msg00013.html
).

  1. Sometimes, it is more convenient to prove transfer rules for
    functions following the pattern
    lemma
    assumes [transfer_rule]: "r1 a b" "r2 c d"
    shows "r3 (f a c) (f' b d)"
    but if I declare that lemmas as a transfer_rule, it is not used. I have
    to explicitly prove "(r1 ===> r2 ===> r3) f f'" from this for it to be
    used. Is there some way around this?

In certain circumstances, the rules stated in a similar format can be
used. For example,

context
includes lifting_syntax
fixes r1 r2 r3 :: "'a ⇒ 'b ⇒ bool"
and f :: "'a ⇒ 'a ⇒ 'a" and f' :: "'b ⇒ 'b ⇒ 'b"
assumes [transfer_rule]: "bi_unique r3"
and [transfer_rule]: "r1 a b ⟹ r2 c d ⟹ r3 (f a c) (f' b d)"
begin

lemma
assumes [transfer_rule]: "r1 a b" "r2 c d"
shows "f' b d = f' b d"
by transfer (rule refl)

end

In this case, "r1 a b" and "r2 c d" are treated as side conditions, and
the transfer infrastructure has some limited support for such
unconventional side conditions (however, I am not certain as to what is the
extent of such support).

If it is more convenient to prove a transfer rule in the form that you
have stated, then you can always use (intro rel_funI) to perform the
conversion, e.g.

lemma
includes lifting_syntax
shows "(r1 ===> r2 ===> r3) f f'"
apply(intro rel_funI)
(⋀x y xa ya. r1 x y ⟹ r2 xa ya ⟹ r3 (f x xa) (f' y ya))

  1. Is there any trick for proving transfer rules for constants defined
    by "inductive" or "fun" that I am unaware of? Doing the induction proofs
    manually is very tedious.

Yes, there is: see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-January/msg00072.html.
I would like to add to the suggestion in the post that, technically, there
is little that is stopping one from recovering the original definitional
axiom in Isabelle/ML using Thm.axiom (e.g. see the implementation of UD in
https://gitlab.com/user9716869/Isabelle-Complement-Library, but keep in
mind that it is still in a reasonably rough experimental state) instead of
using the collection of theorems associated with nitpick. Providing further
automation for this is on my own "to do" list, but it has a very low
priority. If you decide to make an attempt to generalize/automate this
idea, I would highly appreciate it if you could let me know about this to
avoid possible duplication of efforts.

  1. In measure theory, there is the definition
    nn_integral :: 'a measure ⇒ ('a ⇒ ennreal) ⇒ ennreal
    nn_integral M f =
    Sup (simple_integral M `
    {g. simple_function M g ∧ g ≤ f})
    I was able to prove
    lemma transfer_nn_integral [transfer_rule]:
    assumes [transfer_rule]: "bi_unique r"
    shows "(rel_measure r ===> (r ===> (=)) ===> (=))
    nn_integral nn_integral"
    but I needed some trickery to avoid "bi_total r" due to the use of
    "Collect". The reason why it works is that "simple_integral" only
    evaluates the function on values from "space M", so we can replace the
    set in question by
    {g. simple_function M g ∧ (∀x. x ∉ space M ⟶ f x = 0) ∧
    ∀x∈space M. g x ≤ f x}
    which can be shown (with quite a bit of pain!) to be parametric.
    Is there some trick to make any of this easier?

I cannot be certain, but it appears that a pattern similar to the one that
you suggest was used in published work by those whom I would consider to be
well-versed in the functionality of transfer (e.g. see the code associated
with [1]). Thus, it is likely that the problem does not have a generic
solution. However, I would be happy to be wrong about this, as my own work
would benefit from having such a solution.

In this context, I wonder if the types of algorithms used in the work of
Peter Lammich (e.g. [2] and other related articles) would handle this
scenario. I would certainly appreciate any comments from him.

  1. Is there any way of telling the transfer package that some rules have
    higher priority than others?

A slightly hacky way would be to simply rearrange the transfer_raw
programmatically, as you need. Practically, in most circumstances, this
should not be needed. One can always write lemmas [transfer_rule] =
(relevant rules that need to have a higher priority). The duplicates will
not be produced: the theorems in transfer_raw will simply be rearranged
with the restated rules at the top of the list.

Kind Regards,
Mikhail Chekhov

[1]. Immler F, Zhan B. Smooth Manifolds and Types to Sets for Linear
Algebra in Isabelle/HOL. In: 8th ACM SIGPLAN International Conference on
Certified Programs and Proofs. New York: ACM; 2019. p. 65–77. (CPP 2019).
[2]. Lammich P. Automatic Data Refinement. In: Blazy S, Paulin-Mohring C,
Pichardie D, editors. Interactive Theorem Proving. Heidelberg: Springer;
2013. p. 84–99.


Last updated: Jul 15 2022 at 23:21 UTC