Commit 5061c3cb by Robbert Krebbers

### Rename preserving -> mono.

To be consistent with Iris, see Iris commit 9ee62b3a.
parent 81d719c9
 ... @@ -346,11 +346,11 @@ Section simple_collection. ... @@ -346,11 +346,11 @@ Section simple_collection. Proof. set_solver. Qed. Proof. set_solver. Qed. Lemma elem_of_union_r x X Y : x ∈ Y → x ∈ X ∪ Y. Lemma elem_of_union_r x X Y : x ∈ Y → x ∈ X ∪ Y. Proof. set_solver. Qed. 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. 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. 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. Proof. set_solver. Qed. Global Instance union_idemp : IdemP ((≡) : relation C) (∪). Global Instance union_idemp : IdemP ((≡) : relation C) (∪). ... @@ -444,8 +444,8 @@ Section simple_collection. ... @@ -444,8 +444,8 @@ Section simple_collection. by rewrite reverse_cons, union_list_app, by rewrite reverse_cons, union_list_app, union_list_singleton, (comm _), IH. union_list_singleton, (comm _), IH. Qed. Qed. Lemma union_list_preserving Xs Ys : Xs ⊆* Ys → ⋃ Xs ⊆ ⋃ Ys. Lemma union_list_mono Xs Ys : Xs ⊆* Ys → ⋃ Xs ⊆ ⋃ Ys. Proof. induction 1; simpl; auto using union_preserving. Qed. Proof. induction 1; simpl; auto using union_mono. Qed. Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs. Lemma empty_union_list Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs. Proof. Proof. split. split. ... @@ -565,11 +565,11 @@ Section collection. ... @@ -565,11 +565,11 @@ Section collection. Lemma intersection_greatest X Y Z : Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y. Lemma intersection_greatest X Y Z : Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y. Proof. set_solver. Qed. 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. 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. 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. X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∩ Y1 ⊆ X2 ∩ Y2. Proof. set_solver. Qed. Proof. set_solver. Qed. ... @@ -612,12 +612,12 @@ Section collection. ... @@ -612,12 +612,12 @@ Section collection. Lemma difference_disjoint X Y : X ⊥ Y → X ∖ Y ≡ X. Lemma difference_disjoint X Y : X ⊥ Y → X ∖ Y ≡ X. Proof. set_solver. Qed. 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. X1 ⊆ X2 → Y2 ⊆ Y1 → X1 ∖ Y1 ⊆ X2 ∖ Y2. Proof. set_solver. Qed. 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. 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. Proof. set_solver. Qed. (** Disjointness *) (** Disjointness *) ... ...
 ... @@ -1322,17 +1322,17 @@ Proof. intros. trans m2; auto using map_union_subseteq_l. Qed. ... @@ -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) : Lemma map_union_subseteq_r_alt {A} (m1 m2 m3 : M A) : m2 ⊥ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3. m2 ⊥ₘ m3 → m1 ⊆ m3 → m1 ⊆ m2 ∪ m3. Proof. intros. trans m3; auto using map_union_subseteq_r. Qed. 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. Proof. rewrite !map_subseteq_spec. intros ???. rewrite !map_subseteq_spec. intros ???. rewrite !lookup_union_Some_raw. naive_solver. rewrite !lookup_union_Some_raw. naive_solver. Qed. 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. m2 ⊥ₘ m3 → m1 ⊆ m2 → m1 ∪ m3 ⊆ m2 ∪ m3. Proof. Proof. intros. rewrite !(map_union_comm _ m3) intros. rewrite !(map_union_comm _ m3) by eauto using map_disjoint_weaken_l. by eauto using map_disjoint_weaken_l. by apply map_union_preserving_l. by apply map_union_mono_l. Qed. Qed. Lemma map_union_reflecting_l {A} (m1 m2 m3 : M A) : Lemma map_union_reflecting_l {A} (m1 m2 m3 : M A) : m3 ⊥ₘ m1 → m3 ⊥ₘ m2 → m3 ∪ m1 ⊆ m3 ∪ m2 → m1 ⊆ m2. m3 ⊥ₘ m1 → m3 ⊥ₘ m2 → m3 ∪ m1 ⊆ m3 ∪ m2 → m1 ⊆ m2. ... ...
 ... @@ -288,12 +288,12 @@ Lemma gmultiset_union_subseteq_l X Y : X ⊆ X ∪ Y. ... @@ -288,12 +288,12 @@ Lemma gmultiset_union_subseteq_l X Y : X ⊆ X ∪ Y. Proof. intros x. rewrite multiplicity_union. omega. Qed. Proof. intros x. rewrite multiplicity_union. omega. Qed. Lemma gmultiset_union_subseteq_r X Y : Y ⊆ X ∪ Y. Lemma gmultiset_union_subseteq_r X Y : Y ⊆ X ∪ Y. Proof. intros x. rewrite multiplicity_union. omega. Qed. 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. 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. Lemma gmultiset_union_mono_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2. Proof. intros. by apply gmultiset_union_preserving. Qed. Proof. intros. by apply gmultiset_union_mono. Qed. Lemma gmultiset_union_preserving_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y. Lemma gmultiset_union_mono_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y. Proof. intros. by apply gmultiset_union_preserving. Qed. Proof. intros. by apply gmultiset_union_mono. Qed. Lemma gmultiset_subset X Y : X ⊆ Y → size X < size Y → X ⊂ Y. 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. Proof. intros. apply strict_spec_alt; split; naive_solver auto with omega. Qed. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!