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

[Manuel Eberl]

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
>>
>>