Merge branch 'ci/robbert/I' into 'master'

Remove redundant `%I` scopes in definitions.

See merge request iris/iris!457

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 φ).
 

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 := {}.

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 :=

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,

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).

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).

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 φ).
 

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 := {}.

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.

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).

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.

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).

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 ()).
 

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.