QuickChick 3.0: scheduled derivation, proof-local testing, Rocq scorers - #436

…ee, option, list

…r generation to make it correct

…nto internal-rewrite

The Rocq 9.0 job's dependency resolution now exceeds opam's default
60-second limit and fails before anything is built.

The simple derivers declared each function as a fixpoint over the type,
which Coq rejects for a record or a Variant since neither is recursive.
A function that never calls itself is now written into its instance
instead. Fixes #155 and #285.

localMin ignored the maxShrinks argument and always shrank until no
candidate failed. It now stops once that many successful shrinks have
been made. updMaxShrinks sets the limit, like the other Args updaters.

Fixes #293.

Sample, QuickChick, MutateCheck and the related commands applied
sampleGen, show, quickCheck and friends relying on their implicit
arguments, so they broke when a user changed those with Arguments.
They now apply the constants explicitly, with a hole for each leading
argument.

Fixes #351.

Fixes #303.

forAllShrinkNonDet repeated the shrink tree it had already evaluated,
so every retry saw the same result and it behaved like forAllShrink. A
shrink candidate whose test discards is now run again with a fresh
seed, up to the given number of times, before it is rejected.

Fixes #372.

Show QuickChickWith with stdArgs and the update functions, list the
analysis field, and document forAllShrinkNonDet.

Fixes #123.

Extraction toggled the warning flags by hand. The flags were not
restored if extraction failed, and the fuzzing command never restored
them at all.

Fixes #215.

The extraction directory command now has the same spellings as the
other QuickChick commands; QCExtractDir still works. Dir is read as an
identifier, so it does not become a keyword. A relative directory is
resolved where the command is run, which also avoids extraction's
warning about relative output paths.

Port the active DependentTest relations to scheduled public derivations. Check results and input behavior instead of the old generated term shape, and add parameterized relations, fixed and repeated inputs, reordered outputs, and explicit unsupported-output checks.

The regression compiles with local plugins and theories on Coq 8.20 and Rocq 9.1. Two random-generator checks each pass 20 trials; deterministic enumeration and checker assertions also pass.

Relations were referred to by their base names, so in a module M2
defining Test, a premise about M1.Test was read as a recursive call of
M2.Test: the derived checker either failed to typecheck or, when the
types matched, checked the wrong relation. Inductives are now named by
their shortest unambiguous name, and helper names spell M1.Test as
M1_Test.

Fixes #311.

Properties built from <->, True or False could not be checked even
when their parts were decidable.

A premise such as In x l, defined by a function rather than an
inductive relation, could only be scheduled as a producer, which has no
derivation, so quickchick failed. It is now checked after its variables
are generated. quickchick also tests a goal whose variables were
introduced, quantifying them and the hypotheses about them again. The
check for abstract types no longer crashes on a hypothesis that
mentions earlier variables.

Fixes #109.

A typing relation with a context Gamma : nat -> ty concludes with
Gamma x and extends the context with fun k => match k with ... in a
premise. The application of a constructor variable now becomes a fresh
variable with an equality premise, as applications of defined functions
already did, and lambdas and matches in premise arguments are renamed,
generated and scheduled as computed arguments that need their free
variables bound.

Derived generators and printers wrote a constructor by its base name.
When another global had that name, such as a definition Bool next to a
constructor Z.Bool, the generated code referred to the other global
and failed to typecheck. Constructors are now written by the shortest
name that denotes them, as inductives already were; Show still prints
the constructor's own name, and Merge declares base names.

A premise written with an alias such as Definition Step := R was taken
for a function-defined proposition, which is only checked, so it could
not produce its arguments and derivation failed. A constant whose body
is an inductive is now read as that inductive.

A conclusion that computed an index with a match, such as an if over a
sumbool, failed with an anomaly: the branches bind their proofs
anonymously. Such a match now becomes a fresh variable with an equality
premise, as a function call does, and anonymous branch binders get
fresh names.

A premise that passes a computed argument, such as an extended context
fun k => match k with ..., to another relation in a mode that needs an
instance check failed with "cannot infer a dependency containing a
binder". The check now takes the argument's free variables.

A derived checker or constrained enumerator that enumerates values of
an unconstrained variable sees only the values up to the size bound.
When the variable's type is infinite, such as a list, finding no
witness among them does not refute the premise, but the checker
answered Some false. A typing relation whose literals take any label
was refuted for well-typed terms this way.

Such an enumeration is now bound through enumIncomplete, which ends it
with None, so exhausting it answers None. Enumerations of finite types
(non-recursive inductives whose fields are finite) stay complete and
still refute; they replace the previous None marker that checkers
added to every enumeration. Generic code cannot know that a type
parameter's enumerator is complete, so a checker over one with an
empty enumerator now answers None.