From 9fcbbccf6d7d7786f6c59be8cd8cd8939cd14100 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Jun 2012 11:17:07 +0200
Subject: [PATCH] Modify the Hoare judgment such that is also ensures thread
 safity.

Before, it just ensured that whenever one can split up the memory
into two parts before running the program, the framing part can
be split off when the program is finished. Now it also ensure that
it can be split off at any moment during the execution of the
program.

When we extend to non-deterministic expressions/sequence points we
certainly need this for the Hoare judgment for expressions, as C
allows evaluation of them to interleave. However, for consistency,
and further extensions, it is nice to have this property for
statements too.
---
 theories/fin_maps.v | 13 +++++++++++++
 theories/trs.v      |  4 +++-
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2f1a7afd..b85be1f3 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -96,6 +96,19 @@ Section finmap.
   Proof. intros Hm ?. subst. rewrite lookup_delete in Hm. now apply None_not_is_Some in Hm. Qed.
   Lemma lookup_delete_ne (m : M A) i j : i ≠ j → delete i m !! j = m !! j.
   Proof. apply lookup_partial_alter_ne. Qed.
+  Lemma lookup_delete_None (m : M A) i j : m !! j = None → delete i m !! j = None.
+  Proof.
+    destruct (decide (i = j)).
+     subst. now rewrite lookup_delete.
+    now rewrite lookup_delete_ne.
+  Qed.
+  Lemma delete_lookup_None (m : M A) i : m !! i = None → delete i m = m.
+  Proof.
+    intros. apply finmap_eq. intros j. destruct (decide (i = j)).
+     subst. rewrite lookup_delete. congruence.
+    now apply lookup_delete_ne.
+  Qed.
+
   Lemma delete_empty i : delete i (∅ : M A) = ∅.
   Proof. rewrite <-(partial_alter_self ∅) at 2. now rewrite lookup_empty. Qed.
   Lemma delete_singleton i (x : A) : delete i {{ (i, x) }} = ∅.
diff --git a/theories/trs.v b/theories/trs.v
index 5a6d6db4..efb65063 100644
--- a/theories/trs.v
+++ b/theories/trs.v
@@ -90,8 +90,10 @@ Hint Resolve rtc_once rtc_r tc_r : trs.
 Section subrel.
   Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2).
 
+  Lemma red_subrel x : red R1 x → red R2 x.
+  Proof. intros [y ?]. exists y. now apply Hsub. Qed.
   Lemma nf_subrel x : nf R2 x → nf R1 x.
-  Proof. intros Hnf [y ?]. destruct Hnf. exists y. now apply Hsub. Qed.
+  Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed.
 
   Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
   Proof.
-- 
GitLab