Many improvements to `multiset_solver`

1. Support ∈
2. Support ⊂
3. Support case splitting on multiplicity x {[ y ]}, but only do this when there's no other way.

With the improved multiset_solver I am able to solve pretty much all lemmas in the gmultiset file automatically (apart from those that involve elements, size, and other connectives that are out of scope).

The new version also handles @fpottier's test case x ∈ X → {[x]} ⊆ X from #86 (closed).

In addition, I added a bunch of other test cases.

@msammler @snyke7; since you both use multiset_solver could you test this MR so as to see there are no regressions?

added 2 commits

• a3e225ea - Update `multiset_solver` documentation.
• 77408202 - Reorganize and extend test file for `multiset_solver`.

Compare with previous version

Sounds cool!

added 2 commits

• adc79545 - Update `multiset_solver` documentation.
• e964fc78 - Reorganize and extend test file for `multiset_solver`.

Compare with previous version

Does it also handle the testcase in the main issue description of #86 (closed) (so, can we close that issue once this lands)?

added 1 commit

• 0747d547 - Tweak docs.

Compare with previous version

resolved all threads

mentioned in issue #86 (closed)

I added a bunch of other test cases.

That's awesome. :)

LGTM.

mentioned in merge request !232 (closed)

added 12 commits

• 0747d547...6d001c9d - 3 commits from branch master
• 1cba100b - Fix priorities of `SetUnfold` instances for `multisets`.
• d063413c - Extend `multiset_solver` with support for `∈`.
• 8cf6ac9e - Let `multiset_solver` case split on `x = y`/`x ≠ y` for `multiplicity x {[ y ]}`.
• bb8ce569 - Tweak `multiset_simplify_singletons` to avoid needless case-splits.
• 99b2a184 - Extend multiset_solver with support for `⊂`.
• 1efc3af6 - Update `multiset_solver` documentation.
• deb87cfd - Reorganize and extend test file for `multiset_solver`.
• a4bbf88f - Tweak docs.
• 3375dd20 - Turn `x ∈ X` only into `0 < multiplicity x X` at leaves of `∈` to enable...

Compare with previous version

I detected a regression in Iris, I fixed that, and added a testcase.

LGTM.

added 1 commit

• 891f58bf - Put `SetUnfoldElemOf` instances together.

Compare with previous version

added 1 commit

• 691a6000 - Better tests for `∈` in conclusion of `multiset_solver` goal.

Compare with previous version

resolved all threads

merged

mentioned in commit 7fdaea0f