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

[Andreas Lochbihler]

Hi Manuel,

My point with "finite" was that for the current default setup, you don't need any type 
class instantiations (see the code equations below). Only if someone imports Card_UNIV 
from HOL/Library (e.g., for FinFun or for Containers), he or she has to do the 
instantiations for finite_UNIV for the types on which they want to execute big operators. 
But most users do not import Card_UNIV, so they are not affected.

Using a copy of "finite" is also possible and maybe even a good idea. The existing 
constant "finite" is an important concept in many theorems. Using a copy "finite_code" in 
the code equations separates code generation from logical reasoning, which is often a good 
thing. However, if we then implement the existing constant "finite" using the equation

   "finite = finite_code"

then we have not gained much and introduced some amount of duplication. And if we stick to 
the existing setup for "finite" with

   "finite (set xs) = True"
   "finite (List.coset ys) = Code.abort ... ..."

then we run into the very same pattern-match problems that René reported. If we delete all 
code equations for "finite", then this renders quickcheck a little bit less useful, 
because it can no longer work on theorems involving finiteness. But I am not sure how much 
quickcheck can do in practice for theorems involving "finite".

Andreas

On 03/10/16 22:51, Manuel Eberl wrote:
> 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
>>>>>
>>>>>
>>>>>