make solve_ndisj more powerful

Fixes #34 (closed).

namespace_subseteq_difference_l strikes me as something that should be moved to sets.v? It has nothing to do with namespaces.

That probably makes sense.

added 1 commit

• d1b91fbe - move some general set lemmas to sets.v; organize ndisj hints a bit

Compare with previous version

Done.

added 1 commit

• 248a89ff - more generalization of lemmas and a few comments for [solve_ndisj]

Compare with previous version

added 1 commit

• c081e1b7 - more generalization of lemmas and a few comments for [solve_ndisj]

Compare with previous version

I also found even more lemmas in "namespaces" that apply to all sets, and moved them over as well.

added 1 commit

• 5695ee20 - coqdoc++

Compare with previous version

resolved all discussions

LGTM

Would be good to see if this impacts timing of iris, lambdarust, and iris-examples.

Well we can see that after landing.

Sure, but could you make sure we record timing info that includes just this change?

I guess I can try... I need scripts for this stuff.^^

But I can only really do that after you land it so that I know which std++ revisions to use.

But do we have timing information from just before this change? Or does it include random other stuff?

Once I know what "just before this change" is, I can make sure that we have that timing information. But that is only determined after landing the change. :)

Oh, maybe I was not clear, but with !75 (comment 37450) I meant you can merge.

Ah I thought I'd leave pressing the merge button to you, as "project owner". Okay, will do.

merged

mentioned in commit 9d08f65f

Performance impact:

• Iris: +0.02%
• examples: -0.21%
• lambda-rust: -0.59%

The Iris change is within noise range.

Thanks :)