Skip to content
GitLab

Many improvements to `multiset_solver`

Merged 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.