From 5061c3cbfe8954faa67dc5eed061c92eaca65308 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 9 Mar 2017 23:07:52 +0100 Subject: [PATCH] Rename preserving -> mono. To be consistent with Iris, see Iris commit 9ee62b3a. --- theories/collections.v | 22 +++++++++++----------- theories/fin_maps.v | 6 +++--- theories/gmultiset.v | 10 +++++----- 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/theories/collections.v b/theories/collections.v index 28a8f25..b1546e7 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -346,11 +346,11 @@ Section simple_collection. 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. + Lemma union_mono_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. + Lemma union_mono_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. + Lemma union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2. Proof. set_solver. Qed. Global Instance union_idemp : IdemP ((≡) : relation C) (∪). @@ -444,8 +444,8 @@ Section simple_collection. by rewrite reverse_cons, union_list_app, union_list_singleton, (comm _), IH. Qed. - Lemma union_list_preserving Xs Ys : Xs ⊆* Ys → ⋃ Xs ⊆ ⋃ Ys. - Proof. induction 1; simpl; auto using union_preserving. Qed. + Lemma union_list_mono Xs Ys : Xs ⊆* Ys → ⋃ Xs ⊆ ⋃ Ys. + Proof. induction 1; simpl; auto using union_mono. Qed. Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs. Proof. split. @@ -565,11 +565,11 @@ Section collection. Lemma intersection_greatest X Y Z : Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y. Proof. set_solver. Qed. - Lemma intersection_preserving_l X Y1 Y2 : Y1 ⊆ Y2 → X ∩ Y1 ⊆ X ∩ Y2. + Lemma intersection_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∩ Y1 ⊆ X ∩ Y2. Proof. set_solver. Qed. - Lemma intersection_preserving_r X1 X2 Y : X1 ⊆ X2 → X1 ∩ Y ⊆ X2 ∩ Y. + Lemma intersection_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∩ Y ⊆ X2 ∩ Y. Proof. set_solver. Qed. - Lemma intersection_preserving X1 X2 Y1 Y2 : + Lemma intersection_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∩ Y1 ⊆ X2 ∩ Y2. Proof. set_solver. Qed. @@ -612,12 +612,12 @@ Section collection. Lemma difference_disjoint X Y : X ⊥ Y → X ∖ Y ≡ X. Proof. set_solver. Qed. - Lemma difference_preserving X1 X2 Y1 Y2 : + Lemma difference_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y2 ⊆ Y1 → X1 ∖ Y1 ⊆ X2 ∖ Y2. Proof. set_solver. Qed. - Lemma difference_preserving_l X Y1 Y2 : Y2 ⊆ Y1 → X ∖ Y1 ⊆ X ∖ Y2. + Lemma difference_mono_l X Y1 Y2 : Y2 ⊆ Y1 → X ∖ Y1 ⊆ X ∖ Y2. Proof. set_solver. Qed. - Lemma difference_preserving_r X1 X2 Y : X1 ⊆ X2 → X1 ∖ Y ⊆ X2 ∖ Y. + Lemma difference_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∖ Y ⊆ X2 ∖ Y. Proof. set_solver. Qed. (** Disjointness *) diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 2d10c3f..902c6b0 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -1322,17 +1322,17 @@ Proof. intros. trans m2; auto using map_union_subseteq_l. Qed. Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) : m2 ⊥ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3. Proof. intros. trans m3; auto using map_union_subseteq_r. Qed. -Lemma map_union_preserving_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2. +Lemma map_union_mono_l {A} (m1 m2 m3 : M A) : m1 ⊆ m2 → m3 ∪ m1 ⊆ m3 ∪ m2. Proof. rewrite !map_subseteq_spec. intros ???. rewrite !lookup_union_Some_raw. naive_solver. Qed. -Lemma map_union_preserving_r {A} (m1 m2 m3 : M A) : +Lemma map_union_mono_r {A} (m1 m2 m3 : M A) : m2 ⊥ₘ m3 → m1 ⊆ m2 → m1 ∪ m3 ⊆ m2 ∪ m3. Proof. intros. rewrite !(map_union_comm _ m3) by eauto using map_disjoint_weaken_l. - by apply map_union_preserving_l. + by apply map_union_mono_l. Qed. Lemma map_union_reflecting_l {A} (m1 m2 m3 : M A) : m3 ⊥ₘ m1 → m3 ⊥ₘ m2 → m3 ∪ m1 ⊆ m3 ∪ m2 → m1 ⊆ m2. diff --git a/theories/gmultiset.v b/theories/gmultiset.v index 773b72e..f30c725 100644 --- a/theories/gmultiset.v +++ b/theories/gmultiset.v @@ -288,12 +288,12 @@ Lemma gmultiset_union_subseteq_l X Y : X ⊆ X ∪ Y. Proof. intros x. rewrite multiplicity_union. omega. Qed. Lemma gmultiset_union_subseteq_r X Y : Y ⊆ X ∪ Y. Proof. intros x. rewrite multiplicity_union. omega. Qed. -Lemma gmultiset_union_preserving X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2. +Lemma gmultiset_union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2. Proof. intros ?? x. rewrite !multiplicity_union. by apply Nat.add_le_mono. Qed. -Lemma gmultiset_union_preserving_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2. -Proof. intros. by apply gmultiset_union_preserving. Qed. -Lemma gmultiset_union_preserving_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y. -Proof. intros. by apply gmultiset_union_preserving. Qed. +Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2. +Proof. intros. by apply gmultiset_union_mono. Qed. +Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y. +Proof. intros. by apply gmultiset_union_mono. Qed. Lemma gmultiset_subset X Y : X ⊆ Y → size X < size Y → X ⊂ Y. Proof. intros. apply strict_spec_alt; split; naive_solver auto with omega. Qed. -- GitLab