Commit d7766e5d authored by Robbert Krebbers's avatar Robbert Krebbers

Some properties about set disjointness.

parent e4c30558
...@@ -41,6 +41,25 @@ Section simple_collection. ...@@ -41,6 +41,25 @@ Section simple_collection.
Lemma elem_of_disjoint X Y : X Y x, x X x Y False. Lemma elem_of_disjoint X Y : X Y x, x X x Y False.
Proof. done. Qed. 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.
rewrite elem_of_disjoint; setoid_rewrite elem_of_singleton; naive_solver.
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.
rewrite !elem_of_disjoint; setoid_rewrite elem_of_union; naive_solver.
Lemma disjoint_union_r X Y1 Y2 : X Y1 Y2 X Y1 X Y2.
Proof. rewrite !(symmetry_iff () X). apply disjoint_union_l. Qed.
Lemma collection_positive_l X Y : X Y X . Lemma collection_positive_l X Y : X Y X .
Proof. Proof.
rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver. rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment