[isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy

[Andreas Lochbihler]

In 51aa30c9ee4e, I have added lattice instances for the Enum.finite_* types. As expected, 
this suffices for the quickcheck examples in Quickcheck_Lattice_Examples (see 9225b2761126).

This now raises the question what we should do with HOL/Library/Quickcheck_Types. Within 
the Isabelle distribution and the AFP, this theory is no longer used anywhere. I expect 
that almost nobody relies on the quickcheck setup in there. From the quickcheck point of 
view, we can therefore drop this theory. Anyone who needs it can keep their own local copy.

However, the constructions might still be useful, as the following comment from Peter 
Lammich's AFP entry Refine_Monadic shows.

   (* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides
     an isomorphic contruction. *)

So, should we keep Quickcheck_Types (maybe under a different name, say 
Lattice_Constructions) or drop it?

Andreas

On 11/07/14 15:54, Andreas Lochbihler wrote:
> Quickcheck does not use these types, because it is currently configures to only use the
> types finite_1 to finite_3 from Enum, because the finite_types parameter is set by
> default. Quickcheck internally also seems to work differently depending on whether the
> finite_types flag is set.
>
> I have only little insight how the parameters affect the performance of quickcheck, but I
> remember that Quickcheck originally used int as a replacement. Quickcheck_Types clearly is
> from that time. However, int is an infinite type and therefore, quantifiers, set
> comprehensions and function equality are not executable. Later, he switched to the
> finite_X types, which instantiate enum, but not the other type classes.
>
> Therefore, I recommend the following:
>
> 1. Temporarily fix Quickcheck_Types such that it works again, but leave it in HOL/Library.
> Then, anyone who wants to use quickcheck with infinite types can do so. This way, the
> Quickcheck_Examples session can also be reactivated.
>
> 2. Instead of moving Quickcheck_Types to Main, it suffices to make the finite_X types
> instances of the lattice type class hierarchy. Probably most of the stuff in
> Quickcheck_Types can be adapted to work with the Enum types as well. Maybe even all the
> test cases in Quickcheck_Lattice_Examples work with the Enum types, too.
>
> I have already done step 1 in 36041934e429 and 8840fa17e17c, but I won't have time for
> step 2 before the fork of the release branch.
>
> Andreas
>
>
> On 11/07/14 14:28, Tobias Nipkow wrote:
>>
>>
>> On 11/07/2014 13:43, Andreas Lochbihler wrote:
>>> Quickcheck_Types defines a number of artificial types that quickcheck can use to
>>> instantiate type variables that occur in a theorem. Normally, quickcheck
>>> instantiates them with int provided that the sort constraints do not prevent
>>> this. In Enum.thy, there are already the types finite_X that quickcheck uses for
>>> enumerable types (type class enum) such that quantifiers can be unfolded into
>>> conjunctions or disjunctions.
>>>
>>> The types in Quickcheck_Types now do the same for the lattices type class
>>> hierarchy, because int and the finite_X types cannot be used for type variables
>>> with sort lattice (or top/bot/...).
>>>
>>> I believe that it should be fairly simple to adjust Quickcheck_Types to
>>> Isabelle2014. However, this only makes sense if it becomes part of Main.
>>> Otherwise, it will remain just a library theory that hardly anyone knows about
>>> and no one uses.
>>>
>>> Moreover, we should make sure that Quickcheck_Types fits to the current code
>>> generator setup for lattices. IIRC, Florian has reworked a lot there over the
>>> past years. At the very least, we should have some test cases (e.g. in HOL/ex)
>>> to check that Quickcheck_Types works as expected.
>>>
>>> If there's consensus on reviving this theory, I can do the changes to
>>> Quickcheck_Types such that Isabelle2014 digests it. This is probably all that
>>> can be done before the release as most of us will be busy in Vienna next week. A
>>> move to Main is something for the next release.
>>
>> It looks mildly useful. But then Qickcheck would need to use it, which it
>> currently obviously does not. If you (or somebody) is able to make that happen,
>> then I am in favour of reviving that theory.
>>
>> Tobias
>>
>>> Andreas
>>>
>>>
>>> On 11/07/14 13:22, Lawrence Paulson wrote:
>>>> I’m afraid that I don’t even know what it is.
>>>> Larry
>>>>
>>>>
>>>> On 11 Jul 2014, at 12:21, Florian Haftmann
>>>> <florian.haftmann at informatik.tu-muenchen.de> wrote:
>>>>
>>>>> The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken
>>>>> has not been addressed since before the last release.
>>>>>
>>>>> So, which path to follow?  Is there any interested in a serious repair
>>>>> effort?  Otherwise, we should honestly drop it.
>>>>
>>>> _______________________________________________
>>>> 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
>> _______________________________________________
>> 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