Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Query about the transfer method

view this post on Zulip Email Gateway (Aug 19 2022 at 15:50):

From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle experts,

I have defined a function to convert rational polynomials to real ones,
and want to prove this function respects some other operations on
polynomials.

theory Scratch1
imports Complex_Main "~~/src/HOL/Library/Polynomial"
begin

lift_definition real_poly:: "rat poly ⇒ real poly" is
"%p. real_of_rat o p " unfolding almost_everywhere_zero_def by auto

lemma real_poly_plus: "real_poly (p + q) = real_poly p + real_poly q"
(apply transfer)
using real_poly.rep_eq Rat.of_rat_add by (intro poly_eqI,auto)

end

Although the lemma real_poly_plus can be proved by "using
real_poly.rep_eq Rat.of_rat_add by (intro poly_eqI,auto)", I really want
to use the transfer method to convert goals from abstract types to
representation types as many lemmas related to "of_rat" do. However,
after "apply transfer" the lemma real_poly_plus becomes:

  1. !!p q. almost_everywhere_zero p ==>
    almost_everywhere_zero q ==> real_of_rat ∘ ?ad16 p q = ?ae16
    (real_of_rat ∘ p) (real_of_rat ∘ q)

    1. Transfer.Rel (rel_fun (pcr_poly op =) (rel_fun (pcr_poly op =)
      (pcr_poly op =))) ?ad16 op +

    2. Transfer.Rel (rel_fun (pcr_poly op =) (rel_fun (pcr_poly op =)
      (pcr_poly op =))) ?ae16 op +

which I don't know how to proceed. Is there anything I can do to use the
transfer method properly in my case?

Many thanks,
Wenda

view this post on Zulip Email Gateway (Aug 19 2022 at 15:52):

From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle experts,

I have investigated my previous problem. The problem can be solved by
providing an alternative plus operation for polynomials:

lift_definition plus_poly1 :: "'a::comm_monoid_add poly ⇒ 'a poly ⇒ 'a
poly"
is "%p q n. p n + q n" sorry

lemma real_poly_plus: "real_poly (plus_poly1 p q) = plus_poly1
(real_poly p) (real_poly q)"
apply transfer
(as desired)

Compared to the original plus operation for polynomials:

lift_definition plus_poly :: "'a poly ⇒ 'a poly ⇒ 'a poly"
is "%p q n. coeff p n + coeff q n"

then only difference between plus_poly1 and plus_poly is that plus_poly1
takes its arguments as
representation types for polynomials (i.e. "nat => 'a") while plus_poly
takes its arguments as abstract types (i.e. "'a poly"). In my case,
plus_poly1 works much better for the transfer method than plus_poly.

Therefore, it occurs to me when we are using lift_defition, shall we try
to use representation types and avoid abstract types? I have checked
Int.thy, Rat.thy and Real.thy, and they all fit my hypothesis, while
definitions in Polynomial.thy confuse me.

Many thanks for any help,
Wenda

view this post on Zulip Email Gateway (Aug 19 2022 at 15:52):

From: Brian Huffman <huffman.brian.c@gmail.com>
Hi Wenda,

You are completely right about the uses of lift_definition in the
Polynomial theory. The point of lift_definition is to avoid writing
definitions in terms of the Rep/Abs functions for types. Function
"coeff" is the Rep function for the polynomial type, and so it should
be avoided when using lift_definition.

Polynomial.thy was written before lift_definition/transfer existed, so
the original definitions all used "coeff" explicitly. When it was
ported over to use lift_definition (apparently by Florian Haftmann
some time last year), I guess some redundant uses of "coeff" were
overlooked.

If it makes the "transfer" method more useful, it would probably be a
good idea to change the definitions in Polynomial.thy to match the
style of your "plus_poly1". Perhaps Florian is willing to take this
on?

view this post on Zulip Email Gateway (Aug 19 2022 at 15:52):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Wenda & al.

You are completely right about the uses of lift_definition in the
Polynomial theory. The point of lift_definition is to avoid writing
definitions in terms of the Rep/Abs functions for types. Function
"coeff" is the Rep function for the polynomial type, and so it should
be avoided when using lift_definition.

the issue is related to the fact that lifting always operates on
expressions of a certain type, not on expressions consisting of certain
»transferable« operations. Hence, if an expression you want to lift
contains operations not defined using lift_definition, you get
unexpected (unusable) results from transfer.

There are a couple of subissues actually arising here, which should not
bother you at the moment and I will set them out in a separate thread.
For the moment just note that you can often help yourself using the
following pattern

lemma …
unfolding (*) proof transfer
…
qed

where in * you place equational theorems which unfold the
»untransferable« operations to »transferable« ones.

If it makes the "transfer" method more useful, it would probably be a
good idea to change the definitions in Polynomial.thy to match the
style of your "plus_poly1". Perhaps Florian is willing to take this
on?

I am currently absorbed in preparing a co-work for an AFP submission
concerning multivariate polynomials. After that the future of
Polynomial.thy can come on the agenda again.

Cheers,
Florian

On Thu, Sep 18, 2014 at 6:24 AM, Wenda Li <wl302@cam.ac.uk> wrote:

Dear Isabelle experts,

I have investigated my previous problem. The problem can be solved by
providing an alternative plus operation for polynomials:

lift_definition plus_poly1 :: "'a::comm_monoid_add poly ⇒ 'a poly ⇒ 'a poly"
is "%p q n. p n + q n" sorry

lemma real_poly_plus: "real_poly (plus_poly1 p q) = plus_poly1 (real_poly p)
(real_poly q)"
apply transfer
(as desired)

Compared to the original plus operation for polynomials:

lift_definition plus_poly :: "'a poly ⇒ 'a poly ⇒ 'a poly"
is "%p q n. coeff p n + coeff q n"

then only difference between plus_poly1 and plus_poly is that plus_poly1
takes its arguments as
representation types for polynomials (i.e. "nat => 'a") while plus_poly
takes its arguments as abstract types (i.e. "'a poly"). In my case,
plus_poly1 works much better for the transfer method than plus_poly.

Therefore, it occurs to me when we are using lift_defition, shall we try to
use representation types and avoid abstract types? I have checked Int.thy,
Rat.thy and Real.thy, and they all fit my hypothesis, while definitions in
Polynomial.thy confuse me.

Many thanks for any help,
Wenda

On 2014-09-16 13:14, Wenda Li wrote:

Dear Isabelle experts,

I have defined a function to convert rational polynomials to real
ones, and want to prove this function respects some other operations
on polynomials.

theory Scratch1
imports Complex_Main "~~/src/HOL/Library/Polynomial"
begin

lift_definition real_poly:: "rat poly ⇒ real poly" is
"%p. real_of_rat o p " unfolding almost_everywhere_zero_def by auto

lemma real_poly_plus: "real_poly (p + q) = real_poly p + real_poly q"
(apply transfer)
using real_poly.rep_eq Rat.of_rat_add by (intro poly_eqI,auto)

end

Although the lemma real_poly_plus can be proved by "using
real_poly.rep_eq Rat.of_rat_add by (intro poly_eqI,auto)", I really
want to use the transfer method to convert goals from abstract types
to representation types as many lemmas related to "of_rat" do.
However, after "apply transfer" the lemma real_poly_plus becomes:

  1. !!p q. almost_everywhere_zero p ==>
    almost_everywhere_zero q ==> real_of_rat ∘ ?ad16 p q =
    ?ae16 (real_of_rat ∘ p) (real_of_rat ∘ q)
  2. Transfer.Rel (rel_fun (pcr_poly op =) (rel_fun (pcr_poly op =)
    (pcr_poly op =))) ?ad16 op +
  3. Transfer.Rel (rel_fun (pcr_poly op =) (rel_fun (pcr_poly op =)
    (pcr_poly op =))) ?ae16 op +

which I don't know how to proceed. Is there anything I can do to use
the transfer method properly in my case?

Many thanks,
Wenda

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

signature.asc

Last updated: Apr 20 2024 at 01:05 UTC