Add solver `multiset_solver` for multisets

The code contains some documentation how it works.

I added a number of tests, and used it to automate many existing lemmas in the gmultiset file.

Note that this required restructuring the file quite a bit, since I needed some basic lemmas (now in section basic_lemmas) to define the tactic, and wanted to use the tactic subsequently to prove many of the existing lemmas (now in section multiset_unfold). None of the lemma statements changed, only many proofs are replaced by a mere call to multiset_solver.

/cc @msammler

changed the description

I tested the solver on the use-case in RefinedC and it works like a charm.

I trust you that the lemmas stayed the same and except for the small comments looks good to me.

added 4 commits

• d3d95ed9 - Add solver `multiset_solver` for multisets.
• 8f80353d - Add tests for `multiset_solver`.
• f4269240 - CHANGELOG.
• 45b64e21 - Make `multiset_solver` stronger by also considering `multiplicity` in hyps.

Compare with previous version

mentioned in issue #73 (closed)

resolved all threads

I think this is ready. Any objection @jung @msammler ?

LGTM

I don't really understand what happens here but that's okay, I am happy leaving that to you.^^ Having this tactic certainly makes a lot of sense.

I don't really understand what happens here but that's okay

Anything in particular that you don't understand?

No. There's just a couple hundred lines of stuff going into and actually understanding it would require spending more time on it than I think is justified (and than I have right now) -- it's not like I did that with set_solver. I am happy to delegate this entirely to you.

Ok, fair enough.

Just to be clear: this tactic is a heuristic, it's incomplete, so depending on what other goals we get in the future we want to keep tweaking it.

If you want a thorough review from me, I can of course do that, but likely after the POPL deadline.

Nah, I think it's fine. I guess you'll do that once you start using the tactic and start discovering its incompletenesses

mentioned in commit 376e5e05

merged