move the reduction control of the proofmode to its own file and tweak it

* move PROP-envs definitions to environments.v so that we can control them without pulling in coq_tactics
* use reduction-controlled `pm_default` for proofmode accessors

_CoqProject

@@ -99,6 +99,7 @@ theories/proofmode/tokens.v
 theories/proofmode/coq_tactics.v
 theories/proofmode/ltac_tactics.v
 theories/proofmode/environments.v
+theories/proofmode/reduction.v
 theories/proofmode/intro_patterns.v
 theories/proofmode/spec_patterns.v
 theories/proofmode/sel_patterns.v

tests/proofmode_iris.ref

@@ -103,7 +103,7 @@
   --------------------------------------□
   "Hown1" : na_own t E1
   "Hown2" : na_own t (E2 ∖ ↑N)
-  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ id (na_own t E2)
+  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
   --------------------------------------∗
   |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
   

theories/bi/lib/atomic.v

 From iris.bi Require Export bi updates.
 From iris.bi.lib Require Import fixpoint laterable.
 From stdpp Require Import coPset namespaces.
-From iris.proofmode Require Import coq_tactics tactics.
+From iris.proofmode Require Import coq_tactics tactics reduction.
 Set Default Proof Using "Type".
 
 (** Conveniently split a conjunction on both assumption and conclusion. *)
@@ -160,8 +160,8 @@ Section lemmas.
   Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X → PROP) γ' α β Pas Φ :
     ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
             (atomic_acc E1 Ei α Pas β Φ)
-            (λ x', atomic_acc E2 Ei α (β' x' ∗ coq_tactics.maybe_wand (γ' x') Pas)%I β
-                (λ x y, β' x' ∗ coq_tactics.maybe_wand (γ' x') (Φ x y)))%I.
+            (λ x', atomic_acc E2 Ei α (β' x' ∗ pm_maybe_wand (γ' x') Pas)%I β
+                (λ x y, β' x' ∗ pm_maybe_wand (γ' x') (Φ x y)))%I.
   Proof.
     rewrite /ElimAcc.
     (* FIXME: Is there any way to prevent maybe_wand from unfolding?
@@ -281,5 +281,5 @@ Tactic Notation "iAuIntro" :=
   iStartProof; eapply tac_aupd_intro; [
     iSolveTC || fail "iAuIntro: emp is not timeless"
   | iSolveTC || fail "iAuIntro: not all spatial assumptions are laterable"
-  | (* P = ...: make the P pretty *) env_reflexivity
+  | (* P = ...: make the P pretty *) pm_reflexivity
   | (* the new proof mode goal *) ].

theories/heap_lang/proofmode.v

 From iris.program_logic Require Export weakestpre total_weakestpre.
-From iris.proofmode Require Import coq_tactics.
+From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
 From iris.heap_lang Require Import notation.
@@ -319,7 +319,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   let finish _ :=
     first [intros l | fail 1 "wp_alloc:" l "not fresh"];
       eexists; split;
-        [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
+        [pm_reflexivity || fail "wp_alloc:" H "not fresh"
         |wp_expr_simpl; try wp_value_head] in
   iStartProof;
   lazymatch goal with
@@ -379,7 +379,7 @@ Tactic Notation "wp_store" :=
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [iSolveTC
     |solve_mapsto ()
-    |env_cbv; reflexivity
+    |pm_reflexivity
     |finish ()]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
@@ -387,7 +387,7 @@ Tactic Notation "wp_store" :=
          eapply (tac_twp_store _ _ _ _ _ K); [iSolveTC|..])
       |fail 1 "wp_store: cannot find 'Store' in" e];
     [solve_mapsto ()
-    |env_cbv; reflexivity
+    |pm_reflexivity
     |finish ()]
   | _ => fail "wp_store: not a 'wp'"
   end.
@@ -432,7 +432,7 @@ Tactic Notation "wp_cas_suc" :=
     [iSolveTC
     |solve_mapsto ()
     |try congruence
-    |env_cbv; reflexivity
+    |pm_reflexivity
     |simpl; try wp_value_head]
   | |- envs_entails _ (twp ?E ?e ?Q) =>
     first
@@ -441,7 +441,7 @@ Tactic Notation "wp_cas_suc" :=
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
     [solve_mapsto ()
     |try congruence
-    |env_cbv; reflexivity
+    |pm_reflexivity
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_suc: not a 'wp'"
   end.
@@ -459,7 +459,7 @@ Tactic Notation "wp_faa" :=
       |fail 1 "wp_faa: cannot find 'CAS' in" e];
     [iSolveTC
     |solve_mapsto ()
-    |env_cbv; reflexivity
+    |pm_reflexivity
     |wp_expr_simpl; try wp_value_head]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
@@ -467,7 +467,7 @@ Tactic Notation "wp_faa" :=
          eapply (tac_twp_faa _ _ _ _ _ K); [iSolveTC|..])
       |fail 1 "wp_faa: cannot find 'CAS' in" e];
     [solve_mapsto ()
-    |env_cbv; reflexivity
+    |pm_reflexivity
     |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_faa: not a 'wp'"
   end.

theories/program_logic/weakestpre.v

@@ -392,9 +392,9 @@ Section proofmode_classes.
     Atomic (stuckness_to_atomicity s) e →
     ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
             α β γ (WP e @ s; E1 {{ Φ }})
-            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
   Proof.
-    intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+    intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
@@ -403,9 +403,9 @@ Section proofmode_classes.
   Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
     ElimAcc (X:=X) (fupd E E) (fupd E E)
             α β γ (WP e @ s; E {{ Φ }})
-            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
+            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
   Proof.
-    rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+    rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply wp_fupd.
     iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".

theories/proofmode/base.v

@@ -3,6 +3,8 @@ From iris.algebra Require Export base.
 From Coq Require Import Ascii.
 Set Default Proof Using "Type".
 
+(** * Utility definitions used by the proofmode *)
+
 (* Directions of rewrites *)
 Inductive direction := Left | Right.
 
@@ -84,11 +86,18 @@ Qed.
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
 
-(** Copies of some definitions so we can control their unfolding *)
-Definition option_bind {A B} (f : A → option B) (mx : option A) : option B :=
+(** Copies of some [option] combinators for better reduction control. *)
+Definition pm_option_bind {A B} (f : A → option B) (mx : option A) : option B :=
   match mx with Some x => f x | None => None end.
-Arguments option_bind {_ _} _ !_ / : assert.
+Arguments pm_option_bind {_ _} _ !_ /.
 
-Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
+Definition pm_from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
   match mx with None => y | Some x => f x end.
-Arguments from_option {_ _} _ _ !_ / : assert.
+Arguments pm_from_option {_ _} _ _ !_ /.
+
+Definition pm_option_fun {A B} (f : option (A → B)) (x : A) : option B :=
+  match f with None => None | Some f => Some (f x) end.
+Arguments pm_option_fun {_ _} !_ _ /.
+
+(* Can't write [id] here as that would not reduce. *)
+Notation pm_default := (pm_from_option (λ x, x)).

theories/proofmode/class_instances_bi.v

 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes ltac_tactics.
+From iris.proofmode Require Import base modality_instances classes ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
 Section bi_instances.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
+Implicit Types mP : option PROP.
 
 (** AsEmpValid *)
 Global Instance as_emp_valid_emp_valid {PROP : bi} (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0.
@@ -999,7 +1000,8 @@ Global Instance elim_inv_acc_with_close {X : Type}
   IntoAcc Pinv φ1 Pin M1 M2 α β mγ →
   (∀ R, ElimModal φ2 false false (M1 R) R Q Q') →
   ElimInv (X:=X) (φ1 ∧ φ2) Pinv Pin
-          α (Some (λ x, β x -∗ M2 (proofmode.base.from_option id emp (mγ x))))%I
+          α
+          (Some (λ x, β x -∗ M2 (pm_default emp (mγ x))))%I
           Q (λ _, Q').
 Proof.
   rewrite /ElimAcc /IntoAcc /ElimInv.

theories/proofmode/class_instances_sbi.v

 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes class_instances_bi ltac_tactics.
+From iris.proofmode Require Import modality_instances classes class_instances_bi coq_tactics ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -499,9 +499,9 @@ Global Instance elim_acc_fupd `{BiFUpd PROP} {X} E1 E2 E α β mγ Q :
   (* FIXME: Why %I? ElimAcc sets the right scopes! *)
   ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
           (|={E1,E}=> Q)
-          (λ x, |={E2}=> β x ∗ (coq_tactics.maybe_wand (mγ x) (|={E1,E}=> Q)))%I.
+          (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q)))%I.
 Proof.
-  rewrite /ElimAcc. setoid_rewrite coq_tactics.maybe_wand_sound.
+  rewrite /ElimAcc. setoid_rewrite pm_maybe_wand_sound.
   iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
   iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
   iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".

theories/proofmode/classes.v

 From iris.bi Require Export bi.
+From iris.proofmode Require Import base.
 From iris.proofmode Require Export modalities.
 From stdpp Require Import namespaces.
 Set Default Proof Using "Type".
@@ -526,7 +527,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
     instances to recognize the [emp] case and make it look nicer. *)
 Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
            (α β : X → PROP) (mγ : X → option PROP) : PROP :=
-  M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.
+  M1 (∃ x, α x ∗ (β x -∗ M2 (pm_default emp (mγ x))))%I.
 
 (* Typeclass for assertions around which accessors can be elliminated.
    Inputs: [Q], [E1], [E2], [α], [β], [γ]
@@ -582,7 +583,7 @@ Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
 Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
       (Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
       (Q : PROP) (Q' : X → PROP) :=
-  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
+  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (pm_default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
 Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
 Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
 Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.

theories/proofmode/coq_tactics.v

@@ -7,140 +7,7 @@ Import env_notations.
 
 Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
-Record envs (PROP : bi) :=
-  Envs { env_intuitionistic : env PROP; env_spatial : env PROP; env_counter : positive }.
-Add Printing Constructor envs.
-Arguments Envs {_} _ _ _.
-Arguments env_intuitionistic {_} _.
-Arguments env_spatial {_} _.
-Arguments env_counter {_} _.
-
-Record envs_wf {PROP} (Δ : envs PROP) := {
-  env_intuitionistic_valid : env_wf (env_intuitionistic Δ);
-  env_spatial_valid : env_wf (env_spatial Δ);
-  envs_disjoint i : env_intuitionistic Δ !! i = None ∨ env_spatial Δ !! i = None
-}.
-
-Definition of_envs {PROP} (Δ : envs PROP) : PROP :=
-  (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
-Instance: Params (@of_envs) 1.
-Arguments of_envs : simpl never.
-
-(* We seal [envs_entails], so that it does not get unfolded by the
-   proofmode's own tactics, such as [iIntros (?)]. *)
-Definition envs_entails_aux : seal (λ PROP (Δ : envs PROP) (Q : PROP), (of_envs Δ ⊢ Q)).
-Proof. by eexists. Qed.
-Definition envs_entails := envs_entails_aux.(unseal).
-Definition envs_entails_eq : envs_entails = _ := envs_entails_aux.(seal_eq).
-Arguments envs_entails {PROP} Δ Q%I : rename.
-Instance: Params (@envs_entails) 1.
-
-Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
-  env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
-  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
-}.
-
-Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
-  env_dom (env_intuitionistic Δ) ++ env_dom (env_spatial Δ).
-
-Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
-  let (Γp,Γs,n) := Δ in
-  match env_lookup i Γp with
-  | Some P => Some (true, P)
-  | None => P ← env_lookup i Γs; Some (false, P)
-  end.
-
-Definition envs_delete {PROP} (remove_persistent : bool)
-    (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
-  let (Γp,Γs,n) := Δ in
-  match p with
-  | true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs n
-  | false => Envs Γp (env_delete i Γs) n
-  end.
-
-Definition envs_lookup_delete {PROP} (remove_persistent : bool)
-    (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
-  let (Γp,Γs,n) := Δ in
-  match env_lookup_delete i Γp with
-  | Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs n)
-  | None => ''(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
-  end.
-
-Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
-    (js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
-  match js with
-  | [] => Some (true, [], Δ)
-  | j :: js =>
-     ''(p,P,Δ') ← envs_lookup_delete remove_persistent j Δ;
-     ''(q,Hs,Δ'') ← envs_lookup_delete_list remove_persistent js Δ';
-     Some ((p:bool) && q, P :: Hs, Δ'')
-  end.
-
-Definition envs_snoc {PROP} (Δ : envs PROP)
-    (p : bool) (j : ident) (P : PROP) : envs PROP :=
-  let (Γp,Γs,n) := Δ in
-  if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.
-
-Definition envs_app {PROP : bi} (p : bool)
-    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
-  let (Γp,Γs,n) := Δ in
-  match p with
-  | true => _ ← env_app Γ Γs; Γp' ← env_app Γ Γp; Some (Envs Γp' Γs n)
-  | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs' n)
-  end.
-
-Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
-    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
-  let (Γp,Γs,n) := Δ in
-  match p with
-  | true => _ ← env_app Γ Γs; Γp' ← env_replace i Γ Γp; Some (Envs Γp' Γs n)
-  | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs' n)
-  end.
-
-Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
-    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
-  if Bool.eqb p q then envs_simple_replace i p Γ Δ
-  else envs_app q Γ (envs_delete true i p Δ).
-
-Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
-  if env_spatial Δ is Enil then true else false.
-
-Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs (env_intuitionistic Δ) Enil (env_counter Δ).
-
-Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs Enil (env_spatial Δ) (env_counter Δ).
-
-Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
-  Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos.succ (env_counter Δ)).
-
-Fixpoint envs_split_go {PROP}
-    (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
-  match js with
-  | [] => Some (Δ1, Δ2)
-  | j :: js =>
-     ''(p,P,Δ1') ← envs_lookup_delete true j Δ1;
-     if p : bool then envs_split_go js Δ1 Δ2 else
-     envs_split_go js Δ1' (envs_snoc Δ2 false j P)
-  end.
-(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
-   if [d = Left] then [result = (hyps named js, remaining hyps)] *)
-Definition envs_split {PROP} (d : direction)
-    (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
-  ''(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
-  if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
-
-Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
-  let fix aux Γ acc :=
-    match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P ∗ acc)%I end
-  in
-  match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
-
-Definition maybe_wand {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
-  match mP with
-  | None => Q
-  | Some P => (P -∗ Q)%I
-  end.
+Notation pm_maybe_wand mP Q := (pm_from_option (λ P, P -∗ Q)%I Q%I mP).
 
 (* Coq versions of the tactics *)
 Section bi_tactics.
@@ -343,7 +210,7 @@ Lemma envs_replace_sound' Δ Δ' i p q Γ :
   envs_replace i p q Γ Δ = Some Δ' →
   of_envs (envs_delete true i p Δ) ⊢ (if q then □ [∧] Γ else [∗] Γ) -∗ of_envs Δ'.
 Proof.
-  rewrite /envs_replace; destruct (Bool.eqb _ _) eqn:Hpq.
+  rewrite /envs_replace; destruct (beq _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
   - apply envs_app_sound.
 Qed.
@@ -449,8 +316,8 @@ Proof.
   - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.
 
-Lemma maybe_wand_sound (mP : option PROP) Q :
-  maybe_wand mP Q ⊣⊢ (default emp mP -∗ Q).
+Lemma pm_maybe_wand_sound mP Q :
+  pm_maybe_wand mP Q ⊣⊢ (default emp mP -∗ Q).
 Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
 
 Global Instance envs_Forall2_refl (R : relation PROP) :
@@ -751,7 +618,6 @@ Proof.
   rewrite envs_lookup_sound // envs_split_sound //.
   rewrite (envs_app_singleton_sound Δ2) //; simpl.
   rewrite HP1 into_wand /= -(add_modal P1' P1 Q). cancel [P1'].
-
   apply wand_intro_l. by rewrite assoc !wand_elim_r.
 Qed.
 
@@ -1109,7 +975,10 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X
   φ →
   (∀ R, ∃ Δ'',
     envs_app false (Esnoc Enil j
-            (Pin -∗ (∀ x, Pout x -∗ from_option (λ Pclose, Pclose x -∗ Q' x) (Q' x) Pclose) -∗ R)%I) Δ'
+      (Pin -∗
+       (∀ x, Pout x -∗ pm_maybe_wand (pm_option_fun Pclose x) (Q' x)) -∗
+       R
+      )%I) Δ'
       = Some Δ'' ∧
     envs_entails Δ'' R) →
   envs_entails Δ Q.

theories/proofmode/environments.v

 From iris.proofmode Require Import base.
 From iris.algebra Require Export base.
+From iris.bi Require Export bi.
 Set Default Proof Using "Type".
 
 Inductive env (A : Type) : Type :=
@@ -17,7 +18,7 @@ Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
   end.
 
 Module env_notations.
-  Notation "y ≫= f" := (option_bind f y).
+  Notation "y ≫= f" := (pm_option_bind f y).
   Notation "x ← y ; z" := (y ≫= λ x, z).
   Notation "' x1 .. xn ← y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. )).
   Notation "Γ !! j" := (env_lookup j Γ).
@@ -93,8 +94,8 @@ Ltac simplify :=
   | _ => progress simplify_eq/=
   | H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
   | |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
-  | H : context [option_bind _ ?x] |- _ => destruct x eqn:?
-  | |- context [option_bind _ ?x] => destruct x eqn:?
+  | H : context [pm_option_bind _ ?x] |- _ => destruct x eqn:?
+  | |- context [pm_option_bind _ ?x] => destruct x eqn:?
   | _ => case_match
   end.
 
@@ -205,3 +206,132 @@ Global Instance env_to_list_subenv_proper :
   Proper (env_subenv ==> sublist) (@env_to_list A).
 Proof. induction 1; simpl; constructor; auto. Qed.
 End env.
+
+Record envs (PROP : bi) :=
+  Envs { env_intuitionistic : env PROP; env_spatial : env PROP; env_counter : positive }.
+Add Printing Constructor envs.
+Arguments Envs {_} _ _ _.
+Arguments env_intuitionistic {_} _.
+Arguments env_spatial {_} _.
+Arguments env_counter {_} _.
+
+Record envs_wf {PROP} (Δ : envs PROP) := {
+  env_intuitionistic_valid : env_wf (env_intuitionistic Δ);
+  env_spatial_valid : env_wf (env_spatial Δ);
+  envs_disjoint i : env_intuitionistic Δ !! i = None ∨ env_spatial Δ !! i = None
+}.
+
+Definition of_envs {PROP} (Δ : envs PROP) : PROP :=
+  (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
+Instance: Params (@of_envs) 1.
+Arguments of_envs : simpl never.
+
+(* We seal [envs_entails], so that it does not get unfolded by the
+   proofmode's own tactics, such as [iIntros (?)]. *)
+Definition envs_entails_aux : seal (λ PROP (Δ : envs PROP) (Q : PROP), (of_envs Δ ⊢ Q)).
+Proof. by eexists. Qed.
+Definition envs_entails := envs_entails_aux.(unseal).
+Definition envs_entails_eq : envs_entails = _ := envs_entails_aux.(seal_eq).
+Arguments envs_entails {PROP} Δ Q%I : rename.
+Instance: Params (@envs_entails) 1.
+
+Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
+  env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
+  env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
+}.
+
+Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
+  env_dom (env_intuitionistic Δ) ++ env_dom (env_spatial Δ).
+
+Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
+  let (Γp,Γs,n) := Δ in
+  match env_lookup i Γp with
+  | Some P => Some (true, P)
+  | None => P ← env_lookup i Γs; Some (false, P)
+  end.
+
+Definition envs_delete {PROP} (remove_persistent : bool)
+    (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
+  let (Γp,Γs,n) := Δ in
+  match p with
+  | true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs n
+  | false => Envs Γp (env_delete i Γs) n
+  end.
+
+Definition envs_lookup_delete {PROP} (remove_persistent : bool)
+    (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
+  let (Γp,Γs,n) := Δ in
+  match env_lookup_delete i Γp with
+  | Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs n)
+  | None => ''(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
+  end.
+
+Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
+    (js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
+  match js with
+  | [] => Some (true, [], Δ)
+  | j :: js =>
+     ''(p,P,Δ') ← envs_lookup_delete remove_persistent j Δ;
+     ''(q,Hs,Δ'') ← envs_lookup_delete_list remove_persistent js Δ';
+     Some ((p:bool) && q, P :: Hs, Δ'')
+  end.
+
+Definition envs_snoc {PROP} (Δ : envs PROP)
+    (p : bool) (j : ident) (P : PROP) : envs PROP :=
+  let (Γp,Γs,n) := Δ in
+  if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.
+
+Definition envs_app {PROP : bi} (p : bool)
+    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
+  let (Γp,Γs,n) := Δ in
+  match p with
+  | true => _ ← env_app Γ Γs; Γp' ← env_app Γ Γp; Some (Envs Γp' Γs n)
+  | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs' n)
+  end.
+
+Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
+    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
+  let (Γp,Γs,n) := Δ in
+  match p with
+  | true => _ ← env_app Γ Γs; Γp' ← env_replace i Γ Γp; Some (Envs Γp' Γs n)
+  | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs' n)
+  end.
+
+Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
+    (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
+  if beq p q then envs_simple_replace i p Γ Δ
+  else envs_app q Γ (envs_delete true i p Δ).
+
+Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
+  if env_spatial Δ is Enil then true else false.
+
+Definition envs_clear_spatial {