Many updates; using iInv from not yet merged joe/inv_tac of Iris.

0a5da48a · Joseph Tassarotti · a438921d · 0a5da48a · 0a5da48a · 0a5da48a
Commit 0a5da48a authored Feb 21, 2018 by Joseph Tassarotti
--- a/opam
+++ b/opam
@@ -7,5 +7,5 @@ remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/fri" ]
 depends: [
  "coq" { >= "8.7" }
  "coq-stdpp" { (>= "1.1.0") | (>= "dev") }
-  "coq-iris"  { (= "branch.gen_proofmode.2018-02-08.1") } 
+  "coq-iris"  { (= "branch.gen_proofmode.2018-02-19.0") } 
 ]
--- a/theories/algebra/upred.v
+++ b/theories/algebra/upred.v
@@ -17,9 +17,9 @@ Arguments uPred_holds {_} _ _ _ _ : simpl never.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.

-Delimit Scope uPred_scope with I.
+Delimit Scope uPred_scope with IP.
 Bind Scope uPred_scope with uPred.
-Arguments uPred_holds {_} _%I _ _ _.
+Arguments uPred_holds {_} _%IP _ _ _.

 Section cofe.
  Context {M : ucmraT}.
@@ -357,10 +357,10 @@ Definition uPred_emp_eq :
  @uPred_emp = @uPred_emp_def := proj2_sig uPred_emp_aux.


-Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
+Notation "P ⊢ Q" := (uPred_entails P%IP Q%IP)
  (at level 99, Q at level 200, right associativity) : stdpp_scope.
 Notation "(⊢)" := uPred_entails (only parsing) : stdpp_scope.
-Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
+Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%IP Q%IP)
  (at level 95, no associativity) : stdpp_scope.
 Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : stdpp_scope.
 Notation "■ φ" := (uPred_pure φ%stdpp%type)
@@ -380,9 +380,9 @@ Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
 Notation "P -★ Q" := (uPred_wand P Q)
  (at level 99, Q at level 200, right associativity) : uPred_scope.
 Notation "∀ x .. y , P" :=
-  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
+  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%IP) : uPred_scope.
 Notation "∃ x .. y , P" :=
-  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
+  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%IP) : uPred_scope.
 Notation "□ P" := (uPred_relevant P)
  (at level 20, right associativity) : uPred_scope.
 Notation "⧆ P" := (uPred_affine P)
@@ -394,12 +394,12 @@ Notation "▷ P" := (uPred_later P)
 Infix "≡" := (uPred_eq) : uPred_scope.
 Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.

-Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
+Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%IP.
 Instance: Params (@uPred_iff) 1.
 Infix "↔" := uPred_iff : uPred_scope.

 Definition uPred_relevant_if {M} (p : bool) (P : uPred M) : uPred M :=
-  (if p then □ P else P)%I.
+  (if p then □ P else P)%IP.
 Instance: Params (@uPred_relevant_if) 2.
 Arguments uPred_relevant_if _ !_ _/.
 Notation "□? p P" := (uPred_relevant_if p P)
@@ -470,8 +470,8 @@ Context {M : ucmraT}.
 Implicit Types φ : Prop.
 Implicit Types P Q : uPred M.
 Implicit Types A : Type.
-Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
-Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)
+Notation "P ⊢ Q" := (@uPred_entails M P%IP Q%IP). (* Force implicit argument M *)
+Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%IP Q%IP). (* Force implicit argument M *)
 Arguments uPred_holds {_} !_ _ _ _ /.
 Hint Immediate uPred_in_entails.

@@ -744,7 +744,7 @@ Proof. intros; apply impl_elim with Q; auto. Qed.
 Lemma impl_elim_r' P Q R : (Q ⊢ P → R) → P ∧ Q ⊢ R.
 Proof. intros; apply impl_elim with P; auto. Qed.
 Lemma impl_entails P Q : (True ⊢ P → Q) → P ⊢ Q.
-Proof. intros HPQ; apply impl_elim with (P)%I; auto. rewrite -HPQ; auto. Qed.
+Proof. intros HPQ; apply impl_elim with (P)%IP; auto. rewrite -HPQ; auto. Qed.
 Lemma entails_impl P Q : (P ⊢ Q) → True ⊢ P → Q.
 Proof. auto using impl_intro_l. Qed.

@@ -819,21 +819,21 @@ Global Instance or_idem : IdemP (⊣⊢) (@uPred_or M).
 Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
 Global Instance and_comm : Comm (⊣⊢) (@uPred_and M).
 Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.
-Global Instance True_and : LeftId (⊣⊢) True%I (@uPred_and M).
+Global Instance True_and : LeftId (⊣⊢) True%IP (@uPred_and M).
 Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
-Global Instance and_True : RightId (⊣⊢) True%I (@uPred_and M).
+Global Instance and_True : RightId (⊣⊢) True%IP (@uPred_and M).
 Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
-Global Instance False_and : LeftAbsorb (⊣⊢) False%I (@uPred_and M).
+Global Instance False_and : LeftAbsorb (⊣⊢) False%IP (@uPred_and M).
 Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
-Global Instance and_False : RightAbsorb (⊣⊢) False%I (@uPred_and M).
+Global Instance and_False : RightAbsorb (⊣⊢) False%IP (@uPred_and M).
 Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
-Global Instance True_or : LeftAbsorb (⊣⊢) True%I (@uPred_or M).
+Global Instance True_or : LeftAbsorb (⊣⊢) True%IP (@uPred_or M).
 Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
-Global Instance or_True : RightAbsorb (⊣⊢) True%I (@uPred_or M).
+Global Instance or_True : RightAbsorb (⊣⊢) True%IP (@uPred_or M).
 Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
-Global Instance False_or : LeftId (⊣⊢) False%I (@uPred_or M).
+Global Instance False_or : LeftId (⊣⊢) False%IP (@uPred_or M).
 Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
-Global Instance or_False : RightId (⊣⊢) False%I (@uPred_or M).
+Global Instance or_False : RightId (⊣⊢) False%IP (@uPred_or M).
 Proof. intros P; apply (anti_symm (⊢)); auto. Qed.
 Global Instance and_assoc : Assoc (⊣⊢) (@uPred_and M).
 Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.
@@ -841,10 +841,10 @@ Global Instance or_comm : Comm (⊣⊢) (@uPred_or M).
 Proof. intros P Q; apply (anti_symm (⊢)); auto. Qed.
 Global Instance or_assoc : Assoc (⊣⊢) (@uPred_or M).
 Proof. intros P Q R; apply (anti_symm (⊢)); auto. Qed.
-Global Instance True_impl : LeftId (⊣⊢) True%I (@uPred_impl M).
+Global Instance True_impl : LeftId (⊣⊢) True%IP (@uPred_impl M).
 Proof.
  intros P; apply (anti_symm (⊢)).
-  - by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
+  - by rewrite -(left_id True%IP uPred_and (_ → _)%IP) impl_elim_r.
  - by apply impl_intro_l; rewrite left_id.
 Qed.

@@ -875,7 +875,7 @@ Proof.
  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
 Qed.

-Lemma impl_curry P Q R : ((P ∧ Q) → R)%I ⊣⊢ (P → Q → R)%I.
+Lemma impl_curry P Q R : ((P ∧ Q) → R)%IP ⊣⊢ (P → Q → R)%IP.
 Proof.
  apply (anti_symm (⊢)).
  - apply impl_intro_r.
@@ -906,12 +906,12 @@ Lemma equiv_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. by intros ->. Qed.
 Lemma eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
 Proof.
-  specialize (eq_rewrite a b (λ b, b ≡ a)%I). intros H.
+  specialize (eq_rewrite a b (λ b, b ≡ a)%IP). intros H.
  erewrite H; eauto; intros n; solve_proper.
 Qed.
 Lemma eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
 Proof.
-  apply (eq_rewrite P Q (λ Q, P ↔ Q))%I; auto using iff_refl.
+  apply (eq_rewrite P Q (λ Q, P ↔ Q))%IP; auto using iff_refl.
  intros n; solve_proper.
 Qed.

@@ -922,7 +922,7 @@ Proof.
  split; intros n' x y ?? (x1&x2&y1&y2&?&?&?&?); exists x1,x2,y1,y2; ofe_subst x; ofe_subst y.
    split_and!; eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
 Qed.
-Global Instance Emp_sep : LeftId (⊣⊢) Emp%I (@uPred_sep M).
+Global Instance Emp_sep : LeftId (⊣⊢) Emp%IP (@uPred_sep M).
 Proof.
  intros P; unseal; split=> n x y Hvalid Hvalidy; split.
  - intros (x1&x2&y1&y2&?&?&?&?); ofe_subst. 
@@ -991,21 +991,21 @@ Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.

 Lemma emp_True: Emp ⊣⊢ ⧆True.
 Proof. rewrite affine_equiv left_id. auto. Qed.
-Global Instance sep_Emp : RightId (⊣⊢) Emp%I (@uPred_sep M).
+Global Instance sep_Emp : RightId (⊣⊢) Emp%IP (@uPred_sep M).
 Proof. by intros P; rewrite comm left_id. Qed.
 Lemma sep_elim_l P Q : P ★ ⧆Q ⊢ P.
 Proof. by rewrite (True_intro Q) -emp_True right_id. Qed.
 Lemma sep_elim_r P Q : ⧆P ★ Q ⊢ Q.
-Proof. by rewrite (comm (★))%I; apply sep_elim_l. Qed.
+Proof. by rewrite (comm (★))%IP; apply sep_elim_l. Qed.
 Lemma sep_elim_l' P Q R : (P ⊢ R) → P ★ ⧆Q ⊢ R.
 Proof. intros ->; apply sep_elim_l. Qed.
 Lemma sep_elim_r' P Q R : (Q ⊢ R) → ⧆P ★ Q ⊢ R.
 Proof. intros ->; apply sep_elim_r. Qed.
 Hint Resolve sep_elim_l' sep_elim_r'.
 Lemma sep_intro_Emp_l P Q R : (Emp ⊢ P) → (R ⊢ Q) → (R ⊢ P ★ Q).
-Proof. by intros; rewrite -(left_id Emp%I uPred_sep R); apply sep_mono. Qed.
+Proof. by intros; rewrite -(left_id Emp%IP uPred_sep R); apply sep_mono. Qed.
 Lemma sep_intro_Emp_r P Q R : (R ⊢ P) → (Emp ⊢ Q) → (R ⊢ P ★ Q).
-Proof. by intros; rewrite -(right_id Emp%I uPred_sep R); apply sep_mono. Qed.
+Proof. by intros; rewrite -(right_id Emp%IP uPred_sep R); apply sep_mono. Qed.
 Lemma sep_elim_Emp_l P Q R : (Emp ⊢ P) → (P ★ R ⊢ Q) → R ⊢ Q.
 Proof. by intros HP; rewrite -HP left_id. Qed.
 Lemma sep_elim_Emp_r P Q R : (Emp ⊢ P) → (R ★ P ⊢ Q) → R ⊢ Q.
@@ -1054,10 +1054,10 @@ Lemma wand_frame_l P Q R : (Q -★ R) ⊢ P ★ Q -★ P ★ R.
 Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
 Lemma wand_frame_r P Q R : (Q -★ R) ⊢ Q ★ P -★ R ★ P.
 Proof.
-  apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc.
+  apply wand_intro_l. rewrite ![(_ ★ P)%IP]comm -assoc.
  apply sep_mono_r, wand_elim_r.
 Qed.
-Lemma wand_iff_emp P : Emp ⊢ ((P -★ P) ∧ (P -★ P))%I.
+Lemma wand_iff_emp P : Emp ⊢ ((P -★ P) ∧ (P -★ P))%IP.
 Proof. by apply and_intro; apply wand_intro_l; rewrite ?right_id. Qed.
 Lemma equiv_wand_iff P Q : P ⊣⊢ Q → Emp ⊢ ((P -★ Q) ∧ (Q -★ P)).
 Proof. intros ->. apply wand_iff_emp. Qed.
@@ -1110,11 +1110,11 @@ Qed.
 Lemma pure_elim_sep_r φ Q R : (φ → Q ⊢ R) → Q ★ ⧆■ φ ⊢ R.
 Proof. intros; eapply (pure_elim_spare φ _ Q); eauto. rewrite comm; eauto. Qed.

-Global Instance sep_False : LeftAbsorb (⊣⊢) False%I (@uPred_sep M).
+Global Instance sep_False : LeftAbsorb (⊣⊢) False%IP (@uPred_sep M).
 Proof. intros P; apply (anti_symm _); auto. 
       unseal; split; naive_solver.
 Qed.
-Global Instance False_sep : RightAbsorb (⊣⊢) False%I (@uPred_sep M).
+Global Instance False_sep : RightAbsorb (⊣⊢) False%IP (@uPred_sep M).
 Proof. intros P; apply (anti_symm _); auto. 
       unseal; split; naive_solver.
 Qed.
@@ -1547,6 +1547,13 @@ Proof.
  by rewrite Hempty ?persistent_core in HP *.
 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.
+
+
 Global Instance relevant_if_ne n p : Proper (dist n ==> dist n) (@uPred_relevant_if M p).
 Proof. intros ?? ?. destruct p => //=. rewrite H. reflexivity. Qed.
 Global Instance relevant_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_relevant_if M p).
@@ -1686,7 +1693,7 @@ Proof. unseal; by split=> -[|n] x y. Qed.
 Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊢ (▷ ∃ a, Φ a).
 Proof. unseal; by split=> -[|[|n]] x y. Qed.
 Lemma later_exist_2 `{Inhabited A} (Φ : A → uPred M) :
-  (▷ ∃ a, Φ a)%I ⊢ (∃ a, ▷ Φ a)%I.
+  (▷ ∃ a, Φ a)%IP ⊢ (∃ a, ▷ Φ a)%IP.
 Proof. unseal; split=> -[|[|n]] x y; done || by exists inhabitant. Qed.
 Lemma later_sep P Q : ▷ (P ★ Q) ⊣⊢ ▷ P ★ ▷ Q.
 Proof.
@@ -1956,10 +1963,10 @@ Proof.
    apply HP, uPred_closed with n; eauto using cmra_validN_le.
 Qed.

-Global Instance pure_timeless φ : TimelessP (■ φ : uPred M)%I.
+Global Instance pure_timeless φ : TimelessP (■ φ : uPred M)%IP.
 Proof. by apply timelessP_spec; unseal => -[|n] x. Qed.
 Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
-   TimelessP (✓ a : uPred M)%I.
+   TimelessP (✓ a : uPred M)%IP.
 Proof.
  apply timelessP_spec; unseal=> n x y /=. by rewrite -!cmra_discrete_valid_iff.
 Qed.
@@ -2003,7 +2010,7 @@ Proof.
    [|intros [a ?]; exists a; apply HΨ].
 Qed.
 Global Instance eq_timeless {A : ofeT} (a b : A) :
-  Discrete a → TimelessP (a ≡ b : uPred M)%I.
+  Discrete a → TimelessP (a ≡ b : uPred M)%IP.
 Proof.
  intro; apply timelessP_spec; unseal=> n x y ???; by apply equiv_dist, discrete.
 Qed.
@@ -2041,10 +2048,10 @@ Qed.

 (* We could create an instance based on the above, but I will just directly
   create ATimeless instances for all of the things we already know to be Timeless *)
-Global Instance const_atimeless φ : ATimelessP (■ φ : uPred M)%I.
+Global Instance const_atimeless φ : ATimelessP (■ φ : uPred M)%IP.
 Proof. apply timeless_atimeless; apply _. Qed.
 Global Instance valid_atimeless {A : cmraT} `{CMRADiscrete A} (a : A) :
-   ATimelessP (✓ a : uPred M)%I.
+   ATimelessP (✓ a : uPred M)%IP.
 Proof. apply timeless_atimeless; apply _. Qed.
 Global Instance and_atimeless P Q: ATimelessP P → ATimelessP Q → ATimelessP (P ∧ Q).
 Proof. rewrite /ATimelessP later_and ?affine_and or_and_r; apply and_mono. Qed.
@@ -2117,18 +2124,18 @@ Proof.
  by rewrite -affine_affine_later HP affine_affine0.
 Qed.
 Global Instance eq_atimeless {A : ofeT} (a b : A) :
-  Discrete a → ATimelessP (a ≡ b : uPred M)%I.
+  Discrete a → ATimelessP (a ≡ b : uPred M)%IP.
 Proof. intros. apply timeless_atimeless; apply _. Qed.
 Global Instance ownM_atimeless (a : M) : Discrete a → ATimelessP (uPred_ownM a).
 Proof. intros. apply timeless_atimeless; apply _. Qed.

 (* Relevance *)
-Global Instance emp_relevant: RelevantP (Emp: uPred M)%I.
+Global Instance emp_relevant: RelevantP (Emp: uPred M)%IP.
 Proof. 
  rewrite /RelevantP. unseal. split=> n x y ??. simpl; intros ->. 
  rewrite persistent_core; auto.
 Qed.
-Global Instance pure_relevant φ : RelevantP (⧆■ φ : uPred M)%I.
+Global Instance pure_relevant φ : RelevantP (⧆■ φ : uPred M)%IP.
 Proof. by rewrite /RelevantP relevant_pure. Qed.
 Global Instance relevant_relevant P : RelevantP (□ P).
 Proof. by intros; apply relevant_intro'. Qed.
@@ -2155,15 +2162,8 @@ Global Instance exist_relevant {A} (Ψ : A → uPred M) :
  (∀ x, RelevantP (Ψ x)) → RelevantP (∃ x, Ψ x).
 Proof. by intros; rewrite /RelevantP relevant_exist; apply exist_mono. Qed.
 Global Instance eq_relevant {A : ofeT} (a b : A) :
-  RelevantP (⧆ (a ≡ b) : uPred M)%I.
+  RelevantP (⧆ (a ≡ b) : uPred M)%IP.
 Proof. by intros; rewrite /RelevantP relevant_eq. Qed.
-Global Instance valid_relevant {A : cmraT} (a : A) :
-  RelevantP (⧆✓ a : uPred M)%I.
-Proof. by intros; rewrite /RelevantP relevant_valid. Qed.
-Global Instance ownM_relevant : Persistent a → RelevantP (⧆(@uPred_ownM M a)).
-Proof. intros; rewrite /RelevantP. rewrite relevant_affine unlimited_ownM //=. Qed.
-Global Instance ownMl_relevant : Persistent a → RelevantP (@uPred_ownMl M a).
-Proof. intros; rewrite /RelevantP. rewrite relevant_ownMl //=. Qed.
 Global Instance default_relevant {A} P (Ψ : A → uPred M) (mx : option A) :
  RelevantP P → (∀ x, RelevantP (Ψ x)) → RelevantP (default P mx Ψ).
 Proof. destruct mx; apply _. Qed.
@@ -2195,7 +2195,7 @@ Global Instance affine_affine' P : AffineP (⧆ P).
 Proof. rewrite /AffineP ?affine_equiv; auto. Qed.
 Global Instance affine_relevant' P : AffineP P → AffineP (□ P).
 Proof. intros. rewrite /AffineP. rewrite -relevant_affine. auto. Qed.
-Global Instance emp_affine : AffineP (Emp: uPred M)%I.
+Global Instance emp_affine : AffineP (Emp: uPred M)%IP.
 Proof. by intros; rewrite /AffineP affine_equiv; auto. Qed.
 Global Instance and_affine P Q :
  AffineP P → AffineP Q → AffineP (P ∧ Q).
@@ -2244,6 +2244,3 @@ Hint Immediate True_intro False_elim : I.
 Hint Immediate iff_refl eq_refl' : I.

 End uPred.
-
-Undelimit Scope uPred_scope.
-Delimit Scope uPred_scope with IP.
--- a/theories/algebra/upred_bi.v
+++ b/theories/algebra/upred_bi.v
@@ -111,6 +111,7 @@ Canonical Structure uPredSI (M : ucmraT) : sbi :=
  {| sbi_ofe_mixin := ofe_mixin_of (uPred M);
     sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.

+(*
 Global Instance ownM_persistent {M: ucmraT} (a : M) :
  cmra.Persistent a → Persistent (uPred_ownM a).
 Proof.
@@ -120,16 +121,19 @@ Proof.
  - exists (core a). by rewrite cmra_core_r persistent_core.
  - by eexists.
 Qed.
+*)

 Global Notation "■ φ" := (uPred_pure φ%stdpp%type)
  (at level 20, right associativity) : bi_scope.
 Global Notation "⧆ P" := (bi_affinely P%I)
  (at level 20, right associativity) : bi_scope.
 Global Notation "⧈ P" := (bi_affinely (bi_persistently P%I))
-  (at level 20, right associativity) : uPred_scope.
+  (at level 20, right associativity) : bi_scope.
 Global Notation "✓ x" := (uPred_valid x) (at level 20) : bi_scope.
 Infix "★" := bi_sep : bi_scope.
 Notation "P -★ Q" := (bi_wand P Q) : bi_scope.
+Notation "■ φ" := (bi_pure φ%stdpp%type)
+  (at level 20, right associativity) : bi_scope.

 Lemma ownM_op {M: ucmraT} (a1 a2 : M) :
  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
@@ -185,4 +189,33 @@ Proof.
 Qed.

 Lemma ownMl_empty {M: ucmraT} : emp ⊣⊢ uPred_ownMl (∅: M).
-Proof. unseal; split=> n x y ??. rewrite /uPred_holds //=. Qed.
\ No newline at end of file
+Proof. unseal; split=> n x y ??. rewrite /uPred_holds //=. Qed.
+
+Lemma uPred_affine_bi_affinely {M: ucmraT} (P: uPred M):
+  uPred_affine P ⊣⊢  bi_affinely P.
+Proof.
+  rewrite affine_equiv. rewrite and_comm. by repeat unseal.
+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.
+  by rewrite relevant_affine affine_affine0.
+Qed.
+
+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 relevant_affine unlimited_ownM affine_affine0 //=.
+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 relevant_affine relevant_ownMl affine_affine0 //=.
+Qed.
\ No newline at end of file
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -179,7 +179,7 @@ Proof.
    rewrite /big_op ?right_id; auto.
  constructor; last constructor.
  rewrite /ht in Hht.
-  rewrite uPred.relevant_elim uPred.affine_elim in Hht *=>Hht.
+  rewrite bi.affinely_persistently_elim in Hht *=>Hht.
  eapply uPred.wand_elim_l' in Hht.
  rewrite left_id in Hht *=>Hht.
  eapply Hht; eauto.
@@ -229,7 +229,7 @@ Proof.
    exists (Res ∅ (Excl' σ1) ∅), (Res ∅ ∅ m2), (∅: iRes Λ Σ), (∅: iRes Λ Σ); split_and?.
    * by rewrite Res_op ?left_id ?right_id.
    * by rewrite Res_op ?left_id ?right_id.
-    * rewrite /uPred_holds //= /uPred_holds //=.
+    * uPred.unseal. rewrite /uPred_holds //= /uPred_holds //=.
    * by apply ownG_spec.
 Qed.


--- a/theories/program_logic/adequacy_inf.v
+++ b/theories/program_logic/adequacy_inf.v
@@ -255,7 +255,7 @@ Proof.
             econstructor. eapply cmra_stepN_S; eauto.
      ** intros (v&Hv). rewrite wp_eq in Hwp. 
         inversion Hwp as [? r rob v' Hpvs| ? ? ? ? Hnv Hgo]; subst; auto.
-         *** rewrite pvs_eq in Hpvs.
+         *** rewrite /pvs_FUpd pvs_eq in Hpvs.
             edestruct (Hpvs (S (S n)) ∅ σ (big_op k' ⋅ rf) (big_op k'' ⋅ rfl)) as (?&(Hob&?)); eauto.
             {
               rewrite right_id_L. simpl in Hwsat. simpl. 
@@ -558,7 +558,7 @@ Section bounded_nondet_hom2.
        ** rewrite Heq_b. auto.
    - econstructor; [|econstructor].
      rewrite /ht wp_eq in Hht *.
-      rewrite uPred.relevant_elim affine_elim in Hht *=>Hht.
+      rewrite bi.affinely_persistently_elim in Hht * => Hht.
      eapply wand_entails in Hht.
      eapply Hht.
      
@@ -575,7 +575,7 @@ Section bounded_nondet_hom2.
        ** exists (Res ∅ (Excl' σ) ∅), (Res ∅ ∅ m2), (∅: iRes Λ Σ), (∅: iRes Λ Σ); split_and?.
           *** by rewrite Res_op ?left_id ?right_id.
           *** by rewrite Res_op ?left_id ?right_id.
-           *** split; auto. rewrite /uPred_holds //=. 
+           *** uPred.unseal => //=. split; auto; rewrite /uPred_holds //=. 
           *** by apply ownG_spec.
   - simpl. rewrite right_id. rewrite /op //= /cmra_op //=.
     rewrite /res_op. simpl. rewrite ?right_id.

--- a/theories/program_logic/ghost_ownership.v
+++ b/theories/program_logic/ghost_ownership.v
 From stdpp Require Export functions.
-From fri.algebra Require Export iprod.
+From fri.algebra Require Export iprod upred.
 From fri.program_logic Require Export pviewshifts pstepshifts global_functor.
 From fri.program_logic Require Import ownership.
+From iris.proofmode Require Import tactics classes.
 Import uPred.
 Definition own_def `{inG Λ Σ (gmapUR gname A)} (γ : gname) (a : A) : iPropG Λ Σ :=
  ownG (to_globalF γ a).
@@ -49,35 +50,42 @@ Global Instance own_proper γ :

 Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2.
 Proof. by rewrite !own_eq /own_def -ownG_op to_globalF_op. Qed.
+Import uPred.
 Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (@own Λ Σ A _ γ).
 Proof. 
-  move=>a b [c ->]. rewrite own_op own_eq /own. apply sep_elim_l.
+  move=>a b [c ->]. rewrite own_op own_eq /own. apply sep_elim_l. apply _.
 Qed.
 Lemma own_valid γ a : own γ a ⊢ ⧆✓ a.
 Proof.
  rewrite !own_eq /own_def ownG_valid /to_globalF.
  rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
-  apply affine_mono.
+  apply affinely_mono.
  trans (✓ ucmra_transport (@inG_prf _ _ _ i) {[γ := a]} : iPropG Λ Σ)%I;
    last destruct inG_prf; auto.
  by rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
 Qed.
 Lemma own_valid_r γ a : own γ a ⊢ (own γ a ★ ⧆✓ a).
-Proof. apply: uPred.relevant_entails_r. apply own_valid. Qed.
+Proof.
+  iIntros "H". iAssert (bi_affinely (✓ a))%I with "[#]" as "$"; last done.
+  rewrite /bi_absorbingly; iSplitR "H"; auto.
+  by iApply own_valid.
+Qed.
 Lemma own_valid_l γ a : own γ a ⊢ (⧆✓ a ★ own γ a).
 Proof. by rewrite comm -own_valid_r. Qed.
+(*
 Global Instance own_atimeless γ a : Discrete a → ATimelessP (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
-Global Instance own_affine γ a : AffineP (own γ a).
+*)
+Global Instance own_affine γ a : Affine (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
-Global Instance own_core_persistent γ a : Persistent a → RelevantP (own γ a).
+Global Instance own_core_persistent γ a : cmra.Persistent a → Persistent (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.

 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
   assertion. However, the map_updateP_alloc does not suffice to show this. *)

 Lemma own_alloc_strong a E (G : gset gname) :
-  ✓ a → Emp ⊢ |={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a.
+  ✓ a → emp ⊢ |={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a.
 Proof.
  intros Ha.
  rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I).
@@ -90,17 +98,18 @@ Proof.
      exists γ. split_and!; eauto.
    * naive_solver.
  - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
-    by rewrite !own_eq -(exist_intro γ) pure_equiv // left_id.
+    by rewrite !own_eq -(exist_intro γ) pure_True // left_id.
 Qed.
 Lemma own_alloc_strong' a E (G : gset gname) :
-  ✓ a → Emp ⊢ |={E}=> ∃ γ, ⧆■(γ ∉ G) ★ own γ a.
+  ✓ a → emp ⊢ |={E}=> ∃ γ, ⧆■(γ ∉ G) ★ own γ a.
 Proof. 
  intros Ha. rewrite (own_alloc_strong a E G); auto.
  apply pvs_mono, exist_mono=>?.
-  rewrite -(affine_affine (own _ _)) affine_and_r.
-  by rewrite relevant_and_sep_l_1.
+  rewrite -(affine_affinely (own _ _)) affinely_and_r affinely_and.
+  by iIntros "(H1&H2)"; iFrame.
 Qed.
-Lemma own_alloc a E : ✓ a → Emp ⊢ (|={E}=> ∃ γ, own γ a).
+
+Lemma own_alloc a E : ✓ a → emp ⊢ (|={E}=> ∃ γ, own γ a).
 Proof.
  intros Ha. rewrite (own_alloc_strong a E ∅) //; [].
  apply pvs_mono, exist_mono=>?. eauto with I.
@@ -134,7 +143,7 @@ Section global_empty.
 Context `{i : inG Λ Σ (gmapUR gname (A:ucmraT))}.
 Implicit Types a : A.

-Lemma own_empty γ E : Emp ={E}=> own γ (∅:A).
+Lemma own_empty γ E : emp ={E}=> own γ (∅:A).
 Proof.
  rewrite ownG_empty !own_eq /own_def.
  apply pvs_ownG_update, cmra_update_updateP.
@@ -175,18 +184,24 @@ Lemma owne_valid a : owne a ⊢ ⧆✓ a.
 Proof.
  rewrite !owne_eq /owne_def ownG_valid /to_globalFe.
  rewrite iprod_validI (forall_elim (inG_id i)) iprod_lookup_singleton.
-  apply affine_mono.
+  apply affinely_mono.
  trans (✓ ucmra_transport inG_prf a : iPropG Λ Σ)%I; last destruct inG_prf; auto.
 Qed.
 Lemma owne_valid_r a : owne a ⊢ (owne a ★ ⧆✓ a).
-Proof. apply: uPred.relevant_entails_r. apply owne_valid. Qed.
+Proof.
+  iIntros "H". iAssert (bi_affinely (✓ a))%I with "[#]" as "$"; last done.
+  rewrite /bi_absorbingly; iSplitR "H"; auto.
+  by iApply owne_valid.
+Qed.
 Lemma owne_valid_l a : owne a ⊢ (⧆✓ a ★ owne a).
 Proof. by rewrite comm -owne_valid_r. Qed.
+(*
 Global Instance owne_atimeless a : Discrete a → ATimelessP (owne a).
 Proof. rewrite !owne_eq /owne_def; apply _. Qed.
-Global Instance owne_affine a : AffineP (owne a).
+*)
+Global Instance owne_affine a : Affine (owne a).
 Proof. rewrite !owne_eq /owne_def; apply _. Qed.
-Global Instance owne_core_persistent a : Persistent a → RelevantP (owne a).
+Global Instance owne_core_persistent a : cmra.Persistent a → Persistent (owne a).
 Proof. rewrite !owne_eq /owne_def; apply _. Qed.

 (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
@@ -211,7 +226,7 @@ Proof.
 Qed.

 Lemma owne_empty E :
-  Emp ={E}=> owne (∅:A).
+  emp ={E}=> owne (∅:A).
 Proof.
  rewrite ownG_empty !owne_eq /owne_def. apply pvs_ownG_update, cmra_update_updateP.
  eapply (iprod_singleton_updateP_empty (inG_id i)
@@ -263,11 +278,9 @@ Section globale_step.
      ** intros ->. unfold to_globalFe. rewrite ?iprod_lookup_singleton. 
         apply ucmra_transport_stepN. eauto.
      ** intros. eapply (AltTriv X); eauto.
-  - apply exist_elim=>m. apply exist_elim=>ml.
-    apply pure_elim_sep_l. intros (a'&al'&Heq_m&Heq_ml&HP).
-    subst. rewrite -(exist_intro a') -(exist_intro al'). 
-    rewrite pure_equiv; auto. rewrite -emp_True left_id. auto.
-
+  - iIntros "H". iDestruct "H" as (m ml) "(H&?&?)". 
+    iDestruct "H" as %(a'&al'&Heq_m&Heq_ml&HP).
+    subst. iExists a', al'. iFrame. iAlways; done.
 Qed.
  

@@ -289,17 +302,18 @@ Proof. by rewrite !ownle_eq /ownle_def -ownGl_op to_globalFe_op. Qed.