cogset

Add a type cogset A of finite/cofinite sets of elements of countable type A. When A is also infinite, all the usual operations are decidable. The implementation uses a pair of constructors (finite or infinite) each carrying a finite set.

The file includes efficient conversions to and from gset A (for finite cogsets) and to coPset (for arbitrary cogsets), as well as less efficient conversions to and from other finite sets and other sets with a top element.

Two things are marked TODO in the source, which really means "to discuss".

changed the description

mentioned in issue #48

Thanks for the MR. Overall looks good to me.

I'm not sure I'd like the name cogset. Maybe some capitals would make it easier to read?

Would be worth taking a look at the conventions used elsewhere (and also in Iris). I think @jung had some opinions about capitalization of acronyms.

added 3 commits

• fce412de - Avoid Variant.
• 3338e430 - Rename CofinGSet -> CoFinGSet.
• 5041f6f6 - Add another goal set_solver cannot solve.

Compare with previous version

added 1 commit

• a09c9e39 - Add set_unfold_cogset_top for discussion.

Compare with previous version

added 2 commits

• ce3c6219 - Note limitation of [cogset positive].
• 69a94a48 - Drop a TODO (now issue #49 (closed)).

Compare with previous version

added 1 commit

• be1f8d38 - Indicate goals [set_solver] cannot solve.

Compare with previous version

added 1 commit

• 35736d34 - Refine the cogset_elem_of_dec proof.

Compare with previous version

added 1 commit

• cfab3848 - Drop a TODO and mark cogset_dom TC opaque (see #48).

Compare with previous version

added 1 commit

• 8520760b - Adjust cogset_elem_of_dec.

Compare with previous version

added 1 commit

• d1f3df51 - Rename cogset --> coGset.

Compare with previous version

Once @robbertkrebbers responds and we resolve the lingering threads, would it be OK to (i) rebase to master (to use TopSet in this MR) and (ii) eliminate most of the intermediate commits?

My understanding is that rebasing renders gitlab threads hard to follow. Rebasing after all threads are resolved should avoid that problem.

Once @robbertkrebbers responds and we resolve the lingering threads, would it be OK to (i) rebase to master (to use TopSet in this MR) and (ii) eliminate most of the intermediate commits?

Yes, rebasing and squashing on master would be great.

added 1 commit

• a5af0f13 - Whitespace.

Compare with previous version

added 18 commits

• a5af0f13...af368a15 - 16 commits from branch iris:master
• 88cf7a25 - Add lemma `not_elem_of_iff`.
• 367d993f - Add cogset.

Compare with previous version

added 1 commit

• a78687b2 - Add `coGset`.

Compare with previous version

resolved all threads

added 1 commit

• bccca114 - `coGset` comments.

Compare with previous version

resolved all threads

added 1 commit

• 41621488 - Shorten proof of `not_elem_of_iff`.

Compare with previous version

added 8 commits

• 41621488...e0eef94a - 6 commits from branch iris:master
• 157ae750 - Add lemma `not_elem_of_iff`.
• f5abe554 - Add `coGset`.

Compare with previous version

resolved all threads

@robbertkrebbers anything else?

merged

mentioned in commit 74649a4b

Merged. Thanks a lot for the MR and taking all the feedback into account.