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}).
+Proof.
+  intros x [X|X].
+  - abstract (by refine (cast_if (decide (x ∈ X)))).
+  - abstract (by refine (cast_if (decide (x ∉ X)))).
+Defined.
+
+(** * 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.
+
+(* TODO: Resolve the oddity: [set_solver] handles the following goal
+for [coPset] but not [cogset positive]. Both [set_solver by auto] and
+plain [set_solver] with the following instance "work", but it seems
+odd that they're necessary. *)
+(* FTR, teaching [set_solver] to unfold top doesn't help. *)
+Instance set_unfold_cogset_top `{Countable A} (x : A) :
+  SetUnfoldElemOf x (⊤ : cogset A) True.
+Proof. done. Qed.
+(*
+Lemma test1 : dom coPset (∅ : gmap positive unit) ## ⊤.
+Proof. set_solver. Qed.
+Lemma test2 : dom (cogset positive) (∅ : gmap positive unit) ## ⊤.
+Proof. Fail set_solver. set_solver by auto. Qed.
+Instance set_unfold_elem_of_cogset_empty `{Countable K} (x : K) {A} :
+  SetUnfoldElemOf x (dom (cogset K) (∅ : gmap K A)) False.
+Proof. done. Qed.
+Lemma test3 : dom (cogset positive) (∅ : gmap positive unit) ## ⊤.
+Proof. set_solver. Qed.
+*)
+(* A related goal that appears to need the [SetUnfoldElemOf] instance. *)
+(*
+Lemma test4 X : dom coPset (∅ : gmap positive unit) ## X.
+Proof. set_solver. Qed.
+Lemma test5 X : dom (cogset positive) (∅ : gmap positive unit) ## X.
+Proof. Fail set_solver by auto. Abort.
+*)