diff --git a/theories/fin_sets.v b/theories/fin_sets.v index 2e517e29445771cbbfd14ff7d6d28e84e2e366ae..c34f20455d6655163d03812632b9483348412b89 100644 --- a/theories/fin_sets.v +++ b/theories/fin_sets.v @@ -101,6 +101,14 @@ Proof. apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}), elements_union_singleton, elements_empty by set_solver. Qed. +Lemma elements_disj_union (X Y : C) : + X ## Y → elements (X ∪ Y) ≡ₚ elements X ++ elements Y. +Proof. + intros HXY. apply NoDup_Permutation. + - apply NoDup_elements. + - apply NoDup_app. set_solver by eauto using NoDup_elements. + - set_solver. +Qed. Lemma elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y. Proof. intros; apply NoDup_submseteq; eauto using NoDup_elements. @@ -222,6 +230,22 @@ Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R} Proper ((≡) ==> R) (set_fold f b : C → B). Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed. +Lemma set_fold_empty {B} (f : A → B → B) (b : B) : + set_fold f b (∅ : C) = b. +Proof. by unfold set_fold; simpl; rewrite elements_empty. Qed. +Lemma set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) : + set_fold f b ({[a]} : C) = f a b. +Proof. by unfold set_fold; simpl; rewrite elements_singleton. Qed. +Lemma set_fold_disj_union (f : A → A → A) (b : A) X Y : + Comm (=) f → + Assoc (=) f → + X ## Y → + set_fold f b (X ∪ Y) = set_fold f (set_fold f b X) Y. +Proof. + intros Hcomm Hassoc Hdisj. unfold set_fold; simpl. + by rewrite elements_disj_union, <- foldr_app, (comm (++)). +Qed. + (** * Minimal elements *) Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) : X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X. diff --git a/theories/gmultiset.v b/theories/gmultiset.v index ace17583c1935e4853012ae6af8aacf0ce60334a..4c83c31988c31b1678a1018a1e326a8534baa21a 100644 --- a/theories/gmultiset.v +++ b/theories/gmultiset.v @@ -330,7 +330,23 @@ Proof. destruct (X !! x); naive_solver lia. Qed. -(* Properties of the size operation *) +(** Properties of the set_fold operation *) +Lemma gmultiset_set_fold_empty {B} (f : A → B → B) (b : B) : + set_fold f b (∅ : gmultiset A) = b. +Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_empty. Qed. +Lemma gmultiset_set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) : + set_fold f b ({[a]} : gmultiset A) = f a b. +Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_singleton. Qed. +Lemma gmultiset_set_fold_disj_union (f : A → A → A) (b : A) X Y : + Comm (=) f → + Assoc (=) f → + set_fold f b (X ⊎ Y) = set_fold f (set_fold f b X) Y. +Proof. + intros Hcomm Hassoc. unfold set_fold; simpl. + by rewrite gmultiset_elements_disj_union, <- foldr_app, (comm (++)). +Qed. + +(** Properties of the size operation *) Lemma gmultiset_size_empty : size (∅ : gmultiset A) = 0. Proof. done. Qed. Lemma gmultiset_size_empty_inv X : size X = 0 → X = ∅. @@ -370,7 +386,7 @@ Proof. by rewrite gmultiset_elements_disj_union, app_length. Qed. -(* Order stuff *) +(** Order stuff *) Global Instance gmultiset_po : PartialOrder (⊆@{gmultiset A}). Proof. split; [split|]. @@ -464,6 +480,13 @@ Proof. rewrite HX at 2; rewrite gmultiset_size_disj_union. lia. Qed. +Lemma gmultiset_empty_difference X Y : Y ⊆ X → Y ∖ X = ∅. +Proof. + intros HYX. unfold_leibniz. intros x. + rewrite multiplicity_difference, multiplicity_empty. + specialize (HYX x). lia. +Qed. + Lemma gmultiset_non_empty_difference X Y : X ⊂ Y → Y ∖ X ≠ ∅. Proof. intros [_ HXY2] Hdiff; destruct HXY2; intros x. @@ -471,13 +494,16 @@ Proof. rewrite multiplicity_difference, multiplicity_empty; lia. Qed. +Lemma gmultiset_difference_diag X : X ∖ X = ∅. +Proof. by apply gmultiset_empty_difference. 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_disj_union_difference X Y). Qed. -(* Mononicity *) +(** Mononicity *) Lemma gmultiset_elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y. Proof. intros ->%gmultiset_disj_union_difference. rewrite gmultiset_elements_disj_union. @@ -495,7 +521,7 @@ Proof. gmultiset_size_disj_union by auto. lia. Qed. -(* Well-foundedness *) +(** Well-foundedness *) Lemma gmultiset_wf : wf (⊂@{gmultiset A}). Proof. apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf. diff --git a/theories/list.v b/theories/list.v index 8194d802e6208166bda005bf303b709813ab41c9..a38fc6a0281903f770b16157cc9540b460b9d4e5 100644 --- a/theories/list.v +++ b/theories/list.v @@ -3446,6 +3446,16 @@ Lemma foldr_permutation_proper {A B} (R : relation B) `{!PreOrder R} (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) : Proper ((≡ₚ) ==> R) (foldr f b). Proof. intros l1 l2 Hl. apply foldr_permutation; auto. Qed. +Instance foldr_permutation_proper' {A} (R : relation A) `{!PreOrder R} + (f : A → A → A) (a : A) `{!∀ a, Proper (R ==> R) (f a), !Assoc R f, !Comm R f} : + Proper ((≡ₚ) ==> R) (foldr f a). +Proof. + apply (foldr_permutation_proper R f); [solve_proper|]. + assert (Proper (R ==> R ==> R) f). + { intros a1 a2 Ha b1 b2 Hb. by rewrite Hb, (comm f a1), Ha, (comm f). } + intros a1 a2 b. + by rewrite (assoc f), (comm f _ b), (assoc f), (comm f b), (comm f _ a2). +Qed. (** ** Properties of the [zip_with] and [zip] functions *) Section zip_with.