From 84cd1f6322cd1d4683f3c3a13435c75323ee5315 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 25 Oct 2018 19:13:40 +0200
Subject: [PATCH] Document new fupd+plainly laws.

---
 theories/bi/updates.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 4ffe8d176..775c40330 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -84,12 +84,21 @@ only make sense for affine logics. From the axioms below, one could derive
 [■ P ={E}=∗ P] (see the lemma [fupd_plainly_elim]), which in turn gives
 [True ={E}=∗ emp]. *)
 Class BiFUpdPlainly (PROP : sbi) `{!BiFUpd PROP, !BiPlainly PROP} := {
+  (** When proving a fancy update of a plain proposition, you can also prove it
+  while being allowed to open all invariants. *)
   fupd_plainly_mask_empty E (P : PROP) :
     (|={E,∅}=> ■ P) ⊢ |={E}=> P;
+  (** A strong eliminator (a la modus ponens) for the wand-fancy-update with a
+  plain conclusion: We eliminate [R ={E}=∗ ■ P] by supplying an [R], but we get
+  to keep the [R]. *)
   fupd_plainly_keep_l E (P R : PROP) :
     (R ={E}=∗ ■ P) ∗ R ⊢ |={E}=> P ∗ R;
+  (** Later "almost" commutes with fancy updates over plain propositions. It
+  commutes "almost" because of the â—‡ modality, which is needed in the definition
+  of fancy updates so one can remove laters of timeless propositions. *)
   fupd_plainly_later E (P : PROP) :
     (▷ |={E}=> ■ P) ⊢ |={E}=> ▷ ◇ P;
+  (** Forall quantifiers commute with fancy updates over plain propositions. *)
   fupd_plainly_forall_2 E {A} (Φ : A → PROP) :
     (∀ x, |={E}=> ■ Φ x) ⊢ |={E}=> ∀ x, Φ x
 }.
-- 
GitLab