diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index c9b0414bd036adee6ccf79ead28807d6001fb6f2..d5d4ade215f6820fe2aa64c257645ade9c74f07f 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -21,7 +21,7 @@ Section definitions.
Definition auth_own (a : A) : iProp Σ :=
own γ (◯ a).
Definition auth_inv (f : T → A) (φ : T → iProp Σ) : iProp Σ :=
- (∃ t, own γ (◠f t) ∗ φ t)%I.
+ ∃ t, own γ (◠f t) ∗ φ t.
Definition auth_ctx (N : namespace) (f : T → A) (φ : T → iProp Σ) : iProp Σ :=
inv N (auth_inv f φ).
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index a0a9c99ffb7c84ea67c54dd76b54f403d7c71502..eaea54618da18fe222d60306223fb25488d6747d 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -28,16 +28,16 @@ Section box_defs.
own γ (ε, Some (to_agree (Next (iProp_unfold P)))).
Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
- (∃ b, box_own_auth γ (â—E b) ∗ if b then P else True)%I.
+ ∃ b, box_own_auth γ (â—E b) ∗ if b then P else True.
Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
- (box_own_prop γ P ∗ inv N (slice_inv γ P))%I.
+ box_own_prop γ P ∗ inv N (slice_inv γ P).
Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
- (∃ Φ : slice_name → iProp Σ,
+ ∃ Φ : slice_name → iProp Σ,
▷ (P ≡ [∗ map] γ ↦ _ ∈ f, Φ γ) ∗
[∗ map] γ ↦ b ∈ f, box_own_auth γ (◯E b) ∗ box_own_prop γ (Φ γ) ∗
- inv N (slice_inv γ (Φ γ)))%I.
+ inv N (slice_inv γ (Φ γ)).
End box_defs.
Instance: Params (@box_own_prop) 3 := {}.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index f4e50cb5684a4aab56d6682be3e4c052710e7501..ce392cb8229ae41519d8e9a9d7f8a7b5367bd119 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -8,7 +8,7 @@ Export invG.
Import uPred.
Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
- (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
+ wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P).
Definition uPred_fupd_aux `{!invG Σ} : seal uPred_fupd_def. Proof. by eexists. Qed.
Definition uPred_fupd `{!invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
diff --git a/theories/base_logic/lib/fancy_updates_from_vs.v b/theories/base_logic/lib/fancy_updates_from_vs.v
index 12cbff8f3d0b0c6b5dc0ad85c7b4ed4775b6bfce..80b52c855ec7b08ec24cd90fd05929855220c396 100644
--- a/theories/base_logic/lib/fancy_updates_from_vs.v
+++ b/theories/base_logic/lib/fancy_updates_from_vs.v
@@ -29,7 +29,7 @@ Context (vs_persistent_intro_r : ∀ E1 E2 P Q R,
(R -∗ (P ={E1,E2}=> Q)) ⊢ P ∗ R ={E1,E2}=> Q).
Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M :=
- (∃ R, R ∗ vs E1 E2 R P)%I.
+ ∃ R, R ∗ vs E1 E2 R P.
Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
(at level 99, E1, E2 at level 50, Q at level 200,
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index afeaad2084af22e38e601201beb217ce9dfe97ad..5eeff6cdb5bb9a37c39204d345d56c12c3b2f9e3 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -97,12 +97,12 @@ Proof. solve_inG. Qed.
Section definitions.
Context `{Countable L, hG : !gen_heapG L V Σ}.
- Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := (∃ m,
+ Definition gen_heap_ctx (σ : gmap L V) : iProp Σ := ∃ m,
(* The [⊆] is used to avoid assigning ghost information to the locations in
the initial heap (see [gen_heap_init]). *)
⌜ dom _ m ⊆ dom (gset L) σ ⌠∧
own (gen_heap_name hG) (◠(to_gen_heap σ)) ∗
- own (gen_meta_name hG) (â— (to_gen_meta m)))%I.
+ own (gen_meta_name hG) (â— (to_gen_meta m)).
Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
own (gen_heap_name hG) (â—¯ {[ l := (q, to_agree (v : leibnizO V)) ]}).
@@ -111,15 +111,15 @@ Section definitions.
Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
- (∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
- own γm (namespace_map_token E))%I.
+ ∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
+ own γm (namespace_map_token E).
Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
Definition meta_token := meta_token_aux.(unseal).
Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
- (∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
- own γm (namespace_map_data N (to_agree (encode x))))%I.
+ ∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
+ own γm (namespace_map_data N (to_agree (encode x))).
Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index fc4d9fb37c167f293a4f780b28f6f8ff4cadb7aa..43b606651278774da08f714772377f12f531dad7 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -8,7 +8,7 @@ Import uPred.
(** Semantic Invariants *)
Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
- (□ ∀ E, ⌜↑N ⊆ E⌠→ |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True))%I.
+ □ ∀ E, ⌜↑N ⊆ E⌠→ |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
Definition inv {Σ i} := inv_aux.(unseal) Σ i.
Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
@@ -25,7 +25,7 @@ Section inv.
(** ** Internal model of invariants *)
Definition own_inv (N : namespace) (P : iProp Σ) : iProp Σ :=
- (∃ i, ⌜i ∈ (↑N:coPset)⌠∧ ownI i P)%I.
+ ∃ i, ⌜i ∈ (↑N:coPset)⌠∧ ownI i P.
Lemma own_inv_acc E N P :
↑N ⊆ E → own_inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index a283029322e6399e06550ac90744331a88266f9c..05abc0e46770dae5df506d1cfd8b6d5dab3bbec2 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -23,7 +23,7 @@ Section definitions.
Definition sts_own (s : sts.state sts) (T : sts.tokens sts) : iProp Σ :=
own γ (sts_frag_up s T).
Definition sts_inv (φ : sts.state sts → iProp Σ) : iProp Σ :=
- (∃ s, own γ (sts_auth s ∅) ∗ φ s)%I.
+ ∃ s, own γ (sts_auth s ∅) ∗ φ s.
Definition sts_ctx `{!invG Σ} (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ :=
inv N (sts_inv φ).
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 6e367b79e5a86077d1fad23cdd3adee46af5341f..baff426f0f0c40f9f6d039a20068d72bdf361d04 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export invariants.
Set Default Proof Using "Type".
Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
- (□ (P -∗ |={E1,E2}=> Q))%I.
+ □ (P -∗ |={E1,E2}=> Q).
Arguments vs {_ _} _ _ _%I _%I.
Instance: Params (@vs) 4 := {}.
diff --git a/theories/heap_lang/lib/clairvoyant_coin.v b/theories/heap_lang/lib/clairvoyant_coin.v
index 87aa3c437ab14a599e9a3bf95eb09b75bfd17394..a865289baead07a0b4a1eb17917f923d18480911 100644
--- a/theories/heap_lang/lib/clairvoyant_coin.v
+++ b/theories/heap_lang/lib/clairvoyant_coin.v
@@ -29,11 +29,11 @@ Section proof.
(λ v, bool_decide (v = #true)) ∘ snd <$> vs.
Definition coin (cp : val) (bs : list bool) : iProp Σ :=
- (∃ (c : loc) (p : proph_id) (vs : list (val * val)),
- ⌜cp = (#c, #p)%V⌠∗
- ⌜bs ≠[]⌠∗ ⌜tail bs = prophecy_to_list_bool vs⌠∗
- proph p vs ∗
- from_option (λ b : bool, c ↦ #b) (∃ b : bool, c ↦ #b) (head bs))%I.
+ ∃ (c : loc) (p : proph_id) (vs : list (val * val)),
+ ⌜cp = (#c, #p)%V⌠∗
+ ⌜bs ≠[]⌠∗ ⌜tail bs = prophecy_to_list_bool vs⌠∗
+ proph p vs ∗
+ from_option (λ b : bool, c ↦ #b) (∃ b : bool, c ↦ #b) (head bs).
Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c bs, RET c; coin c bs }}}.
Proof.
diff --git a/theories/heap_lang/lib/counter.v b/theories/heap_lang/lib/counter.v
index 1d0fd7083b8554902c43642666309549d43e7ccc..c7992d8b3ff5377d80f50d1004a9f3b9ecb94e76 100644
--- a/theories/heap_lang/lib/counter.v
+++ b/theories/heap_lang/lib/counter.v
@@ -23,10 +23,10 @@ Section mono_proof.
Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ :=
- (∃ n, own γ (◠(n : mnat)) ∗ l ↦ #n)%I.
+ ∃ n, own γ (◠(n : mnat)) ∗ l ↦ #n.
Definition mcounter (l : loc) (n : nat) : iProp Σ :=
- (∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
+ ∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)).
(** The main proofs. *)
Global Instance mcounter_persistent l n : Persistent (mcounter l n).
@@ -97,7 +97,7 @@ Section contrib_spec.
Context `{!heapG Σ, !ccounterG Σ} (N : namespace).
Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
- (∃ n, own γ (â—F n) ∗ l ↦ #n)%I.
+ ∃ n, own γ (â—F n) ∗ l ↦ #n.
Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
inv N (ccounter_inv γ l).
diff --git a/theories/heap_lang/lib/lazy_coin.v b/theories/heap_lang/lib/lazy_coin.v
index c1acf7ed59d9bbca07479f2a67ae4579c07872ae..b22c0707a2cd57826d614118d1cba0108b8c4bcc 100644
--- a/theories/heap_lang/lib/lazy_coin.v
+++ b/theories/heap_lang/lib/lazy_coin.v
@@ -28,9 +28,9 @@ Section proof.
Proof. by destruct b. Qed.
Definition coin (cp : val) (b : bool) : iProp Σ :=
- (∃ (c : loc) (p : proph_id) (vs : list (val * val)),
- ⌜cp = (#c, #p)%V⌠∗ proph p vs ∗
- (c ↦ SOMEV #b ∨ (c ↦ NONEV ∗ ⌜b = prophecy_to_bool vsâŒ)))%I.
+ ∃ (c : loc) (p : proph_id) (vs : list (val * val)),
+ ⌜cp = (#c, #p)%V⌠∗ proph p vs ∗
+ (c ↦ SOMEV #b ∨ (c ↦ NONEV ∗ ⌜b = prophecy_to_bool vsâŒ)).
Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c b, RET c; coin c b }}}.
Proof.
diff --git a/theories/heap_lang/lib/spawn.v b/theories/heap_lang/lib/spawn.v
index 5b78e389c96b194c94e975f55b19d01ce4982d79..78bb229190d7606b06c4f38ce1033e09768976af 100644
--- a/theories/heap_lang/lib/spawn.v
+++ b/theories/heap_lang/lib/spawn.v
@@ -30,11 +30,11 @@ Section proof.
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
- (∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌠∨
- ∃ w, ⌜lv = SOMEV w⌠∗ (Ψ w ∨ own γ (Excl ()))))%I.
+ ∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌠∨
+ ∃ w, ⌜lv = SOMEV w⌠∗ (Ψ w ∨ own γ (Excl ()))).
Definition join_handle (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
- (∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ))%I.
+ ∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ).
Global Instance spawn_inv_ne n γ l :
Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 102024ff3eccef887fd563039ecd816be08e2f43..33d4fa87f7dc2458b2cb69172ba26509b3422583 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -25,10 +25,10 @@ Section proof.
Let N := nroot .@ "spin_lock".
Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
- (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
+ ∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R.
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
- (∃ l: loc, ⌜lk = #l⌠∧ inv N (lock_inv γ l R))%I.
+ ∃ l: loc, ⌜lk = #l⌠∧ inv N (lock_inv γ l R).
Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index be61915fa83a00557e9f934db763c6b070a91659..82ce5f2f921c44cf9ee00b2b6f87ec1b0454a051 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -41,19 +41,19 @@ Section proof.
Let N := nroot .@ "ticket_lock".
Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
- (∃ o n : nat,
+ ∃ o n : nat,
lo ↦ #o ∗ ln ↦ #n ∗
own γ (◠(Excl' o, GSet (set_seq 0 n))) ∗
- ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε, GSet {[ o ]}))))%I.
+ ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε, GSet {[ o ]}))).
Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
- (∃ lo ln : loc,
- ⌜lk = (#lo, #ln)%V⌠∗ inv N (lock_inv γ lo ln R))%I.
+ ∃ lo ln : loc,
+ ⌜lk = (#lo, #ln)%V⌠∗ inv N (lock_inv γ lo ln R).
Definition issued (γ : gname) (x : nat) : iProp Σ :=
- own γ (◯ (ε, GSet {[ x ]}))%I.
+ own γ (◯ (ε, GSet {[ x ]})).
- Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, GSet ∅)))%I.
+ Definition locked (γ : gname) : iProp Σ := ∃ o, own γ (◯ (Excl' o, GSet ∅)).
Global Instance lock_inv_ne γ lo ln : NonExpansive (lock_inv γ lo ln).
Proof. solve_proper. Qed.