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