From 88c1dd291bec5b61d34e3e10abc5baee9775696a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Feb 2016 11:12:57 +0100
Subject: [PATCH] rename uPred_own -> uPred_ownM

---
 algebra/upred.v           | 24 ++++++++++++------------
 program_logic/ownership.v |  6 +++---
 2 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 29779ffb4..fa14a7632 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -174,7 +174,7 @@ Next Obligation.
     eauto using cmra_unit_preserving, cmra_unit_validN.
 Qed.
 
-Program Definition uPred_own {M : cmraT} (a : M) : uPred M :=
+Program Definition uPred_ownM {M : cmraT} (a : M) : uPred M :=
   {| uPred_holds n x := a ≼{n} x |}.
 Next Obligation. by intros M a x1 x2 n [a' ?] Hx; exists a'; rewrite -Hx. Qed.
 Next Obligation.
@@ -327,13 +327,13 @@ Global Instance always_ne n: Proper (dist n ==> dist n) (@uPred_always M).
 Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_validN. Qed.
 Global Instance always_proper :
   Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
-Global Instance own_ne n : Proper (dist n ==> dist n) (@uPred_own M).
+Global Instance own_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
 Proof.
   by intros a1 a2 Ha x n'; split; intros [a' ?]; exists a'; simpl; first
     [rewrite -(dist_le _ _ _ _ Ha); last lia
     |rewrite (dist_le _ _ _ _ Ha); last lia].
 Qed.
-Global Instance own_proper : Proper ((≡) ==> (≡)) (@uPred_own M) := ne_proper _.
+Global Instance own_proper : Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _.
 Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
 Proof. unfold uPred_iff; solve_proper. Qed.
 Global Instance iff_proper :
@@ -785,7 +785,7 @@ Proof. intros; rewrite -always_and_sep_r; auto. Qed.
 
 (* Own and valid *)
 Lemma ownM_op (a1 a2 : M) :
-  uPred_own (a1 ⋅ a2) ≡ (uPred_own a1 ★ uPred_own a2)%I.
+  uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
 Proof.
   intros x n ?; split.
   * intros [z ?]; exists a1, (a2 â‹… z); split; [by rewrite (associative op)|].
@@ -794,19 +794,19 @@ Proof.
     by rewrite (associative op _ z1) -(commutative op z1) (associative op z1)
       -(associative op _ a2) (commutative op z1) -Hy1 -Hy2.
 Qed.
-Lemma always_ownM_unit (a : M) : (□ uPred_own (unit a))%I ≡ uPred_own (unit a).
+Lemma always_ownM_unit (a : M) : (□ uPred_ownM (unit a))%I ≡ uPred_ownM (unit a).
 Proof.
   intros x n; split; [by apply always_elim|intros [a' Hx]]; simpl.
   rewrite -(cmra_unit_idempotent a) Hx.
   apply cmra_unit_preservingN, cmra_includedN_l.
 Qed.
-Lemma always_ownM (a : M) : unit a ≡ a → (□ uPred_own a)%I ≡ uPred_own a.
+Lemma always_ownM (a : M) : unit a ≡ a → (□ uPred_ownM a)%I ≡ uPred_ownM a.
 Proof. by intros <-; rewrite always_ownM_unit. Qed.
-Lemma ownM_something : True ⊑ ∃ a, uPred_own a.
+Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
 Proof. intros x n ??. by exists x; simpl. Qed.
-Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_own ∅.
+Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
 Proof. intros x n ??; by  exists x; rewrite (left_id _ _). Qed.
-Lemma ownM_valid (a : M) : uPred_own a ⊑ ✓ a.
+Lemma ownM_valid (a : M) : uPred_ownM a ⊑ ✓ a.
 Proof. intros x n Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
 Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ ✓ a.
 Proof. by intros ? x n ? _; simpl; apply cmra_valid_validN. Qed.
@@ -819,7 +819,7 @@ Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I
 Proof. done. Qed.
 
 (* Own and valid derived *)
-Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_own a ⊑ False.
+Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
 Proof. by intros; rewrite ownM_valid valid_elim. Qed.
 
 (* Big ops *)
@@ -904,7 +904,7 @@ Qed.
 Global Instance eq_timeless {A : cofeT} (a b : A) :
   Timeless a → TimelessP (a ≡ b : uPred M)%I.
 Proof. by intro; apply timelessP_spec=> x n ??; apply equiv_dist, timeless. Qed.
-Global Instance own_timeless (a : M) : Timeless a → TimelessP (uPred_own a).
+Global Instance own_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
 Proof.
   intros ?; apply timelessP_spec=> x [|n] ?? //; apply cmra_included_includedN,
     cmra_timeless_included_l; eauto using cmra_validN_le.
@@ -934,7 +934,7 @@ Global Instance valid_always_stable {A : cmraT} (a : A) : AS (✓ a : uPred M)%I
 Proof. by intros; rewrite /AlwaysStable always_valid. Qed.
 Global Instance later_always_stable P : AS P → AS (▷ P).
 Proof. by intros; rewrite /AlwaysStable always_later; apply later_mono. Qed.
-Global Instance own_unit_always_stable (a : M) : AS (uPred_own (unit a)).
+Global Instance own_unit_always_stable (a : M) : AS (uPred_ownM (unit a)).
 Proof. by rewrite /AlwaysStable always_ownM_unit. Qed.
 Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A) :
   AS P → (∀ x, AS (Q x)) → AS (default P mx Q).
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 10251bd8d..2f7de641b 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -1,10 +1,10 @@
 Require Export program_logic.model.
 
 Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
-  uPred_own (Res {[ i ↦ to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
+  uPred_ownM (Res {[ i ↦ to_agree (Next (iProp_unfold P)) ]} ∅ ∅).
 Arguments ownI {_ _} _ _%I.
-Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_own (Res ∅ (Excl σ) ∅).
-Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_own (Res ∅ ∅ (Some m)).
+Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_ownM (Res ∅ (Excl σ) ∅).
+Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownM (Res ∅ ∅ (Some m)).
 Instance: Params (@ownI) 3.
 Instance: Params (@ownP) 2.
 Instance: Params (@ownG) 2.
-- 
GitLab