[isabelle-dev] Problem with factorial-ring in combination with containers

[Manuel Eberl]

Hm, that sounds reasonable.

However, I am not sure whether using "finite" is really such a good
idea; it will lead to people having to instantiate "finite_UNIV" for all
kinds of things all the time.

I think I once considered a similar solution using a copy of "finite"
that does Code.abort in cases where finiteness wasn't obvious (e.g.
complement), but I abandoned that idea for some reason. Still, at the
moment, I think that might be the best solution.

Any thoughts?

Manuel


On 03/10/16 17:37, Andreas Lochbihler wrote:
> Hi Manuel,
> 
> Indeed, generic iteration over a set is only well-defined if the set is
> finite. For an infinite set, the generic iteration combinator returns an
> unspecified value, not 0 or 1. In fact, I had imagined a code equation
> like you described, namely
> 
>   "Gcd A = (if finite A then ... else Code.abort (Gcd A))"
> 
> Note that this does *not* pull in finite_UNIV. We could implement the
> finiteness test by
> 
>   "finite (set xs) = True"
>   "finite (List.coset ys) = Code.abort (STR ''Finiteness test on
> Complement'') ..."
> 
> If one imports HOL/Library/Card_UNIV or Containers, then one has to
> provide instances for finite_UNIV and a bunch of other type classes
> anyways. That's the price of using more complicated libraries.
> 
> AFAICS, it does not really matter whether the iteration combinator takes
> an additional argument, because they can be expressed in terms of each
> other:
> 
>   fold_default dflt f A x = (if finite A then dflst A else
> Finite_Set.fold f A x)
>   Finite_Set.fold f A x = fold_default (%A. THE ... A ...) f A x
> 
> The advantage of fold_default with a default value is that the
> finiteness test remains inside the implementation library B whereas with
> Finite_Set.fold, the finiteness test must be done whenever one wants to
> use the combinator. So this might be an argument in favour of fold_default.
> 
> Andreas
> 
> On 03/10/16 16:27, Manuel Eberl wrote:
>> I'm afraid it's not quite as easy as that. You cannot use the existing
>> combinators for comp_fun_commute for Gcd. For infinite sets, these
>> combinators return the neutral element (i.e. "0" for Gcd and "1" for
>> Lcm), but not every infinite set has Gcd 0 or Lcm 1. For setsum/setprod,
>> this works because it is quite simply defined that way, but for Gcd/Lcm
>> it is not.
>>
>> So the alternative would be something like "Gcd A = (if finite A then
>> <combinator magic> else Code.abort …)". This does not work well either,
>> because it requires being able to decide "finite A", which typically
>> introduces the unwanted typeclass requirement "finite_UNIV".
>>
>> My suggestion would be a combinator that, in order to implement a
>> function f :: 'a set => 'a, takes as arguments both a fold operation of
>> type "'a cfc" /and/ the function f itself.
>>
>> It then performs the fold on any "finite by construction" set (e.g. sets
>> represented by the "set" constructor) and returns "Code.abort … (f A)"
>> for anything else (e.g. a set represented by the "coset" constructor).
>>
>> I planned on implementing this at some point, but I've quite a bit of
>> other stuff to do and I wanted to discuss it first, so I never really
>> got around to doing it.
>>
>> Cheers,
>>
>> Manuel
>>
>>
>> On 03/10/16 16:15, Andreas Lochbihler wrote:
>>> Hi René and Manuel,
>>>
>>> Indeed, for sets, expressing the code equations in terms of a generic
>>> iteration operation on sets would do the job for most of the cases. The
>>> comp_fun_commute and comp_fun_idem types  in Containers precisely do
>>> this, but they have not been integrated in the HOL library yet. They
>>> should work all kinds of big operators (setsum, setprod, Gcd, etc) and
>>> could be added to the HOL library.
>>>
>>> Of course, some special case tricks no longer work if go for a generic
>>> iteration operation. For example, one could prove "Gcd (List.coset xs) =
>>> 1" for natural numbers and declare a code equation. Such things would no
>>> longer be possible, but I am not sure whether they are done at all at
>>> the moment.
>>>
>>> Manuel's suggestion of code_abort is a bit cleaner than René's use
>>> Code.abort, because Code.abort does not work with normalisation by
>>> evaluation whereas code_abort does.
>>>
>>> Best,
>>> Andreas
>>>
>>>
>>> On 03/10/16 15:29, Manuel Eberl wrote:
>>>> This is a problem that I have given quite some thought in the past. The
>>>> problem is the following: You have a theory A providing certain
>>>> operations on sets (in this case: Gcd) and a theory B providing
>>>> implementations for sets (in this case: Containers).
>>>>
>>>> The problem is that the code equations for the operations from A depend
>>>> on the implementation that is chosen for sets. A cannot give code
>>>> equations for every possible implementation of sets, while B cannot
>>>> possibly import every theory that has operations involving sets and
>>>> give
>>>> code equations for it.
>>>>
>>>> The best possible solution would be to imitate the way it is currently
>>>> done for setsum, setprod, etc: Define a sufficiently general combinator
>>>> that iterates over the set and give the code equations in A in terms of
>>>> this combinator. Then B only has to reimplement this generic
>>>> combinator.
>>>>
>>>> That would be the cleanest solution, but I'm not sure how such a
>>>> combinator would look like. The folding operation would probably
>>>> have to
>>>> satisfy some associativity/commutativity laws and have that information
>>>> available at the type level (similar to the cfc type in Containers).
>>>>
>>>>
>>>> By the way, my current workaround for this problem is to declare all
>>>> problematic constants as "code_abort".
>>>>
>>>>
>>>> Cheers,
>>>>
>>>> Manuel
>>>>
>>>>
>>>> On 03/10/16 15:21, Thiemann, Rene wrote:
>>>>> Dear all,
>>>>>
>>>>> in the following theory, the export-code fails:
>>>>>
>>>>> (Isabelle 957ba35d1338, AFP 618f04bf906f)
>>>>>
>>>>> theory Problem
>>>>>   imports
>>>>>   "~~/src/HOL/Library/Polynomial_Factorial"
>>>>>   "$AFP/thys/Containers/Set_Impl"
>>>>> begin
>>>>>
>>>>> definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where
>>>>>   "foo x y = gcd y x"
>>>>>
>>>>> definition bar :: "int ⇒ int" where
>>>>>   "bar x = foo x (x - 1)"
>>>>>
>>>>> export_code bar in Haskell
>>>>> end
>>>>>
>>>>>
>>>>> The problem arises from two issues:
>>>>> - factorial_semiring_gcd requires code for
>>>>>   Gcd :: “Set ‘a => ‘a”, not only for the binary “gcd :: ‘a => ‘a =>
>>>>> ‘a”!
>>>>> - the code-equation for Gcd is Gcd_eucl_set: "Gcd_eucl (set xs) =
>>>>> foldl gcd_eucl 0 xs”
>>>>>   where “set” is only a constructor if one does not load the
>>>>> container-library.
>>>>>
>>>>> It would be nice, if one can either alter factorial_semiring_gcd so
>>>>> that it does not
>>>>> require “Gcd” anymore, or if the code-equation is modified in a way
>>>>> that permits
>>>>> co-existence with containers. (Of course, similarly for Lcm).
>>>>>
>>>>>
>>>>> With best regards,
>>>>> Akihisa, Sebastiaan, and René
>>>>>
>>>>> PS: We currently solve the problem by disabling Gcd and Lcm as
>>>>> follows:
>>>>>
>>>>> lemma [code]: "(Gcd_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Gcd
>>>>> on sets'') (λ _. Gcd_eucl)"  by simp
>>>>> lemma [code]: "(Lcm_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Lcm
>>>>> on sets'') (λ _. Lcm_eucl)"  by simp
>>>>> _______________________________________________
>>>>> isabelle-dev mailing list
>>>>> isabelle-dev at in.tum.de
>>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>>>
>>>>>
>>>>>
>>>> _______________________________________________
>>>> isabelle-dev mailing list
>>>> isabelle-dev at in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>>
>>>>
>>>>