diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index ead999ce2a4a649c31912eb8a7f800653ed54d8b..138969cfca5b87a2767ffbb2149a2e74a0a630c0 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -10,7 +10,7 @@ Section upred.
Context {M : ucmra}.
(* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
@@ -146,7 +146,7 @@ Section view.
Qed.
Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b :
(∀ n (x : M), relI n x → rel n a b) →
- ⌜✓dqâŒ%Qp ∧ relI ⊢ ✓ (â—V{dq} a â‹… â—¯V b : view rel).
+ ⌜✓dq⌠∧ relI ⊢ ✓ (â—V{dq} a â‹… â—¯V b : view rel).
Proof.
intros Hrel. uPred.unseal. split=> n x _ /=.
rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
diff --git a/iris/base_logic/bupd_alt.v b/iris/base_logic/bupd_alt.v
index 5c6868233d08f3a66277337671d2979b466c98f2..e97df5dd1b09775cc0083ae0a92ca8accad21f6a 100644
--- a/iris/base_logic/bupd_alt.v
+++ b/iris/base_logic/bupd_alt.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type*".
(** This file contains an alternative version of basic updates, that is
expression in terms of just the plain modality [â– ]. *)
Definition bupd_alt `{BiPlainly PROP} (P : PROP) : PROP :=
- (∀ R, (P -∗ ■R) -∗ ■R)%I.
+ ∀ R, (P -∗ ■R) -∗ ■R.
(** This definition is stated for any BI with a plain modality. The above
definition is akin to the continuation monad, where one should think of [â– R]
diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index b81a3b475cbae9e93dc284185e08de8ed86cbb39..6b92ded310db552e8f47804b329b37b557a2059d 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -15,7 +15,7 @@ Implicit Types P Q : uPred M.
Implicit Types A : Type.
(* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
(** Propers *)
@@ -24,7 +24,7 @@ Global Instance cmra_valid_proper {A : cmra} :
Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
(** Own and valid derived *)
-Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢@{uPredI M} <pers> (✓ a).
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 56fb406b6c04d1fdaa3b670bce37d18e9872f028..ca565ab8c2816234aa73fcd164baa4dcf4f38151 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -292,7 +292,7 @@ Proof.
- iMod (slice_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done.
iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done.
{ by simplify_map_eq. }
- iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
+ iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2) with "[$HQ1 $HQ2] Hbox")
as (γ ?) "[#Hslice Hbox]"; first done.
iExists γ. iIntros "{$% $#} !>". iNext.
iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 87f3719df9f669627df66c9e18e750fc7f0c60e3..ecb038af207aada01a50cbb501931fac3d2a0fb6 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -53,9 +53,9 @@ Section definitions.
Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}.
Definition inv_heap_inv_P : iProp Σ :=
- (∃ h : gmap L (V * (V -d> PropO)),
- own (inv_heap_name gG) (◠to_inv_heap h) ∗
- [∗ map] l ↦ p ∈ h, ⌜p.2 p.1⌠∗ l ↦ p.1)%I.
+ ∃ h : gmap L (V * (V -d> PropO)),
+ own (inv_heap_name gG) (◠to_inv_heap h) ∗
+ [∗ map] l ↦ p ∈ h, ⌜p.2 p.1⌠∗ l ↦ p.1.
Definition inv_heap_inv : iProp Σ := inv inv_heapN inv_heap_inv_P.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index 71131cf0386d88d1da1d3a47068203bb7796994b..d4858462d05fe9f828fe7e1176ca2d0cac30e5ec 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -22,8 +22,8 @@ Section defs.
own p (CoPset E, GSet ∅).
Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
- (∃ i, ⌜i ∈ (↑N:coPset)⌠∧
- inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}))%I.
+ ∃ i, ⌜i ∈ (↑N:coPset)⌠∧
+ inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}).
End defs.
Global Instance: Params (@na_inv) 3 := {}.
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index 59848fa9250a00053d3b63be946640988b80d15a..121e42e621c47e7b48f4368914bce8c78732471f 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -43,8 +43,8 @@ Section definitions.
map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
- (∃ R, ⌜proph_resolves_in_list R pvs ∧
- dom (gset _) R ⊆ ps⌠∗ ghost_map_auth (proph_map_name pG) 1 R)%I.
+ ∃ R, ⌜proph_resolves_in_list R pvs ∧
+ dom (gset _) R ⊆ ps⌠∗ ghost_map_auth (proph_map_name pG) 1 R.
Definition proph_def (p : P) (vs : list V) : iProp Σ :=
p ↪[proph_map_name pG] vs.
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 37ddb62df1b634f4524cabf1e10914a45409aae3..bbfc5a9e9b8d1b47204dcebba37ae9344ae29d7f 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -35,7 +35,6 @@ Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
Next P.
Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
-Global Arguments ownI {_ _} _ _%I.
Typeclasses Opaque ownI.
Global Instance: Params (@invariant_unfold) 1 := {}.
Global Instance: Params (@ownI) 3 := {}.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 824da80c279e7c4f5117cfdf297440e51559c222..e7b702f290ecdd70a65db7c8e2989a21d0c45597 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -718,7 +718,7 @@ Section sep_list2.
Lemma big_sepL2_later_1 `{BiAffine PROP} Φ l1 l2 :
(▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ ◇ [∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2.
Proof.
- rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ âŒ%I).
+ rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ âŒ).
rewrite except_0_and. auto using and_mono, except_0_intro.
Qed.
@@ -1189,7 +1189,7 @@ Section map.
□ (∀ k x, ⌜m !! k = Some x⌠→ Φ k x) ⊢ [∗ map] k↦x ∈ m, Φ k x.
Proof.
revert Φ. induction m as [|i x m ? IH] using map_ind=> Φ.
- { by rewrite (affine (â–¡ _)%I) big_sepM_empty. }
+ { by rewrite (affine (â–¡ _)) big_sepM_empty. }
rewrite big_sepM_insert // intuitionistically_sep_dup. f_equiv.
- rewrite (forall_elim i) (forall_elim x) lookup_insert.
by rewrite pure_True // True_impl intuitionistically_elim.
@@ -1597,11 +1597,11 @@ Section map2.
⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2).
Proof.
rewrite big_sepM2_eq /big_sepM2_def.
- rewrite -{1}(and_idem ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)âŒ%I).
- rewrite -and_assoc.
+ rewrite -{1}(idemp bi_and ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)âŒ%I).
+ rewrite -assoc.
rewrite !persistent_and_affinely_sep_l /=.
- rewrite -sep_assoc. apply sep_proper=>//.
- rewrite sep_assoc (sep_comm _ (<affine> _)%I) -sep_assoc.
+ rewrite -assoc. apply sep_proper=>//.
+ rewrite assoc (comm _ _ (<affine> _)%I) -assoc.
apply sep_proper=>//. apply big_sepM_sep.
Qed.
@@ -1694,7 +1694,7 @@ Section map2.
(▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
Proof.
- rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_âŒ%I).
+ rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_âŒ).
rewrite big_sepM_later except_0_and.
auto using and_mono_r, except_0_intro.
Qed.
@@ -1702,7 +1702,7 @@ Section map2.
([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2)
⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
Proof.
- rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_âŒ%I).
+ rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_âŒ).
apply and_mono_r. by rewrite big_opM_commute.
Qed.
@@ -1904,7 +1904,7 @@ Section gset.
□ (∀ x, ⌜x ∈ X⌠→ Φ x) ⊢ [∗ set] x ∈ X, Φ x.
Proof.
revert Φ. induction X as [|x X ? IH] using set_ind_L=> Φ.
- { by rewrite (affine (â–¡ _)%I) big_sepS_empty. }
+ { by rewrite (affine (â–¡ _)) big_sepS_empty. }
rewrite intuitionistically_sep_dup big_sepS_insert //. f_equiv.
- rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
by rewrite intuitionistically_elim.
@@ -2100,7 +2100,7 @@ Section gmultiset.
□ (∀ x, ⌜x ∈ X⌠→ Φ x) ⊢ [∗ mset] x ∈ X, Φ x.
Proof.
revert Φ. induction X as [|x X IH] using gmultiset_ind=> Φ.
- { by rewrite (affine (â–¡ _)%I) big_sepMS_empty. }
+ { by rewrite (affine (â–¡ _)) big_sepMS_empty. }
rewrite intuitionistically_sep_dup big_sepMS_disj_union.
rewrite big_sepMS_singleton. f_equiv.
- rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver.
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index 0c8ac604a23c267ca2ace7a4b3c65f0410de5eda..0027f0f0de366556f78da609584e52ce856abd12 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -2,13 +2,13 @@ From iris.algebra Require Import monoid.
From iris.bi Require Export interface.
From iris.prelude Require Import options.
-Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
+Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := (P → Q) ∧ (Q → P).
Global Arguments bi_iff {_} _%I _%I : simpl never.
Global Instance: Params (@bi_iff) 1 := {}.
Infix "↔" := bi_iff : bi_scope.
Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
- ((P -∗ Q) ∧ (Q -∗ P))%I.
+ (P -∗ Q) ∧ (Q -∗ P).
Global Arguments bi_wand_iff {_} _%I _%I : simpl never.
Global Instance: Params (@bi_wand_iff) 1 := {}.
Infix "∗-∗" := bi_wand_iff : bi_scope.
@@ -19,7 +19,7 @@ Global Arguments persistent {_} _%I {_}.
Global Hint Mode Persistent + ! : typeclass_instances.
Global Instance: Params (@Persistent) 1 := {}.
-Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
+Definition bi_affinely {PROP : bi} (P : PROP) : PROP := emp ∧ P.
Global Arguments bi_affinely {_} _%I : simpl never.
Global Instance: Params (@bi_affinely) 1 := {}.
Typeclasses Opaque bi_affinely.
@@ -38,7 +38,7 @@ Class BiPositive (PROP : bi) :=
bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
Global Hint Mode BiPositive ! : typeclass_instances.
-Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
+Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := True ∗ P.
Global Arguments bi_absorbingly {_} _%I : simpl never.
Global Instance: Params (@bi_absorbingly) 1 := {}.
Typeclasses Opaque bi_absorbingly.
@@ -88,13 +88,13 @@ Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP :=
match n with
| O => P
| S n' => â–· â–·^n' P
- end%I
+ end
where "â–·^ n P" := (bi_laterN n P) : bi_scope.
Global Arguments bi_laterN {_} !_%nat_scope _%I.
Global Instance: Params (@bi_laterN) 2 := {}.
Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P) : bi_scope.
-Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := (▷ False ∨ P)%I.
+Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := ▷ False ∨ P.
Global Arguments bi_except_0 {_} _%I : simpl never.
Notation "â—‡ P" := (bi_except_0 P) : bi_scope.
Global Instance: Params (@bi_except_0) 1 := {}.
@@ -112,7 +112,7 @@ Global Instance: Params (@Timeless) 1 := {}.
Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
match mP with
| None => Q
- | Some P => (P -∗ Q)%I
+ | Some P => P -∗ Q
end.
Global Arguments bi_wandM {_} !_%I _%I /.
Notation "mP -∗? Q" := (bi_wandM mP Q)
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 53e98c7248aa79c85947eed417df2715631bc4ff..b7bc9d5a913235653d0fd1fcb66573b4833ba0e0 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -607,7 +607,7 @@ Lemma pure_wand_forall φ P `{!Absorbing P} : (⌜φ⌠-∗ P) ⊣⊢ (∀ _ :
Proof.
apply (anti_symm _).
- apply forall_intro=> Hφ.
- rewrite -(pure_intro φ emp%I) // emp_wand //.
+ rewrite -(pure_intro φ emp) // emp_wand //.
- apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ.
apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
Qed.
@@ -794,7 +794,7 @@ Section bi_affine.
Context `{BiAffine PROP}.
Global Instance bi_affine_absorbing P : Absorbing P | 0.
- Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed.
+ Proof. by rewrite /Absorbing /bi_absorbingly (affine True) left_id. Qed.
Global Instance bi_affine_positive : BiPositive PROP.
Proof. intros P Q. by rewrite !affine_affinely. Qed.
@@ -929,7 +929,7 @@ Qed.
Lemma persistently_and_sep_l_1 P Q : <pers> P ∧ Q ⊢ <pers> P ∗ Q.
Proof.
- by rewrite -{1}(emp_sep Q%I) persistently_and_sep_assoc and_elim_l.
+ by rewrite -{1}(emp_sep Q) persistently_and_sep_assoc and_elim_l.
Qed.
Lemma persistently_and_sep_r_1 P Q : P ∧ <pers> Q ⊢ P ∗ <pers> Q.
Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
@@ -937,7 +937,7 @@ Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
Lemma persistently_and_sep P Q : <pers> (P ∧ Q) ⊢ <pers> (P ∗ Q).
Proof.
rewrite persistently_and.
- rewrite -{1}persistently_idemp -persistently_and -{1}(emp_sep Q%I).
+ rewrite -{1}persistently_idemp -persistently_and -{1}(emp_sep Q).
by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
Qed.
@@ -990,7 +990,7 @@ Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed.
Lemma persistently_impl_wand_2 P Q : <pers> (P -∗ Q) ⊢ <pers> (P → Q).
Proof.
apply persistently_intro', impl_intro_r.
- rewrite -{2}(emp_sep P%I) persistently_and_sep_assoc.
+ rewrite -{2}(emp_sep P) persistently_and_sep_assoc.
by rewrite (comm bi_and) persistently_and_emp_elim wand_elim_l.
Qed.
diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index 798d768592490f1c6da915dade29b90b63af11b7..70f0dd6b0d1fa0a8465646e5279028db9d4ae573 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -111,7 +111,7 @@ Lemma löb `{!BiLöb PROP} P : (▷ P → P) ⊢ P.
Proof.
apply entails_impl_True, löb_weak. apply impl_intro_r.
rewrite -{2}(idemp (∧) (▷ P → P))%I.
- rewrite {2}(later_intro (▷ P → P))%I.
+ rewrite {2}(later_intro (▷ P → P)).
rewrite later_impl.
rewrite assoc impl_elim_l.
rewrite impl_elim_r. done.
@@ -131,7 +131,7 @@ Proof.
assert (Q ⊣⊢ (▷ Q → P)) as HQ by (exact: fixpoint_unfold).
intros HP. rewrite -HP.
assert (▷ Q ⊢ P) as HQP.
- { rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q))%I.
+ { rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q)).
by rewrite {1}HQ {1}later_impl impl_elim_l. }
rewrite -HQP HQ -2!later_intro.
apply (entails_impl_True _ P). done.
@@ -139,15 +139,15 @@ Qed.
Lemma löb_wand_intuitionistically `{!BiLöb PROP} P : □ (□ ▷ P -∗ P) ⊢ P.
Proof.
- rewrite -{3}(intuitionistically_elim P) -(löb (□ P)%I). apply impl_intro_l.
+ rewrite -{3}(intuitionistically_elim P) -(löb (□ P)). apply impl_intro_l.
rewrite {1}intuitionistically_into_persistently_1 later_persistently.
rewrite persistently_and_intuitionistically_sep_l.
- rewrite -{1}(intuitionistically_idemp (â–· P)%I) intuitionistically_sep_2.
+ rewrite -{1}(intuitionistically_idemp (â–· P)) intuitionistically_sep_2.
by rewrite wand_elim_r.
Qed.
Lemma löb_wand `{!BiLöb PROP} P : □ (▷ P -∗ P) ⊢ P.
Proof.
- by rewrite -(intuitionistically_elim (▷ P)%I) löb_wand_intuitionistically.
+ by rewrite -(intuitionistically_elim (▷ P)) löb_wand_intuitionistically.
Qed.
(** The proof of the right-to-left direction relies on the BI being affine. It
@@ -322,7 +322,7 @@ Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
Lemma later_affinely_1 `{!Timeless (PROP:=PROP) emp} P : ▷ <affine> P ⊢ ◇ <affine> ▷ P.
Proof.
- rewrite /bi_affinely later_and (timeless emp%I) except_0_and.
+ rewrite /bi_affinely later_and (timeless emp) except_0_and.
by apply and_mono, except_0_intro.
Qed.
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index c2ea7fc4537ddb44ff13144edf03204cd09a8b93..d82e531ee7a6a30d2adc33de980cd9960138b07d 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -21,9 +21,8 @@ Section definition.
(** atomic_acc as the "introduction form" of atomic updates: An accessor
that can be aborted back to [P]. *)
Definition atomic_acc Eo Ei α P β Φ : PROP :=
- (|={Eo, Ei}=> ∃.. x, α x ∗
- ((α x ={Ei, Eo}=∗ P) ∧ (∀.. y, β x y ={Ei, Eo}=∗ Φ x y))
- )%I.
+ |={Eo, Ei}=> ∃.. x, α x ∗
+ ((α x ={Ei, Eo}=∗ P) ∧ (∀.. y, β x y ={Ei, Eo}=∗ Φ x y)).
Lemma atomic_acc_wand Eo Ei α P1 P2 β Φ1 Φ2 :
((P1 -∗ P2) ∧ (∀.. x y, Φ1 x y -∗ Φ2 x y)) -∗
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index fd13d05c11dcd96dee32e3f2e146532a2717b523..195de23afa45a9920e967ea785b27da3c0183878 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -9,7 +9,7 @@ Import bi.
Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
(* TODO: Looks like we want notation for affinely-plainly; that lets us avoid
using conjunction/implication here. *)
- (∀ Q : PROP, <affine> ■(Q -∗ <pers> Q) -∗ <affine> ■(P -∗ Q) -∗ Q)%I.
+ ∀ Q : PROP, <affine> ■(Q -∗ <pers> Q) -∗ <affine> ■(P -∗ Q) -∗ Q.
Global Instance: Params (@coreP) 1 := {}.
Typeclasses Opaque coreP.
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 2ddae631c6a06e1ce7e48caae3a1f8a20847a2db..405653f33cc27777b2ca9902ddda5847c29da090 100644
--- a/iris/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -42,7 +42,7 @@ Module löb_em. Section löb_em.
Lemma later_anything P : ⊢@{PROP} ▷ P.
Proof.
- iDestruct (em (â–· False)%I) as "#[HP|HnotP]".
+ iDestruct (em (â–· False)) as "#[HP|HnotP]".
- iNext. done.
- iExFalso. iLöb as "IH". iSpecialize ("HnotP" with "IH"). done.
Qed.
@@ -81,7 +81,7 @@ Module savedprop. Section savedprop.
Qed.
(** A bad recursive reference: "Assertion with name [i] does not hold" *)
- Definition A (i : ident) : PROP := (∃ P, □ ¬ P ∗ saved i P)%I.
+ Definition A (i : ident) : PROP := ∃ P, □ ¬ P ∗ saved i P.
Lemma A_alloc : ⊢ |==> ∃ i, saved i (A i).
Proof. by apply sprop_alloc_dep. Qed.
@@ -120,7 +120,6 @@ Module inv. Section inv.
(** We have the update modality (two classes: empty/full mask) *)
Inductive mask := M0 | M1.
Context (fupd : mask → PROP → PROP).
- Global Arguments fupd _ _%I.
Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P.
Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q.
Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P.
@@ -198,13 +197,13 @@ Module inv. Section inv.
(** Now to the actual counterexample. We start with a weird form of saved propositions. *)
Definition saved (γ : gname) (P : PROP) : PROP :=
- (∃ i, inv i (start γ ∨ (finished γ ∗ □ P)))%I.
+ ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)).
Global Instance saved_persistent γ P : Persistent (saved γ P) := _.
Lemma saved_alloc (P : gname → PROP) : ⊢ fupd M1 (∃ γ, saved γ (P γ)).
Proof.
iIntros "". iMod (sts_alloc) as (γ) "Hs".
- iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ)))%I with "[Hs]") as (i) "#Hi".
+ iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ))) with "[Hs]") as (i) "#Hi".
{ auto. }
iApply fupd_intro. by iExists γ, i.
Qed.
@@ -231,7 +230,7 @@ Module inv. Section inv.
(** And now we tie a bad knot. *)
Notation not_fupd P := (□ (P -∗ fupd M1 False))%I.
- Definition A i : PROP := (∃ P, not_fupd P ∗ saved i P)%I.
+ Definition A i : PROP := ∃ P, not_fupd P ∗ saved i P.
Global Instance A_persistent i : Persistent (A i) := _.
Lemma A_alloc : ⊢ fupd M1 (∃ i, saved i (A i)).
@@ -287,7 +286,6 @@ Module linear. Section linear.
(** We have the mask-changing update modality (two classes: empty/full mask) *)
Inductive mask := M0 | M1.
Context (fupd : mask → mask → PROP → PROP).
- Global Arguments fupd _ _ _%I.
Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E E P.
Hypothesis fupd_mono : ∀ E1 E2 P Q, (P ⊢ Q) → fupd E1 E2 P ⊢ fupd E1 E2 Q.
Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P.
@@ -324,7 +322,7 @@ Module linear. Section linear.
Lemma leak P : P -∗ fupd M1 M1 emp.
Proof.
iIntros "HP".
- iMod ((cinv_alloc _ True%I) with "[//]") as (γ) "[Hinv Htok]".
+ iMod (cinv_alloc _ True with "[//]") as (γ) "[Hinv Htok]".
iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
iApply "Hclose". done.
Qed.
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 0ab92ec485160213e0dd63e7c6b7860022e04f2a..92fa677087158ca24554e2a942fd88e64303fdba 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -71,7 +71,7 @@ Section instances.
(* A wrapper to obtain a weaker, laterable form of any assertion. *)
Definition make_laterable (Q : PROP) : PROP :=
- (∃ P, ▷ P ∗ □ (▷ P -∗ Q))%I.
+ ∃ P, ▷ P ∗ □ (▷ P -∗ Q).
Global Instance make_laterable_ne : NonExpansive make_laterable.
Proof. solve_proper. Qed.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index 04a640392d1f5b04721a2ba055b2c3c1ceb1bd40..9d7a3763505f108423fdffbdd7c1a8ade19a8008 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -10,7 +10,7 @@ Set Default Proof Using "Type*".
Definition bi_rtc_pre `{!BiInternalEq PROP}
{A : ofe} (R : A → A → PROP)
(x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
- (<affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x')%I.
+ <affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x'.
Global Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
{A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 3c31215a9203dddb89c8bbba166305ba53914324..30f159eb83b8076f79b645d524e04c7f69dc7c19 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -743,19 +743,19 @@ Lemma monPred_objectively_big_sepMS `{BiIndexBottom bot} `{Countable A}
Proof. apply (big_opMS_commute _). Qed.
Global Instance big_sepL_objective {A} (l : list A) Φ `{∀ n x, Objective (Φ n x)} :
- @Objective I PROP ([∗ list] n↦x ∈ l, Φ n x)%I.
+ @Objective I PROP ([∗ list] n↦x ∈ l, Φ n x).
Proof. generalize dependent Φ. induction l=>/=; apply _. Qed.
Global Instance big_sepM_objective `{Countable K} {A}
(Φ : K → A → monPred) (m : gmap K A) `{∀ k x, Objective (Φ k x)} :
- Objective ([∗ map] k↦x ∈ m, Φ k x)%I.
+ Objective ([∗ map] k↦x ∈ m, Φ k x).
Proof. intros ??. rewrite !monPred_at_big_sepM. do 3 f_equiv. by apply objective_at. Qed.
Global Instance big_sepS_objective `{Countable A} (Φ : A → monPred)
(X : gset A) `{∀ y, Objective (Φ y)} :
- Objective ([∗ set] y ∈ X, Φ y)%I.
+ Objective ([∗ set] y ∈ X, Φ y).
Proof. intros ??. rewrite !monPred_at_big_sepS. do 2 f_equiv. by apply objective_at. Qed.
Global Instance big_sepMS_objective `{Countable A} (Φ : A → monPred)
(X : gmultiset A) `{∀ y, Objective (Φ y)} :
- Objective ([∗ mset] y ∈ X, Φ y)%I.
+ Objective ([∗ mset] y ∈ X, Φ y).
Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objective_at. Qed.
(** BUpd *)
@@ -784,7 +784,7 @@ Lemma monPred_at_bupd `{BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
Proof. by rewrite monPred_bupd_eq. Qed.
Global Instance bupd_objective `{BiBUpd PROP} P `{!Objective P} :
- Objective (|==> P)%I.
+ Objective (|==> P).
Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
Global Instance monPred_bi_embed_bupd `{BiBUpd PROP} :
@@ -915,7 +915,7 @@ Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
Proof. by rewrite monPred_fupd_eq. Qed.
Global Instance fupd_objective E1 E2 P `{!Objective P} `{BiFUpd PROP} :
- Objective (|={E1,E2}=> P)%I.
+ Objective (|={E1,E2}=> P).
Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
(** Plainly *)
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 2a016fb621d6889434be53dcf215efa3bd14c304..dff0afd9979582818f504e098295c819d96104b2 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -138,7 +138,7 @@ Proof. destruct p; last done. exact: persistently_elim_plainly. Qed.
Lemma plainly_persistently_elim P : ■<pers> P ⊣⊢ ■P.
Proof.
apply (anti_symm _).
- - rewrite -{1}(left_id True%I bi_and (â– _)%I) (plainly_emp_intro True%I).
+ - rewrite -{1}(left_id True%I bi_and (â– _)%I) (plainly_emp_intro True).
rewrite -{2}(persistently_and_emp_elim P).
rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
- by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
@@ -208,7 +208,7 @@ Proof.
Qed.
Lemma plainly_and_sep_l_1 P Q : ■P ∧ Q ⊢ ■P ∗ Q.
-Proof. by rewrite -{1}(emp_sep Q%I) plainly_and_sep_assoc and_elim_l. Qed.
+Proof. by rewrite -{1}(emp_sep Q) plainly_and_sep_assoc and_elim_l. Qed.
Lemma plainly_and_sep_r_1 P Q : P ∧ ■Q ⊢ P ∗ ■Q.
Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
@@ -217,7 +217,7 @@ Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
Lemma plainly_and_sep P Q : ■(P ∧ Q) ⊢ ■(P ∗ Q).
Proof.
rewrite plainly_and.
- rewrite -{1}plainly_idemp -plainly_and -{1}(emp_sep Q%I).
+ rewrite -{1}plainly_idemp -plainly_and -{1}(emp_sep Q).
by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
Qed.
@@ -244,7 +244,7 @@ Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
Lemma plainly_sep `{BiPositive PROP} P Q : ■(P ∗ Q) ⊣⊢ ■P ∗ ■Q.
Proof.
apply (anti_symm _); auto using plainly_sep_2.
- rewrite -(plainly_affinely_elim (_ ∗ _)%I) affinely_sep -and_sep_plainly. apply and_intro.
+ rewrite -(plainly_affinely_elim (_ ∗ _)) affinely_sep -and_sep_plainly. apply and_intro.
- by rewrite (affinely_elim_emp Q) right_id affinely_elim.
- by rewrite (affinely_elim_emp P) left_id affinely_elim.
Qed.
@@ -260,7 +260,7 @@ Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed.
Lemma plainly_impl_wand_2 P Q : ■(P -∗ Q) ⊢ ■(P → Q).
Proof.
apply plainly_intro', impl_intro_r.
- rewrite -{2}(emp_sep P%I) plainly_and_sep_assoc.
+ rewrite -{2}(emp_sep P) plainly_and_sep_assoc.
by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l.
Qed.
@@ -579,7 +579,7 @@ Section prop_ext.
apply (anti_symm (⊢)); last exact: prop_ext_2.
apply (internal_eq_rewrite' P Q (λ Q, ■(P ∗-∗ Q))%I);
[ solve_proper | done | ].
- rewrite (plainly_emp_intro (P ≡ Q)%I).
+ rewrite (plainly_emp_intro (P ≡ Q)).
apply plainly_mono, wand_iff_refl.
Qed.
@@ -608,7 +608,7 @@ Section prop_ext.
by rewrite wand_elim_r.
- rewrite internal_eq_sym (internal_eq_rewrite _ _
(λ Q, ■(True -∗ Q))%I ltac:(shelve)); last solve_proper.
- by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
+ by rewrite -entails_wand // -(plainly_emp_intro True) True_impl.
Qed.
(* This proof uses [BiPlainlyExist] and [BiLöb] via [plainly_timeless] and
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 47f9ece52feef180e593874b4a282ee5629f7b4b..e0f98d618623359dc33a23ab3d24386bbb122d34 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -358,7 +358,7 @@ Section fupd_derived.
rewrite -(fupd_mask_frame E E'); first apply fupd_mono; last done.
(* The most horrible way to apply fupd_intro_mask *)
rewrite -[X in (X -∗ _)](right_id emp%I).
- rewrite (fupd_mask_intro_subseteq (E1 ∖ E2 ∪ E ∖ E1) (E ∖ E2) emp%I); last first.
+ rewrite (fupd_mask_intro_subseteq (E1 ∖ E2 ∪ E ∖ E1) (E ∖ E2) emp); last first.
{ rewrite {1}(union_difference_L _ _ HE). set_solver. }
rewrite fupd_frame_l fupd_frame_r. apply fupd_elim.
apply fupd_mono.
@@ -411,7 +411,7 @@ Section fupd_derived.
Lemma step_fupd_wand Eo Ei P Q : (|={Eo}[Ei]▷=> P) -∗ (P -∗ Q) -∗ |={Eo}[Ei]▷=> Q.
Proof.
apply wand_intro_l.
- by rewrite (later_intro (P -∗ Q)%I) fupd_frame_l -later_sep fupd_frame_l
+ by rewrite (later_intro (P -∗ Q)) fupd_frame_l -later_sep fupd_frame_l
wand_elim_l.
Qed.
@@ -425,10 +425,10 @@ Section fupd_derived.
Ei2 ⊆ Ei1 → Eo1 ⊆ Eo2 → (|={Eo1}[Ei1]▷=> P) ⊢ |={Eo2}[Ei2]▷=> P.
Proof.
intros ??. rewrite -(emp_sep (|={Eo1}[Ei1]â–·=> P)%I).
- rewrite (fupd_mask_intro_subseteq Eo2 Eo1 emp%I) //.
+ rewrite (fupd_mask_intro_subseteq Eo2 Eo1 emp) //.
rewrite fupd_frame_r -(fupd_trans Eo2 Eo1 Ei2). f_equiv.
rewrite fupd_frame_l -(fupd_trans Eo1 Ei1 Ei2). f_equiv.
- rewrite (fupd_mask_intro_subseteq Ei1 Ei2 (|={_,_}=> emp)%I) //.
+ rewrite (fupd_mask_intro_subseteq Ei1 Ei2 (|={_,_}=> emp)) //.
rewrite fupd_frame_r. f_equiv.
rewrite [X in (X ∗ _)%I]later_intro -later_sep. f_equiv.
rewrite fupd_frame_r -(fupd_trans Ei2 Ei1 Eo2). f_equiv.
@@ -500,7 +500,7 @@ Section fupd_derived.
Qed.
Lemma fupd_plainly_elim E P : ■P ={E}=∗ P.
- Proof. by rewrite (fupd_intro E (â– P)%I) fupd_plainly_mask. Qed.
+ Proof. by rewrite (fupd_intro E (â– P)) fupd_plainly_mask. Qed.
Lemma fupd_plainly_keep_r E P R : R ∗ (R ={E}=∗ ■P) ⊢ |={E}=> R ∗ P.
Proof. by rewrite !(comm _ R) fupd_plainly_keep_l. Qed.
@@ -543,7 +543,7 @@ Section fupd_derived.
trans (∀ x, |={E1}=> Φ x)%I.
{ apply forall_mono=> x. by rewrite fupd_plain_mask. }
rewrite fupd_plain_forall_2. apply fupd_elim.
- rewrite {1}(plain (∀ x, Φ x)) (fupd_mask_intro_discard E1 E2 (■_)%I) //.
+ rewrite {1}(plain (∀ x, Φ x)) (fupd_mask_intro_discard E1 E2 (■_)) //.
apply fupd_elim. by rewrite fupd_plainly_elim.
Qed.
Lemma fupd_plain_forall' E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
@@ -552,7 +552,7 @@ Section fupd_derived.
Lemma step_fupd_plain Eo Ei P `{!Plain P} : (|={Eo}[Ei]▷=> P) ={Eo}=∗ ▷ ◇ P.
Proof.
- rewrite -(fupd_plain_mask _ Ei (â–· â—‡ P)%I).
+ rewrite -(fupd_plain_mask _ Ei (â–· â—‡ P)).
apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
Qed.
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 63f075cbc2436feacc7b07b1e711bbebbd6bd008..fead228df60357bf52b3c5a31bedb5a3c02bd9cd 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -15,9 +15,9 @@ Definition atomic_wp `{!irisG Λ Σ} {TA TB : tele}
(β: TA → TB → iProp Σ) (* atomic post-condition *)
(f: TA → TB → val Λ) (* Turn the return data into the return value *)
: iProp Σ :=
- (∀ (Φ : val Λ → iProp Σ),
- atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
- WP e {{ Φ }})%I.
+ ∀ (Φ : val Λ → iProp Σ),
+ atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
+ WP e {{ Φ }}.
(* Note: To add a private postcondition, use
atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 2695ce19cb064b66a4386e8a2745b0e81fb929fe..d1c470c586b6426bddd2d6b0bca0b561015f84c3 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -11,9 +11,9 @@ Implicit Types e : expr Λ.
Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
(t1 : list (expr Λ)) : iProp Σ :=
- (∀ t2 σ1 ns κ κs σ2 nt, ⌜step (t1,σ1) κ (t2,σ2)⌠-∗
+ ∀ t2 σ1 ns κ κs σ2 nt, ⌜step (t1,σ1) κ (t2,σ2)⌠-∗
state_interp σ1 ns κs nt ={⊤}=∗
- ∃ nt', ⌜κ = []⌠∗ state_interp σ2 (S ns) κs nt' ∗ twptp t2)%I.
+ ∃ nt', ⌜κ = []⌠∗ state_interp σ2 (S ns) κs nt' ∗ twptp t2.
Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
⊢ <pers> (∀ t, twptp1 t -∗ twptp2 t) →
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 9b02c46479e100939616500a66ac1176d55fb165..b72fc6889b77bd98a5fec0821c1618b6413c1a25 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -415,12 +415,12 @@ Global Instance into_wand_affine p q R P Q :
IntoWand p q R P Q → IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
Proof.
rewrite /IntoWand /= => HR. apply wand_intro_r. destruct p; simpl in *.
- - rewrite (affinely_elim R) -(affine_affinely (â–¡ R)%I) HR. destruct q; simpl in *.
- + rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)%I).
+ - rewrite (affinely_elim R) -(affine_affinely (â–¡ R)) HR. destruct q; simpl in *.
+ + rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)).
by rewrite affinely_sep_2 wand_elim_l.
+ by rewrite affinely_sep_2 wand_elim_l.
- rewrite HR. destruct q; simpl in *.
- + rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)%I).
+ + rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)).
by rewrite affinely_sep_2 wand_elim_l.
+ by rewrite affinely_sep_2 wand_elim_l.
Qed.
@@ -437,8 +437,8 @@ Global Instance into_wand_affine_args q R P Q :
IntoWand true q R P Q → IntoWand' true q R (<affine> P) (<affine> Q).
Proof.
rewrite /IntoWand' /IntoWand /= => HR. apply wand_intro_r.
- rewrite -(affine_affinely (â–¡ R)%I) HR. destruct q; simpl.
- - rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)%I).
+ rewrite -(affine_affinely (â–¡ R)) HR. destruct q; simpl.
+ - rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)).
by rewrite affinely_sep_2 wand_elim_l.
- by rewrite affinely_sep_2 wand_elim_l.
Qed.
@@ -645,7 +645,7 @@ Proof. by rewrite /IntoSep. Qed.
Inductive AndIntoSep : PROP → PROP → PROP → PROP → Prop :=
| and_into_sep_affine P Q Q' : Affine P → FromAffinely Q' Q → AndIntoSep P P Q Q'
- | and_into_sep P Q : AndIntoSep P (<affine> P)%I Q Q.
+ | and_into_sep P Q : AndIntoSep P (<affine> P) Q Q.
Existing Class AndIntoSep.
Global Existing Instance and_into_sep_affine | 0.
Global Existing Instance and_into_sep | 2.
@@ -873,7 +873,7 @@ Global Instance into_forall_wand_pure a φ P Q :
Proof.
rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] /=.
apply forall_intro=>? /=. rewrite -affinely_affinely_if.
- by rewrite -(pure_intro _ True%I) // /bi_affinely right_id emp_wand.
+ by rewrite -(pure_intro _ True) // /bi_affinely right_id emp_wand.
Qed.
(* These instances must be used only after [into_forall_wand_pure] and
diff --git a/iris/proofmode/class_instances_embedding.v b/iris/proofmode/class_instances_embedding.v
index 2cbcaf760d0e2efcc3a510431e293e9dfe56885b..44a3e06456590d7bb95b91720c0897c584131e62 100644
--- a/iris/proofmode/class_instances_embedding.v
+++ b/iris/proofmode/class_instances_embedding.v
@@ -67,9 +67,9 @@ Global Instance into_wand_affine_embed_true q P Q R :
IntoWand true q R P Q → IntoWand true q ⎡R⎤ (<affine> ⎡P⎤) (<affine> ⎡Q⎤) | 100.
Proof.
rewrite /IntoWand /=.
- rewrite -(intuitionistically_idemp ⎡ _ ⎤%I) embed_intuitionistically_2=> ->.
+ rewrite -(intuitionistically_idemp ⎡ _ ⎤) embed_intuitionistically_2=> ->.
apply bi.wand_intro_l. destruct q; simpl.
- - rewrite affinely_elim -(intuitionistically_idemp ⎡ _ ⎤%I).
+ - rewrite affinely_elim -(intuitionistically_idemp ⎡ _ ⎤).
rewrite embed_intuitionistically_2 intuitionistically_sep_2 -embed_sep.
by rewrite wand_elim_r intuitionistically_affinely.
- by rewrite intuitionistically_affinely affinely_sep_2 -embed_sep wand_elim_r.
diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index d4c7e2d3ab7c29bdab0946e2b340a679bfdbf776..87d1c84a433f8eec45f7f01c31ffd2e2462d5b3d 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -10,13 +10,13 @@ Implicit Types P Q R : PROP.
(** FromAssumption *)
Global Instance from_assumption_later p P Q :
- FromAssumption p P Q → KnownRFromAssumption p P (▷ Q)%I.
+ FromAssumption p P Q → KnownRFromAssumption p P (▷ Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply later_intro. Qed.
Global Instance from_assumption_laterN n p P Q :
- FromAssumption p P Q → KnownRFromAssumption p P (▷^n Q)%I.
+ FromAssumption p P Q → KnownRFromAssumption p P (▷^n Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply laterN_intro. Qed.
Global Instance from_assumption_except_0 p P Q :
- FromAssumption p P Q → KnownRFromAssumption p P (◇ Q)%I.
+ FromAssumption p P Q → KnownRFromAssumption p P (◇ Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply except_0_intro. Qed.
(** FromPure *)
@@ -39,7 +39,7 @@ Global Instance into_wand_later_args p q R P Q :
Proof.
rewrite /IntoWand' /IntoWand /= => HR.
by rewrite !later_intuitionistically_if_2
- (later_intro (â–¡?p R)%I) -later_wand HR.
+ (later_intro (â–¡?p R)) -later_wand HR.
Qed.
Global Instance into_wand_laterN n p q R P Q :
IntoWand p q R P Q → IntoWand p q (▷^n R) (▷^n P) (▷^n Q).
@@ -52,7 +52,7 @@ Global Instance into_wand_laterN_args n p q R P Q :
Proof.
rewrite /IntoWand' /IntoWand /= => HR.
by rewrite !laterN_intuitionistically_if_2
- (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
+ (laterN_intro _ (â–¡?p R)) -laterN_wand HR.
Qed.
(** FromAnd *)
@@ -186,15 +186,15 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
(** FromForall *)
Global Instance from_forall_later {A} P (Φ : A → PROP) name :
- FromForall P Φ name → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I name.
+ FromForall P Φ name → FromForall (▷ P) (λ a, ▷ (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
Global Instance from_forall_laterN {A} P (Φ : A → PROP) n name :
- FromForall P Φ name → FromForall (▷^n P)%I (λ a, ▷^n (Φ a))%I name.
+ FromForall P Φ name → FromForall (▷^n P) (λ a, ▷^n (Φ a))%I name.
Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed.
Global Instance from_forall_except_0 {A} P (Φ : A → PROP) name :
- FromForall P Φ name → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I name.
+ FromForall P Φ name → FromForall (◇ P) (λ a, ◇ (Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
(** IsExcept0 *)
@@ -238,7 +238,7 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
Global Instance elim_modal_timeless p P P' Q :
IntoExcept0 P P' → IsExcept0 Q → ElimModal True p p P P' Q Q.
Proof.
- intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I) (into_except_0 P).
+ intros. rewrite /ElimModal (except_0_intro (_ -∗ _)) (into_except_0 P).
by rewrite except_0_intuitionistically_if_2 -except_0_sep wand_elim_r.
Qed.
@@ -247,23 +247,23 @@ Qed.
Global Instance add_modal_later_except_0 P Q :
Timeless P → AddModal (▷ P) P (◇ Q) | 0.
Proof.
- intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I) (timeless P).
+ intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P).
by rewrite -except_0_sep wand_elim_r except_0_idemp.
Qed.
Global Instance add_modal_later P Q :
Timeless P → AddModal (▷ P) P (▷ Q) | 0.
Proof.
- intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I) (timeless P).
+ intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P).
by rewrite -except_0_sep wand_elim_r except_0_later.
Qed.
Global Instance add_modal_except_0 P Q : AddModal (â—‡ P) P (â—‡ Q) | 1.
Proof.
- intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I).
+ intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
by rewrite -except_0_sep wand_elim_r except_0_idemp.
Qed.
Global Instance add_modal_except_0_later P Q : AddModal (â—‡ P) P (â–· Q) | 1.
Proof.
- intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I).
+ intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
by rewrite -except_0_sep wand_elim_r except_0_later.
Qed.
diff --git a/iris/proofmode/class_instances_plainly.v b/iris/proofmode/class_instances_plainly.v
index b49f42a76c3a2ac3d24ca5a53c147eef3cccd943..44353c9158d147ed0460dba033e6d08e1933e36b 100644
--- a/iris/proofmode/class_instances_plainly.v
+++ b/iris/proofmode/class_instances_plainly.v
@@ -84,7 +84,7 @@ Global Instance into_forall_plainly {A} P (Φ : A → PROP) :
Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
Global Instance from_forall_plainly {A} P (Φ : A → PROP) name :
- FromForall P Φ name → FromForall (■P)%I (λ a, ■(Φ a))%I name.
+ FromForall P Φ name → FromForall (■P) (λ a, ■(Φ a))%I name.
Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
Global Instance from_modal_plainly P :
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 5fd7fea8bda20e776893c76b74852bc4a532b877..b0ab10ecc7496752cb7f15888c43e40e2a8072ed 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -14,7 +14,7 @@ Global Instance from_assumption_bupd `{!BiBUpd PROP} p P Q :
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.
Global Instance from_assumption_fupd
`{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} E p P Q :
- FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q)%I.
+ FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q).
Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_fupd. Qed.
Global Instance from_pure_bupd `{!BiBUpd PROP} a P φ :
@@ -100,7 +100,7 @@ Global Instance from_forall_fupd
(* Some cases in which [E2 ⊆ E1] holds *)
TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
FromForall P Φ name → (∀ x, Plain (Φ x)) →
- FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I name.
+ FromForall (|={E1,E2}=> P) (λ a, |={E1,E2}=> (Φ a))%I name.
Proof.
rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
Qed.
@@ -109,7 +109,7 @@ Global Instance from_forall_step_fupd
(* Some cases in which [E2 ⊆ E1] holds *)
TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
FromForall P Φ name → (∀ x, Plain (Φ x)) →
- FromForall (|={E1}[E2]▷=> P)%I (λ a, |={E1}[E2]▷=> (Φ a))%I name.
+ FromForall (|={E1}[E2]▷=> P) (λ a, |={E1}[E2]▷=> (Φ a))%I name.
Proof.
rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
Qed.
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 0451e6559912ea8a290ea25172a964ac51598726..617d76f436a64cbaff56b0d98fd781d8bcfb1d46 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -26,7 +26,7 @@ Lemma tac_stop Δ P :
| Enil, Γs => env_to_prop Γs
| Γp, Enil => □ env_to_prop_and Γp
| Γp, Γs => □ env_to_prop_and Γp ∗ env_to_prop Γs
- end%I ⊢ P) →
+ end ⊢ P) →
envs_entails Δ P.
Proof.
rewrite envs_entails_eq !of_envs_eq. intros <-.
@@ -166,7 +166,7 @@ Proof.
- destruct HPQ.
+ rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
by apply pure_elim_l.
- + rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ âŒ%I) absorbingly_sep_lr.
+ + rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ âŒ) absorbingly_sep_lr.
rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
Qed.
@@ -462,10 +462,10 @@ Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
Proof. by rewrite envs_entails_eq /IntoIH. Qed.
Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
- (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x)%I | 2.
+ (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
- IntoIH φ Δ Q → IntoIH (ψ → φ) Δ (⌜ψ⌠→ Q)%I | 1.
+ IntoIH φ Δ Q → IntoIH (ψ → φ) Δ (⌜ψ⌠→ Q) | 1.
Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
@@ -828,7 +828,7 @@ Proof.
destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done. rewrite -Hentails.
rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
- rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)%I) sep_elim_l.
+ rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)) sep_elim_l.
rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
- apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
@@ -1023,7 +1023,7 @@ Section tac_modal_intro.
- intros ?. rewrite HΓ //. destruct Hif as [-> [? ->| ->]| ->].
+ by rewrite (affine P) left_id.
+ by rewrite right_id comm (True_intro P).
- + by rewrite comm -assoc (True_intro (_ ∗ P)%I).
+ + by rewrite comm -assoc (True_intro (_ ∗ P)).
- inversion 1; auto.
- intros j. destruct (ident_beq _ _); naive_solver.
Qed.
@@ -1071,8 +1071,8 @@ Section tac_modal_intro.
rewrite -(right_id emp%I bi_sep (M _)).
eauto using modality_spatial_transform.
- rewrite -HQ' /= right_id comm -{2}(modality_spatial_clear M) //.
- by rewrite (True_intro ([∗] Γs)%I).
- - rewrite -HQ' {1}(modality_spatial_id M ([∗] Γs)%I) //.
+ by rewrite (True_intro ([∗] Γs)).
+ - rewrite -HQ' {1}(modality_spatial_id M ([∗] Γs)) //.
by rewrite -modality_sep.
Qed.
End tac_modal_intro.
diff --git a/iris/proofmode/frame_instances.v b/iris/proofmode/frame_instances.v
index 9b7fba1f78784374c8c5c13610ab9c7149f80328..178576f4dca3c98d5890d684fafe87134c9273ea 100644
--- a/iris/proofmode/frame_instances.v
+++ b/iris/proofmode/frame_instances.v
@@ -210,7 +210,7 @@ Global Instance frame_affinely p R P Q Q' :
Frame p R P Q → MakeAffinely Q Q' → Frame p R (<affine> P) Q'.
Proof.
rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
- by rewrite -{1}(affine_affinely (_ R)%I) affinely_sep_2.
+ by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
Qed.
Global Instance make_intuitionistically_emp :
@@ -347,6 +347,6 @@ Global Instance frame_except_0 p R P Q Q' :
Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
Proof.
rewrite /Frame /MakeExcept0=><- <-.
- by rewrite except_0_sep -(except_0_intro (â–¡?p R)%I).
+ by rewrite except_0_sep -(except_0_intro (â–¡?p R)).
Qed.
End bi.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index bd70d2493afc6c1ef84d5cca1f5a6f609b33ee54..0a7db19c096d2ef2ca5daf3245b66593d90c8805 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -142,7 +142,7 @@ Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
Proof. by rewrite /MakeMonPredAt. Qed.
Global Instance make_monPred_at_bupd `{BiBUpd PROP} i P ð“Ÿ :
- MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|==> P)%I (|==> ð“Ÿ)%I.
+ MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|==> P) (|==> ð“Ÿ).
Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
Global Instance from_assumption_make_monPred_at_l p i j P ð“Ÿ :
@@ -480,16 +480,16 @@ Global Instance make_monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofe} (x y
MakeMonPredAt i (x ≡ y) (x ≡ y).
Proof. by rewrite /MakeMonPredAt monPred_at_internal_eq. Qed.
Global Instance make_monPred_at_except_0 i P ð“ :
- MakeMonPredAt i P ð“ → MakeMonPredAt i (â—‡ P)%I (â—‡ ð“ )%I.
+ MakeMonPredAt i P ð“ → MakeMonPredAt i (â—‡ P) (â—‡ ð“ ).
Proof. by rewrite /MakeMonPredAt monPred_at_except_0=><-. Qed.
Global Instance make_monPred_at_later i P ð“ :
- MakeMonPredAt i P ð“ → MakeMonPredAt i (â–· P)%I (â–· ð“ )%I.
+ MakeMonPredAt i P ð“ → MakeMonPredAt i (â–· P) (â–· ð“ ).
Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
Global Instance make_monPred_at_laterN i n P ð“ :
- MakeMonPredAt i P ð“ → MakeMonPredAt i (â–·^n P)%I (â–·^n ð“ )%I.
+ MakeMonPredAt i P ð“ → MakeMonPredAt i (â–·^n P) (â–·^n ð“ ).
Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P ð“Ÿ :
- MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> ð“Ÿ)%I.
+ MakeMonPredAt i P 𓟠→ MakeMonPredAt i (|={E1,E2}=> P) (|={E1,E2}=> ð“Ÿ).
Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
Global Instance into_internal_eq_monPred_at `{!BiInternalEq PROP}