Remove dependency of fancy updates on the program language.

_CoqProject

@@ -87,7 +87,6 @@ program_logic/sts.v
 program_logic/namespaces.v
 program_logic/boxes.v
 program_logic/counter_examples.v
-program_logic/iris.v
 program_logic/thread_local.v
 program_logic/cancelable_invariants.v
 heap_lang/lang.v

heap_lang/adequacy.v

@@ -11,7 +11,7 @@ Class heapPreG Σ := HeapPreG {
 }.
 
 Definition heapΣ : gFunctors :=
-  #[irisΣ heap_lang; authΣ heapUR].
+  #[irisΣ state; authΣ heapUR].
 Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
 Proof. intros [? ?]%subG_inv. split; apply _. Qed.
 

program_logic/adequacy.v

@@ -5,6 +5,62 @@ From iris.program_logic Require Import wsat.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
+(* Global functor setup *)
+Definition invΣ : gFunctors :=
+  #[GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
+    GFunctor (constRF coPset_disjUR);
+    GFunctor (constRF (gset_disjUR positive))].
+
+Class invPreG (Σ : gFunctors) : Set := WsatPreG {
+  inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+  enabled_inPreG :> inG Σ coPset_disjR;
+  disabled_inPreG :> inG Σ (gset_disjR positive);
+}.
+
+Instance subG_invΣ {Σ} : subG invΣ Σ → invPreG Σ.
+Proof.
+  intros [?%subG_inG [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv; by constructor.
+Qed.
+
+
+Definition irisΣ (Λstate : Type) : gFunctors :=
+  #[invΣ;
+    GFunctor (constRF (authUR (optionUR (exclR (leibnizC Λstate)))))].
+
+Class irisPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
+  inv_inG :> invPreG Σ;
+  state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))))
+}.
+Notation irisPreG Λ Σ := (irisPreG' (state Λ) Σ).
+
+Instance subG_irisΣ {Λstate Σ} : subG (irisΣ Λstate) Σ → irisPreG' Λstate Σ.
+Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
+
+
+(* Allocation *)
+Lemma wsat_alloc `{invPreG Σ} : True ==★ ∃ _ : invG Σ, wsat ★ ownE ⊤.
+Proof.
+  iIntros.
+  iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
+  iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
+  iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
+  iModIntro; iExists (WsatG _ _ _ _ γI γE γD).
+  rewrite /wsat /ownE; iFrame.
+  iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
+Qed.
+
+Lemma iris_alloc `{irisPreG' Λstate Σ} σ :
+  True ==★ ∃ _ : irisG' Λstate Σ, wsat ★ ownE ⊤ ★ ownP_auth σ ★ ownP σ.
+Proof.
+  iIntros.
+  iMod wsat_alloc as (?) "[Hws HE]".
+  iMod (own_alloc (● (Excl' (σ:leibnizC Λstate)) ⋅ ◯ (Excl' σ)))
+    as (γσ) "[Hσ Hσ']"; first done.
+  iModIntro; iExists (IrisG _ _ _ _ γσ). rewrite /ownP_auth /ownP; iFrame.
+Qed.
+
+
+(* Program logic adequacy *)
 Record adequate {Λ} (e1 : expr Λ) (σ1 : state Λ) (φ : val Λ → Prop) := {
   adequate_result t2 σ2 v2 :
    rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2;

program_logic/auth.v

@@ -16,7 +16,7 @@ Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A
 Proof. intros ?%subG_inG ?. by split. Qed.
 
 Section definitions.
-  Context `{irisG Λ Σ, authG Σ A} {T : Type} (γ : gname).
+  Context `{invG Σ, authG Σ A} {T : Type} (γ : gname).
 
   Definition auth_own (a : A) : iProp Σ :=
     own γ (◯ a).
@@ -57,10 +57,10 @@ End definitions.
 Typeclasses Opaque auth_own auth_inv auth_ctx.
 Instance: Params (@auth_own) 4.
 Instance: Params (@auth_inv) 5.
-Instance: Params (@auth_ctx) 8.
+Instance: Params (@auth_ctx) 7.
 
 Section auth.
-  Context `{irisG Λ Σ, authG Σ A}.
+  Context `{invG Σ, authG Σ A}.
   Context {T : Type} `{!Inhabited T}.
   Context (f : T → A) (φ : T → iProp Σ).
   Implicit Types N : namespace.
@@ -146,4 +146,4 @@ Section auth.
   Qed.
 End auth.
 
-Arguments auth_open {_ _ _ _} [_] {_} [_] _ _ _ _ _ _ _.
+Arguments auth_open {_ _ _} [_] {_} [_] _ _ _ _ _ _ _.

program_logic/boxes.v

@@ -11,7 +11,7 @@ Class boxG Σ :=
     (optionR (agreeR (laterC (iPreProp Σ))))).
 
 Section box_defs.
-  Context `{irisG Λ Σ, boxG Σ} (N : namespace).
+  Context `{invG Σ, boxG Σ} (N : namespace).
 
   Definition slice_name := gname.
 
@@ -34,14 +34,13 @@ Section box_defs.
                          inv N (slice_inv γ (Φ γ)))%I.
 End box_defs.
 
-Instance: Params (@box_own_auth) 5.
-Instance: Params (@box_own_prop) 5.
-Instance: Params (@slice_inv) 5.
-Instance: Params (@slice) 6.
-Instance: Params (@box) 6.
+Instance: Params (@box_own_prop) 3.
+Instance: Params (@slice_inv) 3.
+Instance: Params (@slice) 5.
+Instance: Params (@box) 5.
 
 Section box.
-Context `{irisG Λ Σ, boxG Σ} (N : namespace).
+Context `{invG Σ, boxG Σ} (N : namespace).
 Implicit Types P Q : iProp Σ.
 
 Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).

program_logic/cancelable_invariants.v

@@ -6,7 +6,7 @@ Import uPred.
 Class cinvG Σ := cinv_inG :> inG Σ fracR.
 
 Section defs.
-  Context `{irisG Λ Σ, cinvG Σ}.
+  Context `{invG Σ, cinvG Σ}.
 
   Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
 
@@ -14,11 +14,11 @@ Section defs.
     inv N (P ∨ cinv_own γ 1%Qp)%I.
 End defs.
 
-Instance: Params (@cinv) 6.
+Instance: Params (@cinv) 5.
 Typeclasses Opaque cinv_own cinv.
 
 Section proofs.
-  Context `{irisG Λ Σ, cinvG Σ}.
+  Context `{invG Σ, cinvG Σ}.
 
   Global Instance cinv_own_timeless γ p : TimelessP (cinv_own γ p).
   Proof. rewrite /cinv_own; apply _. Qed.

program_logic/fancy_updates.v

-From iris.program_logic Require Export iris.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Export coPset.
 From iris.program_logic Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics classes.
+Export invG.
 Import uPred.
 
-Program Definition fupd_def `{irisG Λ Σ}
+Program Definition fupd_def `{invG Σ}
     (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   (wsat ★ ownE E1 ==★ ◇ (wsat ★ ownE E2 ★ P))%I.
 Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed.
 Definition fupd := proj1_sig fupd_aux.
 Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux.
-Arguments fupd {_ _ _} _ _ _%I.
-Instance: Params (@fupd) 5.
+Arguments fupd {_ _} _ _ _%I.
+Instance: Params (@fupd) 4.
 
 Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
   (at level 99, E1, E2 at level 50, Q at level 200,
@@ -46,12 +48,12 @@ Notation "P ={ E }▷=★ Q" := (P ={E,E}▷=★ Q)%I
    format "P  ={ E }▷=★  Q") : uPred_scope.
 
 Section fupd.
-Context `{irisG Λ Σ}.
+Context `{invG Σ}.
 Implicit Types P Q : iProp Σ.
 
-Global Instance fupd_ne E1 E2 n : Proper (dist n ==> dist n) (@fupd Λ Σ _ E1 E2).
+Global Instance fupd_ne E1 E2 n : Proper (dist n ==> dist n) (@fupd Σ _ E1 E2).
 Proof. rewrite fupd_eq. solve_proper. Qed.
-Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (@fupd Λ Σ _ E1 E2).
+Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (@fupd Σ _ E1 E2).
 Proof. apply ne_proper, _. Qed.
 
 Lemma fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
@@ -92,10 +94,10 @@ Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P) ★ Q ={E1,E2}=★ P ★ Q.
 Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.
 
 (** * Derived rules *)
-Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Λ Σ _ E1 E2).
+Global Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (@fupd Σ _ E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
 Global Instance fupd_flip_mono' E1 E2 :
-  Proper (flip (⊢) ==> flip (⊢)) (@fupd Λ Σ _ E1 E2).
+  Proper (flip (⊢) ==> flip (⊢)) (@fupd Σ _ E1 E2).
 Proof. intros P Q; apply fupd_mono. Qed.
 
 Lemma fupd_intro E P : P ={E}=★ P.
@@ -148,7 +150,7 @@ End fupd.
 
 (** Proofmode class instances *)
 Section proofmode_classes.
-  Context `{irisG Λ Σ}.
+  Context `{invG Σ}.
   Implicit Types P Q : iProp Σ.
 
   Global Instance from_pure_fupd E P φ : FromPure P φ → FromPure (|={E}=> P) φ.

program_logic/invariants.v

@@ -6,20 +6,19 @@ From iris.proofmode Require Import tactics coq_tactics intro_patterns.
 Import uPred.
 
 (** Derived forms and lemmas about them. *)
-Definition inv_def `{irisG Λ Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   (∃ i, ■ (i ∈ nclose N) ∧ ownI i P)%I.
 Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
-Definition inv {Λ Σ i} := proj1_sig inv_aux Λ Σ i.
+Definition inv {Σ i} := proj1_sig inv_aux Σ i.
 Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
-Instance: Params (@inv) 4.
+Instance: Params (@inv) 3.
 Typeclasses Opaque inv.
 
 Section inv.
-Context `{irisG Λ Σ}.
+Context `{invG Σ}.
 Implicit Types i : positive.
 Implicit Types N : namespace.
 Implicit Types P Q R : iProp Σ.
-Implicit Types Φ : val Λ → iProp Σ.
 
 Global Instance inv_contractive N : Contractive (inv N).
 Proof.

program_logic/iris.v

-From iris.base_logic Require Export lib.own.
-From iris.program_logic Require Export language.
-From iris.prelude Require Export coPset.
-From iris.algebra Require Import gmap auth agree gset coPset.
-
-Class irisPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
-  state_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
-  invariant_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
-  enabled_inG :> inG Σ coPset_disjR;
-  disabled_inG :> inG Σ (gset_disjR positive);
-}.
-
-Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG {
-  iris_pre_inG :> irisPreG Λ Σ;
-  state_name : gname;
-  invariant_name : gname;
-  enabled_name : gname;
-  disabled_name : gname;
-}.
-
-Definition irisΣ (Λ : language) : gFunctors :=
-  #[GFunctor (constRF (authUR (optionUR (exclR (stateC Λ)))));
-    GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
-    GFunctor (constRF coPset_disjUR);
-    GFunctor (constRF (gset_disjUR positive))].
-
-Instance subG_irisΣ {Σ Λ} : subG (irisΣ Λ) Σ → irisPreG Λ Σ.
-Proof.
-  intros [?%subG_inG [?%subG_inG
-    [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv]%subG_inv; by constructor.
-Qed.

program_logic/sts.v

@@ -15,7 +15,7 @@ Instance subG_stsΣ Σ sts :
 Proof. intros ?%subG_inG ?. by split. Qed.
 
 Section definitions.
-  Context `{irisG Λ Σ, stsG Σ sts} (γ : gname).
+  Context `{invG Σ, stsG Σ sts} (γ : gname).
 
   Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
     own γ (sts_frag S T).
@@ -51,13 +51,13 @@ Section definitions.
 End definitions.
 
 Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx.
-Instance: Params (@sts_inv) 5.
-Instance: Params (@sts_ownS) 5.
-Instance: Params (@sts_own) 6.
+Instance: Params (@sts_inv) 4.
+Instance: Params (@sts_ownS) 4.
+Instance: Params (@sts_own) 5.
 Instance: Params (@sts_ctx) 6.
 
 Section sts.
-  Context `{irisG Λ Σ, stsG Σ sts} (φ : sts.state sts → iProp Σ).
+  Context `{invG Σ, stsG Σ sts} (φ : sts.state sts → iProp Σ).
   Implicit Types N : namespace.
   Implicit Types P Q R : iProp Σ.
   Implicit Types γ : gname.
@@ -115,7 +115,7 @@ Section sts.
       ■ sts.frame_steps T s0 s ★ ▷ φ s ★ ∀ s' T',
       ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E}=★ ▷ sts_inv γ φ ★ sts_own γ s' T'.
   Proof. by apply sts_accS. Qed.
-    
+
   Lemma sts_openS E N γ S T :
     nclose N ⊆ E →
     sts_ctx γ N φ ★ sts_ownS γ S T ={E,E∖N}=★ ∃ s,

program_logic/thread_local.v

@@ -10,7 +10,7 @@ Class thread_localG Σ :=
   tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
 
 Section defs.
-  Context `{irisG Λ Σ, thread_localG Σ}.
+  Context `{invG Σ, thread_localG Σ}.
 
   Definition tl_own (tid : thread_id) (E : coPset) : iProp Σ :=
     own tid (CoPset E, ∅).
@@ -20,11 +20,11 @@ Section defs.
           inv tlN (P ★ own tid (∅, GSet {[i]}) ∨ tl_own tid {[i]}))%I.
 End defs.
 
-Instance: Params (@tl_inv) 4.
+Instance: Params (@tl_inv) 3.
 Typeclasses Opaque tl_own tl_inv.
 
 Section proofs.
-  Context `{irisG Λ Σ, thread_localG Σ}.
+  Context `{invG Σ, thread_localG Σ}.
 
   Global Instance tl_own_timeless tid E : TimelessP (tl_own tid E).
   Proof. rewrite /tl_own; apply _. Qed.

program_logic/viewshifts.v

 From iris.program_logic Require Export invariants.
 From iris.proofmode Require Import tactics.
 
-Definition vs `{irisG Λ Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
+Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P -★ |={E1,E2}=> Q))%I.
-Arguments vs {_ _ _} _ _ _%I _%I.
+Arguments vs {_ _} _ _ _%I _%I.
 
-Instance: Params (@vs) 5.
+Instance: Params (@vs) 4.
 Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
   (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : uPred_scope.
@@ -21,7 +21,7 @@ Notation "P ={ E }=> Q" := (True ⊢ P ={E}=> Q)%I
    format "P  ={ E }=>  Q") : C_scope.
 
 Section vs.
-Context `{irisG Λ Σ}.
+Context `{invG Σ}.
 Implicit Types P Q R : iProp Σ.
 Implicit Types N : namespace.
 

program_logic/weakestpre.v

-From iris.program_logic Require Export fancy_updates.
-From iris.program_logic Require Import wsat.
+From iris.program_logic Require Export fancy_updates language.
 From iris.base_logic Require Import big_op.
-From iris.prelude Require Export coPset.
 From iris.proofmode Require Import tactics classes.
+From iris.algebra Require Import auth.
 Import uPred.
 
+Class irisG' (Λstate : Type) (Σ : gFunctors) : Set := IrisG {
+  iris_invG :> invG Σ;
+  state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
+  state_name : gname;
+}.
+Notation irisG Λ Σ := (irisG' (state Λ) Σ).
+
+Definition ownP `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
+  own state_name (◯ (Excl' σ)).
+Typeclasses Opaque ownP.
+Instance: Params (@ownP) 3.
+
+Definition ownP_auth `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
+  own state_name (● (Excl' (σ:leibnizC Λstate))).
+Typeclasses Opaque ownP_auth.
+Instance: Params (@ownP_auth) 4.
+
 Definition wp_pre `{irisG Λ Σ}
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ, (
@@ -96,6 +112,24 @@ Implicit Types Φ : val Λ → iProp Σ.
 Implicit Types v : val Λ.
 Implicit Types e : expr Λ.
 
+(* Physical state *)
+Lemma ownP_twice σ1 σ2 : ownP σ1 ★ ownP σ2 ⊢ False.
+Proof. rewrite /ownP own_valid_2. by iIntros (?). Qed.
+Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
+Proof. rewrite /ownP; apply _. Qed.
+
+Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ★ ownP σ2 ⊢ σ1 = σ2.
+Proof.
+  rewrite /ownP /ownP_auth own_valid_2 -auth_both_op.
+  by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
+Qed.
+Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 ==★ ownP_auth σ2 ★ ownP σ2.
+Proof.
+  rewrite /ownP -!own_op.
+  by apply own_update, auth_update, option_local_update, exclusive_local_update.
+Qed.
+
+(* Weakest pre *)
 Lemma wp_unfold E e Φ : WP e @ E {{ Φ }} ⊣⊢ wp_pre wp E e Φ.
 Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.
 

program_logic/wsat.v

-From iris.program_logic Require Export iris.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 
+Module invG.
+  Class invG (Σ : gFunctors) : Set := WsatG {
+    inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+    enabled_inG :> inG Σ coPset_disjR;
+    disabled_inG :> inG Σ (gset_disjR positive);
+    invariant_name : gname;
+    enabled_name : gname;
+    disabled_name : gname;
+  }.
+End invG.
+Import invG.
+
 Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
   to_agree (Next (iProp_unfold P)).
-Definition ownI `{irisG Λ Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (◯ {[ i := invariant_unfold P ]}).
-Arguments ownI {_ _ _} _ _%I.
+Arguments ownI {_ _} _ _%I.
 Typeclasses Opaque ownI.
-Instance: Params (@ownI) 4.
-
-Definition ownP `{irisG Λ Σ} (σ : state Λ) : iProp Σ :=
-  own state_name (◯ (Excl' σ)).
-Typeclasses Opaque ownP.
-Instance: Params (@ownP) 4.
-
-Definition ownP_auth `{irisG Λ Σ} (σ : state Λ) : iProp Σ :=
-  own state_name (● (Excl' σ)).
-Typeclasses Opaque ownP_auth.
-Instance: Params (@ownP_auth) 4.
+Instance: Params (@ownI) 3.
 
-Definition ownE `{irisG Λ Σ} (E : coPset) : iProp Σ :=
+Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
   own enabled_name (CoPset E).
 Typeclasses Opaque ownE.
-Instance: Params (@ownE) 4.
+Instance: Params (@ownE) 3.
 
-Definition ownD `{irisG Λ Σ} (E : gset positive) : iProp Σ :=
+Definition ownD `{invG Σ} (E : gset positive) : iProp Σ :=
   own disabled_name (GSet E).
 Typeclasses Opaque ownD.
-Instance: Params (@ownD) 4.
+Instance: Params (@ownD) 3.
 
-Definition wsat `{irisG Λ Σ} : iProp Σ :=
+Definition wsat `{invG Σ} : iProp Σ :=
   (∃ I : gmap positive (iProp Σ),
     own invariant_name (● (invariant_unfold <$> I : gmap _ _)) ★
     [★ map] i ↦ Q ∈ I, ▷ Q ★ ownD {[i]} ∨ ownE {[i]})%I.
 
-Section ownership.
-Context `{irisG Λ Σ}.
-Implicit Types σ : state Λ.
+Section wsat.
+Context `{invG Σ}.
 Implicit Types P : iProp Σ.
 
-(* Allocation *)
-Lemma iris_alloc `{irisPreG Λ Σ} σ :
-  True ==★ ∃ _ : irisG Λ Σ, wsat ★ ownE ⊤ ★ ownP_auth σ ★ ownP σ.
-Proof.
-  iIntros.
-  iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσ']"; first done.
-  iMod (own_alloc (● (∅ : gmap _ _))) as (γI) "HI"; first done.
-  iMod (own_alloc (CoPset ⊤)) as (γE) "HE"; first done.
-  iMod (own_alloc (GSet ∅)) as (γD) "HD"; first done.
-  iModIntro; iExists (IrisG _ _ _ γσ γI γE γD).
-  rewrite /wsat /ownE /ownP_auth /ownP; iFrame.
-  iExists ∅. rewrite fmap_empty big_sepM_empty. by iFrame.
-Qed.
-
-(* Physical state *)
-Lemma ownP_twice σ1 σ2 : ownP σ1 ★ ownP σ2 ⊢ False.
-Proof. rewrite /ownP own_valid_2. by iIntros (?). Qed.
-Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ _ σ).
-Proof. rewrite /ownP; apply _. Qed.
-
-Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ★ ownP σ2 ⊢ σ1 = σ2.
-Proof.
-  rewrite /ownP /ownP_auth own_valid_2 -auth_both_op.
-  by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
-Qed.
-Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 ==★ ownP_auth σ2 ★ ownP σ2.
-Proof.
-  rewrite /ownP -!own_op.
-  by apply own_update, auth_update, option_local_update, exclusive_local_update.
-Qed.
-
 (* Invariants *)
-Global Instance ownI_contractive i : Contractive (@ownI Λ Σ _ i).
+Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
 Proof.
   intros n P Q HPQ. rewrite /ownI /invariant_unfold. do 4 f_equiv.
   apply Next_contractive=> j ?; by rewrite (HPQ j).
@@ -111,7 +82,7 @@ Qed.
 Lemma ownD_singleton_twice i : ownD {[i]} ★ ownD {[i]} ⊢ False.
 Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.
 
-Lemma invariant_lookup `{irisG Λ Σ} (I : gmap positive (iProp Σ)) i P :
+Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
   own invariant_name (● (invariant_unfold <$> I : gmap _ _)) ★
   own invariant_name (◯ {[i := invariant_unfold P]}) ⊢
   ∃ Q, I !! i = Some Q ★ ▷ (Q ≡ P).
@@ -171,4 +142,4 @@ Proof.
   iApply (big_sepM_insert _ I); first done.
   iFrame "HI". iLeft. by rewrite /ownD; iFrame.
 Qed.
-End ownership.
+End wsat.

tests/proofmode.v

@@ -85,7 +85,7 @@ Lemma demo_7 (M : ucmraT) (P Q1 Q2 : uPred M) : P ★ (Q1 ∧ Q2) ⊢ P ★ Q1.
 Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
 
 Section iris.