feat: unbundle array size constraint from hash map bucket array

[TwoFX]

This PR makes sure that the positivity checker is happy with the following construction:

inductive ContainsItselfInHashMapValues where
  | base
  | recursive (l : HashMap.Imp Bool ContainsItselfInHashMapValues)

Users actually want to do this, see this article (search for "recursive datatype") and the code. The users had to build their own primitive map (see here), but arguably the standard HashMap.Imp should just support this. Users will have to pass the well-formedness constraints around by hand, but that is much better than nothing.

To make this possible, HashMap.Imp.Buckets had to lose the constraint that the bucket array has positive size. This is now part of Buckets.WF. Without knowing that there is at least one bucket, none of the operations are able to access the bucket array, so they are all wrapped in an if 0 < buckets.size. It's not pretty, but we should be able to live with the performance hit. I fixed all of the well-formedness lemmas, though I struggled with expand_size and ended up rewriting that one into a style that I hope is easier to follow for someone without Mario-level Lean skills :-)

This PR targets nightly-testing for now because it uses the new functional induction principles from Lean 4.8.

• Depends on: fix: Data.List.Lemmas shoud import Data.List.Init.Lemmas on nightly-testing #746
• Depends on: feat: List.(take|drop)_set_of_lt #747

[digama0]

I'm concerned about the precedent that this sets. The rules on nested inductives are very strict and also abstraction-breaking, so having such a promise limits our ability to hide implementation details and evolve the library in the future. I think it would be better to support nested inductives of this kind through an external package (or future improvement to the inductive command) which has more semantic requirements on nested inductive occurrences.

[digama0]

This should be a parameter to the function. There is no need to be doing this check here. You can also avoid having an additional parameter in the IR by smuggling the property in a subtype, as in (data : {b : Buckets α β // 0 < b.size}).

[digama0]

Here's a counterproposal which includes elements of my other suggestion and also leads to a much smaller diff, while still meeting the goal of having HashMap.Imp be nested-inductive-safe:

• Change the definition of HashMap.Imp to contain buckets : Array (AssocList α β) instead of buckets : Imp.Buckets α β.
• Buckets retains its original definition as {b : Array (AssocList α β) // 0 < b.size}, and all the operations use this type
• HashMap.WF gets a size : 0 < buckets.size field as in this PR
• Operations on HashMap like HashMap.insert recombine the buckets from the Imp with the property from WF on the fly

This way, there is no need for if statements in the main functions, and most of the hard proofs are unaffected.

[kim-em]

Apologies, I needed to reset nightly-testing, and incorrectly deleted it instead. @TwoFX, you may need to reconsistute this PR.