update dependencies

coq-iris-examples.opam

@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/examples.git"
 synopsis: "A collection of case studies for Iris -- not meant to be used as a dependency of anything"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2022-08-16.2.a58395f1") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-09-25.0.ce054a47") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 

theories/locks/freeable_lock/freeable_logatom_lock.v

@@ -15,36 +15,6 @@ From iris.heap_lang Require Import proofmode notation.
 From iris_examples.locks Require Import freeable_lock.
 From iris.prelude Require Import options.
 
-(* TODO move to std++ *)
-Section theorems.
-Context `{FinMap K M}.
-
-Lemma map_fold_delete {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,
-    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 = Some x →
-  R (map_fold f b m) (f i x (map_fold f b (delete i m))).
-Proof using Type*.
-  intros Hf_proper Hf Hi.
-  rewrite <-map_fold_insert; [|done|done| |].
-  - rewrite insert_delete; done.
-  - intros j1 j2 ????. rewrite insert_delete_insert. auto.
-  - rewrite lookup_delete. done.
-Qed.
-
-Lemma map_fold_delete_L {A B} (f : K → A → B → B) (b : B) (i : K) (x : A) (m : M A) :
-  (∀ j1 j2 z1 z2 y,
-    j1 ≠ j2 → <[i:=x]> m !! j1 = Some z1 → <[i:=x]> m !! j2 = Some z2 →
-    f j1 z1 (f j2 z2 y) = f j2 z2 (f j1 z1 y)) →
-  m !! i = Some x →
-  map_fold f b m = f i x (map_fold f b (delete i m)).
-Proof using Type*. apply map_fold_delete; apply _. Qed.
-
-End theorems.
-
 Inductive state := Free | Locked.
 
 Class lockG Σ := LockG {