Email Gateway (Aug 22 2022 at 10:48): Email Gateway (Aug 22 2022 at 10:48):From: Lars Hupel <hupel@in.tum.de>
Dear list,
is there any reason why there's no Quickcheck setup for finite sets? I
couldn't find any, so I tried setting it up (see attached theory). I'm
hardly a Quickcheck expert, so I have no idea whether it makes sense –
at least it works for some cases I tried.
Slightly related question: How does the interaction between the datatype
package and Quickcheck work? It appears that it produces instances of
full_exhaustive in certain cases and not in others, but I'm not quite
sure in which cases. (Current working hypothesis: It doesn't when nested
recursion is involved.) Is there any other way to conveniently obtain
full_exhaustive instances?
Cheers
Lars
FSet_Quickcheck.thy
Email Gateway (Aug 22 2022 at 10:50):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
quickcheck in its current form was mainly developed by Lukas Bulwahn, who left academia
before fset became usable. So far, nobody cared to add the quickcheck setup. From my
experience with quickcheck, your setup is fine. However, you could also just have used the
command
quickcheck_generator fset constructors: "{||}", finsert
which generates almost the same instances as you did manually. The difference is that the
your instances check whether an new element is already present in the set and if so, they
skip the execution assuming that it has been tested before. This is just an optimisation
which avoids to run the code on equivalent test case several times, but I doubt that this
redundancy causes any problems in practice.
According to the documentation in isar-ref, quickcheck installs random and exhaustive
generators for first-order datatypes. I do not know whether the documentation has been
kept up to date during the transition to the BNF package, but it looks as if it is still
correct. So no nested recursion.
Best,
Andreas
Email Gateway (Aug 22 2022 at 10:50):From: Lars Hupel <hupel@in.tum.de>
Hi Andreas,
However, you could also just have used the command
quickcheck_generator fset constructors: "{||}", finsert
which generates almost the same instances as you did manually.
first of all, I didn't know about that command :-)
Anyway, the way I implemented the generator for 'fset's was to copy the
generator for 'set's and changed the constants (e.g. 'insert' → 'finsert').
If nobody objects, I would add these instances to the 'FSet' theory in
HOL-Library.
According to the documentation in isar-ref, quickcheck installs random
and exhaustive generators for first-order datatypes. I do not know
whether the documentation has been kept up to date during the transition
to the BNF package, but it looks as if it is still correct. So no nested
recursion.
Maybe this is a candidate for consolidation with the 'Derive' AFP entry.
(On the other hand, as far as I know, that one doesn't support nested
recursion through non-datatypes.)
Because you mentioned it in your mail, I also tried
'quickcheck_generator' on my datatype, but it (silently!) fails to
produce instances.
Cheers
Lars
Last updated: Apr 25 2024 at 12:23 UTC