Skip to content

Many improvements to `multiset_solver`

Robbert Krebbers requested to merge robbert/multiset_solver into master
  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.

Merge request reports