From 24c28e2c1e72c2928743809080e65b3f3819a4d2 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 27 Jul 2016 00:52:27 +0200 Subject: [PATCH] Relate subseteq on collections to the extension order. --- prelude/collections.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/prelude/collections.v b/prelude/collections.v index 98a1a93e..7762ce91 100644 --- a/prelude/collections.v +++ b/prelude/collections.v @@ -645,6 +645,11 @@ Section collection. intros ? x; split; rewrite !elem_of_union, elem_of_difference; [|intuition]. destruct (decide (x ∈ X)); intuition. Qed. + 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. Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅. Proof. intros [HXY1 HXY2] Hdiff. destruct HXY2. set_solver. Qed. Lemma empty_difference_subseteq X Y : X ∖ Y ≡ ∅ → X ⊆ Y. @@ -657,6 +662,8 @@ Section collection. Proof. unfold_leibniz. apply non_empty_difference. Qed. Lemma empty_difference_subseteq_L X Y : X ∖ Y = ∅ → X ⊆ Y. Proof. unfold_leibniz. apply empty_difference_subseteq. Qed. + Lemma subseteq_disjoint_union_L X Y : X ⊆ Y ↔ ∃ Z, Y = X ∪ Z ∧ X ⊥ Z. + Proof. unfold_leibniz. apply subseteq_disjoint_union. Qed. End dec. End collection. -- 2.24.1