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

theories/coGset.v

+(* Copyright (c) 2020, Coq-std++ developers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file implements the type [coGset] of finite/cofinite sets of
+elements of any countable type.
+
+Note that [coGset positive] cannot represent all elements of [coPset]
+(e.g., [coPset_suffixes], [coPset_l], and [coPset_r] construct
+infinite sets that cannot be represented). *)
+From stdpp Require Export sets countable.
+From stdpp Require Import decidable finite gmap coPset.
+(* Set Default Proof Using "Type". *)
+
+Inductive coGset `{Countable A} :=
+  | FinGSet (X : gset A)
+  | CoFinGset (X : gset A).
+Arguments coGset _ {_ _} : assert.
+
+Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
+Proof. solve_decision. Defined.
+Instance coGset_countable `{Countable A} : Countable (coGset A).
+Proof.
+  apply (inj_countable'
+    (λ X, match X with FinGSet X => inl X | CoFinGset X => inr X end)
+    (λ s, match s with inl X => FinGSet X | inr X => CoFinGset X end)).
+  by intros [].
+Qed.
+
+Section coGset.
+  Context `{Countable A}.
+
+  Global Instance coGset_elem_of : ElemOf A (coGset A) := λ x X,
+    match X with FinGSet X => x ∈ X | CoFinGset X => x ∉ X end.
+  Global Instance coGset_empty : Empty (coGset A) := FinGSet ∅.
+  Global Instance coGset_top : Top (coGset A) := CoFinGset ∅.
+  Global Instance coGset_singleton : Singleton A (coGset A) := λ x,
+    FinGSet {[x]}.
+  Global Instance coGset_union : Union (coGset A) := λ X Y,
+    match X, Y with
+    | FinGSet X, FinGSet Y => FinGSet (X ∪ Y)
+    | CoFinGset X, CoFinGset Y => CoFinGset (X ∩ Y)
+    | FinGSet X, CoFinGset Y => CoFinGset (Y ∖ X)
+    | CoFinGset X, FinGSet Y => CoFinGset (X ∖ Y)
+    end.
+  Global Instance coGset_intersection : Intersection (coGset A) := λ X Y,
+    match X, Y with
+    | FinGSet X, FinGSet Y => FinGSet (X ∩ Y)
+    | CoFinGset X, CoFinGset Y => CoFinGset (X ∪ Y)
+    | FinGSet X, CoFinGset Y => FinGSet (X ∖ Y)
+    | CoFinGset X, FinGSet Y => FinGSet (Y ∖ X)
+    end.
+  Global Instance coGset_difference : Difference (coGset A) := λ X Y,
+    match X, Y with
+    | FinGSet X, FinGSet Y => FinGSet (X ∖ Y)
+    | CoFinGset X, CoFinGset Y => FinGSet (Y ∖ X)
+    | FinGSet X, CoFinGset Y => FinGSet (X ∩ Y)
+    | CoFinGset X, FinGSet Y => CoFinGset (X ∪ Y)
+    end.
+
+  Global Instance coGset_set : Set_ A (coGset A).
+  Proof.
+    split; [split| |].
+    - by intros ??.
+    - intros x y. unfold elem_of, coGset_elem_of; simpl.
+      by rewrite elem_of_singleton.
+    - intros [X|X] [Y|Y] x; unfold elem_of, coGset_elem_of, coGset_union; simpl.
+      + set_solver.
+      + by rewrite not_elem_of_difference, (comm (∨)).
+      + by rewrite not_elem_of_difference.
+      + by rewrite not_elem_of_intersection.
+    - intros [] [];
+      unfold elem_of, coGset_elem_of, coGset_intersection; set_solver.
+    - intros [X|X] [Y|Y] x;
+      unfold elem_of, coGset_elem_of, coGset_difference; simpl.
+      + set_solver.
+      + rewrite elem_of_intersection. destruct (decide (x ∈ Y)); tauto.
+      + set_solver.
+      + rewrite elem_of_difference. destruct (decide (x ∈ Y)); tauto.
+  Qed.
+End coGset.
+
+Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A}) :=
+  λ x X,
+  match X with
+  | FinGSet X => decide_rel elem_of x X
+  | CoFinGset X => not_dec (decide_rel elem_of x X)
+  end.
+
+(** * Top *)
+Lemma coGset_top_subseteq `{Countable A} (X : coGset A) : X ⊆ ⊤.
+Proof. done. Qed.
+Hint Resolve coGset_top_subseteq : core.
+
+Section infinite.
+  Context `{Countable A, Infinite A}.
+
+  Global Instance coGset_leibniz : LeibnizEquiv (coGset A).
+  Proof.
+    intros [X|X] [Y|Y]; rewrite elem_of_equiv;
+    unfold elem_of, coGset_elem_of; simpl; intros HXY.
+    - f_equal. by apply leibniz_equiv.
+    - by destruct (exist_fresh (X ∪ Y)) as [? [? ?%HXY]%not_elem_of_union].
+    - by destruct (exist_fresh (X ∪ Y)) as [? [?%HXY ?]%not_elem_of_union].
+    - f_equal. apply leibniz_equiv; intros x. by apply not_elem_of_iff.
+  Qed.
+
+  Global Instance coGset_equiv_dec : RelDecision (≡@{coGset A}).
+  Proof.
+    refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz).
+  Defined.
+
+  Global Instance coGset_disjoint_dec : RelDecision (##@{coGset A}).
+  Proof.
+    refine (λ X Y, cast_if (decide (X ∩ Y = ∅)));
+      abstract (by rewrite disjoint_intersection_L).
+  Defined.
+
+  Global Instance coGset_subseteq_dec : RelDecision (⊆@{coGset A}).
+  Proof.
+    refine (λ X Y, cast_if (decide (X ∪ Y = Y)));
+      abstract (by rewrite subseteq_union_L).
+  Defined.
+
+  Definition coGset_finite (X : coGset A) : bool :=
+    match X with FinGSet _ => true | CoFinGset _ => false end.
+  Lemma coGset_finite_spec X : set_finite X ↔ coGset_finite X.
+  Proof.
+    destruct X as [X|X];
+    unfold set_finite, elem_of at 1, coGset_elem_of; simpl.
+    - split; [done|intros _]. exists (elements X). set_solver.
+    - split; [intros [Y HXY]%(pred_finite_set(C:=gset A))|done].
+      by destruct (exist_fresh (X ∪ Y)) as [? [?%HXY ?]%not_elem_of_union].
+  Qed.
+  Global Instance coGset_finite_dec (X : coGset A) : Decision (set_finite X).
+  Proof.
+    refine (cast_if (decide (coGset_finite X)));
+      abstract (by rewrite coGset_finite_spec).
+  Defined.
+End infinite.
+
+(** * Pick elements from infinite sets *)
+Definition cogpick `{Countable A, Infinite A} (X : coGset A) : A :=
+  fresh (match X with FinGSet _ => ∅ | CoFinGset X => X end).
+
+Lemma cogpick_elem_of `{Countable A, Infinite A} X :
+  ¬set_finite X → cogpick X ∈ X.
+Proof.
+  unfold cogpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl.
+  done. by intros _; apply is_fresh.
+Qed.
+
+(** * Conversion to and from gset *)
+Definition coGset_to_gset `{Countable A} (X : coGset A) : gset A :=
+  match X with FinGSet X => X | CoFinGset _ => ∅ end.
+Definition gset_to_coGset `{Countable A} : gset A → coGset A := FinGSet.
+
+Section to_gset.
+  Context `{Countable A, Infinite A}.
+
+  Lemma elem_of_coGset_to_gset (X : coGset A) x :
+    set_finite X → x ∈ coGset_to_gset X ↔ x ∈ X.
+  Proof. rewrite coGset_finite_spec. by destruct X. Qed.
+  Lemma elem_of_gset_to_coGset (X : gset A) x : x ∈ gset_to_coGset X ↔ x ∈ X.
+  Proof. done. Qed.
+  Lemma gset_to_coGset_finite (X : gset A) : set_finite (gset_to_coGset X).
+  Proof. by rewrite coGset_finite_spec. Qed.
+End to_gset.
+
+(** * Inefficient conversion to and from finite sets *)
+Definition coGset_to_fin_set `{Countable A, Empty C, Singleton A C, Union C}
+    (X : coGset A) : C :=
+  match X with
+  | FinGSet X => list_to_set (elements X)
+  | CoFinGset _ => ∅
+  end.
+Definition fin_set_to_coGset `{Countable A, Elements A C} : C → coGset A :=
+  FinGSet ∘ list_to_set ∘ elements.
+
+Section to_fin_set.
+  Context `{FinSet A C, !Countable A, Infinite A}.
+  Implicit Types x : A.
+
+  Lemma elem_of_coGset_to_fin_set X x :
+    set_finite X → x ∈@{C} coGset_to_fin_set X ↔ x ∈ X.
+  Proof.
+    rewrite coGset_finite_spec. destruct X as [X|]; [intros _|done]. simpl.
+    set_solver.
+  Qed.
+  Lemma elem_of_fin_set_to_coGset (X : C) x : x ∈ fin_set_to_coGset X ↔ x ∈ X.
+  Proof. unfold elem_of at 1. set_solver. Qed.
+  Lemma fin_set_to_coGset_finite (X : C) :
+    set_finite (fin_set_to_coGset (A:=A) X).
+  Proof. by rewrite coGset_finite_spec. Qed.
+End to_fin_set.
+
+(** * Conversion to coPset *)
+Definition coGset_to_coPset (X : coGset positive) : coPset :=
+  match X with
+  | FinGSet X => gset_to_coPset X
+  | CoFinGset X => ⊤ ∖ gset_to_coPset X
+  end.
+Lemma elem_of_coGset_to_coPset X x : x ∈ coGset_to_coPset X ↔ x ∈ X.
+Proof.
+  destruct X as [X|X]; simpl.
+  by rewrite elem_of_gset_to_coPset.
+  by rewrite elem_of_difference, elem_of_gset_to_coPset, (left_id True (∧)).
+Qed.
+
+(** * Inefficient conversion to sets with a top element *)
+Definition coGset_to_set `{Countable A, Empty C, Singleton A C, Union C,
+    Top C, Difference C} (X : coGset A) : C :=
+  match X with
+  | FinGSet X => list_to_set (elements X)
+  | CoFinGset X => ⊤ ∖ list_to_set (elements X)
+  end.
+Lemma elem_of_coGset_to_set `{Countable A, Set_ A C, Top C} X x :
+  (∀ X : C, X ⊆ ⊤) → x ∈@{C} coGset_to_set X ↔ x ∈ X.
+Proof.
+  intros Htop. destruct X as [X|X]; simpl.
+  - set_solver.
+  - rewrite elem_of_difference, elem_of_subseteq_singleton,
+      elem_of_list_to_set, elem_of_elements. clear -Htop. naive_solver.
+Qed.
+
+(** * Domain of finite maps *)
+Instance coGset_dom `{Countable K} {A} : Dom (gmap K A) (coGset K) := λ m,
+  gset_to_coGset (dom _ m).
+Instance coGset_dom_spec `{Countable K} : FinMapDom K (gmap K) (coGset K).
+Proof.
+  split; try apply _. intros B m i. unfold dom, coGset_dom.
+  by rewrite elem_of_gset_to_coGset, elem_of_dom.
+Qed.
+
+Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
+Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
+Typeclasses Opaque coGset_dom.