From 5afc013e7a484405536d26214be6b889f123f69b Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 28 Apr 2019 13:43:26 +0200
Subject: [PATCH] =?UTF-8?q?CmraSwappable=20also=20implies=20=E2=96=B7=20co?=
 =?UTF-8?q?mmutes=20with=20-=E2=88=97=20and=20|=3D=3D>?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Commuting with |==> would have been interesting a bunch of times. But I still
don't see a way to commute with fancy updates, even mask-preserving ones.
---
 theories/base_logic/upred.v | 40 +++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 1cbf4261c..d7c69e5da 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -671,6 +671,46 @@ Proof.
     by rewrite -Hnx'x''.
 Qed.
 
+Lemma later_wand `{!CmraSwappable M} P Q : (▷ P -∗ ▷ Q) ⊢ ▷ (P -∗ Q).
+Proof.
+  unseal; split => /= -[//|n] x ? HPQ n' x' ?? HP.
+  specialize (HPQ (S n')); cbn in HPQ.
+  case: (cmra_extend_included n' (Some x) x') => [||x'' []];
+    rewrite /= ?(comm _ _ x) ?Some_validN //.
+  - by eapply cmra_validN_le; eauto.
+  - move => ? Hnx'x''.
+    rewrite Hnx'x''. apply HPQ; eauto.
+    by rewrite -Hnx'x''.
+Qed.
+
+Lemma later_bupd `{!CmraSwappable M} P : (▷ |==> P) ⊢ |==> ▷ P.
+Proof.
+  unseal; split => /= -[|n] x ? HP k yf Hkl.
+  - have ->: k = 0 by lia. by eauto.
+  - case: (decide (k ≤ n)) Hkl => [Hle _ Hv|Hn Hkl].
+    + case (HP k yf Hle Hv) => [x' [Hv' HP']]. exists x'; split_and! => //.
+      case: k Hle {Hv Hv'} HP' => [//|]. eauto using uPred_mono.
+    + have ->: k = S n by lia. move => {Hn Hkl} Hv.
+      case (HP n yf) => [||x' [Hv' HP']]; eauto using cmra_validN_le.
+      case: (cmra_extend_included n (Some yf) x') => [||x'' []];
+      rewrite /= ?(comm _ _ x) ?Some_validN; eauto using cmra_validN_op_r.
+      move => Hv'' Hnx'x''.
+      exists x''; split; first done.
+      by rewrite -Hnx'x''.
+Qed.
+
+Lemma bupd_later `{!CmraSwappable M} P : (|==> ▷ P) ⊢ ▷ |==> P.
+Proof.
+  unseal; split => /= -[//|n] x ? HP k yf Hkl Hv.
+  case: (cmra_extend_included k (Some x) yf) => [||yf' []];
+    rewrite /= ?(comm _ _ x) ?Some_validN //.
+  - by eapply cmra_validN_le; eauto.
+  - move => ? HyfEq.
+    case (HP (S k) yf') => [||x' [Hv' HP']]; eauto.
+    exists x'; rewrite HyfEq; split_and!;
+    eauto using cmra_validN_le.
+Qed.
+
 (** Later *)
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
 Proof.
-- 
GitLab