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

[Tobias Nipkow]

On 15/08/2014 09:30, Andreas Lochbihler wrote:
> 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. *)

Peter, does that mean you could replace your specific construction by something
in Quickcheck_Types.thy? In that case I would recomment to keep
Quickcheck_Types.thy (or some part of it) alive, maybe under a less specific
name, and Peter uses it in his AFP entry.

Tobias

> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev