diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4b290acc607ea8deeb1d72795438d25b6cd30c72..522940facb4d79ced8ee5dec57aa2a8ecac95ed5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -105,6 +105,10 @@ Coq 8.13 is no longer supported.
 * Add `∗-∗` as notation in `stdpp_scope` similar to `-∗`. This means `P ∗-∗ Q`
   can be directly used as lemma statement, and is syntactic sugar for `⊢ P ∗-∗ Q`.
 * Add `≼` connective (`internal_included`) on the BI level. (by Ike Mulder)
+* Move laws of persistence modality out of `BiMixin` into `BiPersistentlyMixin`.
+* Provide smart constructor `bi_persistently_mixin_discrete` for
+  `BiPersistentlyMixin`: Given a discrete BI that enjoys the existential
+  property, a trivial definition of the persistence modality can be given.
 
 **Changes in `proofmode`:**
 
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 5f82577225cd517363c991784a7cd64faa02041c..9077f0feb05865932ba6914c42b082342d73346c 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -13,8 +13,7 @@ Local Existing Instance entails_po.
 Lemma uPred_bi_mixin (M : ucmra) :
   BiMixin
     uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
-    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand
-    uPred_persistently.
+    (@uPred_forall M) (@uPred_exist M) uPred_sep uPred_wand.
 Proof.
   split.
   - exact: entails_po.
@@ -27,7 +26,6 @@ Proof.
   - exact: exist_ne.
   - exact: sep_ne.
   - exact: wand_ne.
-  - exact: persistently_ne.
   - exact: pure_intro.
   - exact: pure_elim'.
   - exact: and_elim_l.
@@ -49,6 +47,15 @@ Proof.
   - exact: sep_assoc'.
   - exact: wand_intro_r.
   - exact: wand_elim_l'.
+Qed.
+
+Lemma uPred_bi_persistently_mixin (M : ucmra) :
+  BiPersistentlyMixin
+    uPred_entails uPred_emp uPred_and
+    (@uPred_exist M) uPred_sep uPred_persistently.
+Proof.
+  split.
+  - exact: persistently_ne.
   - exact: persistently_mono.
   - exact: persistently_idemp_2.
   - (* emp ⊢ <pers> emp (ADMISSIBLE) *)
@@ -96,7 +103,8 @@ Qed.
 Canonical Structure uPredI (M : ucmra) : bi :=
   {| bi_ofe_mixin := ofe_mixin_of (uPred M);
      bi_bi_mixin := uPred_bi_mixin M;
-     bi_bi_later_mixin := uPred_bi_later_mixin M |}.
+     bi_bi_later_mixin := uPred_bi_later_mixin M;
+     bi_bi_persistently_mixin := uPred_bi_persistently_mixin M |}.
 
 Lemma uPred_internal_eq_mixin M : BiInternalEqMixin (uPredI M) (@uPred_internal_eq M).
 Proof.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index c751e3016aba925c338c815933b7a5d215242191..cce7437ae47b99a2192913bf088b8d50f8470615 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -19,7 +19,6 @@ Section bi_mixin.
   Context (bi_exist : ∀ A, (A → PROP) → PROP).
   Context (bi_sep : PROP → PROP → PROP).
   Context (bi_wand : PROP → PROP → PROP).
-  Context (bi_persistently : PROP → PROP).
 
   Bind Scope bi_scope with PROP.
   Local Infix "⊢" := bi_entails.
@@ -36,7 +35,6 @@ Section bi_mixin.
     (bi_exist _ (λ x, .. (bi_exist _ (λ y, P%I)) ..)) : bi_scope.
   Local Infix "∗" := bi_sep : bi_scope.
   Local Infix "-∗" := bi_wand : bi_scope.
-  Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
 
   (** * Axioms for a general BI (logic of bunched implications) *)
 
@@ -64,7 +62,6 @@ Section bi_mixin.
       Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A);
     bi_mixin_sep_ne : NonExpansive2 bi_sep;
     bi_mixin_wand_ne : NonExpansive2 bi_wand;
-    bi_mixin_persistently_ne : NonExpansive bi_persistently;
 
     (** Higher-order logic *)
     bi_mixin_pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝;
@@ -95,8 +92,40 @@ Section bi_mixin.
     bi_mixin_sep_assoc' P Q R : (P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R);
     bi_mixin_wand_intro_r P Q R : (P ∗ Q ⊢ R) → P ⊢ Q -∗ R;
     bi_mixin_wand_elim_l' P Q R : (P ⊢ Q -∗ R) → P ∗ Q ⊢ R;
+  }.
+
+  (** We require any BI to have a persistence modality that carves out the
+  intuitionistic fragment of the separation logic. For logics such as Iris,
+  the persistence modality has a non-trivial definition (involving the [core] of
+  the camera). It is not clear whether a trivial definition exists: while
+  [<pers> P := False] comes close, it does not satisfy [later_persistently_1].
+  
+  However, for some simpler discrete BIs the persistence modality
+  can be defined as:
+
+    <pers> P := ⌜ emp ⊢ P ⌝
+
+  That is, [P] holds persistently if it holds without resources.
+
+  The nesting of the entailment below the pure embedding ⌜ ⌝ only works for
+  discrete BIs: Non-expansiveness of [<pers>] relies on [dist] ignoring the
+  step-index.
+
+  To prove the rule [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> Ψ a] the BI furthermore
+  needs to satisfy the "existential property": [emp ⊢ ∃ x, Φ x] implies
+  [∃ x, emp ⊢ Φ x].
+
+  This construction is formalized by the smart constructor
+  [bi_persistently_mixin_discrete] for [BiPersistentlyMixin]. See
+  [tests/heapprop] and [tests/heapprop_affine] for examples of how to use this
+  smart constructor. *)
+
+  Context (bi_persistently : PROP → PROP).
+  Local Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
+
+  Record BiPersistentlyMixin := {
+    bi_mixin_persistently_ne : NonExpansive bi_persistently;
 
-    (** Persistently *)
     (* In the ordered RA model: Holds without further assumptions. *)
     bi_mixin_persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q;
     (* In the ordered RA model: `core` is idempotent *)
@@ -121,6 +150,50 @@ Section bi_mixin.
     bi_mixin_persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q;
   }.
 
+  Lemma bi_persistently_mixin_discrete :
+    (∀ n (P Q : PROP), P ≡{n}≡ Q → P ≡ Q) →
+    (∀ {A} (Φ : A → PROP), (emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x) →
+    (∀ P : PROP, (<pers> P)%I = ⌜ emp ⊢ P ⌝%I) →
+    BiMixin →
+    BiPersistentlyMixin.
+  Proof.
+    intros Hdiscrete Hex Hpers Hbi. pose proof (bi_mixin_entails_po Hbi).
+    split.
+    - (* [NonExpansive bi_persistently] *)
+      intros n P Q [HPQ HQP]%Hdiscrete%(bi_mixin_equiv_entails Hbi).
+      rewrite !Hpers. apply (bi_mixin_pure_ne Hbi). split=> ?; by etrans.
+    - (*[(P ⊢ Q) → <pers> P ⊢ <pers> Q] *)
+      intros P Q HPQ. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_pure_intro Hbi). by trans P.
+    - (* [<pers> P ⊢ <pers> <pers> P] *)
+      intros P. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> ?.
+      by do 2 apply (bi_mixin_pure_intro Hbi).
+    - (* [emp ⊢ <pers> emp] *)
+      rewrite Hpers. by apply (bi_mixin_pure_intro Hbi).
+    - (* [<pers> P ∧ <pers> Q ⊢ <pers> (P ∧ Q)] *)
+      intros P Q. rewrite !Hpers.
+      apply (bi_mixin_impl_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_impl_intro_r Hbi).
+      etrans; [apply (bi_mixin_and_elim_r Hbi)|].
+      apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_pure_intro Hbi). by apply (bi_mixin_and_intro Hbi).
+    - (* [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> Ψ a] *)
+      intros A Φ. rewrite !Hpers. apply (bi_mixin_pure_elim' Hbi)=> /Hex [x ?].
+      etrans; [|apply (bi_mixin_exist_intro Hbi x)]; simpl.
+      rewrite Hpers. by apply (bi_mixin_pure_intro Hbi).
+    - (* [<pers> P ∗ Q ⊢ <pers> P] *)
+      intros P Q. rewrite !Hpers.
+      apply (bi_mixin_wand_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_wand_intro_r Hbi). by apply (bi_mixin_pure_intro Hbi).
+    - (* [<pers> P ∧ Q ⊢ P ∗ Q] *)
+      intros P Q. rewrite !Hpers.
+      apply (bi_mixin_impl_elim_l' Hbi). apply (bi_mixin_pure_elim' Hbi)=> ?.
+      apply (bi_mixin_impl_intro_r Hbi).
+      etrans; [apply (bi_mixin_and_elim_r Hbi)|].
+      etrans; [apply (bi_mixin_emp_sep_1 Hbi)|].
+      by apply (bi_mixin_sep_mono Hbi).
+  Qed.
+
   (** We equip any BI with a later modality. This avoids an additional layer in
   the BI hierachy and improves performance significantly (see Iris issue #303).
 
@@ -157,7 +230,7 @@ Section bi_mixin.
     BiMixin → BiLaterMixin.
   Proof.
     intros Hlater Hbi. pose proof (bi_mixin_entails_po Hbi).
-    split; repeat intro; rewrite ?Hlater ?Hequiv //.
+    split; repeat intro; rewrite ?Hlater //.
     - apply (bi_mixin_forall_intro Hbi)=> a.
       etrans; [apply (bi_mixin_forall_elim Hbi a)|]. by rewrite Hlater.
     - etrans; [|apply (bi_mixin_or_intro_r Hbi)].
@@ -194,7 +267,9 @@ Structure bi := Bi {
   bi_ofe_mixin : OfeMixin bi_car;
   bi_cofe_aux : Cofe (Ofe bi_car bi_ofe_mixin);
   bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
-                        bi_exist bi_sep bi_wand bi_persistently;
+                        bi_exist bi_sep bi_wand;
+  bi_bi_persistently_mixin :
+    BiPersistentlyMixin bi_entails bi_emp bi_and bi_exist bi_sep bi_persistently;
   bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
                                    bi_forall bi_exist bi_sep bi_persistently bi_later;
 }.
@@ -326,7 +401,7 @@ Proof. eapply bi_mixin_sep_ne, bi_bi_mixin. Qed.
 Global Instance wand_ne : NonExpansive2 (@bi_wand PROP).
 Proof. eapply bi_mixin_wand_ne, bi_bi_mixin. Qed.
 Global Instance persistently_ne : NonExpansive (@bi_persistently PROP).
-Proof. eapply bi_mixin_persistently_ne, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_ne, bi_bi_persistently_mixin. Qed.
 
 (* Higher-order logic *)
 Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
@@ -381,24 +456,28 @@ Proof. eapply bi_mixin_wand_elim_l', bi_bi_mixin. Qed.
 
 (* Persistently *)
 Lemma persistently_mono P Q : (P ⊢ Q) → <pers> P ⊢ <pers> Q.
-Proof. eapply bi_mixin_persistently_mono, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_mono, bi_bi_persistently_mixin. Qed.
 Lemma persistently_idemp_2 P : <pers> P ⊢ <pers> <pers> P.
-Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_idemp_2, bi_bi_persistently_mixin. Qed.
 
 Lemma persistently_emp_2 : emp ⊢@{PROP} <pers> emp.
-Proof. eapply bi_mixin_persistently_emp_2, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_emp_2, bi_bi_persistently_mixin. Qed.
 
 Lemma persistently_and_2 (P Q : PROP) :
   ((<pers> P) ∧ (<pers> Q)) ⊢ <pers> (P ∧ Q).
-Proof. eapply bi_mixin_persistently_and_2, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_and_2, bi_bi_persistently_mixin. Qed.
 Lemma persistently_exist_1 {A} (Ψ : A → PROP) :
   <pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a).
-Proof. eapply bi_mixin_persistently_exist_1, bi_bi_mixin. Qed.
+Proof. eapply bi_mixin_persistently_exist_1, bi_bi_persistently_mixin. Qed.
 
 Lemma persistently_absorbing P Q : <pers> P ∗ Q ⊢ <pers> P.
-Proof. eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_mixin. Qed.
+Proof.
+  eapply (bi_mixin_persistently_absorbing bi_entails), bi_bi_persistently_mixin.
+Qed.
 Lemma persistently_and_sep_elim P Q : <pers> P ∧ Q ⊢ P ∗ Q.
-Proof. eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_mixin. Qed.
+Proof.
+  eapply (bi_mixin_persistently_and_sep_elim bi_entails), bi_bi_persistently_mixin.
+Qed.
 
 (* Later *)
 Global Instance later_ne : NonExpansive (@bi_later PROP).
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 978c53876e234866f3841614098e78a498d06b68..2272e36eed5fd0244edaef65342110db98720364 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -315,8 +315,7 @@ Section instances.
 
   Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
     monPred_entails monPred_emp monPred_pure monPred_and monPred_or
-    monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand
-    monPred_persistently.
+    monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand.
   Proof.
     split; rewrite ?monPred_defs.monPred_unseal;
       try by (split=> ? /=; repeat f_equiv).
@@ -354,6 +353,15 @@ Section instances.
       apply bi.wand_intro_r. by rewrite -HR /= !Hij.
     - intros P Q R [HP]. split=> i. apply bi.wand_elim_l'.
       rewrite HP /= bi.forall_elim bi.pure_impl_forall bi.forall_elim //.
+  Qed.
+
+  Lemma monPred_bi_persistently_mixin :
+    BiPersistentlyMixin (PROP:=monPred I PROP)
+      monPred_entails monPred_emp monPred_and
+      monPred_exist monPred_sep monPred_persistently.
+  Proof.
+    split; rewrite ?monPred_defs.monPred_unseal;
+      try by (split=> ? /=; repeat f_equiv).
     - intros P Q [?]. split=> i /=. by f_equiv.
     - intros P. split=> i. by apply bi.persistently_idemp_2.
     - split=> i. by apply bi.persistently_emp_intro.
@@ -386,7 +394,9 @@ Section instances.
   Qed.
 
   Canonical Structure monPredI : bi :=
-    {| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin;
+    {| bi_ofe_mixin := monPred_ofe_mixin;
+       bi_bi_mixin := monPred_bi_mixin;
+       bi_bi_persistently_mixin := monPred_bi_persistently_mixin;
        bi_bi_later_mixin := monPred_bi_later_mixin |}.
 
   (** We restate the unsealing lemmas so that they also unfold the BI layer. The
diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index 0b4d6389246d1dbf9876e3cf7c007862d872917b..e366744e37159ad902580d563eced26abd07e371 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -20,8 +20,7 @@ Local Existing Instance entails_po.
 Lemma siProp_bi_mixin :
   BiMixin
     siProp_entails siProp_emp siProp_pure siProp_and siProp_or siProp_impl
-    (@siProp_forall) (@siProp_exist) siProp_sep siProp_wand
-    siProp_persistently.
+    (@siProp_forall) (@siProp_exist) siProp_sep siProp_wand.
 Proof.
   split.
   - exact: entails_po.
@@ -34,7 +33,6 @@ Proof.
   - exact: exist_ne.
   - exact: and_ne.
   - exact: impl_ne.
-  - solve_proper.
   - exact: pure_intro.
   - exact: pure_elim'.
   - exact: and_elim_l.
@@ -68,6 +66,15 @@ Proof.
     apply impl_intro_r.
   - (* (P ⊢ Q -∗ R) → P ∗ Q ⊢ R *)
     apply impl_elim_l'.
+Qed.
+
+Lemma siProp_bi_persistently_mixin :
+  BiPersistentlyMixin
+    siProp_entails siProp_emp siProp_and
+    (@siProp_exist) siProp_sep siProp_persistently.
+Proof.
+  split.
+  - solve_proper.
   - (* (P ⊢ Q) → <pers> P ⊢ <pers> Q *)
     done.
   - (* <pers> P ⊢ <pers> <pers> P *)
@@ -119,7 +126,9 @@ Qed.
 
 Canonical Structure siPropI : bi :=
   {| bi_ofe_mixin := ofe_mixin_of siProp;
-     bi_bi_mixin := siProp_bi_mixin; bi_bi_later_mixin := siProp_bi_later_mixin |}.
+     bi_bi_mixin := siProp_bi_mixin;
+     bi_bi_persistently_mixin := siProp_bi_persistently_mixin;
+     bi_bi_later_mixin := siProp_bi_later_mixin |}.
 
 Global Instance siProp_pure_forall : BiPureForall siPropI.
 Proof. exact: @pure_forall_2. Qed.
diff --git a/tests/heapprop.v b/tests/heapprop.v
index 31b5edbee704ac2a64ef3a0300a5d6abc035ee55..69634a3c038d162daa5b06fbc0e7d4520abd3e66 100644
--- a/tests/heapprop.v
+++ b/tests/heapprop.v
@@ -94,7 +94,7 @@ Local Definition heapProp_wand_unseal:
   @heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux.
 
 Local Definition heapProp_persistently_def (P : heapProp) : heapProp :=
-  {| heapProp_holds σ := P ∅ |}.
+  heapProp_pure (heapProp_entails heapProp_emp P).
 Local Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
 Proof. by eexists. Qed.
 Definition heapProp_persistently := unseal heapProp_persistently_aux.
@@ -120,7 +120,7 @@ Section mixins.
     BiMixin
       heapProp_entails heapProp_emp heapProp_pure heapProp_and heapProp_or
       heapProp_impl (@heapProp_forall) (@heapProp_exist)
-      heapProp_sep heapProp_wand heapProp_persistently.
+      heapProp_sep heapProp_wand.
   Proof.
     split.
     - (* [PreOrder heapProp_entails] *)
@@ -145,8 +145,6 @@ Section mixins.
       unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
     - (* [NonExpansive2 bi_wand] *)
       unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
-    - (* [NonExpansive2 bi_persistently] *)
-      unseal=> n P1 P2 [HP]; split; naive_solver.
     - (* [φ → P ⊢ ⌜ φ ⌝] *)
       unseal=> φ P ?; by split.
     - (* [(φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P] *)
@@ -193,21 +191,18 @@ Section mixins.
       unseal=> P Q R [HPQR]; split=> σ1 ? σ2 ??. apply HPQR. by exists σ1, σ2.
     - (* [(P ⊢ Q -∗ R) → P ∗ Q ⊢ R] *)
       unseal=> P Q R [HPQR]; split; intros ? (σ1&σ2&->&?&?&?). by apply HPQR.
-    - (* [(P ⊢ Q) → <pers> P ⊢ <pers> Q] *)
-      unseal=> P Q [HPQ]; split=> σ. apply HPQ.
-    - (* [<pers> P ⊢ <pers> <pers> P] *)
-      unseal=> P; split=> σ; done.
-    - (* [emp ⊢ <pers> emp] *)
-      unseal; split=> σ; done.
-    - (* [(∀ a, <pers> (Ψ a)) ⊢ <pers> (∀ a, Ψ a)] *)
-      unseal=> A Ψ; split=> σ; done.
-    - (* [<pers> (∃ a, Ψ a) ⊢ ∃ a, <pers> (Ψ a)] *)
-      unseal=> A Ψ; split=> σ; done.
-    - (* [<pers> P ∗ Q ⊢ <pers> P] *)
-      unseal=> P Q; split; intros ? (σ1&σ2&->&?&?&?); done.
-    - (* [<pers> P ∧ Q ⊢ P ∗ Q] *)
-      unseal=> P Q; split=> σ [??]. eexists ∅, σ. rewrite left_id_L.
-      split_and!; done || apply map_disjoint_empty_l.
+  Qed.
+
+  Lemma heapProp_bi_persistently_mixin :
+    BiPersistentlyMixin
+      heapProp_entails heapProp_emp heapProp_and
+      (@heapProp_exist) heapProp_sep heapProp_persistently.
+  Proof.
+    eapply bi_persistently_mixin_discrete, heapProp_bi_mixin; [done|..].
+    - (* [(emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x] *)
+      unseal. intros A Φ [H]. destruct (H ∅) as [x ?]; [done|].
+      exists x. by split=> σ ->.
+    - by rewrite heapProp_persistently_unseal.
   Qed.
 
   Lemma heapProp_bi_later_mixin :
@@ -220,7 +215,9 @@ End mixins.
 
 Canonical Structure heapPropI : bi :=
   {| bi_ofe_mixin := ofe_mixin_of heapProp;
-     bi_bi_mixin := heapProp_bi_mixin; bi_bi_later_mixin := heapProp_bi_later_mixin |}.
+     bi_bi_mixin := heapProp_bi_mixin;
+     bi_bi_persistently_mixin := heapProp_bi_persistently_mixin;
+     bi_bi_later_mixin := heapProp_bi_later_mixin |}.
 
 Global Instance heapProp_pure_forall : BiPureForall heapPropI.
 Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.
diff --git a/tests/heapprop_affine.ref b/tests/heapprop_affine.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/heapprop_affine.v b/tests/heapprop_affine.v
new file mode 100644
index 0000000000000000000000000000000000000000..6fd869d1b6880d5f1bfdfa8d9a25a07fc25ac63e
--- /dev/null
+++ b/tests/heapprop_affine.v
@@ -0,0 +1,261 @@
+From stdpp Require Import gmap.
+From iris.bi Require Import interface.
+From iris.proofmode Require Import tactics.
+From iris.prelude Require Import options.
+
+(** This file constructs a simple non step-indexed affine separation logic as
+predicates over heaps (modeled as maps from integer locations to integer values).
+It shows that Iris's [bi] canonical structure can be inhabited, and the Iris
+proof mode can be used to prove lemmas in this separation logic. *)
+Definition loc := Z.
+Definition val := Z.
+
+Record heapProp := HeapProp {
+  heapProp_holds :> gmap loc val → Prop;
+  heapProp_closed σ1 σ2 : heapProp_holds σ1 → σ1 ⊆ σ2 → heapProp_holds σ2;
+}.
+Global Arguments heapProp_holds : simpl never.
+Add Printing Constructor heapProp.
+
+Section ofe.
+  Inductive heapProp_equiv' (P Q : heapProp) : Prop :=
+    { heapProp_in_equiv : ∀ σ, P σ ↔ Q σ }.
+  Local Instance heapProp_equiv : Equiv heapProp := heapProp_equiv'.
+  Local Instance heapProp_equivalence : Equivalence (≡@{heapProp}).
+  Proof. split; repeat destruct 1; constructor; naive_solver. Qed.
+  Canonical Structure heapPropO := discreteO heapProp.
+End ofe.
+
+(** logical entailement *)
+Inductive heapProp_entails (P Q : heapProp) : Prop :=
+  { heapProp_in_entails : ∀ σ, P σ → Q σ }.
+
+(** logical connectives *)
+Local Program Definition heapProp_pure_def (φ : Prop) : heapProp :=
+  {| heapProp_holds _ := φ |}.
+Solve Obligations with done.
+Local Definition heapProp_pure_aux : seal (@heapProp_pure_def). Proof. by eexists. Qed.
+Definition heapProp_pure := unseal heapProp_pure_aux.
+Local Definition heapProp_pure_unseal :
+  @heapProp_pure = @heapProp_pure_def := seal_eq heapProp_pure_aux.
+
+Definition heapProp_emp : heapProp := heapProp_pure True.
+
+Local Program Definition heapProp_and_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := P σ ∧ Q σ |}.
+Solve Obligations with naive_solver eauto using heapProp_closed.
+Local Definition heapProp_and_aux : seal (@heapProp_and_def). Proof. by eexists. Qed.
+Definition heapProp_and := unseal heapProp_and_aux.
+Local Definition heapProp_and_unseal:
+  @heapProp_and = @heapProp_and_def := seal_eq heapProp_and_aux.
+
+Local Program Definition heapProp_or_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := P σ ∨ Q σ |}.
+Solve Obligations with naive_solver eauto using heapProp_closed.
+Local Definition heapProp_or_aux : seal (@heapProp_or_def). Proof. by eexists. Qed.
+Definition heapProp_or := unseal heapProp_or_aux.
+Local Definition heapProp_or_unseal:
+  @heapProp_or = @heapProp_or_def := seal_eq heapProp_or_aux.
+
+Local Program Definition heapProp_impl_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := ∀ σ', σ ⊆ σ' → P σ' → Q σ' |}.
+Next Obligation. intros P Q σ1 σ2 HPQ ? σ' ?; simpl in *. apply HPQ. by etrans. Qed.
+Local Definition heapProp_impl_aux : seal (@heapProp_impl_def). Proof. by eexists. Qed.
+Definition heapProp_impl := unseal heapProp_impl_aux.
+Local Definition heapProp_impl_unseal :
+  @heapProp_impl = @heapProp_impl_def := seal_eq heapProp_impl_aux.
+
+Local Program Definition heapProp_forall_def {A} (Ψ : A → heapProp) : heapProp :=
+  {| heapProp_holds σ := ∀ a, Ψ a σ |}.
+Solve Obligations with naive_solver eauto using heapProp_closed.
+Local Definition heapProp_forall_aux : seal (@heapProp_forall_def). Proof. by eexists. Qed.
+Definition heapProp_forall {A} := unseal heapProp_forall_aux A.
+Local Definition heapProp_forall_unseal :
+  @heapProp_forall = @heapProp_forall_def := seal_eq heapProp_forall_aux.
+
+Local Program Definition heapProp_exist_def {A} (Ψ : A → heapProp) : heapProp :=
+  {| heapProp_holds σ := ∃ a, Ψ a σ |}.
+Solve Obligations with naive_solver eauto using heapProp_closed.
+Local Definition heapProp_exist_aux : seal (@heapProp_exist_def). Proof. by eexists. Qed.
+Definition heapProp_exist {A} := unseal heapProp_exist_aux A.
+Local Definition heapProp_exist_unseal :
+  @heapProp_exist = @heapProp_exist_def := seal_eq heapProp_exist_aux.
+
+Local Program Definition heapProp_sep_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := ∃ σ1 σ2, σ = σ1 ∪ σ2 ∧ σ1 ##ₘ σ2 ∧ P σ1 ∧ Q σ2 |}.
+Next Obligation.
+  intros P Q σ1 σ2 (σ11 & σ12 & -> & ? & ? & ?) ?.
+  assert (σ11 ⊆ σ2) by (by etrans; [apply map_union_subseteq_l|]).
+  exists σ11, (σ2 ∖ σ11). split_and!; [| |done|].
+  - by rewrite map_difference_union.
+  - by apply map_disjoint_difference_r.
+  - eapply heapProp_closed; [done|].
+    apply map_union_reflecting_l with σ11; [done|..].
+    + by apply map_disjoint_difference_r.
+    + by rewrite map_difference_union.
+Qed.
+Local Definition heapProp_sep_aux : seal (@heapProp_sep_def). Proof. by eexists. Qed.
+Definition heapProp_sep := unseal heapProp_sep_aux.
+Local Definition heapProp_sep_unseal:
+  @heapProp_sep = @heapProp_sep_def := seal_eq heapProp_sep_aux.
+
+Local Program Definition heapProp_wand_def (P Q : heapProp) : heapProp :=
+  {| heapProp_holds σ := ∀ σ', σ ##ₘ σ' → P σ' → Q (σ ∪ σ') |}.
+Next Obligation.
+  intros P Q σ1 σ2 HPQ ? σ' ??; simpl in *.
+  apply heapProp_closed with (σ1 ∪ σ'); [by eauto using map_disjoint_weaken_l|].
+  by apply map_union_mono_r.
+Qed.
+Local Definition heapProp_wand_aux : seal (@heapProp_wand_def). Proof. by eexists. Qed.
+Definition heapProp_wand := unseal heapProp_wand_aux.
+Local Definition heapProp_wand_unseal:
+  @heapProp_wand = @heapProp_wand_def := seal_eq heapProp_wand_aux.
+
+Local Definition heapProp_persistently_def (P : heapProp) : heapProp :=
+  heapProp_pure (heapProp_entails heapProp_emp P).
+Local Definition heapProp_persistently_aux : seal (@heapProp_persistently_def).
+Proof. by eexists. Qed.
+Definition heapProp_persistently := unseal heapProp_persistently_aux.
+Local Definition heapProp_persistently_unseal:
+  @heapProp_persistently = @heapProp_persistently_def := seal_eq heapProp_persistently_aux.
+
+(** Iris's [bi] class requires the presence of a later modality, but for non
+step-indexed logics, it can be defined as the identity. *)
+Definition heapProp_later (P : heapProp) : heapProp := P.
+
+Local Definition heapProp_unseal :=
+  (heapProp_pure_unseal, heapProp_and_unseal,
+   heapProp_or_unseal, heapProp_impl_unseal, heapProp_forall_unseal,
+   heapProp_exist_unseal, heapProp_sep_unseal, heapProp_wand_unseal,
+   heapProp_persistently_unseal).
+Ltac unseal := rewrite !heapProp_unseal /=.
+
+Section mixins.
+  (** Enable [simpl] locally, which is useful for proofs in the model. *)
+  Local Arguments heapProp_holds !_ _ /.
+
+  Lemma heapProp_bi_mixin :
+    BiMixin
+      heapProp_entails heapProp_emp heapProp_pure heapProp_and heapProp_or
+      heapProp_impl (@heapProp_forall) (@heapProp_exist)
+      heapProp_sep heapProp_wand.
+  Proof.
+    split.
+    - (* [PreOrder heapProp_entails] *)
+      split; repeat destruct 1; constructor; naive_solver.
+    - (* [P ≡ Q ↔ (P ⊢ Q) ∧ (Q ⊢ P)] *)
+      intros P Q; split.
+      + intros [HPQ]; split; split; naive_solver.
+      + intros [[HPQ] [HQP]]; split; naive_solver.
+    - (* [Proper (iff ==> dist n) bi_pure] *)
+      unseal=> n φ1 φ2 Hφ; split; naive_solver.
+    - (* [NonExpansive2 bi_and] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [NonExpansive2 bi_or] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [NonExpansive2 bi_impl] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [Proper (pointwise_relation _ (dist n) ==> dist n) (bi_forall A)] *)
+      unseal=> A n Φ1 Φ2 HΦ; split=> σ /=; split=> ? x; by apply HΦ.
+    - (* [Proper (pointwise_relation _ (dist n) ==> dist n) (bi_exist A)] *)
+      unseal=> A n Φ1 Φ2 HΦ; split=> σ /=; split=> -[x ?]; exists x; by apply HΦ.
+    - (* [NonExpansive2 bi_sep] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [NonExpansive2 bi_wand] *)
+      unseal=> n P1 P2 [HP] Q1 Q2 [HQ]; split; naive_solver.
+    - (* [φ → P ⊢ ⌜ φ ⌝] *)
+      unseal=> φ P ?; by split.
+    - (* [(φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P] *)
+      unseal=> φ P HP; split=> σ ?. by apply HP.
+    - (* [P ∧ Q ⊢ P] *)
+      unseal=> P Q; split=> σ [??]; done.
+    - (* [P ∧ Q ⊢ Q] *)
+      unseal=> P Q; split=> σ [??]; done.
+    - (* [(P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R] *)
+      unseal=> P Q R [HPQ] [HPR]; split=> σ; split; auto.
+    - (* [P ⊢ P ∨ Q] *)
+      unseal=> P Q; split=> σ; by left.
+    - (* [Q ⊢ P ∨ Q] *)
+      unseal=> P Q; split=> σ; by right.
+    - (* [(P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R] *)
+      unseal=> P Q R [HPQ] [HQR]; split=> σ [?|?]; auto.
+    - (* [(P ∧ Q ⊢ R) → P ⊢ Q → R] *)
+      unseal=> P Q R HPQR; split=> σ ? σ' ??. apply HPQR.
+      split; eauto using heapProp_closed.
+    - (* [(P ⊢ Q → R) → P ∧ Q ⊢ R] *)
+      unseal=> P Q R HPQR; split=> σ [??]. by eapply HPQR.
+    - (* [(∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a] *)
+      unseal=> A P Ψ HPΨ; split=> σ ? a. by apply HPΨ.
+    - (* [(∀ a, Ψ a) ⊢ Ψ a] *)
+      unseal=> A Ψ a; split=> σ ?; done.
+    - (* [Ψ a ⊢ ∃ a, Ψ a] *)
+      unseal=> A Ψ a; split=> σ ?. by exists a.
+    - (* [(∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q] *)
+      unseal=> A Φ Q HΦQ; split=> σ [a ?]. by apply (HΦQ a).
+    - (* [(P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'] *)
+      unseal=> P P' Q Q' [HPQ] [HP'Q']; split; naive_solver.
+    - (* [P ⊢ emp ∗ P] *)
+      unfold heapProp_emp; unseal=> P; split=> σ ? /=.
+      eexists ∅, σ. rewrite left_id_L.
+      split_and!; done || apply map_disjoint_empty_l.
+    - (* [emp ∗ P ⊢ P] *)
+      unfold heapProp_emp; unseal=> P; split; intros ? (?&σ&->&?&_&?).
+      eapply heapProp_closed; [done|]. by apply map_union_subseteq_r.
+    - (* [P ∗ Q ⊢ Q ∗ P] *)
+      unseal=> P Q; split; intros ? (σ1&σ2&->&?&?&?).
+      exists σ2, σ1. by rewrite map_union_comm.
+    - (* [(P ∗ Q) ∗ R ⊢ P ∗ (Q ∗ R)] *)
+      unseal=> P Q R; split; intros ? (?&σ3&->&?&(σ1&σ2&->&?&?&?)&?).
+      exists σ1, (σ2 ∪ σ3). split_and!; [by rewrite assoc_L|solve_map_disjoint|done|].
+      exists σ2, σ3; split_and!; [done|solve_map_disjoint|done..].
+    - (* [(P ∗ Q ⊢ R) → P ⊢ Q -∗ R] *)
+      unseal=> P Q R [HPQR]; split=> σ1 ? σ2 ??. apply HPQR. by exists σ1, σ2.
+    - (* [(P ⊢ Q -∗ R) → P ∗ Q ⊢ R] *)
+      unseal=> P Q R [HPQR]; split; intros ? (σ1&σ2&->&?&?&?). by apply HPQR.
+  Qed.
+
+  Lemma heapProp_bi_persistently_mixin :
+    BiPersistentlyMixin
+      heapProp_entails heapProp_emp heapProp_and
+      (@heapProp_exist) heapProp_sep heapProp_persistently.
+  Proof.
+    eapply bi_persistently_mixin_discrete, heapProp_bi_mixin; [done|..].
+    - (* The "existential property" [(emp ⊢ ∃ x, Φ x) → ∃ x, emp ⊢ Φ x]. For an
+      affine BI the proof relies on there being a smallest resource/the unit
+      (here the empty heap [∅]). *)
+      unfold heapProp_emp. unseal. intros A Φ [H].
+      destruct (H ∅) as [x ?]; [done|]. exists x. split=> σ _.
+      eapply heapProp_closed; [done|]. by apply map_empty_subseteq.
+    - by rewrite heapProp_persistently_unseal.
+  Qed.
+
+  Lemma heapProp_bi_later_mixin :
+    BiLaterMixin
+      heapProp_entails heapProp_pure heapProp_or heapProp_impl
+      (@heapProp_forall) (@heapProp_exist)
+      heapProp_sep heapProp_persistently heapProp_later.
+  Proof. eapply bi_later_mixin_id; [done|apply heapProp_bi_mixin]. Qed.
+End mixins.
+
+Canonical Structure heapPropI : bi :=
+  {| bi_ofe_mixin := ofe_mixin_of heapProp;
+     bi_bi_mixin := heapProp_bi_mixin;
+     bi_bi_persistently_mixin := heapProp_bi_persistently_mixin;
+     bi_bi_later_mixin := heapProp_bi_later_mixin |}.
+
+Global Instance heapProp_pure_forall : BiPureForall heapPropI.
+Proof. intros A φ. rewrite /bi_forall /bi_pure /=. unseal. by split. Qed.
+
+Global Instance heapProp_affine : BiAffine heapPropI.
+Proof. exact: bi.True_intro. Qed.
+
+Lemma heapProp_proofmode_test {A} (P Q Q' R : heapProp) (Φ Ψ : A → heapProp) :
+  P ∗ Q ∗ Q' -∗ (* [Q'] is not used, to demonstrate affinity *)
+  □ R -∗
+  □ (R -∗ ∃ x, Φ x) -∗
+  ∃ x, Φ x ∗ Φ x ∗ P ∗ Q.
+Proof.
+  iIntros "(HP & HQ & HQ') #HR #HRΦ".
+  iDestruct ("HRΦ" with "HR") as (x) "#HΦ".
+  iExists x. iFrame. by iSplitL.
+Qed.