Commit 1804da3f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Simplify collection spaghetti.

There was not really a need for the lattice type classes, so I removed
these.
parent d1fa8150
......@@ -250,6 +250,12 @@ Lemma and_wlog_r (P Q : Prop) : P → (P → Q) → (P ∧ Q).
Proof. tauto. Qed.
Lemma impl_transitive (P Q R : Prop) : (P Q) (Q R) (P R).
Proof. tauto. Qed.
Lemma forall_proper {A} (P Q : A Prop) :
( x, P x Q x) ( x, P x) ( x, Q x).
Proof. firstorder. Qed.
Lemma exist_proper {A} (P Q : A Prop) :
( x, P x Q x) ( x, P x) ( x, Q x).
Proof. firstorder. Qed.
Instance: Comm () (@eq A).
Proof. red; intuition. Qed.
......@@ -872,30 +878,7 @@ Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.
(** * Ordered structures *)
(** We do not use a setoid equality in the following interfaces to avoid the
need for proofs that the relations and operations are proper. Instead, we
define setoid equality generically [λ X Y, X ⊆ Y ∧ Y ⊆ X]. *)
Class EmptySpec A `{Empty A, SubsetEq A} : Prop := subseteq_empty X : X.
Class JoinSemiLattice A `{SubsetEq A, Union A} : Prop := {
join_semi_lattice_pre :>> PreOrder ();
union_subseteq_l X Y : X X Y;
union_subseteq_r X Y : Y X Y;
union_least X Y Z : X Z Y Z X Y Z
}.
Class MeetSemiLattice A `{SubsetEq A, Intersection A} : Prop := {
meet_semi_lattice_pre :>> PreOrder ();
intersection_subseteq_l X Y : X Y X;
intersection_subseteq_r X Y : X Y Y;
intersection_greatest X Y Z : Z X Z Y Z X Y
}.
Class Lattice A `{SubsetEq A, Union A, Intersection A} : Prop := {
lattice_join :>> JoinSemiLattice A;
lattice_meet :>> MeetSemiLattice A;
lattice_distr X Y Z : (X Y) (X Z) X (Y Z)
}.
(** ** Axiomatization of collections *)
(** * Axiomatization of collections *)
(** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
elements of type [A]. *)
Class SimpleCollection A C `{ElemOf A C,
......
......@@ -5,125 +5,90 @@ importantly, it implements some tactics to automatically solve goals involving
collections. *)
From stdpp Require Export base tactics orders.
Instance collection_disjoint `{ElemOf A C} : Disjoint C := λ X Y,
x, x X x Y False.
Instance collection_equiv `{ElemOf A C} : Equiv C := λ X Y,
x, x X x Y.
Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y,
x, x X x Y.
Typeclasses Opaque collection_disjoint collection_subseteq.
Instance collection_disjoint `{ElemOf A C} : Disjoint C := λ X Y,
x, x X x Y False.
Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
(** * Basic theorems *)
Section simple_collection.
(** * Setoids *)
Section setoids_simple.
Context `{SimpleCollection A C}.
Implicit Types x y : A.
Implicit Types X Y : C.
Lemma elem_of_empty x : x False.
Proof. split. apply not_elem_of_empty. done. Qed.
Lemma elem_of_union_l x X Y : x X x X Y.
Proof. intros. apply elem_of_union. auto. Qed.
Lemma elem_of_union_r x X Y : x Y x X Y.
Proof. intros. apply elem_of_union. auto. Qed.
Global Instance: EmptySpec C.
Proof. firstorder auto. Qed.
Global Instance: JoinSemiLattice C.
Proof. firstorder auto. Qed.
Global Instance: AntiSymm () (@collection_subseteq A C _).
Proof. done. Qed.
Lemma elem_of_subseteq X Y : X Y x, x X x Y.
Proof. done. Qed.
Lemma elem_of_equiv X Y : X Y x, x X x Y.
Proof. firstorder. Qed.
Lemma elem_of_equiv_alt X Y :
X Y ( x, x X x Y) ( x, x Y x X).
Proof. firstorder. Qed.
Lemma elem_of_equiv_empty X : X x, x X.
Proof. firstorder. Qed.
Lemma elem_of_disjoint X Y : X Y x, x X x Y False.
Proof. done. Qed.
Global Instance disjoint_sym : Symmetric (@disjoint C _).
Proof. intros ??. rewrite !elem_of_disjoint; naive_solver. Qed.
Lemma disjoint_empty_l Y : Y.
Proof. rewrite elem_of_disjoint; intros x; by rewrite elem_of_empty. Qed.
Lemma disjoint_empty_r X : X .
Proof. rewrite (symmetry_iff _); apply disjoint_empty_l. Qed.
Lemma disjoint_singleton_l x Y : {[ x ]} Y x Y.
Global Instance collection_equivalence: @Equivalence C ().
Proof.
rewrite elem_of_disjoint; setoid_rewrite elem_of_singleton; naive_solver.
split.
- done.
- intros X Y ? x. by symmetry.
- intros X Y Z ?? x; by trans (x Y).
Qed.
Lemma disjoint_singleton_r y X : X {[ y ]} y X.
Proof. rewrite (symmetry_iff ()). apply disjoint_singleton_l. Qed.
Lemma disjoint_union_l X1 X2 Y : X1 X2 Y X1 Y X2 Y.
Global Instance singleton_proper : Proper ((=) ==> ()) (singleton (B:=C)).
Proof. apply _. Qed.
Global Instance elem_of_proper :
Proper ((=) ==> () ==> iff) (@elem_of A C _) | 5.
Proof. by intros x ? <- X Y. Qed.
Global Instance disjoint_proper: Proper (() ==> () ==> iff) (@disjoint C _).
Proof.
rewrite !elem_of_disjoint; setoid_rewrite elem_of_union; naive_solver.
intros X1 X2 HX Y1 Y2 HY; apply forall_proper; intros x. by rewrite HX, HY.
Qed.
Lemma disjoint_union_r X Y1 Y2 : X Y1 Y2 X Y1 X Y2.
Proof. rewrite !(symmetry_iff () X). apply disjoint_union_l. Qed.
Global Instance union_proper : Proper (() ==> () ==> ()) (@union C _).
Proof. intros X1 X2 HX Y1 Y2 HY x. rewrite !elem_of_union. f_equiv; auto. Qed.
Global Instance union_list_proper: Proper (() ==> ()) (union_list (A:=C)).
Proof. by induction 1; simpl; try apply union_proper. Qed.
Global Instance subseteq_proper : Proper (() ==> () ==> iff) (() : relation C).
Proof.
intros X1 X2 HX Y1 Y2 HY. apply forall_proper; intros x. by rewrite HX, HY.
Qed.
End setoids_simple.
Section setoids.
Context `{Collection A C}.
Lemma collection_positive_l X Y : X Y X .
(** * Setoids *)
Global Instance intersection_proper :
Proper (() ==> () ==> ()) (@intersection C _).
Proof.
rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver.
intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_intersection, HX, HY.
Qed.
Lemma collection_positive_l_alt X Y : X X Y .
Proof. eauto using collection_positive_l. Qed.
Lemma elem_of_singleton_1 x y : x {[y]} x = y.
Proof. by rewrite elem_of_singleton. Qed.
Lemma elem_of_singleton_2 x y : x = y x {[y]}.
Proof. by rewrite elem_of_singleton. Qed.
Lemma elem_of_subseteq_singleton x X : x X {[ x ]} X.
Global Instance difference_proper :
Proper (() ==> () ==> ()) (@difference C _).
Proof.
split.
- intros ??. rewrite elem_of_singleton. by intros ->.
- intros Ex. by apply (Ex x), elem_of_singleton.
intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_difference, HX, HY.
Qed.
End setoids.
Global Instance singleton_proper : Proper ((=) ==> ()) (singleton (B:=C)).
Proof. by repeat intro; subst. Qed.
Global Instance elem_of_proper :
Proper ((=) ==> () ==> iff) (@elem_of A C _) | 5.
Proof. intros ???; subst. firstorder. Qed.
Global Instance disjoint_proper: Proper (() ==> () ==> iff) (@disjoint C _).
Proof. intros ??????. by rewrite !elem_of_disjoint; setoid_subst. Qed.
Lemma elem_of_union_list Xs x : x Xs X, X Xs x X.
Section setoids_monad.
Context `{CollectionMonad M}.
Global Instance collection_fmap_proper {A B} :
Proper (pointwise_relation _ (=) ==> () ==> ()) (@fmap M _ A B).
Proof.
split.
- induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
- intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
intros. apply elem_of_union_r; auto.
intros f1 f2 Hf X1 X2 HX x. rewrite !elem_of_fmap. f_equiv; intros z.
by rewrite HX, Hf.
Qed.
Lemma non_empty_singleton x : ({[ x ]} : C) .
Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
Lemma not_elem_of_singleton x y : x {[ y ]} x y.
Proof. by rewrite elem_of_singleton. Qed.
Lemma not_elem_of_union x X Y : x X Y x X x Y.
Proof. rewrite elem_of_union. tauto. Qed.
Section leibniz.
Context `{!LeibnizEquiv C}.
Lemma elem_of_equiv_L X Y : X = Y x, x X x Y.
Proof. unfold_leibniz. apply elem_of_equiv. Qed.
Lemma elem_of_equiv_alt_L X Y :
X = Y ( x, x X x Y) ( x, x Y x X).
Proof. unfold_leibniz. apply elem_of_equiv_alt. Qed.
Lemma elem_of_equiv_empty_L X : X = x, x X.
Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed.
Lemma collection_positive_l_L X Y : X Y = X = .
Proof. unfold_leibniz. apply collection_positive_l. Qed.
Lemma collection_positive_l_alt_L X Y : X X Y .
Proof. unfold_leibniz. apply collection_positive_l_alt. Qed.
Lemma non_empty_singleton_L x : {[ x ]} .
Proof. unfold_leibniz. apply non_empty_singleton. Qed.
End leibniz.
End simple_collection.
Global Instance collection_bind_proper {A B} :
Proper (((=) ==> ()) ==> () ==> ()) (@mbind M _ A B).
Proof.
intros f1 f2 Hf X1 X2 HX x. rewrite !elem_of_bind. f_equiv; intros z.
by rewrite HX, (Hf z z).
Qed.
Global Instance collection_join_proper {A} :
Proper (() ==> ()) (@mjoin M _ A).
Proof.
intros X1 X2 HX x. rewrite !elem_of_join. f_equiv; intros z. by rewrite HX.
Qed.
End setoids_monad.
(** * Tactics *)
(** The tactic [set_unfold] transforms all occurrences of [(∪)], [(∩)], [(∖)],
[(<$>)], [∅], [{[_]}], [(≡)], and [(⊆)] into logically equivalent propositions
involving just [∈]. For example, [A → x ∈ X ∪ ∅] becomes [A → x ∈ X ∨ False].
This transformation is implemented using type classes instead of [rewrite]ing
to ensure that we traverse each term at most once. *)
This transformation is implemented using type classes instead of setoid
rewriting to ensure that we traverse each term at most once and to be able to
deal with occurences of the set operations under binders. *)
Class SetUnfold (P Q : Prop) := { set_unfold : P Q }.
Arguments set_unfold _ _ {_}.
Hint Mode SetUnfold + - : typeclass_instances.
......@@ -179,7 +144,7 @@ Section set_unfold_simple.
Implicit Types X Y : C.
Global Instance set_unfold_empty x : SetUnfold (x ) False.
Proof. constructor; apply elem_of_empty. Qed.
Proof. constructor. split. apply not_elem_of_empty. done. Qed.
Global Instance set_unfold_singleton x y : SetUnfold (x {[ y ]}) (x = y).
Proof. constructor; apply elem_of_singleton. Qed.
Global Instance set_unfold_union x X Y P Q :
......@@ -193,47 +158,48 @@ Section set_unfold_simple.
Global Instance set_unfold_equiv_empty_l X (P : A Prop) :
( x, SetUnfold (x X) (P x)) SetUnfold ( X) ( x, ¬P x) | 5.
Proof.
intros ?; constructor.
rewrite (symmetry_iff equiv), elem_of_equiv_empty; naive_solver.
intros ?; constructor. unfold equiv, collection_equiv.
pose proof not_elem_of_empty; naive_solver.
Qed.
Global Instance set_unfold_equiv_empty_r (P : A Prop) :
( x, SetUnfold (x X) (P x)) SetUnfold (X ) ( x, ¬P x) | 5.
Proof. constructor. rewrite elem_of_equiv_empty; naive_solver. Qed.
Proof.
intros ?; constructor. unfold equiv, collection_equiv.
pose proof not_elem_of_empty; naive_solver.
Qed.
Global Instance set_unfold_equiv (P Q : A Prop) :
( x, SetUnfold (x X) (P x)) ( x, SetUnfold (x Y) (Q x))
SetUnfold (X Y) ( x, P x Q x) | 10.
Proof. constructor. rewrite elem_of_equiv; naive_solver. Qed.
Proof. constructor. apply forall_proper; naive_solver. Qed.
Global Instance set_unfold_subseteq (P Q : A Prop) :
( x, SetUnfold (x X) (P x)) ( x, SetUnfold (x Y) (Q x))
SetUnfold (X Y) ( x, P x Q x).
Proof. constructor. rewrite elem_of_subseteq; naive_solver. Qed.
Proof. constructor. apply forall_proper; naive_solver. Qed.
Global Instance set_unfold_subset (P Q : A Prop) :
( x, SetUnfold (x X) (P x)) ( x, SetUnfold (x Y) (Q x))
SetUnfold (X Y) (( x, P x Q x) ¬∀ x, P x Q x).
SetUnfold (X Y) (( x, P x Q x) ¬∀ x, Q x P x).
Proof.
constructor. rewrite subset_spec, elem_of_subseteq, elem_of_equiv.
repeat f_equiv; naive_solver.
constructor. unfold strict.
repeat f_equiv; apply forall_proper; naive_solver.
Qed.
Global Instance set_unfold_disjoint (P Q : A Prop) :
( x, SetUnfold (x X) (P x)) ( x, SetUnfold (x Y) (Q x))
SetUnfold (X Y) ( x, P x Q x False).
Proof. constructor. rewrite elem_of_disjoint. naive_solver. Qed.
Proof. constructor. unfold disjoint, collection_disjoint. naive_solver. Qed.
Context `{!LeibnizEquiv C}.
Global Instance set_unfold_equiv_same_L X : SetUnfold (X = X) True | 1.
Proof. done. Qed.
Global Instance set_unfold_equiv_empty_l_L X (P : A Prop) :
( x, SetUnfold (x X) (P x)) SetUnfold ( = X) ( x, ¬P x) | 5.
Proof.
constructor. rewrite (symmetry_iff eq), elem_of_equiv_empty_L; naive_solver.
Qed.
Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_l. Qed.
Global Instance set_unfold_equiv_empty_r_L (P : A Prop) :
( x, SetUnfold (x X) (P x)) SetUnfold (X = ) ( x, ¬P x) | 5.
Proof. constructor. rewrite elem_of_equiv_empty_L; naive_solver. Qed.
Proof. constructor. unfold_leibniz. by apply set_unfold_equiv_empty_r. Qed.
Global Instance set_unfold_equiv_L (P Q : A Prop) :
( x, SetUnfold (x X) (P x)) ( x, SetUnfold (x Y) (Q x))
SetUnfold (X = Y) ( x, P x Q x) | 10.
Proof. constructor. rewrite elem_of_equiv_L; naive_solver. Qed.
Proof. constructor. unfold_leibniz. by apply set_unfold_equiv. Qed.
End set_unfold_simple.
Section set_unfold.
......@@ -244,14 +210,14 @@ Section set_unfold.
Global Instance set_unfold_intersection x X Y P Q :
SetUnfold (x X) P SetUnfold (x Y) Q SetUnfold (x X Y) (P Q).
Proof.
intros ??; constructor. by rewrite elem_of_intersection,
(set_unfold (x X) P), (set_unfold (x Y) Q).
intros ??; constructor. rewrite elem_of_intersection.
by rewrite (set_unfold (x X) P), (set_unfold (x Y) Q).
Qed.
Global Instance set_unfold_difference x X Y P Q :
SetUnfold (x X) P SetUnfold (x Y) Q SetUnfold (x X Y) (P ¬Q).
Proof.
intros ??; constructor. by rewrite elem_of_difference,
(set_unfold (x X) P), (set_unfold (x Y) Q).
intros ??; constructor. rewrite elem_of_difference.
by rewrite (set_unfold (x X) P), (set_unfold (x Y) Q).
Qed.
End set_unfold.
......@@ -283,9 +249,8 @@ Ltac set_unfold :=
end in
apply set_unfold_2; unfold_hyps; csimpl in *.
(** Since [firstorder] fails or loops on very small goals generated by
[set_solver] already. We use the [naive_solver] tactic as a substitute.
This tactic either fails or proves the goal. *)
(** Since [firstorder] already fails or loops on very small goals generated by
[set_solver], we use the [naive_solver] tactic as a substitute. *)
Tactic Notation "set_solver" "by" tactic3(tac) :=
try fast_done;
intros; setoid_subst;
......@@ -305,98 +270,295 @@ Hint Extern 1000 (_ ∉ _) => set_solver : set_solver.
Hint Extern 1000 (_ _) => set_solver : set_solver.
Hint Extern 1000 (_ _) => set_solver : set_solver.
(** * Conversion of option and list *)
Definition of_option `{Singleton A C, Empty C} (mx : option A) : C :=
match mx with None => | Some x => {[ x ]} end.
Fixpoint of_list `{Singleton A C, Empty C, Union C} (l : list A) : C :=
match l with [] => | x :: l => {[ x ]} of_list l end.
Section of_option_list.
(** * Collections with [∪], [∅] and [{[_]}] *)
Section simple_collection.
Context `{SimpleCollection A C}.
Lemma elem_of_of_option (x : A) mx: x of_option mx mx = Some x.
Proof. destruct mx; set_solver. Qed.
Lemma elem_of_of_list (x : A) l : x of_list l x l.
Implicit Types x y : A.
Implicit Types X Y : C.
Implicit Types Xs Ys : list C.
(** Equality *)
Lemma elem_of_equiv X Y : X Y x, x X x Y.
Proof. set_solver. Qed.
Lemma collection_equiv_spec X Y : X Y X Y Y X.
Proof. set_solver. Qed.
(** Subset relation *)
Global Instance collection_subseteq_antisymm: AntiSymm () (() : relation C).
Proof. intros ??. set_solver. Qed.
Global Instance collection_subseteq_preorder: PreOrder (() : relation C).
Proof. split. by intros ??. intros ???; set_solver. Qed.
Lemma subseteq_union X Y : X Y X Y Y.
Proof. set_solver. Qed.
Lemma subseteq_union_1 X Y : X Y X Y Y.
Proof. by rewrite subseteq_union. Qed.
Lemma subseteq_union_2 X Y : X Y Y X Y.
Proof. by rewrite subseteq_union. Qed.
Lemma union_subseteq_l X Y : X X Y.
Proof. set_solver. Qed.
Lemma union_subseteq_r X Y : Y X Y.
Proof. set_solver. Qed.
Lemma union_least X Y Z : X Z Y Z X Y Z.
Proof. set_solver. Qed.
Lemma elem_of_subseteq X Y : X Y x, x X x Y.
Proof. done. Qed.
Lemma elem_of_subset X Y : X Y ( x, x X x Y) ¬( x, x Y x X).
Proof. set_solver. Qed.
(** Union *)
Lemma not_elem_of_union x X Y : x X Y x X x Y.
Proof. set_solver. Qed.
Lemma elem_of_union_l x X Y : x X x X Y.
Proof. set_solver. Qed.
Lemma elem_of_union_r x X Y : x Y x X Y.
Proof. set_solver. Qed.
Lemma union_preserving_l X Y1 Y2 : Y1 Y2 X Y1 X Y2.
Proof. set_solver. Qed.
Lemma union_preserving_r X1 X2 Y : X1 X2 X1 Y X2 Y.
Proof. set_solver. Qed.
Lemma union_preserving X1 X2 Y1 Y2 : X1 X2 Y1 Y2 X1 Y1 X2 Y2.
Proof. set_solver. Qed.
Global Instance union_idemp : IdemP (() : relation C) ().
Proof. intros X. set_solver. Qed.
Global Instance union_empty_l : LeftId (() : relation C) ().
Proof. intros X. set_solver. Qed.
Global Instance union_empty_r : RightId (() : relation C) ().
Proof. intros X. set_solver. Qed.
Global Instance union_comm : Comm (() : relation C) ().
Proof. intros X Y. set_solver. Qed.
Global Instance union_assoc : Assoc (() : relation C) ().
Proof. intros X Y Z. set_solver. Qed.
Lemma empty_union X Y : X Y X Y .
Proof. set_solver. Qed.
(** Empty *)
Lemma elem_of_equiv_empty X : X x, x X.
Proof. set_solver. Qed.
Lemma elem_of_empty x : x False.
Proof. set_solver. Qed.
Lemma equiv_empty X : X X .
Proof. set_solver. Qed.
Lemma union_positive_l X Y : X Y X .
Proof. set_solver. Qed.
Lemma union_positive_l_alt X Y : X X Y .
Proof. set_solver. Qed.
Lemma non_empty_inhabited x X : x X X .
Proof. set_solver. Qed.
(** Singleton *)
Lemma elem_of_singleton_1 x y : x {[y]} x = y.
Proof. by rewrite elem_of_singleton. Qed.
Lemma elem_of_singleton_2 x y : x = y x {[y]}.
Proof. by rewrite elem_of_singleton. Qed.
Lemma elem_of_subseteq_singleton x X : x X {[ x ]} X.
Proof. set_solver. Qed.
Lemma non_empty_singleton x : ({[ x ]} : C) .
Proof. set_solver. Qed.
Lemma not_elem_of_singleton x y : x {[ y ]} x y.
Proof. by rewrite elem_of_singleton. Qed.
(** Disjointness *)
Lemma elem_of_disjoint X Y : X Y x, x X x Y False.
Proof. done. Qed.
Global Instance disjoint_sym : Symmetric (@disjoint C _).
Proof. intros X Y. set_solver. Qed.
Lemma disjoint_empty_l Y : Y.
Proof. set_solver. Qed.
Lemma disjoint_empty_r X : X .
Proof. set_solver. Qed.
Lemma disjoint_singleton_l x Y : {[ x ]} Y x Y.
Proof. set_solver. Qed.
Lemma disjoint_singleton_r y X : X {[ y ]} y X.
Proof. set_solver. Qed.
Lemma disjoint_union_l X1 X2 Y : X1 X2 Y X1 Y X2 Y.
Proof. set_solver. Qed.
Lemma disjoint_union_r X Y1 Y2 : X Y1 Y2 X Y1 X Y2.
Proof. set_solver. Qed.
(** Big unions *)
Lemma elem_of_union_list Xs x : x Xs X, X Xs x X.
Proof.
split.
- induction l; simpl; [by rewrite elem_of_empty|].
rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
- induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
- induction Xs; simpl; intros HXs; [by apply elem_of_empty in HXs|].
setoid_rewrite elem_of_cons. apply elem_of_union in HXs. naive_solver.
- intros [X []]. induction 1; simpl; [by apply elem_of_union_l |].
intros. apply elem_of_union_r; auto.
Qed.
Global Instance set_unfold_of_option (mx : option A) x :
SetUnfold (x of_option mx) (mx = Some x).
Proof. constructor; apply elem_of_of_option. Qed.
Global Instance set_unfold_of_list (l : list A) x P :
SetUnfold (x l) P SetUnfold (x of_list l) P.
Proof. constructor. by rewrite elem_of_of_list, (set_unfold (x l) P). Qed.
End of_option_list.
Section list_unfold.
Context {A : Type}.
Implicit Types x : A.
Implicit Types l : list A.
Global Instance set_unfold_nil x : SetUnfold (x []) False.
Proof. constructor; apply elem_of_nil. Qed.
Global Instance set_unfold_cons x y l P :
SetUnfold (x l) P SetUnfold (x y :: l) (x = y P).
Proof. constructor. by rewrite elem_of_cons, (set_unfold (x l) P). Qed.
Global Instance set_unfold_app x l k P Q :
SetUnfold (x l) P SetUnfold (x k) Q SetUnfold (x l ++ k) (P Q).
Lemma union_list_nil : @nil C = .
Proof. done. Qed.
Lemma union_list_cons X Xs : (X :: Xs) = X Xs.
Proof. done. Qed.
Lemma union_list_singleton X : [X] X.
Proof. simpl. by rewrite (right_id _). Qed.
Lemma union_list_app Xs1 Xs2 : (Xs1 ++ Xs2) Xs1 Xs2.
Proof.
intros ??; constructor.
by rewrite elem_of_app, (set_unfold (x l) P), (set_unfold (x k) Q).
induction Xs1 as [|X Xs1 IH]; simpl; [by rewrite (left_id _)|].
by rewrite IH, (assoc _).
Qed.
Global Instance set_unfold_included l k (P Q : A Prop) :
( x, SetUnfold (x l) (P x)) ( x, SetUnfold (x k) (Q x))
SetUnfold (l `included` k) ( x, P x Q x).
Proof. by constructor; unfold included; set_unfold. Qed.
End list_unfold.
(** * Guard *)
Global Instance collection_guard `{CollectionMonad M} : MGuard M :=
λ P dec A x, match dec with left H => x H | _ => end.
Section collection_monad_base.
Context `{CollectionMonad M}.