From da93f3572d1df7fe6ca55afb09994a32e7c172fd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 5 Mar 2019 16:08:55 +0100
Subject: [PATCH] use ! when possible to avoid overzealous generalization
---
tests/algebra.v | 2 +-
tests/heap_lang.ref | 24 +++++-----
tests/heap_lang.v | 6 +--
tests/heap_lang2.ref | 2 +-
tests/heap_lang2.v | 2 +-
tests/ipm_paper.v | 2 +-
tests/proofmode.ref | 2 +-
tests/proofmode.v | 6 +--
tests/proofmode_iris.ref | 48 +++++++++----------
tests/proofmode_iris.v | 4 +-
theories/algebra/agree.v | 2 +-
theories/algebra/auth.v | 8 ++--
theories/algebra/excl.v | 2 +-
theories/algebra/gmap.v | 2 +-
theories/algebra/gset.v | 2 +-
theories/algebra/list.v | 4 +-
theories/base_logic/bi.v | 2 +-
theories/base_logic/derived.v | 2 +-
theories/base_logic/lib/auth.v | 4 +-
theories/base_logic/lib/boxes.v | 4 +-
.../base_logic/lib/cancelable_invariants.v | 4 +-
theories/base_logic/lib/fancy_updates.v | 28 +++++------
theories/base_logic/lib/gen_heap.v | 6 +--
theories/base_logic/lib/invariants.v | 4 +-
theories/base_logic/lib/na_invariants.v | 4 +-
theories/base_logic/lib/own.v | 18 +++----
theories/base_logic/lib/saved_prop.v | 24 +++++-----
theories/base_logic/lib/sts.v | 4 +-
theories/base_logic/lib/viewshifts.v | 4 +-
theories/base_logic/lib/wsat.v | 12 ++---
theories/base_logic/proofmode.v | 2 +-
theories/base_logic/upred.v | 4 +-
theories/heap_lang/adequacy.v | 4 +-
theories/heap_lang/lib/assert.v | 4 +-
theories/heap_lang/lifting.v | 6 +--
theories/heap_lang/proofmode.v | 18 +++----
theories/heap_lang/proph_map.v | 6 +--
theories/heap_lang/total_adequacy.v | 4 +-
theories/program_logic/adequacy.v | 22 ++++-----
theories/program_logic/atomic.v | 4 +-
theories/program_logic/ectx_language.v | 2 +-
theories/program_logic/ectx_lifting.v | 2 +-
theories/program_logic/ectxi_language.v | 4 +-
theories/program_logic/hoare.v | 6 +--
theories/program_logic/language.v | 15 +++---
theories/program_logic/lifting.v | 12 ++---
theories/program_logic/ownp.v | 20 ++++----
theories/program_logic/total_adequacy.v | 6 +--
theories/program_logic/total_ectx_lifting.v | 2 +-
theories/program_logic/total_lifting.v | 8 ++--
theories/program_logic/total_weakestpre.v | 24 +++++-----
theories/program_logic/weakestpre.v | 20 ++++----
52 files changed, 217 insertions(+), 216 deletions(-)
diff --git a/tests/algebra.v b/tests/algebra.v
index cc94ecc72..028272cea 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,7 +1,7 @@
From iris.base_logic.lib Require Import invariants.
Section tests.
- Context `{invG Σ}.
+ Context `{!invG Σ}.
Program Definition test : (iProp Σ -n> iProp Σ) -n> (iProp Σ -n> iProp Σ) :=
λne P v, (▷ (P v))%I.
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 4a88fed5e..cd621a876 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -1,7 +1,7 @@
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
E : coPset
============================
--------------------------------------∗
@@ -10,7 +10,7 @@
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
E : coPset
l : loc
============================
@@ -21,7 +21,7 @@
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
E : coPset
l : loc
============================
@@ -35,7 +35,7 @@
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
l : loc
============================
_ : ▷ l ↦ #0
@@ -45,7 +45,7 @@
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
l : loc
============================
_ : l ↦ #1
@@ -55,7 +55,7 @@
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
l : loc
============================
"Hl1" : l ↦{1 / 2} #0
@@ -66,7 +66,7 @@
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
l : loc
============================
--------------------------------------∗
@@ -81,7 +81,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
============================
--------------------------------------∗
WP "x" {{ _, True }}
@@ -89,7 +89,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
fun1, fun2, fun3 : expr
============================
--------------------------------------∗
@@ -101,7 +101,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iPropI Σ
============================
@@ -114,7 +114,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iPropI Σ
E : coPset
@@ -128,7 +128,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
fun1, fun2, fun3 : expr
============================
{{{ True }}}
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index a738ffb97..69c99fab2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -6,7 +6,7 @@ Set Ltac Backtrace.
Set Default Proof Using "Type".
Section tests.
- Context `{heapG Σ}.
+ Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
@@ -147,7 +147,7 @@ Section tests.
End tests.
Section printing_tests.
- Context `{heapG Σ}.
+ Context `{!heapG Σ}.
(* These terms aren't even closed, but that's not what this is about. The
length of the variable names etc. has been carefully chosen to trigger
@@ -192,7 +192,7 @@ Section printing_tests.
End printing_tests.
Section error_tests.
- Context `{heapG Σ}.
+ Context `{!heapG Σ}.
Check "not_cas".
Lemma not_cas :
diff --git a/tests/heap_lang2.ref b/tests/heap_lang2.ref
index eb393dc01..73cfb45d3 100644
--- a/tests/heap_lang2.ref
+++ b/tests/heap_lang2.ref
@@ -1,7 +1,7 @@
1 subgoal
Σ : gFunctors
- H : heapG Σ
+ heapG0 : heapG Σ
fun1, fun2, fun3 : expr
============================
--------------------------------------∗
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index cada4949b..f2e7050b0 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -6,7 +6,7 @@ From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Section printing_tests.
- Context `{heapG Σ}.
+ Context `{!heapG Σ}.
Lemma wp_print_long_expr (fun1 fun2 fun3 : expr) :
True -∗ WP let: "val1" := fun1 #() in
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index abd2b0549..7dcf6bde7 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -107,7 +107,7 @@ under max can be found in [theories/heap_lang/lib/counter.v]. *)
update modalities (which we did not cover in the paper). Normally we use these
mask changing update modalities directly in our proofs, but in this file we use
the first prove the rule as a lemma, and then use that. *)
-Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ :
+Lemma wp_inv_open `{!irisG Λ Σ} N E P e Φ :
nclose N ⊆ E → Atomic WeaklyAtomic e →
inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
Proof.
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index be465b628..b9a27dc9e 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -131,7 +131,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
- H : BiAffine PROP
+ BiAffine0 : BiAffine PROP
P, Q : PROP
============================
_ : â–¡ P
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 981242fe3..c5689c2eb 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -69,7 +69,7 @@ Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
Q ∗ (Q -∗ P) -∗ P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.
-Lemma test_iDestruct_intuitionistic_affine_bi `{BiAffine PROP} P Q `{!Persistent P}:
+Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persistent P}:
Q ∗ (Q -∗ P) -∗ P ∗ Q.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
@@ -180,7 +180,7 @@ Lemma test_iFrame_conjunction_2 P Q :
P -∗ Q -∗ (P ∧ P) ∗ (Q ∧ Q).
Proof. iIntros "HP HQ". iFrame "HP HQ". Qed.
-Lemma test_iFrame_later `{BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
+Lemma test_iFrame_later `{!BiAffine PROP} P Q : P -∗ Q -∗ ▷ P ∗ Q.
Proof. iIntros "H1 H2". by iFrame "H1". Qed.
Lemma test_iAssert_modality P : ◇ False -∗ ▷ P.
@@ -555,7 +555,7 @@ Proof.
Qed.
Check "test_and_sep_affine_bi".
-Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
+Lemma test_and_sep_affine_bi `{!BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
Proof.
iIntros "[??]". iSplit; last done. Show. done.
Qed.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index fda29fc12..0dbca72f4 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -1,9 +1,9 @@
1 subgoal
Σ : gFunctors
- H : invG Σ
- H0 : cinvG Σ
- H1 : na_invG Σ
+ invG0 : invG Σ
+ cinvG0 : cinvG Σ
+ na_invG0 : na_invG Σ
N : namespace
P : iProp Σ
============================
@@ -15,9 +15,9 @@
1 subgoal
Σ : gFunctors
- H : invG Σ
- H0 : cinvG Σ
- H1 : na_invG Σ
+ invG0 : invG Σ
+ cinvG0 : cinvG Σ
+ na_invG0 : na_invG Σ
N : namespace
P : iProp Σ
============================
@@ -31,9 +31,9 @@
1 subgoal
Σ : gFunctors
- H : invG Σ
- H0 : cinvG Σ
- H1 : na_invG Σ
+ invG0 : invG Σ
+ cinvG0 : cinvG Σ
+ na_invG0 : na_invG Σ
γ : gname
p : Qp
N : namespace
@@ -49,9 +49,9 @@
1 subgoal
Σ : gFunctors
- H : invG Σ
- H0 : cinvG Σ
- H1 : na_invG Σ
+ invG0 : invG Σ
+ cinvG0 : cinvG Σ
+ na_invG0 : na_invG Σ
γ : gname
p : Qp
N : namespace
@@ -68,14 +68,14 @@
1 subgoal
Σ : gFunctors
- H : invG Σ
- H0 : cinvG Σ
- H1 : na_invG Σ
+ invG0 : invG Σ
+ cinvG0 : cinvG Σ
+ na_invG0 : na_invG Σ
t : na_inv_pool_name
N : namespace
E1, E2 : coPset
P : iProp Σ
- H2 : ↑N ⊆ E2
+ H : ↑N ⊆ E2
============================
_ : na_inv t N (<pers> P)
"HP" : â–· <pers> P
@@ -89,14 +89,14 @@
1 subgoal
Σ : gFunctors
- H : invG Σ
- H0 : cinvG Σ
- H1 : na_invG Σ
+ invG0 : invG Σ
+ cinvG0 : cinvG Σ
+ na_invG0 : na_invG Σ
t : na_inv_pool_name
N : namespace
E1, E2 : coPset
P : iProp Σ
- H2 : ↑N ⊆ E2
+ H : ↑N ⊆ E2
============================
_ : na_inv t N (<pers> P)
"HP" : â–· <pers> P
@@ -132,12 +132,12 @@ Tactic failure: iInv: invariant "H2" not found.
1 subgoal
Σ : gFunctors
- H : invG Σ
+ invG0 : invG Σ
I : biIndex
N : namespace
E : coPset
𓟠: iProp Σ
- H0 : ↑N ⊆ E
+ H : ↑N ⊆ E
============================
"HP" : ⎡ ▷ 𓟠⎤
--------------------------------------∗
@@ -148,12 +148,12 @@ Tactic failure: iInv: invariant "H2" not found.
1 subgoal
Σ : gFunctors
- H : invG Σ
+ invG0 : invG Σ
I : biIndex
N : namespace
E : coPset
𓟠: iProp Σ
- H0 : ↑N ⊆ E
+ H : ↑N ⊆ E
============================
"HP" : ⎡ ▷ 𓟠⎤
"Hclose" : ⎡ ▷ 𓟠={E ∖ ↑N,E}=∗ emp ⎤
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 545967539..d369d746b 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -50,7 +50,7 @@ Section base_logic_tests.
End base_logic_tests.
Section iris_tests.
- Context `{invG Σ, cinvG Σ, na_invG Σ}.
+ Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
Implicit Types P Q R : iProp Σ.
Lemma test_masks N E P Q R :
@@ -223,7 +223,7 @@ Section iris_tests.
End iris_tests.
Section monpred_tests.
- Context `{invG Σ}.
+ Context `{!invG Σ}.
Context {I : biIndex}.
Local Notation monPred := (monPred I (iPropI Σ)).
Local Notation monPredI := (monPredI I (iPropI Σ)).
diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 28cf7fdec..f62241eab 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -266,7 +266,7 @@ Lemma agree_map_to_agree {A B} (f : A → B) (x : A) :
Proof. by apply agree_eq. Qed.
Section agree_map.
- Context {A B : ofeT} (f : A → B) `{Hf: NonExpansive f}.
+ Context {A B : ofeT} (f : A → B) {Hf: NonExpansive f}.
Instance agree_map_ne : NonExpansive (agree_map f).
Proof.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 7bfb354c4..d6f038dd5 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -43,7 +43,7 @@ Definition auth_ofe_mixin : OfeMixin (auth A).
Proof. by apply (iso_ofe_mixin (λ x, (authoritative x, auth_own x))). Qed.
Canonical Structure authC := OfeT (auth A) auth_ofe_mixin.
-Global Instance auth_cofe `{Cofe A} : Cofe authC.
+Global Instance auth_cofe `{!Cofe A} : Cofe authC.
Proof.
apply (iso_cofe (λ y : _ * _, Auth (y.1) (y.2))
(λ x, (authoritative x, auth_own x))); by repeat intro.
@@ -113,7 +113,7 @@ Proof.
destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN.
Qed.
-Lemma auth_valid_discrete `{CmraDiscrete A} x :
+Lemma auth_valid_discrete `{!CmraDiscrete A} x :
✓ x ↔ match authoritative x with
| Excl' a => auth_own x ≼ a ∧ ✓ a
| None => ✓ auth_own x
@@ -125,12 +125,12 @@ Proof.
Qed.
Lemma auth_validN_2 n a b : ✓{n} (◠a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
Proof. by rewrite auth_validN_eq /= left_id. Qed.
-Lemma auth_valid_discrete_2 `{CmraDiscrete A} a b : ✓ (◠a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
+Lemma auth_valid_discrete_2 `{!CmraDiscrete A} a b : ✓ (◠a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
Proof. by rewrite auth_valid_discrete /= left_id. Qed.
Lemma authoritative_valid x : ✓ x → ✓ authoritative x.
Proof. by destruct x as [[[]|]]. Qed.
-Lemma auth_own_valid `{CmraDiscrete A} x : ✓ x → ✓ auth_own x.
+Lemma auth_own_valid `{!CmraDiscrete A} x : ✓ x → ✓ auth_own x.
Proof.
rewrite auth_valid_discrete.
destruct x as [[[]|]]; naive_solver eauto using cmra_valid_included.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 849a8ab8e..41956b441 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -52,7 +52,7 @@ Proof.
Qed.
Canonical Structure exclC : ofeT := OfeT (excl A) excl_ofe_mixin.
-Global Instance excl_cofe `{Cofe A} : Cofe exclC.
+Global Instance excl_cofe `{!Cofe A} : Cofe exclC.
Proof.
apply (iso_cofe (from_option Excl ExclBot) (maybe Excl)).
- by intros n [a|] [b|]; split; inversion_clear 1; constructor.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 018ae8697..408e75386 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -353,7 +353,7 @@ Qed.
Section freshness.
Local Set Default Proof Using "Type*".
- Context `{Infinite K}.
+ Context `{!Infinite K}.
Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
Proof.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index 380c874b8..cdfbfdbd7 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -163,7 +163,7 @@ Section gset_disj.
Section fresh_updates.
Local Set Default Proof Using "Type*".
- Context `{Infinite K}.
+ Context `{!Infinite K}.
Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X :
(∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index 5e57d9d16..8d9aa0db0 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -58,12 +58,12 @@ Program Definition list_chain
(c : chain listC) (x : A) (k : nat) : chain A :=
{| chain_car n := default x (c n !! k) |}.
Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
-Definition list_compl `{Cofe A} : Compl listC := λ c,
+Definition list_compl `{!Cofe A} : Compl listC := λ c,
match c 0 with
| [] => []
| x :: _ => compl ∘ list_chain c x <$> seq 0 (length (c 0))
end.
-Global Program Instance list_cofe `{Cofe A} : Cofe listC :=
+Global Program Instance list_cofe `{!Cofe A} : Cofe listC :=
{| compl := list_compl |}.
Next Obligation.
intros ? n c; rewrite /compl /list_compl.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 08ba333b2..9db6cf683 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -202,7 +202,7 @@ Lemma option_validI {A : cmraT} (mx : option A) :
Proof. exact: uPred_primitive.option_validI. Qed.
Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
Proof. exact: uPred_primitive.discrete_valid. Qed.
-Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
(** Consistency/soundness statement *)
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index d3ff12d81..aa2e11301 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -60,7 +60,7 @@ Proof.
Qed.
(** Timeless instances *)
-Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
+Global Instance valid_timeless {A : cmraT} `{!CmraDiscrete A} (a : A) :
Timeless (✓ a : uPred M)%I.
Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 09e64079f..c4a2fb347 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -16,7 +16,7 @@ Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → authG Σ A
Proof. solve_inG. Qed.
Section definitions.
- Context `{invG Σ, authG Σ A} {T : Type} (γ : gname).
+ Context `{!invG Σ, !authG Σ A} {T : Type} (γ : gname).
Definition auth_own (a : A) : iProp Σ :=
own γ (◯ a).
@@ -60,7 +60,7 @@ Instance: Params (@auth_inv) 5 := {}.
Instance: Params (@auth_ctx) 7 := {}.
Section auth.
- Context `{invG Σ, authG Σ A}.
+ Context `{!invG Σ, !authG Σ A}.
Context {T : Type} `{!Inhabited T}.
Context (f : T → A) (φ : T → iProp Σ).
Implicit Types N : namespace.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 9e5046219..881772bad 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -17,7 +17,7 @@ Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
Proof. solve_inG. Qed.
Section box_defs.
- Context `{invG Σ, boxG Σ} (N : namespace).
+ Context `{!invG Σ, !boxG Σ} (N : namespace).
Definition slice_name := gname.
@@ -46,7 +46,7 @@ Instance: Params (@slice) 5 := {}.
Instance: Params (@box) 5 := {}.
Section box.
-Context `{invG Σ, boxG Σ} (N : namespace).
+Context `{!invG Σ, !boxG Σ} (N : namespace).
Implicit Types P Q : iProp Σ.
Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 8239e7e3b..9d0ebd580 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -12,7 +12,7 @@ Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
Proof. solve_inG. Qed.
Section defs.
- Context `{invG Σ, cinvG Σ}.
+ Context `{!invG Σ, !cinvG Σ}.
Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
@@ -23,7 +23,7 @@ End defs.
Instance: Params (@cinv) 5 := {}.
Section proofs.
- Context `{invG Σ, cinvG Σ}.
+ Context `{!invG Σ, !cinvG Σ}.
Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
Proof. rewrite /cinv_own; apply _. Qed.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 2277c86d0..0889c404d 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -7,14 +7,14 @@ Set Default Proof Using "Type".
Export invG.
Import uPred.
-Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
(wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
-Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
-Definition uPred_fupd `{invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
-Definition uPred_fupd_eq `{invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
+Definition uPred_fupd_aux `{!invG Σ} : seal uPred_fupd_def. by eexists. Qed.
+Definition uPred_fupd `{!invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
+Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
uPred_fupd_aux.(seal_eq).
-Lemma uPred_fupd_mixin `{invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
+Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
Proof.
split.
- rewrite uPred_fupd_eq. solve_proper.
@@ -32,13 +32,13 @@ Proof.
iIntros "!> !>". by iApply "HP".
- rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
Qed.
-Instance uPred_bi_fupd `{invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
+Instance uPred_bi_fupd `{!invG Σ} : BiFUpd (uPredSI (iResUR Σ)) :=
{| bi_fupd_mixin := uPred_fupd_mixin |}.
-Instance uPred_bi_bupd_fupd `{invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
+Instance uPred_bi_bupd_fupd `{!invG Σ} : BiBUpdFUpd (uPredSI (iResUR Σ)).
Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
-Instance uPred_bi_fupd_plainly `{invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
+Instance uPred_bi_fupd_plainly `{!invG Σ} : BiFUpdPlainly (uPredSI (iResUR Σ)).
Proof.
split.
- rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
@@ -59,8 +59,8 @@ Proof.
by iFrame.
Qed.
-Lemma fupd_plain_soundness `{invPreG Σ} E (P: iProp Σ) `{!Plain P}:
- (∀ `{Hinv: invG Σ}, (|={⊤,E}=> P)%I) → (▷ P)%I.
+Lemma fupd_plain_soundness `{!invPreG Σ} E (P: iProp Σ) `{!Plain P}:
+ (∀ `{Hinv: !invG Σ}, (|={⊤,E}=> P)%I) → (▷ P)%I.
Proof.
iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
iPoseProof (Hfupd Hinv) as "H".
@@ -68,8 +68,8 @@ Proof.
iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
Qed.
-Lemma step_fupdN_soundness `{invPreG Σ} φ n :
- (∀ `{Hinv: invG Σ}, (|={⊤,∅}▷=>^n |={⊤,∅}=> ⌜ φ ⌠: iProp Σ)%I) →
+Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
+ (∀ `{Hinv: !invG Σ}, (|={⊤,∅}▷=>^n |={⊤,∅}=> ⌜ φ ⌠: iProp Σ)%I) →
φ.
Proof.
intros Hiter.
@@ -86,8 +86,8 @@ Proof.
iNext. by iMod "Hφ".
Qed.
-Lemma step_fupdN_soundness' `{invPreG Σ} φ n :
- (∀ `{Hinv: invG Σ}, (|={⊤,∅}▷=>^n ⌜ φ ⌠: iProp Σ)%I) →
+Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
+ (∀ `{Hinv: !invG Σ}, (|={⊤,∅}▷=>^n ⌜ φ ⌠: iProp Σ)%I) →
φ.
Proof.
iIntros (Hiter). eapply (step_fupdN_soundness _ n).
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index dfbaa78bf..494844854 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -28,7 +28,7 @@ Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
Proof. solve_inG. Qed.
Section definitions.
- Context `{hG : gen_heapG L V Σ}.
+ Context `{Countable L, hG : !gen_heapG L V Σ}.
Definition gen_heap_ctx (σ : gmap L V) : iProp Σ :=
own (gen_heap_name hG) (◠(to_gen_heap σ)).
@@ -72,7 +72,7 @@ Section to_gen_heap.
Proof. by rewrite /to_gen_heap fmap_delete. Qed.
End to_gen_heap.
-Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
+Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
(|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
Proof.
iMod (own_alloc (◠to_gen_heap σ)) as (γ) "Hh".
@@ -81,7 +81,7 @@ Proof.
Qed.
Section gen_heap.
- Context `{gen_heapG L V Σ}.
+ Context `{Countable L, !gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V → iProp Σ.
Implicit Types σ : gmap L V.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 4e0c9016e..cadd6f231 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
Import uPred.
(** Derived forms and lemmas about them. *)
-Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
(∃ i P', ⌜i ∈ (↑N:coPset)⌠∧ ▷ □ (P' ↔ P) ∧ ownI i P')%I.
Definition inv_aux : seal (@inv_def). by eexists. Qed.
Definition inv {Σ i} := inv_aux.(unseal) Σ i.
@@ -16,7 +16,7 @@ Instance: Params (@inv) 3 := {}.
Typeclasses Opaque inv.
Section inv.
-Context `{invG Σ}.
+Context `{!invG Σ}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Σ.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 41b81ed33..c92594bf0 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -16,7 +16,7 @@ Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
Proof. solve_inG. Qed.
Section defs.
- Context `{invG Σ, na_invG Σ}.
+ Context `{!invG Σ, !na_invG Σ}.
Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
own p (CoPset E, GSet ∅).
@@ -30,7 +30,7 @@ Instance: Params (@na_inv) 3 := {}.
Typeclasses Opaque na_own na_inv.
Section proofs.
- Context `{invG Σ, na_invG Σ}.
+ Context `{!invG Σ, !na_invG Σ}.
Global Instance na_own_timeless p E : Timeless (na_own p E).
Proof. rewrite /na_own; apply _. Qed.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index e55af99d3..7c6eebf43 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -47,11 +47,11 @@ Ltac solve_inG :=
split; (assumption || by apply _).
(** * Definition of the connective [own] *)
-Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
+Definition iRes_singleton {Σ A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4 := {}.
-Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
+Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (iRes_singleton γ a).
Definition own_aux : seal (@own_def). by eexists. Qed.
Definition own {Σ A i} := own_aux.(unseal) Σ A i.
@@ -61,7 +61,7 @@ Typeclasses Opaque own.
(** * Properties about ghost ownership *)
Section global.
-Context `{inG Σ A}.
+Context `{Hin: !inG Σ A}.
Implicit Types a : A.
(** ** Properties of [iRes_singleton] *)
@@ -113,9 +113,9 @@ Proof. rewrite !own_eq /own_def; apply _. Qed.
Lemma later_own γ a : ▷ own γ a -∗ ◇ (∃ b, own γ b ∧ ▷ (a ≡ b)).
Proof.
rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
- assert (NonExpansive (λ r : iResUR Σ, r (inG_id H) !! γ)).
+ assert (NonExpansive (λ r : iResUR Σ, r (inG_id Hin) !! γ)).
{ intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id _)). }
- rewrite (f_equiv (λ r : iResUR Σ, r (inG_id H) !! γ) _ r).
+ rewrite (f_equiv (λ r : iResUR Σ, r (inG_id Hin) !! γ) _ r).
rewrite {1}/iRes_singleton ofe_fun_lookup_singleton lookup_singleton.
rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
{ by rewrite and_elim_r /sbi_except_0 -or_intro_l. }
@@ -125,7 +125,7 @@ Proof.
cmra_transport Heq (cmra_transport (eq_sym Heq) a) = a) as ->
by (by intros ?? ->).
apply ownM_mono=> /=.
- exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id H))) r).
+ exists (ofe_fun_insert (inG_id _) (delete γ (r (inG_id Hin))) r).
intros i'. rewrite ofe_fun_lookup_op.
destruct (decide (i' = inG_id _)) as [->|?].
+ rewrite ofe_fun_lookup_insert ofe_fun_lookup_singleton.
@@ -196,7 +196,7 @@ Arguments own_update {_ _} [_] _ _ _ _.
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
-Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
+Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Proof.
rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
apply bupd_ownM_update, ofe_fun_singleton_update_empty.
@@ -206,13 +206,13 @@ Proof.
Qed.
(** Big op class instances *)
-Instance own_cmra_sep_homomorphism `{inG Σ (A:ucmraT)} :
+Instance own_cmra_sep_homomorphism `{!inG Σ (A:ucmraT)} :
WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
Proof. split; try apply _. apply own_op. Qed.
(** Proofmode class instances *)
Section proofmode_classes.
- Context `{inG Σ A}.
+ Context `{!inG Σ A}.
Implicit Types a b : A.
Global Instance into_sep_own γ a b1 b2 :
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index bc0a581d9..fc0710c9c 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -17,14 +17,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
Proof. solve_inG. Qed.
-Definition saved_anything_own `{savedAnythingG Σ F}
+Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : F (iProp Σ)) : iProp Σ :=
own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
Typeclasses Opaque saved_anything_own.
Instance: Params (@saved_anything_own) 4 := {}.
Section saved_anything.
- Context `{savedAnythingG Σ F}.
+ Context `{!savedAnythingG Σ F}.
Implicit Types x y : F (iProp Σ).
Implicit Types γ : gname.
@@ -65,22 +65,22 @@ End saved_anything.
Notation savedPropG Σ := (savedAnythingG Σ (▶ ∙)).
Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
-Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
+Definition saved_prop_own `{!savedPropG Σ} (γ : gname) (P: iProp Σ) :=
saved_anything_own (F := ▶ ∙) γ (Next P).
-Instance saved_prop_own_contractive `{savedPropG Σ} γ :
+Instance saved_prop_own_contractive `{!savedPropG Σ} γ :
Contractive (saved_prop_own γ).
Proof. solve_contractive. Qed.
-Lemma saved_prop_alloc_strong `{savedPropG Σ} (G : gset gname) (P: iProp Σ) :
+Lemma saved_prop_alloc_strong `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
(|==> ∃ γ, ⌜γ ∉ G⌠∧ saved_prop_own γ P)%I.
Proof. iApply saved_anything_alloc_strong. Qed.
-Lemma saved_prop_alloc `{savedPropG Σ} (P: iProp Σ) :
+Lemma saved_prop_alloc `{!savedPropG Σ} (P: iProp Σ) :
(|==> ∃ γ, saved_prop_own γ P)%I.
Proof. iApply saved_anything_alloc. Qed.
-Lemma saved_prop_agree `{savedPropG Σ} γ P Q :
+Lemma saved_prop_agree `{!savedPropG Σ} γ P Q :
saved_prop_own γ P -∗ saved_prop_own γ Q -∗ ▷ (P ≡ Q).
Proof.
iIntros "HP HQ". iApply later_equivI. iApply (saved_anything_agree with "HP HQ").
@@ -90,25 +90,25 @@ Qed.
Notation savedPredG Σ A := (savedAnythingG Σ (A -c> ▶ ∙)).
Notation savedPredΣ A := (savedAnythingΣ (A -c> ▶ ∙)).
-Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
+Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
saved_anything_own (F := A -c> ▶ ∙) γ (CofeMor Next ∘ Φ).
-Instance saved_pred_own_contractive `{savedPredG Σ A} γ :
+Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
Contractive (saved_pred_own γ : (A -c> iProp Σ) → iProp Σ).
Proof.
solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
Qed.
-Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
(|==> ∃ γ, ⌜γ ∉ G⌠∧ saved_pred_own γ Φ)%I.
Proof. iApply saved_anything_alloc_strong. Qed.
-Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A → iProp Σ) :
(|==> ∃ γ, saved_pred_own γ Φ)%I.
Proof. iApply saved_anything_alloc. Qed.
(* We put the `x` on the outside to make this lemma easier to apply. *)
-Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x :
+Lemma saved_pred_agree `{!savedPredG Σ A} γ Φ Ψ x :
saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
Proof.
unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 368cb41ed..6004e1b4b 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -16,7 +16,7 @@ Instance subG_stsΣ Σ sts :
Proof. solve_inG. Qed.
Section definitions.
- Context `{stsG Σ sts} (γ : gname).
+ Context `{!stsG Σ sts} (γ : gname).
Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ :=
own γ (sts_frag S T).
@@ -57,7 +57,7 @@ Instance: Params (@sts_own) 5 := {}.
Instance: Params (@sts_ctx) 6 := {}.
Section sts.
- Context `{invG Σ, stsG Σ sts}.
+ Context `{!invG Σ, !stsG Σ sts}.
Implicit Types φ : sts.state sts → iProp Σ.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Σ.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 7443ddc9b..a727317d2 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
-Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
+Definition vs `{!invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
(□ (P -∗ |={E1,E2}=> Q))%I.
Arguments vs {_ _} _ _ _%I _%I.
@@ -22,7 +22,7 @@ Notation "P ={ E }=> Q" := (P ={E}=> Q)%I
format "P ={ E }=> Q") : stdpp_scope.
Section vs.
-Context `{invG Σ}.
+Context `{!invG Σ}.
Implicit Types P Q R : iProp Σ.
Implicit Types N : namespace.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index cf629405a..78cb9f764 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -35,30 +35,30 @@ Import invG.
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) :=
to_agree (Next (iProp_unfold P)).
-Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
Arguments ownI {_ _} _ _%I.
Typeclasses Opaque ownI.
Instance: Params (@invariant_unfold) 1 := {}.
Instance: Params (@ownI) 3 := {}.
-Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
+Definition ownE `{!invG Σ} (E : coPset) : iProp Σ :=
own enabled_name (CoPset E).
Typeclasses Opaque ownE.
Instance: Params (@ownE) 3 := {}.
-Definition ownD `{invG Σ} (E : gset positive) : iProp Σ :=
+Definition ownD `{!invG Σ} (E : gset positive) : iProp Σ :=
own disabled_name (GSet E).
Typeclasses Opaque ownD.
Instance: Params (@ownD) 3 := {}.
-Definition wsat `{invG Σ} : iProp Σ :=
+Definition wsat `{!invG Σ} : iProp Σ :=
locked (∃ I : gmap positive (iProp Σ),
own invariant_name (◠(invariant_unfold <$> I : gmap _ _)) ∗
[∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
Section wsat.
-Context `{invG Σ}.
+Context `{!invG Σ}.
Implicit Types P : iProp Σ.
(* Invariants *)
@@ -194,7 +194,7 @@ Qed.
End wsat.
(* Allocation of an initial world *)
-Lemma wsat_alloc `{invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
+Lemma wsat_alloc `{!invPreG Σ} : (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
Proof.
iIntros.
iMod (own_alloc (◠(∅ : gmap _ _))) as (γI) "HI"; first done.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index 6caa4627b..9475d6c5a 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -8,7 +8,7 @@ Section class_instances.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
-Global Instance into_pure_cmra_valid `{CmraDiscrete A} (a : A) :
+Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
@IntoPure (uPredI M) (✓ a) (✓ a).
Proof. by rewrite /IntoPure discrete_valid. Qed.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 1e14ffb24..f6052c634 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -693,7 +693,7 @@ Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) :
NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
-Lemma fun_ext `{B : A → ofeT} (g1 g2 : ofe_fun B) :
+Lemma fun_ext {A} {B : A → ofeT} (g1 g2 : ofe_fun B) :
(∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
Proof. by unseal. Qed.
Lemma sig_eq {A : ofeT} (P : A → Prop) (x y : sigC P) :
@@ -797,7 +797,7 @@ Proof. unseal. by destruct mx. Qed.
Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ aâŒ.
Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
-Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
Proof. by unseal. Qed.
(** Consistency/soundness statement *)
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 02301b8fb..4bfe13696 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -14,8 +14,8 @@ Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val; proph_mapΣ proph_
Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
Proof. solve_inG. Qed.
-Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
- (∀ `{heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌠}}%I) →
+Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
+ (∀ `{!heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌠}}%I) →
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
diff --git a/theories/heap_lang/lib/assert.v b/theories/heap_lang/lib/assert.v
index c44b33126..d1d6513d3 100644
--- a/theories/heap_lang/lib/assert.v
+++ b/theories/heap_lang/lib/assert.v
@@ -9,7 +9,7 @@ Definition assert : val :=
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
-Lemma twp_assert `{heapG Σ} E (Φ : val → iProp Σ) e :
+Lemma twp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
WP e @ E [{ v, ⌜v = #true⌠∧ Φ #() }] -∗
WP assert (LamV BAnon e)%V @ E [{ Φ }].
Proof.
@@ -17,7 +17,7 @@ Proof.
wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
Qed.
-Lemma wp_assert `{heapG Σ} E (Φ : val → iProp Σ) e :
+Lemma wp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
WP e @ E {{ v, ⌜v = #true⌠∧ ▷ Φ #() }} -∗
WP assert (LamV BAnon e)%V @ E {{ Φ }}.
Proof.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 453b67420..17571589b 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -14,7 +14,7 @@ Class heapG Σ := HeapG {
heapG_proph_mapG :> proph_mapG proph_id val Σ
}.
-Instance heapG_irisG `{heapG Σ} : irisG heap_lang Σ := {
+Instance heapG_irisG `{!heapG Σ} : irisG heap_lang Σ := {
iris_invG := heapG_invG;
state_interp σ κs _ :=
(gen_heap_ctx σ.(heap) ∗ proph_map_ctx κs σ.(used_proph_id))%I;
@@ -117,7 +117,7 @@ Instance pure_injrc (v : val) :
PureExec True 1 (InjR $ Val v) (Val $ InjRV v).
Proof. solve_pure_exec. Qed.
-Instance pure_beta f x (erec : expr) (v1 v2 : val) `{AsRecV v1 f x erec} :
+Instance pure_beta f x (erec : expr) (v1 v2 : val) `{!AsRecV v1 f x erec} :
PureExec True 1 (App (Val v1) (Val v2)) (subst' x v2 (subst' f v1 erec)).
Proof. unfold AsRecV in *. solve_pure_exec. Qed.
@@ -152,7 +152,7 @@ Instance pure_case_inr v e1 e2 :
Proof. solve_pure_exec. Qed.
Section lifting.
-Context `{heapG Σ}.
+Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types efs : list expr.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index fe7726148..2f718e7f6 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -7,11 +7,11 @@ From iris.heap_lang Require Import notation.
Set Default Proof Using "Type".
Import uPred.
-Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
+Lemma tac_wp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
(∀ (e'':=e'), e = e'') →
envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
Proof. by intros ->. Qed.
-Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
+Lemma tac_twp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
(∀ (e'':=e'), e = e'') →
envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
Proof. by intros ->. Qed.
@@ -28,7 +28,7 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
| _ => fail "wp_expr_eval: not a 'wp'"
end.
-Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
+Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
MaybeIntoLaterNEnvs n Δ Δ' →
@@ -38,7 +38,7 @@ Proof.
rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
-Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ n Φ :
+Lemma tac_twp_pure `{!heapG Σ} Δ s E e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
envs_entails Δ (WP e2 @ s; E [{ Φ }]) →
@@ -47,10 +47,10 @@ Proof.
rewrite envs_entails_eq=> ?? ->. rewrite -total_lifting.twp_pure_step //.
Qed.
-Lemma tac_wp_value `{heapG Σ} Δ s E Φ v :
+Lemma tac_wp_value `{!heapG Σ} Δ s E Φ v :
envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
Proof. rewrite envs_entails_eq=> ->. by apply wp_value. Qed.
-Lemma tac_twp_value `{heapG Σ} Δ s E Φ v :
+Lemma tac_twp_value `{!heapG Σ} Δ s E Φ v :
envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
@@ -135,12 +135,12 @@ Tactic Notation "wp_inj" := wp_pure (InjL _) || wp_pure (InjR _).
Tactic Notation "wp_pair" := wp_pure (Pair _ _).
Tactic Notation "wp_closure" := wp_pure (Rec _ _ _).
-Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e f :
+Lemma tac_wp_bind `{!heapG Σ} K Δ s E Φ e f :
f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
Proof. rewrite envs_entails_eq=> -> ->. by apply: wp_bind. Qed.
-Lemma tac_twp_bind `{heapG Σ} K Δ s E Φ e f :
+Lemma tac_twp_bind `{!heapG Σ} K Δ s E Φ e f :
f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I →
envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
@@ -171,7 +171,7 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
(** Heap tactics *)
Section heap.
-Context `{heapG Σ}.
+Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
Implicit Types Δ : envs (uPredI (iResUR Σ)).
diff --git a/theories/heap_lang/proph_map.v b/theories/heap_lang/proph_map.v
index 39308f1a9..4e965dd67 100644
--- a/theories/heap_lang/proph_map.v
+++ b/theories/heap_lang/proph_map.v
@@ -31,7 +31,7 @@ Instance subG_proph_mapPreG {Σ P V} `{Countable P} :
Proof. solve_inG. Qed.
Section definitions.
- Context `{pG : proph_mapG P V Σ}.
+ Context `{Countable P, pG : !proph_mapG P V Σ}.
(** The first resolve for [p] in [pvs] *)
Definition first_resolve (pvs : proph_val_list P V) (p : P) : option V :=
@@ -127,7 +127,7 @@ Section to_proph_map.
End to_proph_map.
-Lemma proph_map_init `{proph_mapPreG P V PVS} pvs ps :
+Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
(|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
Proof.
iMod (own_alloc (◠to_proph_map ∅)) as (γ) "Hh".
@@ -137,7 +137,7 @@ Proof.
Qed.
Section proph_map.
- Context `{proph_mapG P V Σ}.
+ Context `{Countable P, !proph_mapG P V Σ}.
Implicit Types p : P.
Implicit Types v : option V.
Implicit Types R : proph_map P V.
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 8cfbfb39b..df83c1542 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -4,8 +4,8 @@ From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
-Definition heap_total Σ `{heapPreG Σ} s e σ φ :
- (∀ `{heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌠}]%I) →
+Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
+ (∀ `{!heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌠}]%I) →
sn erased_step ([e], σ).
Proof.
intros Hwp; eapply (twp_total _ _); iIntros (?) "".
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 770e56fb1..6bca02624 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -33,7 +33,7 @@ Proof.
Qed.
Section adequacy.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
Implicit Types e : expr Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
@@ -173,8 +173,8 @@ Proof.
Qed.
End adequacy.
-Theorem wp_strong_adequacy Σ Λ `{invPreG Σ} s e σ φ :
- (∀ `{Hinv : invG Σ} κs,
+Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
+ (∀ `{Hinv : !invG Σ} κs,
(|={⊤}=> ∃
(stateI : state Λ → list (observation Λ) → nat → iProp Σ)
(fork_post : val Λ → iProp Σ),
@@ -198,8 +198,8 @@ Proof.
iApply (@wptp_safe _ _ (IrisG _ _ Hinv stateI fork_post) with "[Hσ] Hwp"); eauto.
Qed.
-Theorem wp_adequacy Σ Λ `{invPreG Σ} s e σ φ :
- (∀ `{Hinv : invG Σ} κs,
+Theorem wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
+ (∀ `{Hinv : !invG Σ} κs,
(|={⊤}=> ∃ stateI : state Λ → list (observation Λ) → iProp Σ,
let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) (λ _, True%I) in
stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌠}})%I) →
@@ -212,8 +212,8 @@ Proof.
iIntros "_". by iApply fupd_mask_weaken.
Qed.
-Theorem wp_strong_all_adequacy Σ Λ `{invPreG Σ} s e σ1 v vs σ2 φ :
- (∀ `{Hinv : invG Σ} κs,
+Theorem wp_strong_all_adequacy Σ Λ `{!invPreG Σ} s e σ1 v vs σ2 φ :
+ (∀ `{Hinv : !invG Σ} κs,
(|={⊤}=> ∃
(stateI : state Λ → list (observation Λ) → nat → iProp Σ)
(fork_post : val Λ → iProp Σ),
@@ -232,8 +232,8 @@ Proof.
with "[Hσ] [Hwp]"); eauto. by rewrite right_id_L.
Qed.
-Theorem wp_invariance Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
- (∀ `{Hinv : invG Σ} κs κs',
+Theorem wp_invariance Σ Λ `{!invPreG Σ} s e σ1 t2 σ2 φ :
+ (∀ `{Hinv : !invG Σ} κs κs',
(|={⊤}=> ∃
(stateI : state Λ → list (observation Λ) → nat → iProp Σ)
(fork_post : val Λ → iProp Σ),
@@ -253,8 +253,8 @@ Qed.
(* An equivalent version that does not require finding [fupd_intro_mask'], but
can be confusing to use. *)
-Corollary wp_invariance' Σ Λ `{invPreG Σ} s e σ1 t2 σ2 φ :
- (∀ `{Hinv : invG Σ} κs κs',
+Corollary wp_invariance' Σ Λ `{!invPreG Σ} s e σ1 t2 σ2 φ :
+ (∀ `{Hinv : !invG Σ} κs κs',
(|={⊤}=> ∃
(stateI : state Λ → list (observation Λ) → nat → iProp Σ)
(fork_post : val Λ → iProp Σ),
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 25df772be..487acd356 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
(* This hard-codes the inner mask to be empty, because we have yet to find an
example where we want it to be anything else. *)
-Definition atomic_wp `{irisG Λ Σ} {TA TB : tele}
+Definition atomic_wp `{!irisG Λ Σ} {TA TB : tele}
(e: expr Λ) (* expression *)
(Eo : coPset) (* (outer) mask *)
(α: TA → iProp Σ) (* atomic pre-condition *)
@@ -94,7 +94,7 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
(** Theory *)
Section lemmas.
- Context `{irisG Λ Σ} {TA TB : tele}.
+ Context `{!irisG Λ Σ} {TA TB : tele}.
Notation iProp := (iProp Σ).
Implicit Types (α : TA → iProp) (β : TA → TB → iProp) (f : TA → TB → val Λ).
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 68b183168..dd0fff991 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -201,7 +201,7 @@ Section ectx_language.
Qed.
(* Every evaluation context is a context. *)
- Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
+ Global Instance ectx_lang_ctx K : LanguageCtx _ (fill K).
Proof.
split; simpl.
- eauto using fill_not_val.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 12c6d3f0e..a164cb131 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section wp.
-Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
+Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
Implicit Types s : stuckness.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 603d21651..c23bfbef3 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -137,8 +137,8 @@ Section ectxi_language.
intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
Qed.
- Global Instance ectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
- Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
+ Global Instance ectxi_lang_ctx_item Ki : LanguageCtx _ (fill_item Ki).
+ Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed.
End ectxi_language.
Arguments fill {_} _ _%E.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index b6587a441..ff46550fc 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export viewshifts.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
-Definition ht `{irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
+Definition ht `{!irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
(e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
(□ (P -∗ WP e @ s; E {{ Φ }}))%I.
Instance: Params (@ht) 5 := {}.
@@ -41,7 +41,7 @@ Notation "{{ P } } e ? {{ v , Q } }" := (ht MaybeStuck ⊤ P%I e%E (λ v, Q)%I)
format "{{ P } } e ? {{ v , Q } }") : stdpp_scope.
Section hoare.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
Implicit Types s : stuckness.
Implicit Types P Q : iProp Σ.
Implicit Types Φ Ψ : val Λ → iProp Σ.
@@ -89,7 +89,7 @@ Proof.
iIntros (v) "Hv". by iApply "HΦ".
Qed.
-Lemma ht_bind `{LanguageCtx Λ K} s E P Φ Φ' e :
+Lemma ht_bind `{!LanguageCtx Λ K} s E P Φ Φ' e :
{{ P }} e @ s; E {{ Φ }} ∧ (∀ v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
⊢ {{ P }} K e @ s; E {{ Φ' }}.
Proof.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 378d68c79..483d9a244 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -53,8 +53,9 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
to_val e1' = None → prim_step (K e1') σ1 κ e2 σ2 efs →
∃ e2', e2 = K e2' ∧ prim_step e1' σ1 κ e2' σ2 efs
}.
+Arguments LanguageCtx : clear implicits.
-Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
+Instance language_ctx_id Λ : LanguageCtx Λ (@id (expr Λ)).
Proof. constructor; naive_solver. Qed.
Inductive atomicity := StronglyAtomic | WeaklyAtomic.
@@ -141,19 +142,19 @@ Section language.
Atomic StronglyAtomic e → Atomic a e.
Proof. unfold Atomic. destruct a; eauto using val_irreducible. Qed.
- Lemma reducible_fill `{LanguageCtx Λ K} e σ :
+ Lemma reducible_fill `{!LanguageCtx Λ K} e σ :
to_val e = None → reducible (K e) σ → reducible e σ.
Proof.
intros ? (e'&σ'&k&efs&Hstep); unfold reducible.
apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
Qed.
- Lemma reducible_no_obs_fill `{LanguageCtx Λ K} e σ :
+ Lemma reducible_no_obs_fill `{!LanguageCtx Λ K} e σ :
to_val e = None → reducible_no_obs (K e) σ → reducible_no_obs e σ.
Proof.
intros ? (e'&σ'&efs&Hstep); unfold reducible_no_obs.
apply fill_step_inv in Hstep as (e2' & _ & Hstep); eauto.
Qed.
- Lemma irreducible_fill `{LanguageCtx Λ K} e σ :
+ Lemma irreducible_fill `{!LanguageCtx Λ K} e σ :
to_val e = None → irreducible e σ → irreducible (K e) σ.
Proof. rewrite -!not_reducible. naive_solver eauto using reducible_fill. Qed.
@@ -185,7 +186,7 @@ Section language.
Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
pure_exec : φ → relations.nsteps pure_step n e1 e2.
- Lemma pure_step_ctx K `{LanguageCtx Λ K} e1 e2 :
+ Lemma pure_step_ctx K `{!LanguageCtx Λ K} e1 e2 :
pure_step e1 e2 →
pure_step (K e1) (K e2).
Proof.
@@ -197,13 +198,13 @@ Section language.
+ edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
Qed.
- Lemma pure_step_nsteps_ctx K `{LanguageCtx Λ K} n e1 e2 :
+ Lemma pure_step_nsteps_ctx K `{!LanguageCtx Λ K} n e1 e2 :
relations.nsteps pure_step n e1 e2 →
relations.nsteps pure_step n (K e1) (K e2).
Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
(* We do not make this an instance because it is awfully general. *)
- Lemma pure_exec_ctx K `{LanguageCtx Λ K} φ n e1 e2 :
+ Lemma pure_exec_ctx K `{!LanguageCtx Λ K} φ n e1 e2 :
PureExec φ n e1 e2 →
PureExec φ n (K e1) (K e2).
Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index 4d9e79a9d..3219b1456 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section lifting.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
Implicit Types s : stuckness.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
@@ -53,7 +53,7 @@ Proof.
iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !> !>". by iApply "H".
Qed.
-Lemma wp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E E' Φ e1 :
+Lemma wp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E E' Φ e1 :
(∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
(|={E,E'}▷=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌠→ WP e2 @ s; E {{ Φ }})
@@ -70,7 +70,7 @@ Proof.
iDestruct ("H" with "[//]") as "H". simpl. iFrame.
Qed.
-Lemma wp_lift_pure_stuck `{Inhabited (state Λ)} E Φ e :
+Lemma wp_lift_pure_stuck `{!Inhabited (state Λ)} E Φ e :
(∀ σ, stuck e σ) →
True ⊢ WP e @ E ?{{ Φ }}.
Proof.
@@ -120,7 +120,7 @@ Proof.
by iApply "H".
Qed.
-Lemma wp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E E' Φ} e1 e2 :
+Lemma wp_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E E' Φ} e1 e2 :
(∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
@@ -132,7 +132,7 @@ Proof.
iIntros (κ e' efs' σ (_&?&->&?)%Hpuredet); auto.
Qed.
-Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
+Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
(|={E,E'}▷=>^n WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
@@ -145,7 +145,7 @@ Proof.
- by iApply (step_fupd_wand with "Hwp").
Qed.
-Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
+Lemma wp_pure_step_later `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
▷^n WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 17530e77e..d48ef7a93 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -20,7 +20,7 @@ Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
ownP_name : gname;
}.
-Instance ownPG_irisG `{ownPG Λ Σ} : irisG Λ Σ := {
+Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
iris_invG := ownP_invG;
state_interp σ κs _ := own ownP_name (◠(Excl' σ))%I;
fork_post _ := True%I;
@@ -40,15 +40,15 @@ Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPPreG Λ Σ.
Proof. solve_inG. Qed.
(** Ownership *)
-Definition ownP `{ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
+Definition ownP `{!ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
own ownP_name (◯ (Excl' σ)).
Typeclasses Opaque ownP.
Instance: Params (@ownP) 3 := {}.
(* Adequacy *)
-Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
- (∀ `{ownPG Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌠}}) →
+Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
+ (∀ `{!ownPG Λ Σ}, ownP σ ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌠}}) →
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply (wp_adequacy Σ _).
@@ -59,8 +59,8 @@ Proof.
iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
Qed.
-Theorem ownP_invariance Σ `{ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
- (∀ `{ownPG Λ Σ},
+Theorem ownP_invariance Σ `{!ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
+ (∀ `{!ownPG Λ Σ},
ownP σ1 ={⊤}=∗ WP e @ s; ⊤ {{ _, True }} ∗
|={⊤,∅}=> ∃ σ', ownP σ' ∧ ⌜φ σ'âŒ) →
rtc erased_step ([e], σ1) (t2, σ2) →
@@ -81,7 +81,7 @@ Qed.
(** Lifting *)
Section lifting.
- Context `{ownPG Λ Σ}.
+ Context `{!ownPG Λ Σ}.
Implicit Types s : stuckness.
Implicit Types e : expr Λ.
Implicit Types Φ : val Λ → iProp Σ.
@@ -134,7 +134,7 @@ Section lifting.
by iDestruct (ownP_eq with "Hσ Hσf") as %->.
Qed.
- Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
+ Lemma ownP_lift_pure_step `{!Inhabited (state Λ)} s E Φ e1 :
(∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1) →
(▷ ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌠→
@@ -193,7 +193,7 @@ Section lifting.
iSplitL "Hs"; first by iFrame. iModIntro. iIntros "Hσ2". iApply "Hs'". iFrame.
Qed.
- Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
+ Lemma ownP_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E Φ} e1 e2 :
(∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
(∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' → κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
@@ -204,7 +204,7 @@ End lifting.
Section ectx_lifting.
Import ectx_language.
- Context {Λ : ectxLanguage} `{ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
+ Context {Λ : ectxLanguage} `{!ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
Implicit Types s : stuckness.
Implicit Types Φ : val Λ → iProp Σ.
Implicit Types e : expr Λ.
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index b6243370d..9e8ba8f6d 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
Import uPred.
Section adequacy.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
Implicit Types e : expr Λ.
Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
@@ -114,8 +114,8 @@ Proof.
Qed.
End adequacy.
-Theorem twp_total Σ Λ `{invPreG Σ} s e σ Φ :
- (∀ `{Hinv : invG Σ},
+Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
+ (∀ `{Hinv : !invG Σ},
(|={⊤}=> ∃
(stateI : state Λ → list (observation Λ) → nat → iProp Σ)
(fork_post : val Λ → iProp Σ),
diff --git a/theories/program_logic/total_ectx_lifting.v b/theories/program_logic/total_ectx_lifting.v
index 7a3e8e977..3e1168bfc 100644
--- a/theories/program_logic/total_ectx_lifting.v
+++ b/theories/program_logic/total_ectx_lifting.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section wp.
-Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
+Context {Λ : ectxLanguage} `{!irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
Implicit Types v : val Λ.
diff --git a/theories/program_logic/total_lifting.v b/theories/program_logic/total_lifting.v
index fe953845e..c2e7a9086 100644
--- a/theories/program_logic/total_lifting.v
+++ b/theories/program_logic/total_lifting.v
@@ -4,7 +4,7 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section lifting.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
@@ -26,7 +26,7 @@ Lemma twp_lift_step s E Φ e1 :
Proof. by rewrite twp_unfold /twp_pre=> ->. Qed.
(** Derived lifting lemmas. *)
-Lemma twp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E Φ e1 :
+Lemma twp_lift_pure_step_no_fork `{!Inhabited (state Λ)} s E Φ e1 :
(∀ σ1, reducible_no_obs e1 σ1) →
(∀ σ1 κ e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs → κ = [] ∧ σ2 = σ1 ∧ efs = []) →
(|={E}=> ∀ κ e2 efs σ, ⌜prim_step e1 σ κ e2 σ efs⌠→ WP e2 @ s; E [{ Φ }])
@@ -65,7 +65,7 @@ Proof.
iApply twp_value; last done. by apply of_to_val.
Qed.
-Lemma twp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
+Lemma twp_lift_pure_det_step_no_fork `{!Inhabited (state Λ)} {s E Φ} e1 e2 :
(∀ σ1, reducible_no_obs e1 σ1) →
(∀ σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs' →
κ = [] ∧ σ2 = σ1 ∧ e2' = e2 ∧ efs' = []) →
@@ -76,7 +76,7 @@ Proof.
iIntros "!>" (κ' e' efs' σ (_&_&->&->)%Hpuredet); auto.
Qed.
-Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
+Lemma twp_pure_step `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
PureExec φ n e1 e2 →
φ →
WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index e3da620ff..24173b691 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -4,7 +4,7 @@ From iris.bi Require Import fixpoint big_op.
Set Default Proof Using "Type".
Import uPred.
-Definition twp_pre `{irisG Λ Σ} (s : stuckness)
+Definition twp_pre `{!irisG Λ Σ} (s : stuckness)
(wp : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := λ E e1 Φ,
match to_val e1 with
@@ -19,7 +19,7 @@ Definition twp_pre `{irisG Λ Σ} (s : stuckness)
[∗ list] ef ∈ efs, wp ⊤ ef fork_post
end%I.
-Lemma twp_pre_mono `{irisG Λ Σ} s
+Lemma twp_pre_mono `{!irisG Λ Σ} s
(wp1 wp2 : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ) :
((□ ∀ E e Φ, wp1 E e Φ -∗ wp2 E e Φ) →
∀ E e Φ, twp_pre s wp1 E e Φ -∗ twp_pre s wp2 E e Φ)%I.
@@ -36,12 +36,12 @@ Proof.
Qed.
(* Uncurry [twp_pre] and equip its type with an OFE structure *)
-Definition twp_pre' `{irisG Λ Σ} (s : stuckness) :
+Definition twp_pre' `{!irisG Λ Σ} (s : stuckness) :
(prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ) →
prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ :=
curry3 ∘ twp_pre s ∘ uncurry3.
-Local Instance twp_pre_mono' `{irisG Λ Σ} s : BiMonoPred (twp_pre' s).
+Local Instance twp_pre_mono' `{!irisG Λ Σ} s : BiMonoPred (twp_pre' s).
Proof.
constructor.
- iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
@@ -51,15 +51,15 @@ Proof.
rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
Qed.
-Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
+Definition twp_def `{!irisG Λ Σ} (s : stuckness) (E : coPset)
(e : expr Λ) (Φ : val Λ → iProp Σ) :
iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
-Definition twp_aux `{irisG Λ Σ} : seal (@twp_def Λ Σ _). by eexists. Qed.
-Instance twp' `{irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
-Definition twp_eq `{irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
+Definition twp_aux `{!irisG Λ Σ} : seal (@twp_def Λ Σ _). by eexists. Qed.
+Instance twp' `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
+Definition twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
Section twp.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
Implicit Types s : stuckness.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
@@ -147,7 +147,7 @@ Proof.
iModIntro. iSplit; first done. iFrame "Hσ Hefs". by iApply twp_value'.
Qed.
-Lemma twp_bind K `{!LanguageCtx K} s E e Φ :
+Lemma twp_bind K `{!LanguageCtx Λ K} s E e Φ :
WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }] -∗ WP K e @ s; E [{ Φ }].
Proof.
revert Φ. cut (∀ Φ', WP e @ s; E [{ Φ' }] -∗ ∀ Φ,
@@ -169,7 +169,7 @@ Proof.
- by setoid_rewrite and_elim_r.
Qed.
-Lemma twp_bind_inv K `{!LanguageCtx K} s E e Φ :
+Lemma twp_bind_inv K `{!LanguageCtx Λ K} s E e Φ :
WP K e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, WP K (of_val v) @ s; E [{ Φ }] }].
Proof.
iIntros "H". remember (K e) as e' eqn:He'.
@@ -251,7 +251,7 @@ End twp.
(** Proofmode class instances *)
Section proofmode_classes.
- Context `{irisG Λ Σ}.
+ Context `{!irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 65513253b..47ba39abe 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -22,7 +22,7 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
}.
Global Opaque iris_invG.
-Definition wp_pre `{irisG Λ Σ} (s : stuckness)
+Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
@@ -36,20 +36,20 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
[∗ list] i ↦ ef ∈ efs, wp ⊤ ef fork_post
end%I.
-Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).
+Local Instance wp_pre_contractive `{!irisG Λ Σ} s : Contractive (wp_pre s).
Proof.
rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
repeat (f_contractive || f_equiv); apply Hwp.
Qed.
-Definition wp_def `{irisG Λ Σ} (s : stuckness) :
+Definition wp_def `{!irisG Λ Σ} (s : stuckness) :
coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
-Definition wp_aux `{irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
-Instance wp' `{irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
-Definition wp_eq `{irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
+Definition wp_aux `{!irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
+Instance wp' `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
+Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
Section wp.
-Context `{irisG Λ Σ}.
+Context `{!irisG Λ Σ}.
Implicit Types s : stuckness.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
@@ -143,7 +143,7 @@ Proof.
iIntros (v) "H". by iApply "H".
Qed.
-Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
+Lemma wp_bind K `{!LanguageCtx Λ K} s E e Φ :
WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }} ⊢ WP K e @ s; E {{ Φ }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
@@ -160,7 +160,7 @@ Proof.
iModIntro. iFrame "Hσ Hefs". by iApply "IH".
Qed.
-Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
+Lemma wp_bind_inv K `{!LanguageCtx Λ K} s E e Φ :
WP K e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
@@ -252,7 +252,7 @@ End wp.
(** Proofmode class instances *)
Section proofmode_classes.
- Context `{irisG Λ Σ}.
+ Context `{!irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ → iProp Σ.
--
GitLab