Library stdpp.coGset

This file implements the type coGset A of finite/cofinite sets of elements of any countable type A.
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.
From stdpp Require Import options.

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 Xinl X | CoFinGset Xinr X end)
    (λ s, match s with inl XFinGSet X | inr XCoFinGset 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 Xx X | CoFinGset Xx 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 YFinGSet (X Y)
    | CoFinGset X, CoFinGset YCoFinGset (X Y)
    | FinGSet X, CoFinGset YCoFinGset (Y X)
    | CoFinGset X, FinGSet YCoFinGset (X Y)
    end.
  Global Instance coGset_intersection : Intersection (coGset A) := λ X Y,
    match X, Y with
    | FinGSet X, FinGSet YFinGSet (X Y)
    | CoFinGset X, CoFinGset YCoFinGset (X Y)
    | FinGSet X, CoFinGset YFinGSet (X Y)
    | CoFinGset X, FinGSet YFinGSet (Y X)
    end.
  Global Instance coGset_difference : Difference (coGset A) := λ X Y,
    match X, Y with
    | FinGSet X, FinGSet YFinGSet (X Y)
    | CoFinGset X, CoFinGset YFinGSet (Y X)
    | FinGSet X, CoFinGset YFinGSet (X Y)
    | CoFinGset X, FinGSet YCoFinGset (X Y)
    end.

  Global Instance coGset_set : TopSet A (coGset A).
  Proof.
    split; [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.
    - done.
  Qed.
End coGset.

Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A}) :=
  λ x X,
  match X with
  | FinGSet Xdecide_rel elem_of x X
  | CoFinGset Xnot_dec (decide_rel elem_of x X)
  end.

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 _]. (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 XX 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 XX | CoFinGset _ end.
Definition gset_to_coGset `{Countable A} : gset A coGset A := FinGSet.

Section to_gset.
  Context `{Countable A}.

  Lemma elem_of_gset_to_coGset (X : gset A) x : x gset_to_coGset X x X.
  Proof. done. Qed.

  Context `{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 gset_to_coGset_finite (X : gset A) : set_finite (gset_to_coGset X).
  Proof. by rewrite coGset_finite_spec. Qed.
End to_gset.

Conversion to coPset

Definition coGset_to_coPset (X : coGset positive) : coPset :=
  match X with
  | FinGSet Xgset_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 arbitrary sets with a top element

This shows that, when A is countable, coGset A is initial among sets with , , , , {[_]}, and .
Definition coGset_to_top_set `{Countable A, Empty C, Singleton A C, Union C,
    Top C, Difference C} (X : coGset A) : C :=
  match X with
  | FinGSet Xlist_to_set (elements X)
  | CoFinGset X list_to_set (elements X)
  end.
Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
  x ∈@{C} coGset_to_top_set X x X.
Proof. destruct X; set_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.