[isabelle] lift_definition + constructor · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] lift_definition + constructor

Email Gateway (Aug 19 2022 at 12:34):

From: Walther Neuper <wneuper@ist.tugraz.at>
In Isabelle2013-1 in HOL/Library/Polynomial there is

lift_definition pCons :: "'a::zero => 'a poly => 'a poly"
is "λa p. nat_case a (coeff p)"
using coeff_almost_everywhere_zero by (rule
almost_everywhere_zero_nat_case)

Is there a way to have a constructor "pCons" instead of function
"pCons"? I.e. a constructor like

datatype 'a pcons = Zero | pCons 'a "'a pcons"

could be somehow associated with lift_definition ? Or is this possible
with datatype_new ?

Walther

PS: For those who find the question strange: If there is a "yes" then we
could have a mCons for distributive representation of polynomials.

Email Gateway (Aug 19 2022 at 12:35):

From: Brian Huffman <huffman.brian.c@gmail.com>
On Tue, Nov 19, 2013 at 9:57 AM, Walther Neuper <wneuper@ist.tugraz.at> wrote:

In Isabelle2013-1 in HOL/Library/Polynomial there is

lift_definition pCons :: "'a::zero => 'a poly => 'a poly"
is "λa p. nat_case a (coeff p)"
...
Is there a way to have a constructor "pCons" instead of function "pCons"?
I.e. a constructor like

datatype 'a pcons = Zero | pCons 'a "'a pcons"

could be somehow associated with lift_definition ? Or is this possible with
datatype_new ?

What exactly do you mean by "constructor"? HOL doesn't have any
built-in logical distinction between constructors and other functions.

The datatype package maintains its own internal database of
"constructor" functions, which is used for various kinds of proof
automation. Independently defined constructors can be registered after
the fact with "rep_datatype". However, Zero and pCons do not meet the
datatype package's requirement for distinctness, as pCons 0 Zero =
Zero.

Perhaps you hope to gain access to some form of automation for pCons
that would normally be provided by the datatype package? (E.g.
cases/induct proofs, case expressions, code generation, function
definitions by pattern matching, etc.) If so, then it is likely that
there is another way to get what you want with a little more work.

Brian

Email Gateway (Aug 19 2022 at 12:59):

From: Walther Neuper <wneuper@ist.tugraz.at>
Brian,

thanks for your hints !
In the course of general considerations [1] we come back to this
specific question:

On 11/19/2013 08:24 PM, Brian Huffman wrote:

On Tue, Nov 19, 2013 at 9:57 AM, Walther Neuper <wneuper@ist.tugraz.at> wrote:

In Isabelle2013-1 in HOL/Library/Polynomial there is

lift_definition pCons :: "'a::zero => 'a poly => 'a poly"
is "λa p. nat_case a (coeff p)"

Other kinds of representations, for instance sparse distributive
polynomial representation like [2], could be lifted as well
(establishing respective morphisms) by something like

lift_definition dCons :: "..."
is "..."

and then there is the question, how to distinguish between "pCons" and
"dCons": pattern matching, for instance by ...

case p of
pCons _ => ...
| dCons _ => ...

... on constructors "pCons" and "dCons" was an idea ...

Is there a way to have a constructor "pCons" instead of function "pCons"?
I.e. a constructor like

datatype 'a pcons = Zero | pCons 'a "'a pcons"

could be somehow associated with lift_definition ? Or is this possible with
datatype_new ?
What exactly do you mean by "constructor"? HOL doesn't have any
built-in logical distinction between constructors and other functions.

The signatures of pCons, dCons, etc are under question, also the
location with respect to the lift_definition --- do you find anything
realisable about this idea ?

Walther

[1]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00262.html
[2] http://afp.sourceforge.net/entries/Polynomials.shtml

Email Gateway (Aug 19 2022 at 13:02):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Walther,

Let me comment a bit, even though I am not an expert on polynomials in Isabelle. The
definition in HOL/Library/Polynomials gives you a logically unique representation for
polynomials, i.e., if two polynomials evaluate to the same at all points, then they are
equal (in the sense of op =). Your construction with the datatype does not give you this
identity, i.e., you get a different type with different properties. Of course, you can do
so on your own, but in my experience redundancy in a type usually makes proving harder.
Although you can interpret a polynomial in one representation or in the other, the logic
does not distinguish them and neither can you in your proofs.

However, if you need pattern-matching only for code generation (e.g., to pick an efficient
implementation), then that's still possible (to some extent) even if polynomials are not
defined as a datatype. You haven't mentioned code generation, but if you are interested,
I'd be happy to explain the details.

Andreas

Email Gateway (Aug 19 2022 at 13:03):

From: Walther Neuper <wneuper@ist.tugraz.at>
Andreas,

thanks for your kind offer ...

[...] You haven't mentioned code generation, but if you are
interested, I'd be happy to explain the details.

... because code generation is in our focus: we want to generate
algorithms from theories in algebraic geometry, while different
algorithms require different representations of polynomials for
efficiency reasons. So we are happy to hear ...

if you need pattern-matching only for code generation (e.g., to pick
an efficient implementation), then that's still possible (to some
extent) even if polynomials are not defined as a datatype.

... and in your paper [1] to find a quick guide to the following code
snippets derived from [3]:

datatype ('a, 'b) phantom = phantom 'b

datatype poly_impl = Poly_IMPL
definition poly_Recursive :: poly_impl where "poly_Recursive = Poly_IMPL"
definition poly_Distrib_Sparse :: poly_impl where
"poly_Distrib_Sparse = Poly_IMPL"
definition poly_Distrib_Sense :: poly_impl where "poly_Distrib_Sense
= Poly_IMPL"

class poly_impl =
fixes poly_impl :: "('a, poly_impl) phantom"

code_datatype poly_Recursive poly_Distrib_Sparse poly_Distrib_Sense

From now on we probably have to go another way: we need to choose
different representations not specific with respect to types, but
specific with respect to algorithms.

We are looking forward with great interest, how we can ...

flexibly switch between representations of polynomials (probably even
within one single, but complex algorithm)
derive properties for algorithms uniformly from a "logically unique
representation for polynomials" like [2]

... and are going to study your approach in detail. Any hints are
appreciated.

Walther

[1]
http://www.infsec.ethz.ch/research/publications/pub2013/lochbihler13itp.pdf
[2] http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Polynomial.html
[3] http://afp.sourceforge.net/entries/Collections.shtml

On 12/16/2013 08:46 AM, Andreas Lochbihler wrote:

Walther,

Let me comment a bit, even though I am not an expert on polynomials in
Isabelle. The definition in HOL/Library/Polynomials gives you a
logically unique representation for polynomials, i.e., if two
polynomials evaluate to the same at all points, then they are equal
(in the sense of op =). Your construction with the datatype does not
give you this identity, i.e., you get a different type with different
properties. Of course, you can do so on your own, but in my experience
redundancy in a type usually makes proving harder. Although you can
interpret a polynomial in one representation or in the other, the
logic does not distinguish them and neither can you in your proofs.

However, if you need pattern-matching only for code generation (e.g.,
to pick an efficient implementation), then that's still possible (to
some extent) even if polynomials are not defined as a datatype.
Andreas
On 13/12/13 15:17, Walther Neuper wrote:

Brian,

thanks for your hints !
In the course of general considerations [1] we come back to this
specific question:

On 11/19/2013 08:24 PM, Brian Huffman wrote:

On Tue, Nov 19, 2013 at 9:57 AM, Walther Neuper
<wneuper@ist.tugraz.at> wrote:

In Isabelle2013-1 in HOL/Library/Polynomial there is

lift_definition pCons :: "'a::zero => 'a poly => 'a poly"
is "λa p. nat_case a (coeff p)"

Other kinds of representations, for instance sparse distributive
polynomial representation
like [2], could be lifted as well (establishing respective morphisms)
by something like

lift_definition dCons :: "..."
is "..."

and then there is the question, how to distinguish between "pCons"
and "dCons": pattern
matching, for instance by ...

case p of
pCons _ => ...
| dCons _ => ...

... on constructors "pCons" and "dCons" was an idea ...

Is there a way to have a constructor "pCons" instead of function
"pCons"?
I.e. a constructor like

datatype 'a pcons = Zero | pCons 'a "'a pcons"

could be somehow associated with lift_definition ? Or is this
possible with
datatype_new ?
What exactly do you mean by "constructor"? HOL doesn't have any
built-in logical distinction between constructors and other functions.

The signatures of pCons, dCons, etc are under question, also the
location with respect to
the lift_definition --- do you find anything realisable about this
idea ?

Walther

[1]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00262.html
[2] http://afp.sourceforge.net/entries/Polynomials.shtml

Last updated: May 06 2024 at 12:29 UTC