Commit 603f0048 authored by Robbert Krebbers's avatar Robbert Krebbers

Hint Resolve for X ⊆ ⊤.

parent 10e16fe0
Pipeline #181 passed with stage
......@@ -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 :=
......
......@@ -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
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment