Define persistent from pre-existing connectives instead of in the model.

theories/algebra/cmra.v

@@ -573,6 +573,11 @@ Section ucmra.
   Proof. by intros x; rewrite (comm op) left_id. Qed.
   Global Instance ucmra_unit_persistent : Persistent (∅:A).
   Proof. apply ucmra_pcore_unit. Qed.
+  Lemma ucmra_core_unit {M : ucmraT} : core (∅ : M) ≡ ∅.
+  Proof.
+    rewrite /core/core'//= ucmra_pcore_unit //=.
+  Qed.
+
 
   Lemma ucmra_unit_unique x y:
     (∀ x', x ⋅ x' ≡ x') →

theories/algebra/upred.v

@@ -254,24 +254,6 @@ Definition uPred_relevant {M} := proj1_sig uPred_relevant_aux M.
 Definition uPred_relevant_eq :
   @uPred_relevant = @uPred_relevant_def := proj2_sig uPred_relevant_aux.
 
-Program Definition uPred_persistent_def {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x y:= P n (core x) ∅ |}.
-Next Obligation.
-  intros M P n x1 x2 y1 y2 ? Hx Hy. 
-  naive_solver eauto using uPred_mono, @cmra_core_monoN.
-Qed.
-Next Obligation. 
-  intros M P n1 n2 x y ? ???. 
-  rewrite //= in H. rewrite //=. 
-  eapply uPred_closed; eauto.
-  - apply @cmra_core_validN; eauto. 
-  - apply ucmra_unit_validN.
-Qed.
-Definition uPred_persistent_aux : { x | x = @uPred_persistent_def }. by eexists. Qed.
-Definition uPred_persistent {M} := proj1_sig uPred_persistent_aux M.
-Definition uPred_persistent_eq :
-  @uPred_persistent = @uPred_persistent_def := proj2_sig uPred_persistent_aux.
-
 Program Definition uPred_affine_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x y:= P n x y ∧ y ≡{n}≡ ∅ |}.
 Next Obligation. 
@@ -411,7 +393,7 @@ Module Unseal.
 Definition unseal_eqs :=
   (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
   uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq,
-  uPred_plainly_eq, uPred_persistent_eq, uPred_later_eq, uPred_ownM_eq,
+  uPred_plainly_eq, uPred_later_eq, uPred_ownM_eq,
   uPred_valid_eq, uPred_relevant_eq, uPred_affine_eq, uPred_ownMl_eq, uPred_emp_eq, uPred_stopped_eq).
 Import iris.bi.derived_connectives. 
 Ltac unfold_bi := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
@@ -554,14 +536,6 @@ Proof.
 Qed.
 Global Instance relevant_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_relevant M) := ne_proper _.
-Global Instance persistent_ne n : Proper (dist n ==> dist n) (@uPred_persistent M).
-Proof.
-  intros P1 P2 HP.
-  unseal; split=> n' x y.
-  intros ???; apply HP; eauto using @cmra_core_validN, @ucmra_unit_validN.
-Qed.
-Global Instance persistent_proper :
-  Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_relevant M) := ne_proper _.
 Global Instance affine_ne n : Proper (dist n ==> dist n) (@uPred_affine M).
 Proof.
   intros P1 P2 HP.
@@ -626,6 +600,10 @@ Proof.
 Qed.
 Lemma impl_elim P Q R : (P ⊢ Q → R) → (P ⊢ Q) → P ⊢ R.
 Proof. by unseal; intros HP HP'; split=> n x y ???; apply HP with n x, HP'. Qed.
+Lemma impl_elim_l P Q : (P → Q) ∧ P ⊢ Q.
+Proof. apply impl_elim with P; auto using and_elim_l, and_elim_r. Qed.
+Lemma impl_elim_r P Q : P ∧ (P → Q) ⊢ Q.
+Proof. apply impl_elim with P; auto using and_elim_l, and_elim_r. Qed.
 Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
 Proof. unseal; intros HPΨ; split=> n x y ??? a; by apply HPΨ. Qed.
 Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
@@ -682,6 +660,17 @@ Proof.
     + by rewrite (assoc op) -Hw -Hy.
     + by exists z2, x2, w2, y2.
 Qed.
+Lemma sep_intro_True P Q: (P ⊢ Q) → (P ⊢ (Q ★ True)).
+Proof.
+  intros HPQ. rewrite -(left_id _ _ P) comm. apply sep_mono; auto.
+  by unseal.
+Qed.
+
+Lemma True_absorb P : True ★ P ⊢ True.
+Proof.
+  unseal; split => n x y ???. rewrite /uPred_holds //=.
+Qed.
+
 Lemma wand_intro_r P Q R : (P ★ Q ⊢ R) → P ⊢ Q -★ R.
 Proof.
   unseal=> HPQR; split=> n x y ??? n' x' y' ????. apply HPQR; auto.
@@ -706,13 +695,6 @@ Proof.
   * split; auto.
 Qed.
 
-Lemma persistent_intro' P Q : (uPred_persistent P ⊢ Q) → uPred_persistent P ⊢ uPred_persistent Q.
-Proof.
-  unseal=> HPQ.
-  split=> n x y ?? ?.
-  apply HPQ; simpl; auto using @cmra_core_validN, @ucmra_unit_validN. by rewrite ?cmra_core_idemp.
-Qed.
-
 Lemma relevant_elim P : □ P ⊢ P.
 Proof.
   unseal; split=> n x y ?? /=. 
@@ -751,10 +733,14 @@ Proof. unseal. split=>-[|n] x y ??; auto.
 Qed.
 Lemma relevant_later_1 P : (□ ▷ P) ⊢ (▷ □ P).
 Proof. rewrite relevant_relevant_later. rewrite relevant_elim //=. Qed.
-Lemma relevant_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
-Proof. unseal. intro HPQ. econstructor; intros n x y ?? [? ?]. 
-       split; auto. eapply HPQ; eauto using @cmra_core_validN.
+Lemma relevant_intro P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
+Proof.
+  unseal=> HPQ.
+  split=> n x y ?? [? ?].
+  split; auto. apply HPQ; simpl; auto using @cmra_core_validN. by rewrite ?cmra_core_idemp.
 Qed.
+Lemma relevant_mono P Q : (P ⊢ Q) → □ P ⊢ □ Q.
+Proof. intros HP. apply relevant_intro. rewrite relevant_elim. done. Qed.
 
 Lemma pure_elim_spare φ Q Q' R : (Q ⊢ ⧆■ φ ★ Q') → (φ → (Q ⊢ R)) → Q ⊢ R.
 Proof.
@@ -764,6 +750,12 @@ Proof.
   naive_solver.
 Qed.
 
+Lemma emp_relevant: Emp ⊢ □ Emp. 
+Proof.
+  unseal. split=> n x y ??. simpl; intros ->. 
+  rewrite persistent_core; auto.
+Qed.
+
 Hint Resolve relevant_mono.
 
 (* Affine *)
@@ -825,6 +817,13 @@ Proof.
 Qed.
 Lemma affine_mono P Q: (P ⊢ Q) → ⧆P ⊢ ⧆Q.
 Proof. intros HP. split. unseal => n x y ?? [? ?]; split; auto. eapply HP; eauto. Qed.
+Lemma affine_affine_sep P Q: ⧆(⧆P ★ Q) ⊢ ⧆P ★ ⧆Q.
+Proof.
+  split. unseal => n x y ?? [HPQ Hemp_y].
+  destruct HPQ as (x1&x2&y1&y2&Heqx&Heqy&[HP Hemp_y1]&HQ).
+  exists x1, x2, y1, y2; split_and!; auto.
+  rewrite -Hemp_y Heqy Hemp_y1 left_id //.
+Qed.
 
 Lemma affine_relevant_later P: ⧆▷□P ⊣⊢ ⧆□▷ P.
 Proof.
@@ -836,21 +835,6 @@ Proof.
   - apply affine_mono, relevant_later_1.
 Qed.
 
-Lemma unlimited_persistent P: ⧈P ⊢ (uPred_persistent P).
-Proof.
-  unseal. split => n x y ??.
-  intros ((?&Heq1)&Heq2). rewrite /uPred_holds//=. rewrite -Heq2 Heq1. done. 
-Qed.
-
-Lemma unlimited_affine_persistent P: ⧈P ⊣⊢ uPred_affine (uPred_persistent P).
-Proof.
-  unseal; split; intros n x y ??; split.
-  - intros ((?&Heq1)&Heq2). rewrite /uPred_holds//=. rewrite -Heq2 Heq1. done. 
-  - intros (HP&Heq1). rewrite /uPred_holds//= Heq1.
-    rewrite /core/core'//= ucmra_pcore_unit //=.
-Qed.
-
-
 (* Later *)
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
 Proof.

theories/algebra/upred_bi.v

@@ -4,10 +4,11 @@ From iris.proofmode Require Import coq_tactics classes class_instances tactics.
 
 
 Import uPred.
+
 Lemma uPred_bi_mixin (M : ucmraT) : BiMixin
   uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
                 (@uPred_forall M) (@uPred_exist M) 
-                uPred_sep uPred_wand uPred_persistent.
+                uPred_sep uPred_wand (λ P, (Emp ∧ □ P) ★ True)%IP. 
 Proof.
   split; try apply _; eauto with I.
   - (* (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P) *)
@@ -15,6 +16,7 @@ Proof.
     + intros HPQ; split; split=> x i; apply HPQ.
     + intros [HPQ HQP]; split=> x n; by split; [apply HPQ|apply HQP].
   - intros n P Q HPQ. apply equiv_dist. unseal; split => ?????; auto.
+  - intros. solve_proper.
   - intros ?? Himpl; eapply pure_elim; eauto; intros. etransitivity; last eapply Himpl; eauto.
   - by unseal.
   - intros P Q. unseal. by split=> n x y ?? [? ?].
@@ -36,35 +38,60 @@ Proof.
   - intros; by rewrite assoc.
   - intros; by apply wand_intro_r.
   - intros; by apply wand_elim_l'.
-  - unseal. intros P. split => n x y ?? => //=. rewrite /uPred_holds //=.
-    intros HP. eapply H; eauto.
-    * apply cmra_core_validN; eauto.
-    * apply ucmra_unit_validN.
-  - unseal. split => n x y ?? => //=. rewrite /uPred_holds //= => H.
-    rewrite /uPred_holds //=. rewrite cmra_core_idemp //.
-  - unseal. split => n x y ?? => //=.
-    do 2 rewrite /uPred_holds //=.
-  - unseal. split => n x y ?? => //=.
-  - unseal. split => n x y ?? => //=.
-  - intros.
-    unseal; split=>n x y ??. 
-    intros (x1&x2&y1&y2&Heq1&Heq2&HP&HQ).
-    eapply (uPred_mono _ _ _ x1 y); eauto. 
-    eexists; done.
-  - intros.
-    unseal; split=>n x y ??.
-    intros (HP&HQ). 
-    exists (core x), x, (∅: M), y; split_and!.
-    * by rewrite cmra_core_l.
-    * by rewrite left_id.
-    * move: HP. rewrite /uPred_holds//=.
-    * done.
+  - intros P Q HPQ. apply sep_mono; auto. apply and_intro; auto using and_elim_l.
+    etransitivity; first eapply and_elim_r. by apply relevant_mono.
+  - intros P. apply sep_mono; auto.
+    apply and_intro.
+    * apply and_elim_l.
+    * etransitivity.
+      { apply and_intro.
+        * etransitivity; first eapply and_elim_l.  apply emp_relevant.
+        * apply and_elim_r.
+      }
+      rewrite -relevant_and. apply relevant_intro.
+      apply sep_intro_True. apply and_intro.
+      rewrite relevant_elim and_elim_l //.
+
+      apply relevant_mono, and_elim_r.
+  - intros. unseal; split => n x y ?? H.
+    exists (∅ : M), x, (∅ : M), y;
+      rewrite ?right_id ?left_id //=; split_and!; auto.
+    repeat split; rewrite /uPred_holds //= ucmra_core_unit //.
+  - intros. unseal; split => n x y ?? H. 
+    exists x, (∅ : M), (∅ : M), y. rewrite ?left_id ?right_id; split_and!; auto.
+    split.
+    * rewrite /uPred_holds //=.
+    * split; auto. intros a.
+      edestruct (H a) as (x1&x2&y1&y2&Hex&Heqy&(Hemp&HP)&_).
+      rewrite Hemp in HP * => HP.
+      destruct HP as [HP ?]. eapply uPred_mono; eauto.
+      eapply cmra_core_monoN. eexists; eauto.
+      rewrite ucmra_core_unit //=.
+  - intros A Ψ. unseal; split => n x y ?? H.
+    edestruct H as (x1&x2&y1&y2&Heqx&Heqy&(Hemp&HP)&_).
+    rewrite Hemp in HP * => HP. destruct HP as ((a&HP)&Hcore).
+    exists a.
+    exists x1, x2, (∅ : M), y; split_and!; rewrite ?left_id; auto.
+    * split; auto.
+      ** rewrite /uPred_holds //=. 
+      ** split; auto.
+    * rewrite /uPred_holds //=. 
+  - intros P Q. rewrite -sep_assoc; apply sep_mono => //=.
+    unseal; split => n x y; done.
+  - intros P Q. unseal; split => n x y ?? [HP HQ].
+    destruct HP as (x1&x2&y1&y2&Heqx&?&(Hemp&HP)&?).
+    rewrite Hemp //= in HP * => HP.
+    exists (core x1: M), x, (∅ : M), y.
+    split_and!; rewrite ?left_id ?right_id //=.
+    { rewrite {2}Heqx assoc cmra_core_l //. }
+    destruct HP as [? ->].
+    auto.
 Qed.
 
 Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
   uPred_entails uPred_pure uPred_or uPred_impl
                 (@uPred_forall M) (@uPred_exist M) 
-                uPred_sep uPred_persistent (@uPred_eq M)
+                uPred_sep (λ P, (Emp ∧ □ P) ★ True)%IP (@uPred_eq M)
                 uPred_later.
 Proof.
   split; try apply _; eauto with I.
@@ -87,8 +114,26 @@ Proof.
     * destruct Hsat as (a&?). right. by exists a.
   - intros; by rewrite later_sep.
   - intros; by rewrite later_sep.
-  - by unseal. 
-  - by unseal. 
+  - intros P. unseal; split => n x y ?? Hsat /=.
+    exists (x : M), (∅ : M), (∅ : M), y.
+    rewrite ?left_id ?right_id //=; split_and!; auto.
+    split.
+    * rewrite /uPred_holds //=.
+    * split; rewrite ucmra_core_unit //.
+      destruct n => //=. destruct Hsat as (x1&x2&y1&y2&?&?&((Hemp&HP)&?)).
+      rewrite Hemp in HP * => HP.
+      destruct HP as (?&Hcore). rewrite /uPred_holds//=.
+      eapply uPred_mono; eauto.
+      apply cmra_core_monoN. eexists; eauto.
+  - intros P.  unseal; split => -[|n] x y ?? Hsat //=.
+    destruct Hsat as (x1&x2&y1&y2&?&?&(HP&_)).
+    destruct HP as (Hemp&(HP&Hcore)).
+    exists x1, x2, y1, y2; split_and!; eauto using dist_S => //=.
+    split.
+    * eapply (uPred_closed _ _ (S n)); eauto.
+      ** eapply cmra_validN_S, cmra_validN_includedN; last by (eexists; eauto). eauto.
+      ** eapply cmra_validN_S, cmra_validN_includedN; last by (eexists; eauto). eauto.
+    * split; eauto. by apply dist_S.
   - (* ▷ P ⊢ ▷ False ∨ (▷ False → P) *)
     intros P. unseal; split=> -[|n] x y ?? /= HP; [by left|right].
     intros [|n'] x' y' ????; [|done].
@@ -179,11 +224,38 @@ Proof.
   rewrite affine_equiv. rewrite comm. by repeat unseal.
 Qed.
 
+Lemma bi_persistently_unfold_alt {M: ucmraT} (P: uPred M):
+  bi_persistently P ⊣⊢ (emp ∧ uPred_relevant P) ∗ True.
+Proof. unfold_bi => //=. Qed.
+
+Lemma unlimited_affine_persistent {M: ucmraT} (P: uPred M):
+  uPred_affine (uPred_relevant P) ⊣⊢ bi_affinely (bi_persistently P).
+Proof.
+  rewrite uPred_affine_bi_affinely. rewrite bi_persistently_unfold_alt. apply (anti_symm (⊢)).
+  * iIntros "HP". iApply bi.affinely_sep_2; iSplitR "".
+    ** iAlways. iSplit; auto.
+    ** iPureIntro; done.
+  * iIntros "HP".
+    iPoseProof (affine_affine_sep (uPred_relevant P) (bi_pure True) with "[HP]") as "HP'".
+    {
+      rewrite ?uPred_affine_bi_affinely. iAlways.
+      rewrite bi.affinely_elim. unfold_bi. rewrite /bi_emp//=.
+    }
+    rewrite ?uPred_affine_bi_affinely.
+    iDestruct "HP'" as "(HP&_)". done.
+Qed.
+
+Lemma unlimited_persistent {M: ucmraT} (P: uPred M):
+  uPred_affine (uPred_relevant P) ⊢ (bi_persistently P).
+Proof.
+  rewrite unlimited_affine_persistent bi.affinely_elim //.
+Qed.
+
 Global Instance valid_persistent {M: ucmraT} {A : cmraT} (a : A) :
   Persistent ((⧆✓ a) : uPred M)%I.
 Proof.
   intros; rewrite /Persistent. rewrite -uPred_affine_bi_affinely.
-  rewrite -{1}relevant_valid. unfold_bi. rewrite -unlimited_persistent.
+  rewrite -{1}relevant_valid. rewrite -unlimited_persistent.
   by rewrite relevant_affine affine_affine_idemp.
 Qed.
 
@@ -191,14 +263,14 @@ Global Instance ownM_persistent {M: ucmraT} (a: M) :
   cmra.Persistent a → Persistent (⧆(@uPred_ownM M a)).
 Proof.
   intros; rewrite /Persistent. rewrite -uPred_affine_bi_affinely.
-  unfold_bi. rewrite -unlimited_persistent.
+  rewrite -unlimited_persistent.
   rewrite relevant_affine unlimited_ownM affine_affine_idemp //=.
 Qed.
 Global Instance ownMl_relevant {M: ucmraT} (a: M) :
   cmra.Persistent a → Persistent (⧆(@uPred_ownMl M a)).
 Proof.
   intros; rewrite /Persistent. rewrite -uPred_affine_bi_affinely.
-  unfold_bi. rewrite -unlimited_persistent.
+  rewrite -unlimited_persistent.
   rewrite relevant_affine relevant_ownMl affine_affine_idemp //=.
 Qed.
 
@@ -227,25 +299,11 @@ Section ATimeless_sbi.
     intros; rewrite /ATimeless affinely_or except_0_or later_or affinely_or; auto with *.
   Qed.
 
-  (*
-Global Instance impl_atimeless P Q : ATimeless Q → ATimeless (P → Q).
-Proof.
-  rewrite /ATimeless=> HQ. rewrite later_false_em.
-  rewrite affinely_or.
-  apply or_mono.
-  { rewrite affinely_elim.  done. }
-  apply affinely_mono, impl_intro_l.
-  rewrite -{2}(löb Q); apply impl_intro_l.
-  rewrite HQ /sbi_except_0. !and_or_r. apply or_elim; last auto.
-  by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
-  rewrite !atimelessP_spec; unseal=> HP [|n] x ? HPQ  [|n'] x' ?????; auto.
-  apply HP, HPQ, uPred_closed with (S n'); eauto using cmra_validN_le.
-Qed.
-*)
   Global Instance sep_atimeless P Q: Timeless P → Timeless Q → ATimeless (P ∗ Q).
   Proof.
     intros; rewrite /ATimeless. apply timeless_atimeless; apply _. 
   Qed.
+
   Global Instance affinely_atimeless P :
     ATimeless P → ATimeless (bi_affinely P).
   Proof.
@@ -302,8 +360,8 @@ Section ATimeless_uPred.
   Global Instance persistently_atimeless P : ATimeless P → ATimeless (□ P).
   Proof.
     rewrite /ATimeless.
-    rewrite -?uPred_affine_bi_affinely.
     rewrite -unlimited_affine_persistent.
+    rewrite -?uPred_affine_bi_affinely.
     rewrite -relevant_affine affine_relevant_later.
     rewrite -relevant_affine.
     rewrite ?uPred_affine_bi_affinely => H.