From 06317bc1b0b353181591cd3d50b19bf7fad8e8a4 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 27 May 2021 23:33:04 +0200 Subject: [PATCH 1/4] Add lemma `set_fold_disj_union_strong`. Stronger version of a lemma suggested by @jihgfee. --- theories/fin_sets.v | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/theories/fin_sets.v b/theories/fin_sets.v index a4581571..089766d7 100644 --- a/theories/fin_sets.v +++ b/theories/fin_sets.v @@ -254,7 +254,24 @@ Lemma set_fold_disj_union (f : A → A → A) (b : A) 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 (++)). + by rewrite elements_disj_union, <-foldr_app, (comm (++)). +Qed. +Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R} + (f : A → B → B) (b : B) X Y : + (∀ x, Proper (R ==> R) (f x)) → + (∀ x1 x2 b', + x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 → R (f x1 (f x2 b')) (f x2 (f x1 b'))) → + X ## Y → + R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y). +Proof. + intros ? Hf Hdisj. unfold set_fold; simpl. + rewrite <-foldr_app. apply (foldr_permutation R f b). + - intros j1 x1 j2 x2 b' Hj Hj1 Hj2. apply Hf. + + apply elem_of_list_lookup_2 in Hj1. set_solver. + + apply elem_of_list_lookup_2 in Hj2. set_solver. + + intros ->. pose proof (NoDup_elements (X ∪ Y)). + by eapply Hj, NoDup_lookup. + - by rewrite elements_disj_union, (comm (++)). Qed. (** * Minimal elements *) -- GitLab From d8420d64e508aca48724619989fac5cc475bb2d6 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Mon, 31 May 2021 08:16:35 +0200 Subject: [PATCH 2/4] Derive `set_fold_disj_union` from `_strong` version. This ensures that the strong version is indeed stronger. --- theories/fin_sets.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/theories/fin_sets.v b/theories/fin_sets.v index 089766d7..f24fdfdd 100644 --- a/theories/fin_sets.v +++ b/theories/fin_sets.v @@ -247,15 +247,6 @@ 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. Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R} (f : A → B → B) (b : B) X Y : (∀ x, Proper (R ==> R) (f x)) → @@ -273,6 +264,15 @@ Proof. by eapply Hj, NoDup_lookup. - by rewrite elements_disj_union, (comm (++)). 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. apply (set_fold_disj_union_strong _ _ _ _ _ _); [|done]. + intros x1 x2 b' _ _ _. by rewrite !(assoc_L f), (comm_L f x1). +Qed. (** * Minimal elements *) Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) : -- GitLab From aab66de53c51adb0e47d1f320b1a2f36116f1814 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 2 Jun 2021 17:22:29 +0200 Subject: [PATCH 3/4] Comment. --- theories/fin_sets.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/theories/fin_sets.v b/theories/fin_sets.v index f24fdfdd..7b5b81bc 100644 --- a/theories/fin_sets.v +++ b/theories/fin_sets.v @@ -247,11 +247,16 @@ 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. +(** Generalization of [set_fold_disj_union] (below) with a.) a relation [R] +instead of equality b.) a function [f : A → B → B] instead of [f : A → A → A], +and c.) premises that ensure the elements are in [X ∪ Y]. *) Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R} (f : A → B → B) (b : B) X Y : (∀ x, Proper (R ==> R) (f x)) → (∀ x1 x2 b', - x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 → R (f x1 (f x2 b')) (f x2 (f x1 b'))) → + (** This is morally commutativity + associativity *) + x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 → + R (f x1 (f x2 b')) (f x2 (f x1 b'))) → X ## Y → R (set_fold f b (X ∪ Y)) (set_fold f (set_fold f b X) Y). Proof. -- GitLab From d953670232edc209bc0cbe4fef2ed49f04bcd477 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 2 Jun 2021 15:39:32 +0000 Subject: [PATCH 4/4] Apply 1 suggestion(s) to 1 file(s) --- theories/fin_sets.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/fin_sets.v b/theories/fin_sets.v index 7b5b81bc..8ae76e19 100644 --- a/theories/fin_sets.v +++ b/theories/fin_sets.v @@ -254,7 +254,7 @@ Lemma set_fold_disj_union_strong {B} (R : relation B) `{!PreOrder R} (f : A → B → B) (b : B) X Y : (∀ x, Proper (R ==> R) (f x)) → (∀ x1 x2 b', - (** This is morally commutativity + associativity *) + (** This is morally commutativity + associativity for elements of [X ∪ Y] *) x1 ∈ X ∪ Y → x2 ∈ X ∪ Y → x1 ≠ x2 → R (f x1 (f x2 b')) (f x2 (f x1 b'))) → X ## Y → -- GitLab