Commit e5cd45f3 by Robbert Krebbers

More multiset properties.

parent b64b3e9b
 ... ... @@ -73,18 +73,6 @@ Proof. repeat case_match; naive_solver. Qed. Global Instance gmultiset_po : PartialOrder (@subseteq (gmultiset A) _). Proof. split; [split|]. - by intros X x. - intros X Y Z HXY HYZ x. by trans (multiplicity x Y). - intros X Y HXY HYX; apply gmultiset_eq; intros x. by apply (anti_symm (≤)). Qed. Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y. Proof. by intros [??]. Qed. Hint Resolve gmultiset_subset_subseteq. (* Multiplicity *) Lemma multiplicity_empty x : multiplicity x ∅ = 0. Proof. done. Qed. ... ... @@ -145,24 +133,10 @@ Qed. Global Instance gmultiset_union_inj_2 X : Inj (=) (=) (∪ X). Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed. Lemma gmultiset_union_difference X Y : X ⊆ Y → Y = X ∪ Y ∖ X. Proof. intros HXY. apply gmultiset_eq; intros x; specialize (HXY x). rewrite multiplicity_union, multiplicity_difference; omega. Qed. Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≠ ∅. Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠ (∅ : gmultiset A). Proof. intros [_ HXY2] Hdiff; destruct HXY2; intros x. generalize (f_equal (multiplicity x) Hdiff). rewrite multiplicity_difference, multiplicity_empty; omega. Qed. (* Order stuff *) Lemma gmultiset_elem_of_subseteq x X : x ∈ X → {[ x ]} ⊆ X. Proof. rewrite elem_of_multiplicity. intros Hx y; destruct (decide (x = y)) as [->|]. - rewrite multiplicity_singleton; omega. - rewrite multiplicity_singleton_ne by done; omega. rewrite gmultiset_eq. intros Hx; generalize (Hx x). by rewrite multiplicity_singleton, multiplicity_empty. Qed. (* Properties of the elements operation *) ... ... @@ -204,11 +178,6 @@ Proof. by (by rewrite ?lookup_union_with, ?HX, ?HY). by rewrite <-(assoc_L (++)), <-IH. Qed. Lemma gmultiset_elements_contains X Y : X ⊆ Y → elements X `contains` elements Y. Proof. intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union. by apply contains_inserts_r. Qed. Lemma gmultiset_elem_of_elements x X : x ∈ elements X ↔ x ∈ X. Proof. destruct X as [X]. unfold elements, gmultiset_elements. ... ... @@ -260,20 +229,93 @@ Proof. unfold size, gmultiset_size; simpl. by rewrite gmultiset_elements_union, app_length. Qed. (* Order stuff *) Global Instance gmultiset_po : PartialOrder (@subseteq (gmultiset A) _). Proof. split; [split|]. - by intros X x. - intros X Y Z HXY HYZ x. by trans (multiplicity x Y). - intros X Y HXY HYX; apply gmultiset_eq; intros x. by apply (anti_symm (≤)). Qed. Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y. Proof. apply strict_include. Qed. Hint Resolve gmultiset_subset_subseteq. Lemma gmultiset_empty_subseteq X : ∅ ⊆ X. Proof. intros x. rewrite multiplicity_empty. omega. Qed. 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. 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_subset X Y : X ⊆ Y → size X < size Y → X ⊂ Y. Proof. intros. apply strict_spec_alt; split; naive_solver auto with omega. Qed. Lemma gmultiset_union_subset_l X Y : Y ≠ ∅ → X ⊂ X ∪ Y. Proof. intros HY%gmultiset_size_non_empty_iff. apply gmultiset_subset; auto using gmultiset_union_subseteq_l. rewrite gmultiset_size_union; omega. Qed. Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ∪ Y. Proof. rewrite (comm_L (∪)). apply gmultiset_union_subset_l. Qed. Lemma gmultiset_elem_of_subseteq x X : x ∈ X → {[ x ]} ⊆ X. Proof. rewrite elem_of_multiplicity. intros Hx y; destruct (decide (x = y)) as [->|]. - rewrite multiplicity_singleton; omega. - rewrite multiplicity_singleton_ne by done; omega. Qed. Lemma gmultiset_union_difference X Y : X ⊆ Y → Y = X ∪ Y ∖ X. Proof. intros HXY. apply gmultiset_eq; intros x; specialize (HXY x). rewrite multiplicity_union, multiplicity_difference; omega. Qed. Lemma gmultiset_union_difference' x Y : x ∈ Y → Y = {[ x ]} ∪ Y ∖ {[ x ]}. Proof. auto using gmultiset_union_difference, gmultiset_elem_of_subseteq. Qed. Lemma gmultiset_size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y. Proof. intros HX%gmultiset_union_difference. rewrite HX at 2; rewrite gmultiset_size_union. omega. Qed. Lemma gmultiset_non_empty_difference X Y : X ⊂ Y → Y ∖ X ≠ ∅. Proof. intros [_ HXY2] Hdiff; destruct HXY2; intros x. generalize (f_equal (multiplicity x) Hdiff). rewrite multiplicity_difference, multiplicity_empty; omega. Qed. Lemma gmultiset_difference_subset X Y : X ≠ ∅ → X ⊆ Y → Y ∖ X ⊂ Y. Proof. intros. eapply strict_transitive_l; [by apply gmultiset_union_subset_r|]. by rewrite <-(gmultiset_union_difference X Y). Qed. (* Mononicity *) Lemma gmultiset_elements_contains X Y : X ⊆ Y → elements X `contains` elements Y. Proof. intros ->%gmultiset_union_difference. rewrite gmultiset_elements_union. by apply contains_inserts_r. Qed. Lemma gmultiset_subseteq_size X Y : X ⊆ Y → size X ≤ size Y. Proof. intros. by apply contains_length, gmultiset_elements_contains. Qed. Lemma gmultiset_subset_size X Y : X ⊂ Y → size X < size Y. Proof. intros HXY. assert (size (Y ∖ X) ≠ 0). { by apply gmultiset_size_non_empty_iff, non_empty_difference. } { by apply gmultiset_size_non_empty_iff, gmultiset_non_empty_difference. } rewrite (gmultiset_union_difference X Y), gmultiset_size_union by auto. lia. Qed. ... ... @@ -282,4 +324,14 @@ Lemma gmultiset_wf : wf (strict (@subseteq (gmultiset A) _)). Proof. apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf. Qed. Lemma gmultiset_ind (P : gmultiset A → Prop) : P ∅ → (∀ x X, P X → P ({[ x ]} ∪ X)) → ∀ X, P X. Proof. intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH]. destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto. rewrite (gmultiset_union_difference' x X) by done. apply Hinsert, IH, gmultiset_difference_subset; auto using gmultiset_elem_of_subseteq, gmultiset_non_empty_singleton. Qed. End lemmas.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment