From 06317bc1b0b353181591cd3d50b19bf7fad8e8a4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
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 <mail@robbertkrebbers.nl>
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 <mail@robbertkrebbers.nl>
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 <jung@mpi-sws.org>
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