From 7b0f3340947d060c88e55ae3466850342ffb1bc7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 10 Dec 2018 12:20:03 +0100
Subject: [PATCH] Get rid of some `uPred M` coercions.
---
theories/algebra/agree.v | 4 ++--
theories/algebra/auth.v | 16 ++++++++--------
theories/algebra/csum.v | 22 +++++++++++-----------
theories/algebra/excl.v | 16 ++++++++--------
theories/algebra/gmap.v | 4 ++--
theories/algebra/list.v | 4 ++--
6 files changed, 33 insertions(+), 33 deletions(-)
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 34c9e7e43..171bc5bf3 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -233,13 +233,13 @@ Lemma agree_op_invL' `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b)
Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed.
(** Internalized properties *)
-Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢ (a ≡ b : uPred M).
+Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ b).
Proof.
uPred.unseal. do 2 split.
- intros Hx. exact: to_agree_injN.
- intros Hx. exact: to_agree_ne.
Qed.
-Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢ (x ≡ y : uPred M).
+Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢@{uPredI M} x ≡ y.
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
End agree.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index a5f62158a..eb3952222 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -191,15 +191,15 @@ Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
Proof. do 2 constructor; simpl; auto. by apply core_id_core. Qed.
(** Internalized properties *)
-Lemma auth_equivI {M} (x y : auth A) :
- x ≡ y ⊣⊢ (authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y : uPred M).
+Lemma auth_equivI {M} x y :
+ x ≡ y ⊣⊢@{uPredI M} authoritative x ≡ authoritative y ∧ auth_own x ≡ auth_own y.
Proof. by uPred.unseal. Qed.
-Lemma auth_validI {M} (x : auth A) :
- ✓ x ⊣⊢ (match authoritative x with
- | Excl' a => (∃ b, a ≡ auth_own x ⋅ b) ∧ ✓ a
- | None => ✓ auth_own x
- | ExclBot' => False
- end : uPred M).
+Lemma auth_validI {M} x :
+ ✓ x ⊣⊢@{uPredI M} match authoritative x with
+ | Excl' a => (∃ b, a ≡ auth_own x ⋅ b) ∧ ✓ a
+ | None => ✓ auth_own x
+ | ExclBot' => False
+ end.
Proof. uPred.unseal. by destruct x as [[[]|]]. Qed.
Lemma auth_frag_op a b : â—¯ (a â‹… b) = â—¯ a â‹… â—¯ b.
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 7e3c9047c..cab3953aa 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -284,22 +284,22 @@ Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
(** Internalized properties *)
Lemma csum_equivI {M} (x y : csum A B) :
- x ≡ y ⊣⊢ (match x, y with
- | Cinl a, Cinl a' => a ≡ a'
- | Cinr b, Cinr b' => b ≡ b'
- | CsumBot, CsumBot => True
- | _, _ => False
- end : uPred M).
+ x ≡ y ⊣⊢@{uPredI M} match x, y with
+ | Cinl a, Cinl a' => a ≡ a'
+ | Cinr b, Cinr b' => b ≡ b'
+ | CsumBot, CsumBot => True
+ | _, _ => False
+ end.
Proof.
uPred.unseal; do 2 split; first by destruct 1.
by destruct x, y; try destruct 1; try constructor.
Qed.
Lemma csum_validI {M} (x : csum A B) :
- ✓ x ⊣⊢ (match x with
- | Cinl a => ✓ a
- | Cinr b => ✓ b
- | CsumBot => False
- end : uPred M).
+ ✓ x ⊣⊢@{uPredI M} match x with
+ | Cinl a => ✓ a
+ | Cinr b => ✓ b
+ | CsumBot => False
+ end.
Proof. uPred.unseal. by destruct x. Qed.
(** Updates *)
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index ddf7a9295..8eff76e1a 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -95,17 +95,17 @@ Global Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
Proof. split. apply _. by intros []. Qed.
(** Internalized properties *)
-Lemma excl_equivI {M} (x y : excl A) :
- x ≡ y ⊣⊢ (match x, y with
- | Excl a, Excl b => a ≡ b
- | ExclBot, ExclBot => True
- | _, _ => False
- end : uPred M).
+Lemma excl_equivI {M} x y :
+ x ≡ y ⊣⊢@{uPredI M} match x, y with
+ | Excl a, Excl b => a ≡ b
+ | ExclBot, ExclBot => True
+ | _, _ => False
+ end.
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
Qed.
-Lemma excl_validI {M} (x : excl A) :
- ✓ x ⊣⊢ (if x is ExclBot then False else True : uPred M).
+Lemma excl_validI {M} x :
+ ✓ x ⊣⊢@{uPredI M} if x is ExclBot then False else True.
Proof. uPred.unseal. by destruct x. Qed.
(** Exclusive *)
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 835c77941..9b194ac4f 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -177,9 +177,9 @@ Qed.
Canonical Structure gmapUR := UcmraT (gmap K A) gmap_ucmra_mixin.
(** Internalized properties *)
-Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
+Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢@{uPredI M} ∀ i, m1 !! i ≡ m2 !! i.
Proof. by uPred.unseal. Qed.
-Lemma gmap_validI {M} m : ✓ m ⊣⊢ (∀ i, ✓ (m !! i) : uPred M).
+Lemma gmap_validI {M} m : ✓ m ⊣⊢@{uPredI M} ∀ i, ✓ (m !! i).
Proof. by uPred.unseal. Qed.
End cmra.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index c620e931f..5e57d9d16 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -247,9 +247,9 @@ Section cmra.
Qed.
(** Internalized properties *)
- Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M).
+ Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢@{uPredI M} ∀ i, l1 !! i ≡ l2 !! i.
Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
- Lemma list_validI {M} l : ✓ l ⊣⊢ (∀ i, ✓ (l !! i) : uPred M).
+ Lemma list_validI {M} l : ✓ l ⊣⊢@{uPredI M} ∀ i, ✓ (l !! i).
Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
End cmra.
--
GitLab