From 1244bcfbf13fd207e11f93ed968e8c0cb93fba24 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 25 Jun 2018 18:27:51 +0200
Subject: [PATCH] prove a variant of wp_invariance that does not require
 finding fupd_intro_mask'

---
 theories/program_logic/adequacy.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index b7e9d42c7..9d5a3bcee 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -1,3 +1,4 @@
+From stdpp Require Import namespaces.
 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic.lib Require Import wsat.
@@ -203,3 +204,20 @@ Proof.
   iDestruct "Hwp" as (Istate) "(HIstate & Hwp & Hclose)".
   iApply (@wptp_invariance _ _ (IrisG _ _ Hinv Istate)); eauto with iFrame.
 Qed.
+
+(* An equivalent version that does not require finding [fupd_intro_mask'], but
+can be confusing to use. *)
+Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
+  (∀ `{Hinv : invG Σ},
+     (|={⊤}=> ∃ stateI : state Λ → iProp Σ,
+       let _ : irisG Λ Σ := IrisG _ _ Hinv stateI in
+       stateI σ1 ∗ WP e @ s; ⊤ {{ _, True }} ∗ (stateI σ2 -∗ ∃ E, |={⊤,E}=> ⌜φ⌝))%I) →
+  rtc step ([e], σ1) (t2, σ2) →
+  φ.
+Proof.
+  intros Hwp. eapply wp_invariance; first done.
+  intros Hinv. iMod (Hwp Hinv) as (stateI) "(? & ? & Hφ)".
+  iModIntro. iExists stateI. iFrame. iIntros "Hσ".
+  iDestruct ("Hφ" with "Hσ") as (E) ">Hφ".
+  iMod (fupd_intro_mask') as "_"; last by iModIntro. solve_ndisj.
+Qed.
-- 
GitLab