From 603f0048b2b85d6d01d17c7771a0e52bc2a2ac8a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 27 Feb 2016 01:45:27 +0100
Subject: [PATCH] =?UTF-8?q?Hint=20Resolve=20for=20X=20=E2=8A=86=20?=
 =?UTF-8?q?=E2=8A=A4.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 prelude/co_pset.v | 3 +++
 prelude/sets.v    | 9 ++++++---
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/prelude/co_pset.v b/prelude/co_pset.v
index 315bc6a9f..d2feb8203 100644
--- a/prelude/co_pset.v
+++ b/prelude/co_pset.v
@@ -179,6 +179,9 @@ Proof.
   apply (sig_eq_pi _), coPset_eq; try apply proj2_sig.
   intros p; apply eq_bool_prop_intro, (HXY p).
 Qed.
+Lemma coPset_top_subseteq (X : coPset) : X ⊆ ⊤.
+Proof. done. Qed.
+Hint Resolve coPset_top_subseteq.
 
 (** * Finite sets *)
 Fixpoint coPset_finite (t : coPset_raw) : bool :=
diff --git a/prelude/sets.v b/prelude/sets.v
index 9198692cc..dbb25e14a 100644
--- a/prelude/sets.v
+++ b/prelude/sets.v
@@ -12,7 +12,7 @@ Notation "{[ x | P ]}" := (mkSet (λ x, P))
 
 Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.
 
-Instance set_all {A} : Top (set A) := {[ _ | True ]}.
+Instance set_top {A} : Top (set A) := {[ _ | True ]}.
 Instance set_empty {A} : Empty (set A) := {[ _ | False ]}.
 Instance set_singleton {A} : Singleton A (set A) := λ y, {[ x | y = x ]}.
 Instance set_union {A} : Union (set A) := λ X1 X2, {[ x | x ∈ X1 ∨ x ∈ X2 ]}.
@@ -23,12 +23,15 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
 Instance set_collection : Collection A (set A).
 Proof. split; [split | |]; by repeat intro. Qed.
 
-Lemma elem_of_all {A} (x : A) : x ∈ ⊤ ↔ True.
+Lemma elem_of_top {A} (x : A) : x ∈ ⊤ ↔ True.
 Proof. done. Qed.
 Lemma elem_of_mkSet {A} (P : A → Prop) x : x ∈ {[ x | P x ]} ↔ P x.
 Proof. done. Qed.
 Lemma not_elem_of_mkSet {A} (P : A → Prop) x : x ∉ {[ x | P x ]} ↔ ¬P x.
 Proof. done. Qed.
+Lemma top_subseteq {A} (X : set A) : X ⊆ ⊤.
+Proof. done. Qed.
+Hint Resolve top_subseteq.
 
 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
 Instance set_bind : MBind set := λ A B (f : A → set B) (X : set A),
@@ -46,6 +49,6 @@ Instance set_unfold_mkSet {A} (P : A → Prop) x Q :
   SetUnfoldSimpl (P x) Q → SetUnfold (x ∈ mkSet P) Q.
 Proof. intros HPQ. constructor. apply HPQ. Qed.
 
-Global Opaque set_elem_of set_all set_empty set_singleton.
+Global Opaque set_elem_of set_top set_empty set_singleton.
 Global Opaque set_union set_intersection set_difference.
 Global Opaque set_ret set_bind set_fmap set_join.
\ No newline at end of file
-- 
GitLab