Re: [isabelle] Code setup for Fraction_Field



> In fact, from what I can see, the equivalences are not provable at all
> in Isabelle2015, because euclidean_ring_gcd also talks about the set
> versions Gcd and Lcm. And in Euclidean_Algorithm, Lcm_eucl and
> Gcd_eucl are defined such that they also work for infinite sets
> whereas in GCD, Lcm for nat is defined to be 0 for infinite sets. So
> what is the plan here? 

The Lcm of an infinite number of nats /is/ 0. Think about it: We are
looking for a natural number that has infinitely many divisors. The only
such number is 0. You can think of 1 as the "biggest" element w.r.t.
divisibility and 0 as the "smallest" â 1 divides anything and is divided
by nothing (except itself); 0 is divided by everything and divides
nothing but itself.

So I don't really see any reason why this should not work. I'll have a
look at it and see what I can do.


Cheers,

Manuel


On 04/09/15 12:01, Andreas Lochbihler wrote:
> Hi Manuel,
>
> On 04/09/15 11:44, Manuel Eberl wrote:
>>> 1. I noticed that there are the type classes euclidean_ring and
>>> euclidean_ring_gcd. Most of the theorems about gcd which I need are in
>>> euclidean_ring_gcd, but not in euclidean_ring itself. Unfortunately,
>>> the instantiations for nat, int, etc. are only done for
>>> euclidean_ring, not for euclidean_ring_gcd. What are the plans for
>>> these type classes? Should I spend any effort on adding instances for
>>> euclidean_ring_gcd? Or will this become obsolete with the polishing
>>> that is still due?
>>
>> euclidean_ring_gcd is nothing but euclidean_ring with the additional
>> assumption that gcd and Gcd (which are introduced in a syntactical
>> typeclass and therefore have no a priori properties associated with
>> them) are the same as the euclidean GCD (and the same for LCM).
>>
>> So, in a sense, there is usually no proof work to be done to make
>> anything an instance of euclidean_ring_gcd if you already have
>> euclidean_ring; you can just define "gcd = gcd_eucl", "Gcd = Gcd_eucl"
>> and so on and you get the instance for free.
> That's clear. However, nat and int already have their own
> implementation of the GCD...
>
>> If there is already an existing definition of gcd, you have to prove its
>> equivalence to the Euclidean GCD etc., which you can do by showing that
>> it fulfils the defining properties of the GCD and that it returns a
>> normalised GCD, i.e. "1" and not "-1" for integers.
> Well, it is exactly this equivalence proof of which I am uncertain. If
> Florian restructures the whole hierarchy such that gcd/lcm definitions
> for int and nat are done in terms of gcd_eucl, then the equivalence
> proof becomes irrelevant.
>
> In fact, from what I can see, the equivalences are not provable at all
> in Isabelle2015, because euclidean_ring_gcd also talks about the set
> versions Gcd and Lcm. And in Euclidean_Algorithm, Lcm_eucl and
> Gcd_eucl are defined such that they also work for infinite sets
> whereas in GCD, Lcm for nat is defined to be 0 for infinite sets. So
> what is the plan here?
>
> Best,
> Andreas
>
>> On 04/09/15 11:32, Andreas Lochbihler wrote:
>>> Hi Florian and Manuel,
>>>
>>> I have experimented a bit with a normalisation function to be used in
>>> the operations over fraction fields and had a look at
>>> Euclidean_Algorithm in Number_Theory.
>>>
>>>
>>>
>>> 2. I am no longer sure that an invariant-based approach is the optimal
>>> thing for fraction field. In the code equation for the arithmetic
>>> operation, I don't see any big opportunities to exploit the invariant
>>> that nominator and denominator are normalised in some unspecified
>>> form. Only the equality tests become simpler (as normal forms are
>>> unique and we thus save two multiplications). Instead, it seems much
>>> simpler to treat cancellation of common factors as an optimisation
>>> without logical significance. For example, we could just add a call to
>>> a simplification function before calls to the Fract constructor. The
>>> simplification function only has to return an element of the same
>>> equivalence class, so for nat and int, we could use a normalisation
>>> function based on Euclid's algorithm. For other types, the
>>> simplification function could also just be the identity. What do you
>>> think?
>>>
>>> Best,
>>> Andreas
>>>
>>>
>>> On 27/08/15 12:02, Florian Haftmann wrote:
>>>> Hi Andreas and Prathamesh,
>>>>
>>>>> We noticed that the code setup for the theory Fraction_Field in
>>>>> HOL/Library is broken, at least since Isabelle2013. We would like to
>>>>> use
>>>>> code generation in his formalisation of knot theory where the
>>>>> elements
>>>>> of the fraction fields are polynomials over integers. I had a brief
>>>>> look
>>>>> at the theory Fraction_Field and noticed that there is a smart
>>>>> pseudo-constructor Fract, which is declared as code_datatype. So this
>>>>> feels as if the code generation was working at some time in the
>>>>> distant
>>>>> past and got broken somewhen.
>>>>>
>>>>> Does anyone know about the status of Fraction_Field?
>>>>
>>>> I dimly remember that initially Fraction_Field just took over the
>>>> then-used code setup from the rationals, and maybe it never worked as
>>>> intended (would need a closer investigation to find out actually).
>>>>
>>>> When code generation had been equipped with invariants, I revisited
>>>> Fraction_Field to make a code setup close to the rationals but soon
>>>> realized thatâ
>>>>
>>>>> I believe that it would be fairly easy to "fix" the problem of code
>>>>> generator setup by deriving a few code equation from the lemmas, but
>>>>> this will clearly result in suboptimal code for two reasons.
>>>>> First, we
>>>>> need tests whether the denominator is 0 all over the place.
>>>>> Second, the
>>>>> elements of the fraction fields will not be normalised automatically.
>>>>
>>>> âI need a generalized gcd for that, and so I let everything stand as
>>>> it is.
>>>>
>>>>> For the application on polynomials, this means that we would need
>>>>> some
>>>>> Euclidean algorithm for cancelling common factors of polynomials. I
>>>>> dimly remember that there is some support for the Euclidean
>>>>> algorithm in
>>>>> the pipeline. What is the status there?
>>>>
>>>> I think you can build on the corresponding theory in Number_Theory,
>>>> but
>>>> that needs some further rounds of polishing before I would
>>>> recommend to
>>>> turn it into a Âhard dependency.  Instead I suggest to put the code
>>>> setup into a separate theory ÂExecutable_Fraction_FieldÂ.  This is
>>>> what
>>>> we did 8 years ago when code generation was still highly experimentalâ
>>>>
>>>> Hope this helps,
>>>>      Florian
>>>>
>>>>>
>>>>> Best,
>>>>> Andreas and Prathamesh
>>>>>
>>>>>
>>>>
>>
>>






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