From 59032a594567cfbb4340887e3bef667f8da3c672 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Sep 2022 12:50:26 +0200
Subject: [PATCH] update dependencies
---
coq-iris-examples.opam | 2 +-
.../freeable_lock/freeable_logatom_lock.v | 30 -------------------
2 files changed, 1 insertion(+), 31 deletions(-)
diff --git a/coq-iris-examples.opam b/coq-iris-examples.opam
index 4192e10f..8425436c 100644
--- a/coq-iris-examples.opam
+++ b/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" }
]
diff --git a/theories/locks/freeable_lock/freeable_logatom_lock.v b/theories/locks/freeable_lock/freeable_logatom_lock.v
index d1a8f125..6ac6b470 100644
--- a/theories/locks/freeable_lock/freeable_logatom_lock.v
+++ b/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 {
--
GitLab