Add class `TopSet` for sets with ⊤ element.

This closes issue #49.

theories/base.v

@@ -1202,16 +1202,18 @@ Notation "⊥" := bottom (format "⊥") : stdpp_scope.
 
 
 (** * Axiomatization of sets *)
-(** The classes [SemiSet A C] and [Set_ A C] axiomatize sset of type [C] with
-elements of type [A]. The first class, [SemiSet] does not include intersection
-and difference. It is useful for the case of lists, where decidable equality
-is needed to implement intersection and difference, but not union.
+(** The classes [SemiSet A C], [Set_ A C], and [TopSet A C] axiomatize sets of
+type [C] with elements of type [A]. The first class, [SemiSet] does not include
+intersection and difference. It is useful for the case of lists, where decidable
+equality is needed to implement intersection and difference, but not union.
 
 Note that we cannot use the name [Set] since that is a reserved keyword. Hence
 we use [Set_]. *)
 Class SemiSet A C `{ElemOf A C,
     Empty C, Singleton A C, Union C} : Prop := {
-  not_elem_of_empty (x : A) : x ∉@{C} ∅;
+  not_elem_of_empty (x : A) : x ∉@{C} ∅; (* We prove
+  [elem_of_empty : x ∈@{C} ∅ ↔ False] in [sets.v], which is more convenient for
+  rewriting. *)
   elem_of_singleton (x y : A) : x ∈@{C} {[ y ]} ↔ x = y;
   elem_of_union (X Y : C) (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
 }.
@@ -1221,6 +1223,12 @@ Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
   elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
   elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
+Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
+    Union C, Intersection C, Difference C} : Prop := {
+  top_set_set :> Set_ A C;
+  elem_of_top' (x : A) : x ∈@{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
+  in [sets.v], which is more convenient for rewriting. *)
+}.
 
 (** We axiomative a finite set as a set whose elements can be
 enumerated as a list. These elements, given by the [elements] function, may be

theories/coPset.v

@@ -169,9 +169,9 @@ Instance coPset_difference : Difference coPset := λ X Y,
   let (t1,Ht1) := X in let (t2,Ht2) := Y in
   (t1 ∩ coPset_opp_raw t2) ↾ coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
 
-Instance coPset_set : Set_ positive coPset.
+Instance coPset_top_set : TopSet positive coPset.
 Proof.
-  split; [split| |].
+  split; [split; [split| |]|].
   - by intros ??.
   - intros p q. apply coPset_elem_of_singleton.
   - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_union; simpl.
@@ -181,6 +181,7 @@ Proof.
   - intros [t] [t'] p; unfold elem_of, coPset_elem_of, coPset_difference; simpl.
     by rewrite coPset_elem_of_intersection,
       coPset_elem_of_opp, andb_True, negb_True.
+  - done.
 Qed.
 
 Instance coPset_leibniz : LeibnizEquiv coPset.
@@ -204,11 +205,6 @@ Proof.
  refine (λ X Y, cast_if (decide (X ∪ Y = Y))); abstract (by rewrite subseteq_union_L).
 Defined.
 
-(** * Top *)
-Lemma coPset_top_subseteq (X : coPset) : X ⊆ ⊤.
-Proof. done. Qed.
-Hint Resolve coPset_top_subseteq : core.
-
 (** * Finite sets *)
 Fixpoint coPset_finite (t : coPset_raw) : bool :=
   match t with

theories/namespaces.v

@@ -80,6 +80,7 @@ Create HintDb ndisj.
 considering they are. *)
 Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
+Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : ndisj.
 Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress. *)
 Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.

theories/propset.v

@@ -21,18 +21,13 @@ Instance propset_intersection {A} : Intersection (propset A) := λ X1 X2,
   {[ x | x ∈ X1 ∧ x ∈ X2 ]}.
 Instance propset_difference {A} : Difference (propset A) := λ X1 X2,
   {[ x | x ∈ X1 ∧ x ∉ X2 ]}.
-Instance propset_set : Set_ A (propset A).
-Proof. split; [split | |]; by repeat intro. Qed.
+Instance propset_top_set {A} : TopSet A (propset A).
+Proof. split; [split; [split| |]|]; by repeat intro. Qed.
 
-Lemma elem_of_top {A} (x : A) : x ∈ (⊤ : propset A) ↔ True.
-Proof. done. Qed.
 Lemma elem_of_PropSet {A} (P : A → Prop) x : x ∈ {[ x | P x ]} ↔ P x.
 Proof. done. Qed.
 Lemma not_elem_of_PropSet {A} (P : A → Prop) x : x ∉ {[ x | P x ]} ↔ ¬P x.
 Proof. done. Qed.
-Lemma top_subseteq {A} (X : propset A) : X ⊆ ⊤.
-Proof. done. Qed.
-Hint Resolve top_subseteq : core.
 
 Definition set_to_propset `{ElemOf A C} (X : C) : propset A :=
   {[ x | x ∈ X ]}.
@@ -50,8 +45,6 @@ Instance propset_join : MJoin propset := λ A (XX : propset (propset A)),
 Instance propset_monad_set : MonadSet propset.
 Proof. by split; try apply _. Qed.
 
-Instance set_unfold_propset_top {A} (x : A) : SetUnfoldElemOf x (⊤ : propset A) True.
-Proof. by constructor. Qed.
 Instance set_unfold_PropSet {A} (P : A → Prop) x Q :
   SetUnfoldSimpl (P x) Q → SetUnfoldElemOf x (PropSet P) Q.
 Proof. intros HPQ. constructor. apply HPQ. Qed.

theories/sets.v

@@ -242,6 +242,10 @@ Section set_unfold.
   Qed.
 End set_unfold.
 
+Instance set_unfold_top `{TopSet A C} (x : A) :
+  SetUnfoldElemOf x (⊤ : C) True.
+Proof. constructor. split; [done|intros; apply elem_of_top']. Qed.
+
 Section set_unfold_monad.
   Context `{MonadSet M}.
 
@@ -793,6 +797,19 @@ Section set.
 End set.
 
 
+(** * Sets with [∪], [∩], [∖], [∅], [{[_]}], and [⊤] *)
+Section top_set.
+  Context `{TopSet A C}.
+  Implicit Types x y : A.
+  Implicit Types X Y : C.
+
+  Lemma elem_of_top x : x ∈@{C} ⊤ ↔ True.
+  Proof. split; [done|intros; apply elem_of_top']. Qed.
+  Lemma top_subseteq X : X ⊆ ⊤.
+  Proof. intros x. by rewrite elem_of_top. Qed.
+End top_set.
+
+
 (** * Conversion of option and list *)
 Section option_and_list_to_set.
   Context `{SemiSet A C}.