From 2db8a61ccf1ac55675d0021191ff3815c9cf57da Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 May 2017 11:15:41 +0200
Subject: [PATCH] Stronger version of map_fold_insert.

---
 theories/fin_maps.v | 14 +++++++++++---
 theories/list.v     | 18 +++++++++++++++++-
 2 files changed, 28 insertions(+), 4 deletions(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index ecb3ef76..aaed1ad0 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -928,15 +928,23 @@ Proof. unfold map_fold; simpl. by rewrite map_to_list_empty. Qed.
 Lemma map_fold_insert {A B} (R : relation B) `{!PreOrder R}
     (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) :
   (∀ j z, Proper (R ==> R) (f j z)) →
-  (∀ j1 j2 z1 z2 y, R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
+  (∀ j1 j2 z1 z2 y,
+    j1 ≠ j2 → <[i:=x]> m !! j1 = Some z1 → <[i:=x]> m !! j2 = Some z2 →
+    R (f j1 z1 (f j2 z2 y)) (f j2 z2 (f j1 z1 y))) →
   m !! i = None →
   R (map_fold f b (<[i:=x]> m)) (f i x (map_fold f b m)).
 Proof.
-  intros. unfold map_fold; simpl.
+  intros Hf_proper Hf Hi. unfold map_fold; simpl.
   assert (∀ kz, Proper (R ==> R) (curry f kz)) by (intros []; apply _).
   trans (foldr (curry f) b ((i, x) :: map_to_list m)); [|done].
   eapply (foldr_permutation R (curry f) b), map_to_list_insert; auto.
-  intros [] []; simpl; eauto.
+  intros j1 [k1 y1] j2 [k2 y2] c Hj Hj1 Hj2. apply Hf.
+  - intros ->.
+    eapply Hj, NoDup_lookup; [apply (NoDup_fst_map_to_list (<[i:=x]> m))| | ].
+    + by rewrite list_lookup_fmap, Hj1.
+    + by rewrite list_lookup_fmap, Hj2.
+  - by eapply elem_of_map_to_list, elem_of_list_lookup_2.
+  - by eapply elem_of_map_to_list, elem_of_list_lookup_2.
 Qed.
 
 Lemma map_fold_ind {A B} (P : B → M A → Prop) (f : K → A → B → B) (b : B) :
diff --git a/theories/list.v b/theories/list.v
index 4bdc361c..50dcc652 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3259,10 +3259,26 @@ Lemma foldl_app {A B} (f : A → B → A) (l k : list B) (a : A) :
   foldl f a (l ++ k) = foldl f (foldl f a l) k.
 Proof. revert a. induction l; simpl; auto. Qed.
 Lemma foldr_permutation {A B} (R : relation B) `{!PreOrder R}
+    (f : A → B → B) (b : B) `{Hf : !∀ x, Proper (R ==> R) (f x)} (l1 l2 : list A) :
+  (∀ j1 a1 j2 a2 b,
+    j1 ≠ j2 → l1 !! j1 = Some a1 → l1 !! j2 = Some a2 →
+    R (f a1 (f a2 b)) (f a2 (f a1 b))) →
+  l1 ≡ₚ l2 → R (foldr f b l1) (foldr f b l2).
+Proof.
+  intros Hf'. induction 1 as [|x l1 l2 _ IH|x y l|l1 l2 l3 Hl12 IH _ IH']; simpl.
+  - done.
+  - apply Hf, IH; eauto.
+  - apply (Hf' 0 _ 1); eauto.
+  - etrans; [eapply IH, Hf'|].
+    apply IH'; intros j1 a1 j2 a2 b' ???.
+    symmetry in Hl12; apply Permutation_inj in Hl12 as [_ (g&?&Hg)].
+    apply (Hf' (g j1) _ (g j2)); [naive_solver|by rewrite <-Hg..].
+Qed.
+Lemma foldr_permutation_proper {A B} (R : relation B) `{!PreOrder R}
     (f : A → B → B) (b : B) `{!∀ x, Proper (R ==> R) (f x)}
     (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
   Proper ((≡ₚ) ==> R) (foldr f b).
-Proof. induction 1; simpl; [done|by f_equiv|apply Hf|etrans; eauto]. Qed.
+Proof. intros l1 l2 Hl. apply foldr_permutation; auto. Qed.
 
 (** ** Properties of the [zip_with] and [zip] functions *)
 Section zip_with.
-- 
GitLab