From df8e3df59431eb646d1c61bebcb197a53618c9fb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Apr 2020 18:08:54 +0200
Subject: [PATCH] Make `_iff` and `_alter` lemmas for invariants consistent.

They follow the pattern of `wp_wand`.
---
 theories/base_logic/lib/cancelable_invariants.v |  7 +++----
 theories/base_logic/lib/invariants.v            | 11 +++++------
 theories/base_logic/lib/na_invariants.v         |  6 +++---
 3 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 6eb3ef024..234123b57 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -53,11 +53,10 @@ Section proofs.
     iDestruct (cinv_own_valid with "H1 H2") as %[]%(exclusive_l 1%Qp).
   Qed.
 
-  Lemma cinv_iff N γ P P' :
-    ▷ □ (P ↔ P') -∗ cinv N γ P -∗ cinv N γ P'.
+  Lemma cinv_iff N γ P Q : cinv N γ P -∗ ▷ □ (P ↔ Q) -∗ cinv N γ Q.
   Proof.
-    iIntros "#HP". iApply inv_iff. iIntros "!> !>".
-    iSplit; iIntros "[?|$]"; iLeft; by iApply "HP".
+    iIntros "HI #HPQ". iApply (inv_iff with "HI"). iIntros "!> !>".
+    iSplit; iIntros "[?|$]"; iLeft; by iApply "HPQ".
   Qed.
 
   (*** Allocation rules. *)
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index c8e996fa2..a1af8026d 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -97,18 +97,17 @@ Section inv.
   Global Instance inv_persistent N P : Persistent (inv N P).
   Proof. rewrite inv_eq. apply _. Qed.
 
-  Lemma inv_alter N P Q:
-    inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
+  Lemma inv_alter N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
   Proof.
-    rewrite inv_eq. iIntros "#HI #Acc !>" (E H).
+    rewrite inv_eq. iIntros "#HI #HPQ !>" (E H).
     iMod ("HI" $! E H) as "[HP Hclose]".
-    iDestruct ("Acc" with "HP") as "[$ HQP]".
+    iDestruct ("HPQ" with "HP") as "[$ HQP]".
     iIntros "!> HQ". iApply "Hclose". iApply "HQP". done.
   Qed.
 
-  Lemma inv_iff N P Q : ▷ □ (P ↔ Q) -∗ inv N P -∗ inv N Q.
+  Lemma inv_iff N P Q : inv N P -∗ ▷ □ (P ↔ Q) -∗ inv N Q.
   Proof.
-    iIntros "#HPQ #HI". iApply (inv_alter with "HI").
+    iIntros "#HI #HPQ". iApply (inv_alter with "HI").
     iIntros "!> !> HP". iSplitL "HP".
     - by iApply "HPQ".
     - iIntros "HQ". by iApply "HPQ".
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 25c749dad..00d4452b8 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -43,10 +43,10 @@ Section proofs.
   Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
   Proof. rewrite /na_inv; apply _. Qed.
 
-  Lemma na_inv_iff p N P Q : ▷ □ (P ↔ Q) -∗ na_inv p N P -∗ na_inv p N Q.
+  Lemma na_inv_iff p N P Q : na_inv p N P -∗ ▷ □ (P ↔ Q) -∗ na_inv p N Q.
   Proof.
-    iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
-    iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
+    iIntros "HI #HPQ". rewrite /na_inv. iDestruct "HI" as (i ?) "HI".
+    iExists i. iSplit; first done. iApply (inv_iff with "HI").
     iIntros "!> !>".
     iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
   Qed.
-- 
GitLab