diff --git a/prelude/co_pset.v b/prelude/co_pset.v index 315bc6a9f892a3230ac0cc58aa41cbb701bbaf46..d2feb82036b2725d6b639076fe55b49a27212d10 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 9198692cc834a3465cca555a936d5793140ed0bd..dbb25e14ac0a6e646458bf255ddba6a1e7bbcdc9 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