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

@@ -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) }} = ∅.

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.