phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/sets.v *)
Lemma subseteq_union_2_L X Y : X ∪ Y = Y → X ⊆ Y.
Proof. unfold_leibniz. apply subseteq_union_2. Qed.
(* stdpp/sets.v *)
(* Union *)
Instance union_idemp_L : IdemP (=@{C}) (∪).
Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
(* stdpp/sets.v *)
Instance union_empty_l_L : LeftId (=@{C}) ∅ (∪).
Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed.
(* stdpp/sets.v *)
Instance union_empty_r_L : RightId (=@{C}) ∅ (∪).
Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed.
(* stdpp/sets.v *)
Instance union_comm_L : Comm (=@{C}) (∪).
Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
(* stdpp/sets.v *)
Instance union_assoc_L : Assoc (=@{C}) (∪).
Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
(* stdpp/sets.v *)
Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅.
Proof. unfold_leibniz. apply empty_union. Qed.
(* stdpp/sets.v *)
Lemma union_cancel_l_L X Y Z : Z ## X → Z ## Y → Z ∪ X = Z ∪ Y → X = Y.
Proof. unfold_leibniz. apply union_cancel_l. Qed.
(* stdpp/sets.v *)
Lemma union_cancel_r_L X Y Z : X ## Z → Y ## Z → X ∪ Z = Y ∪ Z → X = Y.
Proof. unfold_leibniz. apply union_cancel_r. Qed.
(* stdpp/sets.v *)
(* Empty *)
Lemma elem_of_equiv_empty_L X : X = ∅ ↔ ∀ x, x ∉ X.
Proof. unfold_leibniz. apply elem_of_equiv_empty. Qed.
(* stdpp/sets.v *)
Lemma equiv_empty_L X : X ⊆ ∅ → X = ∅.
Proof. unfold_leibniz. apply equiv_empty. Qed.
(* stdpp/sets.v *)
Lemma union_positive_l_L X Y : X ∪ Y = ∅ → X = ∅.
Proof. unfold_leibniz. apply union_positive_l. Qed.
(* stdpp/sets.v *)
Lemma union_positive_l_alt_L X Y : X ≠ ∅ → X ∪ Y ≠ ∅.
Proof. unfold_leibniz. apply union_positive_l_alt. Qed.
(* stdpp/sets.v *)
Lemma non_empty_inhabited_L x X : x ∈ X → X ≠ ∅.
Proof. unfold_leibniz. apply non_empty_inhabited. Qed.
(* stdpp/sets.v *)
(* Singleton *)
Lemma non_empty_singleton_L x : {[ x ]} ≠@{C} ∅.
Proof. unfold_leibniz. apply non_empty_singleton. Qed.
(* stdpp/sets.v *)
(* Disjointness *)
Lemma disjoint_top_l_L `{!Top C, !TopSet A C} X : ⊤ ## X ↔ X = ∅.
Proof. unfold_leibniz. apply disjoint_top_l. Qed.
(* stdpp/sets.v *)
Lemma disjoint_top_r_L `{!Top C, !TopSet A C} X : X ## ⊤ ↔ X = ∅.
Proof. unfold_leibniz. apply disjoint_top_r. Qed.
(* stdpp/sets.v *)
(* Big unions *)
Lemma union_list_singleton_L X : ⋃ [X] = X.
Proof. unfold_leibniz. apply union_list_singleton. Qed.
(* stdpp/sets.v *)
Lemma union_list_app_L Xs1 Xs2 : ⋃ (Xs1 ++ Xs2) = ⋃ Xs1 ∪ ⋃ Xs2.
Proof. unfold_leibniz. apply union_list_app. Qed.
(* stdpp/sets.v *)
Lemma union_list_reverse_L Xs : ⋃ (reverse Xs) = ⋃ Xs.
Proof. unfold_leibniz. apply union_list_reverse. Qed.
(* stdpp/sets.v *)
Lemma empty_union_list_L Xs : ⋃ Xs = ∅ ↔ Forall (.= ∅) Xs.
Proof. unfold_leibniz. apply empty_union_list. Qed.
(* stdpp/sets.v *)
Instance union_list_permutation_proper_L `{!LeibnizEquiv C} :
      Proper ((≡ₚ) ==> (=)) (union_list (A:=C)).
Proof. apply (foldr_permutation_proper' _); apply _. Qed.
(* stdpp/sets.v *)
Lemma not_elem_of_iff `{!RelDecision (∈@{C})} X Y x :
    (x ∈ X ↔ x ∈ Y) ↔ (x ∉ X ↔ x ∉ Y).
Proof. destruct (decide (x ∈ X)), (decide (x ∈ Y)); tauto. Qed.
(* stdpp/sets.v *)
Lemma set_subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.
Proof. destruct (decide (X ≡ Y)); [by right|left;set_solver]. Qed.
(* stdpp/sets.v *)
Lemma set_not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y.
Proof. destruct (decide (X ≡ Y)); [by right|left;set_solver]. Qed.
(* stdpp/sets.v *)
Lemma non_empty_union X Y : X ∪ Y ≢ ∅ ↔ X ≢ ∅ ∨ Y ≢ ∅.
Proof. destruct (decide (X ≡ ∅)); set_solver. Qed.
(* stdpp/sets.v *)
Lemma non_empty_union_list Xs : ⋃ Xs ≢ ∅ → Exists (.≢ ∅) Xs.
Proof. rewrite empty_union_list. apply (not_Forall_Exists _). Qed.
(* stdpp/sets.v *)
Lemma set_subseteq_inv_L X Y : X ⊆ Y → X ⊂ Y ∨ X = Y.
Proof. unfold_leibniz. apply set_subseteq_inv. Qed.
(* stdpp/sets.v *)
Lemma set_not_subset_inv_L X Y : X ⊄ Y → X ⊈ Y ∨ X = Y.
Proof. unfold_leibniz. apply set_not_subset_inv. Qed.
(* stdpp/sets.v *)
Lemma non_empty_union_L X Y : X ∪ Y ≠ ∅ ↔ X ≠ ∅ ∨ Y ≠ ∅.
Proof. unfold_leibniz. apply non_empty_union. Qed.
(* stdpp/sets.v *)
Lemma non_empty_union_list_L Xs : ⋃ Xs ≠ ∅ → Exists (.≠ ∅) Xs.
Proof. unfold_leibniz. apply non_empty_union_list. Qed.
(* stdpp/sets.v *)
(* Intersection *)
Lemma subseteq_intersection X Y : X ⊆ Y ↔ X ∩ Y ≡ X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma subseteq_intersection_1 X Y : X ⊆ Y → X ∩ Y ≡ X.
Proof. apply subseteq_intersection. Qed.
(* stdpp/sets.v *)
Lemma subseteq_intersection_2 X Y : X ∩ Y ≡ X → X ⊆ Y.
Proof. apply subseteq_intersection. Qed.
(* stdpp/sets.v *)
Lemma intersection_subseteq_l X Y : X ∩ Y ⊆ X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma intersection_subseteq_r X Y : X ∩ Y ⊆ Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma intersection_greatest X Y Z : Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma intersection_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∩ Y1 ⊆ X ∩ Y2.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma intersection_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∩ Y ⊆ X2 ∩ Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma intersection_mono X1 X2 Y1 Y2 :
    X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∩ Y1 ⊆ X2 ∩ Y2.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Instance intersection_idemp : IdemP (≡@{C}) (∩).
Proof. intros X; set_solver. Qed.
(* stdpp/sets.v *)
Instance intersection_comm : Comm (≡@{C}) (∩).
Proof. intros X Y; set_solver. Qed.
(* stdpp/sets.v *)
Instance intersection_assoc : Assoc (≡@{C}) (∩).
Proof. intros X Y Z; set_solver. Qed.
(* stdpp/sets.v *)
Instance intersection_empty_l : LeftAbsorb (≡@{C}) ∅ (∩).
Proof. intros X; set_solver. Qed.
(* stdpp/sets.v *)
Instance intersection_empty_r: RightAbsorb (≡@{C}) ∅ (∩).
Proof. intros X; set_solver. Qed.
(* stdpp/sets.v *)
Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡@{C} {[x]}.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma union_intersection_l X Y Z : X ∪ (Y ∩ Z) ≡ (X ∪ Y) ∩ (X ∪ Z).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma union_intersection_r X Y Z : (X ∩ Y) ∪ Z ≡ (X ∪ Z) ∩ (Y ∪ Z).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma intersection_union_l X Y Z : X ∩ (Y ∪ Z) ≡ (X ∩ Y) ∪ (X ∩ Z).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma intersection_union_r X Y Z : (X ∪ Y) ∩ Z ≡ (X ∩ Z) ∪ (Y ∩ Z).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
(* Difference *)
Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma subseteq_empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_diag X : X ∖ X ≡ ∅.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_empty X : X ∖ ∅ ≡ X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma empty_difference X : ∅ ∖ X ≡ ∅.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_union_distr_l X Y Z : (X ∪ Y) ∖ Z ≡ X ∖ Z ∪ Y ∖ Z.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_union_distr_r X Y Z : Z ∖ (X ∪ Y) ≡ (Z ∖ X) ∩ (Z ∖ Y).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_disjoint X Y : X ## Y → X ∖ Y ≡ X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma subset_difference_elem_of x X : x ∈ X → X ∖ {[ x ]} ⊂ X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_difference_l X Y Z : (X ∖ Y) ∖ Z ≡ X ∖ (Y ∪ Z).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_mono X1 X2 Y1 Y2 :
    X1 ⊆ X2 → Y2 ⊆ Y1 → X1 ∖ Y1 ⊆ X2 ∖ Y2.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_mono_l X Y1 Y2 : Y2 ⊆ Y1 → X ∖ Y1 ⊆ X ∖ Y2.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∖ Y ⊆ X2 ∖ Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma subseteq_difference_r X Y1 Y2 :
    X ## Y2 → X ⊆ Y1 → X ⊆ Y1 ∖ Y2.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma subseteq_difference_l X1 X2 Y : X1 ⊆ Y → X1 ∖ X2 ⊆ Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
(* Disjointness *)
Lemma disjoint_intersection X Y : X ## Y ↔ X ∩ Y ≡ ∅.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma disjoint_difference_l1 X1 X2 Y : Y ⊆ X2 → X1 ∖ X2 ## Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma disjoint_difference_l2 X1 X2 Y : X1 ## Y → X1 ∖ X2 ## Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma disjoint_difference_r1 X Y1 Y2 : X ⊆ Y2 → X ## Y1 ∖ Y2.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma disjoint_difference_r2 X Y1 Y2 : X ## Y1 → X ## Y1 ∖ Y2.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
(* Intersection *)
Lemma subseteq_intersection_L X Y : X ⊆ Y ↔ X ∩ Y = X.
Proof. unfold_leibniz. apply subseteq_intersection. Qed.
(* stdpp/sets.v *)
Lemma subseteq_intersection_1_L X Y : X ⊆ Y → X ∩ Y = X.
Proof. unfold_leibniz. apply subseteq_intersection_1. Qed.
(* stdpp/sets.v *)
Lemma subseteq_intersection_2_L X Y : X ∩ Y = X → X ⊆ Y.
Proof. unfold_leibniz. apply subseteq_intersection_2. Qed.
(* stdpp/sets.v *)
Instance intersection_idemp_L : IdemP (=@{C}) (∩).
Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
(* stdpp/sets.v *)
Instance intersection_comm_L : Comm (=@{C}) (∩).
Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
(* stdpp/sets.v *)
Instance intersection_assoc_L : Assoc (=@{C}) (∩).
Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
(* stdpp/sets.v *)
Instance intersection_empty_l_L: LeftAbsorb (=@{C}) ∅ (∩).
Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed.
(* stdpp/sets.v *)
Instance intersection_empty_r_L: RightAbsorb (=@{C}) ∅ (∩).
Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.
(* stdpp/sets.v *)
Lemma intersection_singletons_L x : {[x]} ∩ {[x]} =@{C} {[x]}.
Proof. unfold_leibniz. apply intersection_singletons. Qed.
(* stdpp/sets.v *)
Lemma union_intersection_l_L X Y Z : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z).
Proof. unfold_leibniz; apply union_intersection_l. Qed.
(* stdpp/sets.v *)
Lemma union_intersection_r_L X Y Z : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z).
Proof. unfold_leibniz; apply union_intersection_r. Qed.
(* stdpp/sets.v *)
Lemma intersection_union_l_L X Y Z : X ∩ (Y ∪ Z) = (X ∩ Y) ∪ (X ∩ Z).
Proof. unfold_leibniz; apply intersection_union_l. Qed.
(* stdpp/sets.v *)
Lemma intersection_union_r_L X Y Z : (X ∪ Y) ∩ Z = (X ∩ Z) ∪ (Y ∩ Z).
Proof. unfold_leibniz; apply intersection_union_r. Qed.
(* stdpp/sets.v *)
(* Difference *)
Lemma difference_twice_L X Y : (X ∖ Y) ∖ Y = X ∖ Y.
Proof. unfold_leibniz. apply difference_twice. Qed.
(* stdpp/sets.v *)
Lemma subseteq_empty_difference_L X Y : X ⊆ Y → X ∖ Y = ∅.
Proof. unfold_leibniz. apply subseteq_empty_difference. Qed.
(* stdpp/sets.v *)
Lemma difference_diag_L X : X ∖ X = ∅.
Proof. unfold_leibniz. apply difference_diag. Qed.
(* stdpp/sets.v *)
Lemma difference_empty_L X : X ∖ ∅ = X.
Proof. unfold_leibniz. apply difference_empty. Qed.
(* stdpp/sets.v *)
Lemma empty_difference_L X : ∅ ∖ X = ∅.
Proof. unfold_leibniz. apply empty_difference. Qed.
(* stdpp/sets.v *)
Lemma difference_union_distr_l_L X Y Z : (X ∪ Y) ∖ Z = X ∖ Z ∪ Y ∖ Z.
Proof. unfold_leibniz. apply difference_union_distr_l. Qed.
(* stdpp/sets.v *)
Lemma difference_union_distr_r_L X Y Z : Z ∖ (X ∪ Y) = (Z ∖ X) ∩ (Z ∖ Y).
Proof. unfold_leibniz. apply difference_union_distr_r. Qed.
(* stdpp/sets.v *)
Lemma difference_intersection_distr_l_L X Y Z :
      (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z.
Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
(* stdpp/sets.v *)
Lemma difference_disjoint_L X Y : X ## Y → X ∖ Y = X.
Proof. unfold_leibniz. apply difference_disjoint. Qed.
(* stdpp/sets.v *)
Lemma difference_difference_l_L X Y Z : (X ∖ Y) ∖ Z = X ∖ (Y ∪ Z).
Proof. unfold_leibniz. apply difference_difference_l. Qed.
(* stdpp/sets.v *)
(* Disjointness *)
Lemma disjoint_intersection_L X Y : X ## Y ↔ X ∩ Y = ∅.
Proof. unfold_leibniz. apply disjoint_intersection. Qed.
(* stdpp/sets.v *)
Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
Proof. rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto. Qed.
(* stdpp/sets.v *)
Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
Proof. rewrite elem_of_difference. destruct (decide (x ∈ Y)); tauto. Qed.
(* stdpp/sets.v *)
Lemma union_difference X Y : X ⊆ Y → Y ≡ X ∪ Y ∖ X.
Proof.
      intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition].
      destruct (decide (x ∈ X)); intuition.
    Qed.
(* stdpp/sets.v *)
Lemma union_difference_singleton x Y : x ∈ Y → Y ≡ {[x]} ∪ Y ∖ {[x]}.
Proof. intros ?. apply union_difference. set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_union X Y : X ∖ Y ∪ Y ≡ X ∪ Y.
Proof.
      intros x. rewrite !elem_of_union; rewrite elem_of_difference.
      split; [ | destruct (decide (x ∈ Y)) ]; intuition.
    Qed.
(* stdpp/sets.v *)
Lemma difference_difference_r X Y Z : X ∖ (Y ∖ Z) ≡ (X ∖ Y) ∪ (X ∩ Z).
Proof. intros x. destruct (decide (x ∈ Z)); set_solver. Qed.
(* stdpp/sets.v *)
Lemma difference_union_intersection X Y : (X ∖ Y) ∪ (X ∩ Y) ≡ X.
Proof. rewrite union_intersection_l, difference_union. set_solver. Qed.
(* stdpp/sets.v *)
Lemma subseteq_difference_inj_l X1 X2 X3 :
      X3 ⊆ X1 → X3 ⊆ X2 → X1 ∖ X3 ≡ X2 ∖ X3 → X1 ≡ X2.
Proof. split; set_solver. (* TODO prove without split, see !696. *) Qed.
(* stdpp/sets.v *)
Lemma subseteq_difference_inj_r X1 X2 X3 :
      X3 ⊆ X1 → X2 ⊆ X1 → X1 ∖ X2 ≡ X1 ∖ X3 → X2 ≡ X3.
Proof. split; set_solver. (* TODO prove without split, see !696. *) Qed.
(* stdpp/sets.v *)
Lemma subseteq_disjoint_union X Y : X ⊆ Y ↔ ∃ Z, Y ≡ X ∪ Z ∧ X ## Z.
Proof.
      split; [|set_solver].
      exists (Y ∖ X); split; [auto using union_difference|set_solver].
    Qed.
(* stdpp/sets.v *)
Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅.
Proof. intros [HXY1 HXY2] Hdiff. destruct HXY2. set_solver. Qed.
(* stdpp/sets.v *)
Lemma empty_difference_subseteq X Y : X ∖ Y ≡ ∅ → X ⊆ Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma singleton_union_difference X Y x :
      {[x]} ∪ (X ∖ Y) ≡ ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
Proof. intro y; destruct (decide (y ∈@{C} {[x]})); set_solver. Qed.
(* stdpp/sets.v *)
Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
Proof. unfold_leibniz. apply union_difference. Qed.
(* stdpp/sets.v *)
Lemma union_difference_singleton_L x Y : x ∈ Y → Y = {[x]} ∪ Y ∖ {[x]}.
Proof. unfold_leibniz. apply union_difference_singleton. Qed.
(* stdpp/sets.v *)
Lemma difference_union_L X Y : X ∖ Y ∪ Y = X ∪ Y.
Proof. unfold_leibniz. apply difference_union. Qed.
(* stdpp/sets.v *)
Lemma non_empty_difference_L X Y : X ⊂ Y → Y ∖ X ≠ ∅.
Proof. unfold_leibniz. apply non_empty_difference. Qed.
(* stdpp/sets.v *)
Lemma empty_difference_subseteq_L X Y : X ∖ Y = ∅ → X ⊆ Y.
Proof. unfold_leibniz. apply empty_difference_subseteq. Qed.
(* stdpp/sets.v *)
Lemma subseteq_disjoint_union_L X Y : X ⊆ Y ↔ ∃ Z, Y = X ∪ Z ∧ X ## Z.
Proof. unfold_leibniz. apply subseteq_disjoint_union. Qed.
(* stdpp/sets.v *)
Lemma singleton_union_difference_L X Y x :
      {[x]} ∪ (X ∖ Y) = ({[x]} ∪ X) ∖ (Y ∖ {[x]}).
Proof. unfold_leibniz. apply singleton_union_difference. Qed.
(* stdpp/sets.v *)
Lemma difference_difference_r_L X Y Z : X ∖ (Y ∖ Z) = (X ∖ Y) ∪ (X ∩ Z).
Proof. unfold_leibniz. apply difference_difference_r. Qed.
(* stdpp/sets.v *)
Lemma difference_union_intersection_L X Y : (X ∖ Y) ∪ (X ∩ Y) = X.
Proof. unfold_leibniz. apply difference_union_intersection. Qed.
(* stdpp/sets.v *)
Lemma subseteq_difference_inj_l_L X1 X2 X3 :
      X3 ⊆ X1 → X3 ⊆ X2 → X1 ∖ X3 = X2 ∖ X3 → X1 = X2.
Proof. unfold_leibniz. apply subseteq_difference_inj_l. Qed.
(* stdpp/sets.v *)
Lemma subseteq_difference_inj_r_L X1 X2 X3 :
      X3 ⊆ X1 → X2 ⊆ X1 → X1 ∖ X2 = X1 ∖ X3 → X2 = X3.
Proof. unfold_leibniz. apply subseteq_difference_inj_r. Qed.
(* stdpp/sets.v *)
Lemma elem_of_top x : x ∈@{C} ⊤ ↔ True.
Proof. split; [done|intros; apply elem_of_top']. Qed.
(* stdpp/sets.v *)
Lemma top_subseteq X : X ⊆ ⊤.
Proof. intros x. by rewrite elem_of_top. Qed.
(* stdpp/sets.v *)
Lemma elem_of_option_to_set (x : A) mx: x ∈ option_to_set (C:=C) mx ↔ mx = Some x.
Proof. destruct mx; set_solver. Qed.
(* stdpp/sets.v *)
Lemma not_elem_of_option_to_set (x : A) mx: x ∉ option_to_set (C:=C) mx ↔ mx ≠ Some x.
Proof. by rewrite elem_of_option_to_set. Qed.
(* stdpp/sets.v *)
Lemma elem_of_list_to_set (x : A) l : x ∈ list_to_set (C:=C) l ↔ x ∈ l.
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.
  Qed.
(* stdpp/sets.v *)
Lemma not_elem_of_list_to_set (x : A) l : x ∉ list_to_set (C:=C) l ↔ x ∉ l.
Proof. by rewrite elem_of_list_to_set. Qed.
(* stdpp/sets.v *)
Instance set_unfold_option_to_set (mx : option A) x :
    SetUnfoldElemOf x (option_to_set (C:=C) mx) (mx = Some x).
Proof. constructor; apply elem_of_option_to_set. Qed.
(* stdpp/sets.v *)
Instance set_unfold_list_to_set (l : list A) x P :
    SetUnfoldElemOf x l P → SetUnfoldElemOf x (list_to_set (C:=C) l) P.
Proof. constructor. by rewrite elem_of_list_to_set, (set_unfold (x ∈ l) P). Qed.
(* stdpp/sets.v *)
Lemma list_to_set_nil : list_to_set [] =@{C} ∅.
Proof. done. Qed.
(* stdpp/sets.v *)
Lemma list_to_set_cons x l : list_to_set (x :: l) =@{C} {[ x ]} ∪ list_to_set l.
Proof. done. Qed.
(* stdpp/sets.v *)
Lemma list_to_set_app l1 l2 : list_to_set (l1 ++ l2) ≡@{C} list_to_set l1 ∪ list_to_set l2.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma list_to_set_singleton x : list_to_set [x] ≡@{C} {[ x ]}.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma list_to_set_snoc l x : list_to_set (l ++ [x]) ≡@{C} list_to_set l ∪ {[ x ]}.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Instance list_to_set_perm : Proper ((≡ₚ) ==> (≡)) (list_to_set (C:=C)).
Proof. induction 1; set_solver. Qed.
(* stdpp/sets.v *)
Lemma list_to_set_app_L l1 l2 :
      list_to_set (l1 ++ l2) =@{C} list_to_set l1 ∪ list_to_set l2.
Proof. unfold_leibniz. apply list_to_set_app. Qed.
(* stdpp/sets.v *)
Lemma list_to_set_singleton_L x : list_to_set [x] =@{C} {[ x ]}.
Proof. unfold_leibniz. apply list_to_set_singleton. Qed.
(* stdpp/sets.v *)
Lemma list_to_set_snoc_L l x : list_to_set (l ++ [x]) =@{C} list_to_set l ∪ {[ x ]}.
Proof. unfold_leibniz. apply list_to_set_snoc. Qed.
(* stdpp/sets.v *)
Instance list_to_set_perm_L : Proper ((≡ₚ) ==> (=)) (list_to_set (C:=C)).
Proof. intros ???. unfold_leibniz. by apply list_to_set_perm. Qed.
(* stdpp/sets.v *)
(* * Finite types to sets. *)
Definition fin_to_set (A : Type) `{Singleton A C, Empty C, Union C, Finite A} : C
:=
  list_to_set (enum A).
(* stdpp/sets.v *)
Lemma elem_of_fin_to_set a : a ∈@{C} fin_to_set A.
Proof. apply elem_of_list_to_set, elem_of_enum. Qed.
(* stdpp/sets.v *)
Instance set_unfold_fin_to_set a :
    SetUnfoldElemOf (C:=C) a (fin_to_set A) True.
Proof. constructor. split; auto using elem_of_fin_to_set. Qed.
(* stdpp/sets.v *)
(* * Guard *)
Instance set_mfail `{MonadSet M} : MFail M
:= λ _ _, ∅.
(* stdpp/sets.v *)
Lemma elem_of_mfail {A} x : x ∈@{M A} mfail ↔ False.
Proof. unfold mfail, set_mfail. by rewrite elem_of_empty. Qed.
(* stdpp/sets.v *)
Instance set_unfold_elem_of_mfail {A} (x : A) :
    SetUnfoldElemOf x (mfail : M A) False.
Proof. constructor. by apply elem_of_mfail. Qed.
(* stdpp/sets.v *)
(* This lemma includes a bind, to avoid equalities of proofs. We cannot have
  [p ∈ guard P ↔ P] unless [P] is proof irrelant. The best (but less usable)
  self-contained alternative would be [p ∈ guard P ↔ decide P = left p]. *)
Lemma elem_of_guard `{Decision P} {A} (x : A) (X : M A) :
    x ∈ (guard P;; X) ↔ P ∧ x ∈ X.
Proof.
    case_guard; rewrite elem_of_bind;
      [setoid_rewrite elem_of_ret | setoid_rewrite elem_of_mfail];
      naive_solver.
  Qed.
(* stdpp/sets.v *)
Lemma elem_of_guard_2 `{Decision P} {A} (x : A) (X : M A) :
    P → x ∈ X → x ∈ (guard P;; X).
Proof. by rewrite elem_of_guard. Qed.
(* stdpp/sets.v *)
Lemma guard_empty `{Decision P} {A} (X : M A) : (guard P;; X) ≡ ∅ ↔ ¬P ∨ X ≡ ∅.
Proof.
    rewrite !elem_of_equiv_empty; setoid_rewrite elem_of_guard.
    destruct (decide P); naive_solver.
  Qed.
(* stdpp/sets.v *)
Instance set_unfold_guard `{Decision P} {A} (x : A) (X : M A) Q :
    SetUnfoldElemOf x X Q → SetUnfoldElemOf x (guard P;; X) (P ∧ Q).
Proof. constructor. by rewrite elem_of_guard, (set_unfold (x ∈ X) Q). Qed.
(* stdpp/sets.v *)
Lemma bind_empty {A B} (f : A → M B) X :
    X ≫= f ≡ ∅ ↔ X ≡ ∅ ∨ ∀ x, x ∈ X → f x ≡ ∅.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
(* * Quantifiers *)
Definition set_Forall `{ElemOf A C} (P : A → Prop) (X : C)
:= ∀ x, x ∈ X → P x.
(* stdpp/sets.v *)
Definition set_Exists `{ElemOf A C} (P : A → Prop) (X : C)
:= ∃ x, x ∈ X ∧ P x.
(* stdpp/sets.v *)
Instance set_unfold_set_Forall X (QX QP : A → Prop) :
    (∀ x, SetUnfoldElemOf x X (QX x)) →
    (∀ x, SetUnfold (P x) (QP x)) →
    SetUnfold (set_Forall P X) (∀ x, QX x → QP x).
Proof.
    intros HX HP; constructor. unfold set_Forall. apply forall_proper; intros x.
    by rewrite (set_unfold (x ∈ X) _), (set_unfold (P x) _).
  Qed.
(* stdpp/sets.v *)
Instance set_unfold_set_Exists X (QX QP : A → Prop) :
    (∀ x, SetUnfoldElemOf x X (QX x)) →
    (∀ x, SetUnfold (P x) (QP x)) →
    SetUnfold (set_Exists P X) (∃ x, QX x ∧ QP x).
Proof.
    intros HX HP; constructor. unfold set_Exists. f_equiv; intros x.
    by rewrite (set_unfold (x ∈ X) _), (set_unfold (P x) _).
  Qed.
(* stdpp/sets.v *)
Lemma set_Forall_empty : set_Forall P (∅ : C).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Forall_singleton x : set_Forall P ({[ x ]} : C) ↔ P x.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Forall_union X Y :
    set_Forall P X → set_Forall P Y → set_Forall P (X ∪ Y).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Forall_union_inv_1 X Y : set_Forall P (X ∪ Y) → set_Forall P X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Forall_union_inv_2 X Y : set_Forall P (X ∪ Y) → set_Forall P Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Forall_list_to_set l : set_Forall P (list_to_set (C:=C) l) ↔ Forall P l.
Proof. rewrite Forall_forall. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Exists_empty : ¬set_Exists P (∅ : C).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Exists_singleton x : set_Exists P ({[ x ]} : C) ↔ P x.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Exists_union_1 X Y : set_Exists P X → set_Exists P (X ∪ Y).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Exists_union_2 X Y : set_Exists P Y → set_Exists P (X ∪ Y).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Exists_union_inv X Y :
    set_Exists P (X ∪ Y) → set_Exists P X ∨ set_Exists P Y.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Exists_list_to_set l : set_Exists P (list_to_set (C:=C) l) ↔ Exists P l.
Proof. rewrite Exists_exists. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Forall_impl (P Q : A → Prop) X :
    set_Forall P X → (∀ x, P x → Q x) → set_Forall Q X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_Exists_impl (P Q : A → Prop) X :
    set_Exists P X → (∀ x, P x → Q x) → set_Exists Q X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Instance set_fmap_mono {A B} :
    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B).
Proof. intros f g ? X Y ?; set_solver by eauto. Qed.
(* stdpp/sets.v *)
Instance set_bind_mono {A B} :
    Proper (pointwise_relation _ (⊆) ==> (⊆) ==> (⊆)) (@mbind M _ A B).
Proof. unfold respectful, pointwise_relation; intros f g Hfg X Y ?. set_solver. Qed.
(* stdpp/sets.v *)
Instance set_join_mono {A} :
    Proper ((⊆) ==> (⊆)) (@mjoin M _ A).
Proof. intros X Y ?; set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_guard_True {A} `{Decision P} (X : M A) : P → (guard P;; X) ≡ X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma set_fmap_compose {A B C} (f : A → B) (g : B → C) (X : M A) :
    g ∘ f <$> X ≡ g <$> (f <$> X).
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma elem_of_fmap_1 {A B} (f : A → B) (X : M A) (y : B) :
    y ∈ f <$> X → ∃ x, y = f x ∧ x ∈ X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma elem_of_fmap_2 {A B} (f : A → B) (X : M A) (x : A) :
    x ∈ X → f x ∈ f <$> X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma elem_of_fmap_2_alt {A B} (f : A → B) (X : M A) (x : A) (y : B) :
    x ∈ X → y = f x → y ∈ f <$> X.
Proof. set_solver. Qed.
(* stdpp/sets.v *)
Lemma elem_of_mapM {A B} (f : A → M B) l k :
    l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k.
Proof.
    split.
    - revert l. induction k; set_solver by eauto.
    - induction 1; set_solver.
  Qed.