slim_check is broken

Stream: mathlib4

[Scott Morrison]

!4#3114 adds a tactic frontend for slim_check. It's been sitting there for a while, and @Heather Macbeth just added an example where it isn't finding an easy counterexample.

Motivated by this, I decided to try adding some further instances of ExtSampleable and Testable, but I think I decided that the current design of the plumbing is actually broken. (This doesn't affect the porcelain in !4#3114, which could still be merged either way.)

In particular, I claim it is impossible to make, with the current design, a polymorphic Shrinkable (List α) instance.

The problem is that we have Shrinkable extend WellFoundedRel, which pulls in fields rel and wf : WellFounded rel. However we have no control over what that rel is, and that lack of control will bite us. In the instances that exist so far, the instance that gets found provides rel a b := sizeOf a < sizeOf b, and indeed there are places in the documentation that assume that the relation is actually this!

Suppose we try to construct instance [Shrinkable α] : Shrinkable (List α). (It doesn't really matter how we plan to implement it: perhaps some combination of dropping elements and/or shrinking elements.). Then we'll pull in the WellFoundRel instance for List α, which is in terms of the default SizeOf instance for lists. However there's no guarantee that the relation embedded in Shrinkable α has anything to do with SizeOf...

One possible fix would be to not extend WellFoundRel, and instead just change the signature of Shrinkable.shrink, so it reads

shrink : (x : α) → List { y : α // sizeOf y < sizeOf x }

i.e. force always using sizeOf. This would require us to parametrize Shrinkable α by a SizeOf α instance.

The problem we quickly run into here is that the SizeOf instances available are, well, crap. They're often noncomputable, and often not the convenient thing to work with.

A solution would be to just add a field size : α → ℕ to Shrinkable, and then have

shrink : (x : α) → List { y : α // size y < size x }

This, I think, would actually be workable.

However I want to propose something else, which is to just drop all the proofs from Shrinkable entirely. I don't really see why they are there, and they add considerably to the burden for someone wanting to create new SampleableExt instances.

The only thing we gain from these proofs is that docs4#SlimCheck.Testable.minimize is an entire function. Without these proofs, we have to put partial on minimizeAux. But ... who cares? It's not like we are ever going to need a proof that if slim_check finds a counterexample, and then it finds a smaller one, that smaller one is really smaller... It's still a perfectly fine counterexample. Nor do we care about proofs that slim_check will actually terminate.

This would make everything simpler, a function only used in metaprogramming gains a partial, and we can actually (and easily) implement Shrinkable (List α).

@Henrik Böving, @Simon Hudon, others, any opinions on all this? You can see this worked out at https://github.com/leanprover-community/mathlib4/compare/slim_check_frontend...slim_check_no_proofs?expand=1.

[Eric Wieser]

A related observation about slim_check; in lean 3 it was only able to verify counterexamples with by decide, which means it's useless for equalities of real numbers even in places where norm_num knew the answer

[Henrik Böving]

So this SizeOf behavior that you are seeing right now is precisely what we also observed while designing this API. In fact I would say 60% of the port was hammering slim_check into a form where this proof would work out, Simon and I spent several days trying to figure something out that worked.

I think dropping the termination proof could be fine. For me slim_check was mostly a project to see whether Lean at the time could actually verify a non trivial piece of software in a way that is not completely convoluted and I think it did^^ But for usability sake I would say it is fine that we drop this property and instead just assume the users are providing lawful instances (maybe until one day the automation is good enough to add it back!!)

[Scott Morrison]

It seems like to answer Eric's question, some rearrangement of the monads is necessary. We need to work with both Rand (for generating examples) and MetaM (for e.g. running norm_num or whatever to generate proofs).

[Scott Morrison]

I made !4#3835, removing the proofs, and adding a sampleable instance for List.

[Eric Wieser]

At risk of a tangent, is there a way to write a function (s : Finset X) (hs : s.nonempty) : Rand X without needing unsafe or partial?

[Henrik Böving]

Is there a function for getting a list from a finset?

[Eric Wieser]

docs4#Quot.unquot

[Eric Wieser]

Oh, or you can sort

[Eric Wieser]

Maybe the answer is that in practice any concrete type can be sorted

[Henrik Böving]

Right, if you can get a list there is a function for grabbing a random value from it, oneOf I think

[Eric Wieser]

Yeah, but getting a list is unsafe without the handwave of "randomness lets me pull a value out of the quotient"

[Scott Morrison]

@Eric Wieser , @Henrik Böving, !4#3838 makes some tweaks to Rand, Gen, and then slim_check that I think should allow it to call norm_num or other tactics while testing. It comes at some expense: Rand is now a monad transformer, not just a monad...

I didn't actually implement a Testable that makes use of this new-found freedom to work in MetaM, but I'm out of time for now and thought I'd show you both this at this stage. I think it should be straightforward from here to add some Testables that use norm_num to do computations in Real, etc.