From 31bb46c510d206720483e20fff970e143b4f402c Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gmalecha@gmail.com>
Date: Mon, 16 Mar 2020 15:03:35 +0100
Subject: [PATCH] CLEAN cleanup
- remove "odd" comment
- move atomic triples to bi_scope
---
tests/atomic.ref | 58 ++++++++++---------
tests/atomic.v | 26 ++++-----
tests/heap_lang.v | 34 +++++------
tests/ipm_paper.v | 10 ++--
tests/one_shot.v | 4 +-
tests/one_shot_once.v | 4 +-
tests/proofmode.v | 58 +++++++++----------
tests/proofmode_iris.v | 4 +-
tests/proofmode_monpred.v | 2 +-
tests/proofmode_siprop.v | 6 +-
theories/base_logic/bi.v | 2 -
theories/base_logic/derived.v | 14 +----
theories/base_logic/lib/auth.v | 2 +-
theories/base_logic/lib/boxes.v | 2 +-
.../base_logic/lib/cancelable_invariants.v | 10 ++--
theories/base_logic/lib/fancy_updates.v | 4 +-
theories/base_logic/lib/gen_heap.v | 2 +-
theories/base_logic/lib/invariants.v | 4 +-
theories/base_logic/lib/na_invariants.v | 2 +-
theories/base_logic/lib/own.v | 20 +++----
theories/base_logic/lib/proph_map.v | 2 +-
theories/base_logic/lib/saved_prop.v | 18 +++---
theories/base_logic/lib/viewshifts.v | 8 +--
theories/base_logic/lib/wsat.v | 10 ++--
theories/bi/derived_laws_bi.v | 24 ++++----
theories/bi/embedding.v | 4 +-
theories/bi/interface.v | 6 +-
theories/bi/lib/atomic.v | 4 +-
theories/bi/lib/counterexamples.v | 18 +++---
theories/bi/lib/fixpoint.v | 2 +-
theories/bi/lib/relations.v | 2 +-
theories/bi/notation.v | 3 +
theories/bi/updates.v | 2 +-
theories/heap_lang/adequacy.v | 2 +-
theories/heap_lang/array.v | 2 +-
theories/heap_lang/lib/atomic_heap.v | 18 +++---
theories/heap_lang/lib/diverge.v | 2 +-
theories/heap_lang/lib/increment.v | 8 +--
theories/heap_lang/total_adequacy.v | 2 +-
theories/program_logic/adequacy.v | 12 ++--
theories/program_logic/atomic.v | 8 +--
theories/program_logic/ectx_lifting.v | 2 +-
theories/program_logic/hoare.v | 4 +-
theories/program_logic/total_adequacy.v | 10 ++--
theories/program_logic/total_weakestpre.v | 4 +-
theories/proofmode/coq_tactics.v | 2 +-
theories/si_logic/bi.v | 2 -
47 files changed, 222 insertions(+), 227 deletions(-)
diff --git a/tests/atomic.ref b/tests/atomic.ref
index ba5c5ad60..c9e56f2c4 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -26,7 +26,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
P : val → iProp Σ
============================
- <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
+ ⊢ <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
1 subgoal
Σ : gFunctors
@@ -58,7 +58,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
- <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
+ ⊢ <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
@@ -89,7 +89,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
- <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+ ⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
@@ -121,7 +121,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
- <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
+ ⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
@@ -154,7 +154,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
- <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+ ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
+ code @ ⊤
+ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
@@ -173,9 +175,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
- <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
- code @ ⊤
- <<< ∃ y : val, l ↦ y, RET #() >>>
+ ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+ code @ ⊤
+ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
@@ -194,10 +196,10 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
- <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
- code @ ⊤
- <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
- RET #() >>>
+ ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+ code @ ⊤
+ <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+ RET #() >>>
1 subgoal
Σ : gFunctors
@@ -218,9 +220,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
heapG0 : heapG Σ
l : loc
============================
- <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
- code @ ⊤
- <<< l ↦ x, RET #() >>>
+ ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+ code @ ⊤
+ <<< l ↦ x, RET #() >>>
1 subgoal
Σ : gFunctors
@@ -240,9 +242,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
l : loc
x : val
============================
- <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
- code @ ⊤
- <<< ∃ y : val, l ↦ y, RET #() >>>
+ ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+ code @ ⊤
+ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
Σ : gFunctors
@@ -263,9 +265,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
l : loc
x : val
============================
- <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
- code @ ⊤
- <<< l ↦ #(), RET #() >>>
+ ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+ code @ ⊤
+ <<< l ↦ #(), RET #() >>>
1 subgoal
Σ : gFunctors
@@ -286,9 +288,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
l : loc
xx, yyyy : val
============================
- <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
- code @ ⊤
- <<< l ↦ yyyy, RET #() >>>
+ ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+ code @ ⊤
+ <<< l ↦ yyyy, RET #() >>>
1 subgoal
Σ : gFunctors
@@ -309,10 +311,10 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
l : loc
xx, yyyy : val
============================
- <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
- code @ ⊤
- <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
- RET #() >>>
+ ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+ code @ ⊤
+ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+ RET #() >>>
1 subgoal
Σ : gFunctors
diff --git a/tests/atomic.v b/tests/atomic.v
index 125a261c1..7e9ed0726 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -41,28 +41,28 @@ Section printing.
Definition code : expr := #().
Lemma print_both_quant (P : val → iProp Σ) :
- <<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
+ ⊢ <<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_first_quant l :
- <<< ∀ x, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+ ⊢ <<< ∀ x, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_second_quant l :
- <<< l ↦ #() >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+ ⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
Abort.
Lemma print_no_quant l :
- <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
+ ⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
iPoseProof (aupd_aacc with "AU") as "?". Show.
@@ -71,49 +71,49 @@ Section printing.
Check "Now come the long pre/post tests".
Lemma print_both_quant_long l :
- <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+ ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_both_quant_longpre l :
- <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+ ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_both_quant_longpost l :
- <<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+ ⊢ <<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
Proof.
Show. iIntros (Φ) "?". Show.
Abort.
Lemma print_first_quant_long l :
- <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
+ ⊢ <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_second_quant_long l x :
- <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
+ ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_long l x :
- <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
+ ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_longpre l xx yyyy :
- <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy, RET #() >>>.
+ ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
Lemma print_no_quant_longpost l xx yyyy :
- <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
+ ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
Proof.
Show. iIntros (Φ) "AU". Show.
Abort.
@@ -121,7 +121,7 @@ Section printing.
Check "Prettification".
Lemma iMod_prettify (P : val → iProp Σ) :
- <<< ∀ x, P x >>> !#0 @ ⊤ <<< ∃ y, P y, RET #() >>>.
+ ⊢ <<< ∀ x, P x >>> !#0 @ ⊤ <<< ∃ y, P y, RET #() >>>.
Proof.
iIntros (Φ) "AU". iMod "AU". Show.
Abort.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 942b4bb79..6a9e55e54 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -24,7 +24,7 @@ Section tests.
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
- Lemma heap_e_spec E : WP heap_e @ E {{ v, ⌜v = #2⌠}}%I.
+ Lemma heap_e_spec E : ⊢ WP heap_e @ E {{ v, ⌜v = #2⌠}}.
Proof.
iIntros "". rewrite /heap_e. Show.
wp_alloc l as "?". wp_load. Show.
@@ -36,7 +36,7 @@ Section tests.
let: "y" := ref #1 in
"x" <- !"x" + #1 ;; !"x".
- Lemma heap_e2_spec E : WP heap_e2 @ E [{ v, ⌜v = #2⌠}]%I.
+ Lemma heap_e2_spec E : ⊢ WP heap_e2 @ E [{ v, ⌜v = #2⌠}].
Proof.
iIntros "". rewrite /heap_e2.
wp_alloc l as "Hl". Show. wp_alloc l'.
@@ -48,7 +48,7 @@ Section tests.
let: "f" := λ: "z", "z" + #1 in
if: "x" then "f" #0 else "f" #1.
- Lemma heap_e3_spec E : WP heap_e3 @ E [{ v, ⌜v = #1⌠}]%I.
+ Lemma heap_e3_spec E : ⊢ WP heap_e3 @ E [{ v, ⌜v = #1⌠}].
Proof.
iIntros "". rewrite /heap_e3.
by repeat (wp_pure _).
@@ -58,7 +58,7 @@ Section tests.
let: "x" := (let: "y" := ref (ref #1) in ref "y") in
! ! !"x".
- Lemma heap_e4_spec : WP heap_e4 [{ v, ⌜ v = #1 ⌠}]%I.
+ Lemma heap_e4_spec : ⊢ WP heap_e4 [{ v, ⌜ v = #1 ⌠}].
Proof.
rewrite /heap_e4. wp_alloc l. wp_alloc l'.
wp_alloc l''. by repeat wp_load.
@@ -67,7 +67,7 @@ Section tests.
Definition heap_e5 : expr :=
let: "x" := ref (ref #1) in ! ! "x" + FAA (!"x") (#10 + #1).
- Lemma heap_e5_spec E : WP heap_e5 @ E [{ v, ⌜v = #13⌠}]%I.
+ Lemma heap_e5_spec E : ⊢ WP heap_e5 @ E [{ v, ⌜v = #13⌠}].
Proof.
rewrite /heap_e5. wp_alloc l. wp_alloc l'.
wp_load. wp_faa. do 2 wp_load. by wp_pures.
@@ -76,7 +76,7 @@ Section tests.
Definition heap_e6 : val := λ: "v", "v" = "v".
Lemma heap_e6_spec (v : val) :
- val_is_unboxed v → (WP heap_e6 v {{ w, ⌜ w = #true ⌠}})%I.
+ val_is_unboxed v → ⊢ WP heap_e6 v {{ w, ⌜ w = #true ⌠}}.
Proof. intros ?. wp_lam. wp_op. by case_bool_decide. Qed.
Definition heap_e7 : val := λ: "v", CmpXchg "v" #0 #1.
@@ -117,7 +117,7 @@ Section tests.
Qed.
Lemma Pred_user E :
- WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌠}]%I.
+ ⊢ WP let: "x" := Pred #42 in Pred "x" @ E [{ v, ⌜v = #40⌠}].
Proof. iIntros "". wp_apply Pred_spec. by wp_apply Pred_spec. Qed.
Lemma wp_apply_evar e P :
@@ -132,22 +132,22 @@ Section tests.
Qed.
Lemma wp_alloc_split :
- WP Alloc #0 {{ _, True }}%I.
+ ⊢ WP Alloc #0 {{ _, True }}.
Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.
Lemma wp_alloc_drop :
- WP Alloc #0 {{ _, True }}%I.
+ ⊢ WP Alloc #0 {{ _, True }}.
Proof. wp_alloc l as "_". Show. done. Qed.
Check "wp_nonclosed_value".
Lemma wp_nonclosed_value :
- WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}%I.
+ ⊢ WP let: "x" := #() in (λ: "y", "x")%V #() {{ _, True }}.
Proof. wp_let. wp_lam. Fail wp_pure _. Show. Abort.
Lemma wp_alloc_array n : 0 < n →
- {{{ True }}}
- AllocN #n #0
- {{{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}}}%I.
+ ⊢ {{{ True }}}
+ AllocN #n #0
+ {{{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}}}.
Proof.
iIntros (? Φ) "!> _ HΦ".
wp_alloc l as "?"; first done.
@@ -155,9 +155,9 @@ Section tests.
Qed.
Lemma twp_alloc_array n : 0 < n →
- [[{ True }]]
- AllocN #n #0
- [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}]]%I.
+ ⊢ [[{ True }]]
+ AllocN #n #0
+ [[{ l, RET #l; l ↦∗ replicate (Z.to_nat n) #0}]].
Proof.
iIntros (? Φ) "!> _ HΦ".
wp_alloc l as "?"; first done. Show.
@@ -258,7 +258,7 @@ Section error_tests.
Check "not_cmpxchg".
Lemma not_cmpxchg :
- (WP #() #() {{ _, True }})%I.
+ ⊢ WP #() #() {{ _, True }}.
Proof.
Fail wp_cmpxchg_suc.
Abort.
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index ac07123e5..1822dfc3b 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -75,7 +75,7 @@ Section list_reverse.
end.
Lemma rev_acc_ht hd acc xs ys :
- {{ is_list hd xs ∗ is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
+ ⊢ {{ is_list hd xs ∗ is_list acc ys }} rev hd acc {{ w, is_list w (reverse xs ++ ys) }}.
Proof.
iIntros "!> [Hxs Hys]".
iLöb as "IH" forall (hd acc xs ys). wp_rec; wp_let.
@@ -89,7 +89,7 @@ Section list_reverse.
Qed.
Lemma rev_ht hd xs :
- {{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
+ ⊢ {{ is_list hd xs }} rev hd NONEV {{ w, is_list w (reverse xs) }}.
Proof.
iIntros "!> Hxs". rewrite -(right_id_L [] (++) (reverse xs)).
iApply (rev_acc_ht hd NONEV with "[Hxs]"); simpl; by iFrame.
@@ -202,7 +202,7 @@ Section counter_proof.
Proof. apply _. Qed.
Lemma newcounter_spec :
- {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌠∧ C l 0 }}.
+ ⊢ {{ True }} newcounter #() {{ v, ∃ l, ⌜v = #l⌠∧ C l 0 }}.
Proof.
iIntros "!> _ /=". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Auth 0)) as (γ) "Hγ"; first done.
@@ -214,7 +214,7 @@ Section counter_proof.
Qed.
Lemma incr_spec l n :
- {{ C l n }} incr #l {{ v, ⌜v = #()⌠∧ C l (S n) }}.
+ ⊢ {{ C l n }} incr #l {{ v, ⌜v = #()⌠∧ C l (S n) }}.
Proof.
iIntros "!> Hl /=". iLöb as "IH". wp_rec.
iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
@@ -239,7 +239,7 @@ Section counter_proof.
Check "read_spec".
Lemma read_spec l n :
- {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌠∧ C l m }}.
+ ⊢ {{ C l n }} read #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌠∧ C l m }}.
Proof.
iIntros "!> Hl /=". iDestruct "Hl" as (N γ) "[#Hinv Hγf]".
rewrite /read /=. wp_lam. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 89ad969fb..756b8f406 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -88,7 +88,7 @@ Proof.
Qed.
Lemma ht_one_shot (Φ : val → iProp Σ) :
- {{ True }} one_shot_example #()
+ ⊢ {{ True }} one_shot_example #()
{{ ff,
(∀ n : Z, {{ True }} Fst ff #n {{ w, ⌜w = #true⌠∨ ⌜w = #false⌠}}) ∗
{{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
@@ -108,7 +108,7 @@ Definition client : expr :=
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
- Lemma client_safe : WP client {{ _, True }}%I.
+ Lemma client_safe : ⊢ WP client {{ _, True }}.
Proof using Type*.
rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2) "[#Hf1 #Hf2]".
wp_let. wp_apply wp_par.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 6ad376e9e..f11b93903 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -105,7 +105,7 @@ Proof.
Qed.
Lemma ht_one_shot (Φ : val → iProp Σ) :
- {{ True }} one_shot_example #()
+ ⊢ {{ True }} one_shot_example #()
{{ ff, ∃ T, T ∗
(∀ n : Z, {{ T }} Fst ff #n {{ _, True }}) ∗
{{ True }} Snd ff #() {{ g, {{ True }} g #() {{ _, True }} }}
@@ -126,7 +126,7 @@ Definition client : expr :=
Section client.
Context `{!heapG Σ, !one_shotG Σ, !spawnG Σ}.
- Lemma client_safe : WP client {{ _, True }}%I.
+ Lemma client_safe : ⊢ WP client {{ _, True }}.
Proof using Type*.
rewrite /client. wp_apply wp_one_shot. iIntros (f1 f2 T) "(HT & #Hf1 & #Hf2)".
wp_let. wp_apply (wp_par with "[HT]").
diff --git a/tests/proofmode.v b/tests/proofmode.v
index eaf0b0b93..d5782bd97 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -8,10 +8,10 @@ Implicit Types P Q R : PROP.
Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
Proof. eauto 6. Qed.
-Lemma test_eauto_isplit_biwand P : (P ∗-∗ P)%I.
+Lemma test_eauto_isplit_biwand P : ⊢ P ∗-∗ P.
Proof. eauto. Qed.
-Fixpoint test_fixpoint (n : nat) {struct n} : True → emp ⊢@{PROP} ⌜ (n + 0)%nat = n âŒ%I.
+Fixpoint test_fixpoint (n : nat) {struct n} : True → emp ⊢@{PROP} ⌜ (n + 0)%nat = n âŒ.
Proof.
case: n => [|n] /=; first (iIntros (_) "_ !%"; reflexivity).
iIntros (_) "_".
@@ -53,7 +53,7 @@ Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
Definition foo (P : PROP) := (P -∗ P)%I.
Definition bar : PROP := (∀ P, foo P)%I.
-Lemma test_unfold_constants : bar.
+Lemma test_unfold_constants : ⊢ bar.
Proof. iIntros (P) "HP //". Qed.
Check "test_iStopProof".
@@ -74,7 +74,7 @@ Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
P ∧ emp -∗ emp ∧ Q -∗ <affine> (P ∗ Q).
Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
-Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∧ Q)%I.
+Lemma test_iIntros_persistent P Q `{!Persistent Q} : ⊢ (P → Q → P ∧ Q).
Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
Lemma test_iDestruct_intuitionistic_1 P Q `{!Persistent P}:
@@ -104,15 +104,15 @@ Qed.
Lemma test_iDestruct_spatial_noop Q : Q -∗ Q.
Proof. iIntros "-#HQ". done. Qed.
-Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌠→ P → ⌜ φ ∧ ψ ⌠∧ P)%I.
+Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → ⊢ ⌜ φ ⌠→ P → ⌜ φ ∧ ψ ⌠∧ P.
Proof. iIntros (??) "H". auto. Qed.
-Lemma test_iIntros_pure_not : (⌜ ¬False ⌠: PROP)%I.
+Lemma test_iIntros_pure_not : ⊢@{PROP} ⌜ ¬False âŒ.
Proof. by iIntros (?). Qed.
Lemma test_fast_iIntros P Q :
- (∀ x y z : nat,
- ⌜x = plus 0 x⌠→ ⌜y = 0⌠→ ⌜z = 0⌠→ P → □ Q → foo (x ≡ x))%I.
+ ⊢ ∀ x y z : nat,
+ ⌜x = plus 0 x⌠→ ⌜y = 0⌠→ ⌜z = 0⌠→ P → □ Q → foo (x ≡ x).
Proof.
iIntros (a) "*".
iIntros "#Hfoo **".
@@ -120,11 +120,11 @@ Proof.
Qed.
Lemma test_very_fast_iIntros P :
- ∀ x y : nat, (⌜ x = y ⌠→ P -∗ P)%I.
+ ∀ x y : nat, ⊢ ⌜ x = y ⌠→ P -∗ P.
Proof. by iIntros. Qed.
Definition tc_opaque_test : PROP := tc_opaque (∀ x : nat, ⌜ x = x âŒ)%I.
-Lemma test_iIntros_tc_opaque : tc_opaque_test.
+Lemma test_iIntros_tc_opaque : ⊢ tc_opaque_test.
Proof. by iIntros (x). Qed.
(** Prior to 0b84351c this used to loop, now `iAssumption` instantiates `R` with
@@ -163,12 +163,12 @@ Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
-Lemma test_iSpecialize_pure (φ : Prop) Q R:
- φ → (⌜φ⌠-∗ Q) → Q.
+Lemma test_iSpecialize_pure (φ : Prop) Q R :
+ φ → (⌜φ⌠-∗ Q) → ⊢ Q.
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
Lemma test_iSpecialize_Coq_entailment P Q R :
- P → (P -∗ Q) → Q.
+ (⊢ P) → (P -∗ Q) → (⊢ Q).
Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
Lemma test_iSpecialize_intuitionistic P Q R :
@@ -271,7 +271,7 @@ Qed.
Lemma test_iExist_coercion (P : Z → PROP) : (∀ x, P x) -∗ ∃ x, P x.
Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
-Lemma test_iExist_tc `{Set_ A C} P : (∃ x1 x2 : gset positive, P -∗ P)%I.
+Lemma test_iExist_tc `{Set_ A C} P : ⊢ ∃ x1 x2 : gset positive, P -∗ P.
Proof. iExists {[ 1%positive ]}, ∅. auto. Qed.
Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P.
@@ -384,7 +384,7 @@ Proof.
iIntros "#H HP". iDestruct ("H" with "HP") as (x) "#H2". eauto with iFrame.
Qed.
-Lemma test_iLöb P : (∃ n, ▷^n P)%I.
+Lemma test_iLöb P : ⊢ ∃ n, ▷^n P.
Proof.
iLöb as "IH". iDestruct "IH" as (n) "IH".
by iExists (S n).
@@ -408,7 +408,7 @@ Proof.
Qed.
Lemma test_iIntros_start_proof :
- (True : PROP)%I.
+ ⊢@{PROP} True.
Proof.
(* Make sure iIntros actually makes progress and enters the proofmode. *)
progress iIntros. done.
@@ -437,7 +437,7 @@ Proof.
Qed.
Lemma test_iIntros_modalities `(!Absorbing P) :
- (<pers> (▷ ∀ x : nat, ⌜ x = 0 ⌠→ ⌜ x = 0 ⌠-∗ False -∗ P -∗ P))%I.
+ ⊢ <pers> (▷ ∀ x : nat, ⌜ x = 0 ⌠→ ⌜ x = 0 ⌠-∗ False -∗ P -∗ P).
Proof.
iIntros (x ??).
iIntros "* **". (* Test that fast intros do not work under modalities *)
@@ -613,11 +613,11 @@ Check "test_iSimpl_in4".
Lemma test_iSimpl_in4 x y : ⌜ (3 + x)%nat = y ⌠-∗ ⌜ S (S (S x)) = y ⌠: PROP.
Proof. iIntros "H". Fail iSimpl in "%". by iSimpl in "H". Qed.
-Lemma test_iIntros_pure_neg : (⌜ ¬False ⌠: PROP)%I.
+Lemma test_iIntros_pure_neg : ⊢@{PROP} ⌜ ¬False âŒ.
Proof. by iIntros (?). Qed.
Lemma test_iPureIntro_absorbing (φ : Prop) :
- φ → sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φâŒ)%I.
+ φ → ⊢@{PROP} <absorb> ⌜φâŒ.
Proof. intros ?. iPureIntro. done. Qed.
Check "test_iFrame_later_1".
@@ -829,25 +829,25 @@ Abort.
Check "long_impl".
Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
- (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
+ ⊢ PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ).
Proof.
iStartProof. Show.
Abort.
Check "long_impl_nested".
Lemma long_impl_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
- (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
+ ⊢ PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ).
Proof.
iStartProof. Show.
Abort.
Check "long_wand".
Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
- (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
+ ⊢ PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ).
Proof.
iStartProof. Show.
Abort.
Check "long_wand_nested".
Lemma long_wand_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
- (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
+ ⊢ PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ).
Proof.
iStartProof. Show.
Abort.
@@ -911,14 +911,14 @@ Abort.
Check "iSplitL_non_splittable".
Lemma iSplitL_non_splittable P :
- P.
+ ⊢ P.
Proof.
Fail iSplitL "".
Abort.
Check "iSplitR_non_splittable".
Lemma iSplitR_non_splittable P :
- P.
+ ⊢ P.
Proof.
Fail iSplitR "".
Abort.
@@ -1022,18 +1022,18 @@ Lemma iApply_fail_not_affine_1 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q.
Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort.
Check "iRevert_wrong_var".
-Lemma iRevert_wrong_var (k : nat) (Φ : nat → PROP) : Φ (S k).
+Lemma iRevert_wrong_var (k : nat) (Φ : nat → PROP) : ⊢ Φ (S k).
Proof.
Fail iRevert (k1).
Fail iLöb as "IH" forall (k1).
Abort.
Check "iRevert_dup_var".
-Lemma iRevert_dup_var (k : nat) (Φ : nat → PROP) : Φ (S k).
+Lemma iRevert_dup_var (k : nat) (Φ : nat → PROP) : ⊢ Φ (S k).
Proof. Fail iRevert (k k). Abort.
Check "iRevert_dep_var_coq".
-Lemma iRevert_dep_var_coq (k : nat) (Φ : nat → PROP) : k = 0 → Φ (S k).
+Lemma iRevert_dep_var_coq (k : nat) (Φ : nat → PROP) : k = 0 → ⊢ Φ (S k).
Proof. intros Hk. Fail iRevert (k). Abort.
Check "iRevert_dep_var".
@@ -1046,6 +1046,6 @@ Context {PROP : bi}.
Implicit Types P Q R : PROP.
Check "iLöb_no_sbi".
-Lemma iLöb_no_sbi P : P.
+Lemma iLöb_no_sbi P : ⊢ P.
Proof. Fail iLöb as "IH". Abort.
End error_tests_bi.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 3392c95df..74630ab6f 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -7,13 +7,13 @@ Section base_logic_tests.
Implicit Types P Q R : uPred M.
Lemma test_random_stuff (P1 P2 P3 : nat → uPred M) :
- (∀ (x y : nat) a b,
+ ⊢ ∀ (x y : nat) a b,
x ≡ y →
□ (uPred_ownM (a ⋅ b) -∗
(∃ y1 y2 c, P1 ((x + y1) + y2) ∧ True ∧ □ uPred_ownM c) -∗
□ ▷ (∀ z, P2 z ∨ True → P2 z) -∗
▷ (∀ n m : nat, P1 n → □ ((True ∧ P2 n) → □ (⌜n = n⌠↔ P3 n))) -∗
- ▷ ⌜x = 0⌠∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)))%I.
+ ▷ ⌜x = 0⌠∨ ∃ x z, ▷ P3 (x + z) ∗ uPred_ownM b ∗ uPred_ownM (core b)).
Proof.
iIntros (i [|j] a b ?) "!> [Ha Hb] H1 #H2 H3"; setoid_subst.
{ iLeft. by iNext. }
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index a1b445dbb..8f46f5ced 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -26,7 +26,7 @@ Section tests.
Proof. iStartProof PROP. iIntros (i) "$". Qed.
Lemma test_iStartProof_6 P : P ⊣⊢ P.
Proof. iStartProof PROP. iIntros (i). iSplit; iIntros "$". Qed.
- Lemma test_iStartProof_7 P : ((P ≡ P)%I : monPredI).
+ Lemma test_iStartProof_7 P : ⊢@{monPredI} P ≡ P.
Proof. iStartProof PROP. done. Qed.
Lemma test_intowand_1 P Q : (P -∗ Q) -∗ P -∗ Q.
diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v
index 61d894ea4..1788f69c4 100644
--- a/tests/proofmode_siprop.v
+++ b/tests/proofmode_siprop.v
@@ -10,12 +10,12 @@ Section si_logic_tests.
Lemma test_everything_affine P : P -∗ True.
Proof. by iIntros "_". Qed.
- Lemma test_iIntro_impl P Q R : (P → Q ∧ R → P ∧ R)%I.
+ Lemma test_iIntro_impl P Q R : ⊢ P → Q ∧ R → P ∧ R.
Proof. iIntros "#HP #[HQ HR]". auto. Qed.
- Lemma test_iApply_impl_1 P Q R : (P → (P → Q) → Q)%I.
+ Lemma test_iApply_impl_1 P Q R : ⊢ P → (P → Q) → Q.
Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.
- Lemma test_iApply_impl_2 P Q R : (P → (P → Q) → Q)%I.
+ Lemma test_iApply_impl_2 P Q R : ⊢ P → (P → Q) → Q.
Proof. iIntros "#HP #HPQ". by iApply "HPQ". Qed.
End si_logic_tests.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index f7971a8a9..df9d498f1 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -98,8 +98,6 @@ Canonical Structure uPredSI (M : ucmraT) : sbi :=
{| sbi_ofe_mixin := ofe_mixin_of (uPred M);
sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
-Coercion uPred_valid {M} : uPred M → Prop := bi_emp_valid.
-
Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
Proof.
split.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index ff82d926f..e300eb8e5 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -18,14 +18,6 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
(** Propers *)
-Global Instance uPred_valid_proper : Proper ((⊣⊢) ==> iff) (@uPred_valid M).
-Proof. solve_proper. Qed.
-Global Instance uPred_valid_mono : Proper ((⊢) ==> impl) (@uPred_valid M).
-Proof. solve_proper. Qed.
-Global Instance uPred_valid_flip_mono :
- Proper (flip (⊢) ==> flip impl) (@uPred_valid M).
-Proof. solve_proper. Qed.
-
Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
Global Instance cmra_valid_proper {A : cmraT} :
Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
@@ -98,17 +90,17 @@ Proof.
apply: plain.
Qed.
-Corollary soundness φ n : (▷^n ⌜ φ ⌠: uPred M)%I → φ.
+Corollary soundness φ n : (⊢@{uPredI M} â–·^n ⌜ φ âŒ) → φ.
Proof.
induction n as [|n IH]=> /=.
- apply pure_soundness.
- intros H. by apply IH, later_soundness.
Qed.
-Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
+Corollary consistency_modal n : ¬ ⊢@{uPredI M} ▷^n False.
Proof. exact (soundness False n). Qed.
-Corollary consistency : ¬(False : uPred M)%I.
+Corollary consistency : ¬ ⊢@{uPredI M} False.
Proof. exact (consistency_modal 0). Qed.
End derived.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 9e14b4cb3..fd2f103eb 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -129,7 +129,7 @@ Section auth.
iMod (auth_alloc_cofinite N E t ∅ with "Hφ") as (γ) "[_ ?]"; eauto.
Qed.
- Lemma auth_empty γ : (|==> auth_own γ ε)%I.
+ Lemma auth_empty γ : ⊢ |==> auth_own γ ε.
Proof. by rewrite /auth_own -own_unit. Qed.
Lemma auth_inv_acc E γ a :
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index d247efe8f..a0a9c99ff 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -98,7 +98,7 @@ Proof.
iRewrite "HQ". by rewrite iProp_fold_unfold.
Qed.
-Lemma box_alloc : box N ∅ True%I.
+Lemma box_alloc : ⊢ box N ∅ True.
Proof.
iIntros. iExists (λ _, True)%I. by rewrite !big_opM_empty.
Qed.
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 38f1a16b7..6eb3ef024 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -65,7 +65,7 @@ Section proofs.
until after [γ] was chosen.*)
Lemma cinv_alloc_strong (I : gname → Prop) E N :
pred_infinite I →
- (|={E}=> ∃ γ, ⌜ I γ ⌠∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I.
+ ⊢ |={E}=> ∃ γ, ⌜ I γ ⌠∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P.
Proof.
iIntros (?). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|].
iExists γ. iIntros "!> {$Hγ $Hfresh}" (P) "HP".
@@ -78,8 +78,8 @@ Section proofs.
Lemma cinv_alloc_strong_open (I : gname → Prop) E N :
pred_infinite I →
↑N ⊆ E →
- (|={E}=> ∃ γ, ⌜ I γ ⌠∗ cinv_own γ 1 ∗ ∀ P,
- |={E,E∖↑N}=> cinv N γ P ∗ (▷ P ={E∖↑N,E}=∗ True))%I.
+ ⊢ |={E}=> ∃ γ, ⌜ I γ ⌠∗ cinv_own γ 1 ∗ ∀ P,
+ |={E,E∖↑N}=> cinv N γ P ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
iIntros (??). iMod (own_alloc_strong 1%Qp I) as (γ) "[Hfresh Hγ]"; [done|done|].
iExists γ. iIntros "!> {$Hγ $Hfresh}" (P).
@@ -88,7 +88,7 @@ Section proofs.
Qed.
Lemma cinv_alloc_cofinite (G : gset gname) E N :
- (|={E}=> ∃ γ, ⌜ γ ∉ G ⌠∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P)%I.
+ ⊢ |={E}=> ∃ γ, ⌜ γ ∉ G ⌠∗ cinv_own γ 1 ∗ ∀ P, ▷ P ={E}=∗ cinv N γ P.
Proof.
apply cinv_alloc_strong. apply (pred_infinite_set (C:=gset gname))=> E'.
exists (fresh (G ∪ E')). apply not_elem_of_union, is_fresh.
@@ -101,7 +101,7 @@ Section proofs.
Qed.
Lemma cinv_alloc_open E N P :
- ↑N ⊆ E → (|={E,E∖↑N}=> ∃ γ, cinv N γ P ∗ cinv_own γ 1 ∗ (▷ P ={E∖↑N,E}=∗ True))%I.
+ ↑N ⊆ E → ⊢ |={E,E∖↑N}=> ∃ γ, cinv N γ P ∗ cinv_own γ 1 ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
iIntros (?). iMod (cinv_alloc_strong_open (λ _, True)) as (γ) "(_ & Htok & Hmake)"; [|done|].
{ apply pred_infinite_True. }
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 6db93b131..3be5ca307 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -70,7 +70,7 @@ Proof.
Qed.
Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
- (∀ `{Hinv: !invG Σ}, (|={⊤,∅}▷=>^n |={⊤,∅}=> ⌜ φ ⌠: iProp Σ)%I) →
+ (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}â–·=>^n |={⊤,∅}=> ⌜ φ âŒ) →
φ.
Proof.
intros Hiter.
@@ -88,7 +88,7 @@ Proof.
Qed.
Lemma step_fupdN_soundness' `{!invPreG Σ} φ n :
- (∀ `{Hinv: !invG Σ}, (|={⊤,∅}▷=>^n ⌜ φ ⌠: iProp Σ)%I) →
+ (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤,∅}â–·=>^n ⌜ φ âŒ) →
φ.
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 6a3c44d0b..2292f8d59 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -164,7 +164,7 @@ Section to_gen_heap.
End to_gen_heap.
Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
- (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
+ ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ.
Proof.
iMod (own_alloc (◠to_gen_heap σ)) as (γh) "Hh".
{ rewrite auth_auth_valid. exact: to_gen_heap_valid. }
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index aa807e221..2d13f5937 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -58,7 +58,7 @@ Section inv.
(* This does not imply [own_inv_alloc] due to the extra assumption [↑N ⊆ E]. *)
Lemma own_inv_alloc_open N E P :
- ↑N ⊆ E → (|={E, E∖↑N}=> own_inv N P ∗ (▷P ={E∖↑N, E}=∗ True))%I.
+ ↑N ⊆ E → ⊢ |={E, E∖↑N}=> own_inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
Proof.
rewrite uPred_fupd_eq. iIntros (Sub) "[Hw HE]".
iMod (ownI_alloc_open (.∈ (↑N : coPset)) P with "Hw")
@@ -121,7 +121,7 @@ Section inv.
Qed.
Lemma inv_alloc_open N E P :
- ↑N ⊆ E → (|={E, E∖↑N}=> inv N P ∗ (▷P ={E∖↑N, E}=∗ True))%I.
+ ↑N ⊆ E → ⊢ |={E, E∖↑N}=> inv N P ∗ (▷P ={E∖↑N, E}=∗ True).
Proof.
iIntros (?). iMod own_inv_alloc_open as "[HI $]"; first done.
iApply own_inv_to_inv. done.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 8ce782b03..25c749dad 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -51,7 +51,7 @@ Section proofs.
iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
Qed.
- Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
+ Lemma na_alloc : ⊢ |==> ∃ p, na_own p ⊤.
Proof. by apply own_alloc. Qed.
Lemma na_own_disjoint p E1 E2 : na_own p E1 -∗ na_own p E2 -∗ ⌜E1 ## E2âŒ.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 80fa6b5bc..ae3d91ff5 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -149,11 +149,11 @@ Qed.
Lemma own_alloc_strong_dep (f : gname → A) (P : gname → Prop) :
pred_infinite P →
(∀ γ, P γ → ✓ (f γ)) →
- (|==> ∃ γ, ⌜P γ⌠∧ own γ (f γ))%I.
+ ⊢ |==> ∃ γ, ⌜P γ⌠∧ own γ (f γ).
Proof.
intros HP Ha.
rewrite -(bupd_mono (∃ m, ⌜∃ γ, P γ ∧ m = iRes_singleton γ (f γ)⌠∧ uPred_ownM m)%I).
- - rewrite /uPred_valid /bi_emp_valid (ownM_unit emp).
+ - rewrite /bi_emp_valid (ownM_unit emp).
eapply bupd_ownM_updateP, (discrete_fun_singleton_updateP_empty (inG_id Hin)).
+ eapply alloc_updateP_strong_dep'; first done.
intros i _ ?. eapply cmra_transport_valid, Ha. done.
@@ -162,7 +162,7 @@ Proof.
by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
Qed.
Lemma own_alloc_cofinite_dep (f : gname → A) (G : gset gname) :
- (∀ γ, γ ∉ G → ✓ (f γ)) → (|==> ∃ γ, ⌜γ ∉ G⌠∧ own γ (f γ))%I.
+ (∀ γ, γ ∉ G → ✓ (f γ)) → ⊢ |==> ∃ γ, ⌜γ ∉ G⌠∧ own γ (f γ).
Proof.
intros Ha.
apply (own_alloc_strong_dep f (λ γ, γ ∉ G))=> //.
@@ -171,20 +171,20 @@ Proof.
exists i. apply not_elem_of_union, is_fresh.
Qed.
Lemma own_alloc_dep (f : gname → A) :
- (∀ γ, ✓ (f γ)) → (|==> ∃ γ, own γ (f γ))%I.
+ (∀ γ, ✓ (f γ)) → ⊢ |==> ∃ γ, own γ (f γ).
Proof.
- intros Ha. rewrite /uPred_valid /bi_emp_valid (own_alloc_cofinite_dep f ∅) //; [].
+ intros Ha. rewrite /bi_emp_valid (own_alloc_cofinite_dep f ∅) //; [].
apply bupd_mono, exist_mono=>?. eauto using and_elim_r.
Qed.
Lemma own_alloc_strong a (P : gname → Prop) :
pred_infinite P →
- ✓ a → (|==> ∃ γ, ⌜P γ⌠∧ own γ a)%I.
+ ✓ a → ⊢ |==> ∃ γ, ⌜P γ⌠∧ own γ a.
Proof. intros HP Ha. eapply own_alloc_strong_dep with (f := λ _, a); eauto. Qed.
Lemma own_alloc_cofinite a (G : gset gname) :
- ✓ a → (|==> ∃ γ, ⌜γ ∉ G⌠∧ own γ a)%I.
+ ✓ a → ⊢ |==> ∃ γ, ⌜γ ∉ G⌠∧ own γ a.
Proof. intros Ha. eapply own_alloc_cofinite_dep with (f := λ _, a); eauto. Qed.
-Lemma own_alloc a : ✓ a → (|==> ∃ γ, own γ a)%I.
+Lemma own_alloc a : ✓ a → ⊢ |==> ∃ γ, own γ a.
Proof. intros Ha. eapply own_alloc_dep with (f := λ _, a); eauto. Qed.
(** ** Frame preserving updates *)
@@ -222,9 +222,9 @@ Arguments own_update {_ _} [_] _ _ _ _.
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
-Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : (|==> own γ (ε:A))%I.
+Lemma own_unit A `{!inG Σ (A:ucmraT)} γ : ⊢ |==> own γ (ε:A).
Proof.
- rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
+ rewrite /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
apply bupd_ownM_update, discrete_fun_singleton_update_empty.
apply (alloc_unit_singleton_update (cmra_transport inG_prf ε)); last done.
- apply cmra_transport_valid, ucmra_unit_valid.
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index 4891e0b9e..b22092767 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -108,7 +108,7 @@ Section to_proph_map.
End to_proph_map.
Lemma proph_map_init `{Countable P, !proph_mapPreG P V PVS} pvs ps :
- (|==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps)%I.
+ ⊢ |==> ∃ _ : proph_mapG P V PVS, proph_map_ctx pvs ps.
Proof.
iMod (own_alloc (◠to_proph_map ∅)) as (γ) "Hh".
{ rewrite auth_auth_valid. exact: to_proph_map_valid. }
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 8e1a9e59a..3ba56d398 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -41,14 +41,14 @@ Section saved_anything.
Lemma saved_anything_alloc_strong x (I : gname → Prop) :
pred_infinite I →
- (|==> ∃ γ, ⌜I γ⌠∧ saved_anything_own γ x)%I.
+ ⊢ |==> ∃ γ, ⌜I γ⌠∧ saved_anything_own γ x.
Proof. intros ?. by apply own_alloc_strong. Qed.
Lemma saved_anything_alloc_cofinite x (G : gset gname) :
- (|==> ∃ γ, ⌜γ ∉ G⌠∧ saved_anything_own γ x)%I.
+ ⊢ |==> ∃ γ, ⌜γ ∉ G⌠∧ saved_anything_own γ x.
Proof. by apply own_alloc_cofinite. Qed.
- Lemma saved_anything_alloc x : (|==> ∃ γ, saved_anything_own γ x)%I.
+ Lemma saved_anything_alloc x : ⊢ |==> ∃ γ, saved_anything_own γ x.
Proof. by apply own_alloc. Qed.
Lemma saved_anything_agree γ x y :
@@ -81,15 +81,15 @@ Proof. solve_contractive. Qed.
Lemma saved_prop_alloc_strong `{!savedPropG Σ} (I : gname → Prop) (P: iProp Σ) :
pred_infinite I →
- (|==> ∃ γ, ⌜I γ⌠∧ saved_prop_own γ P)%I.
+ ⊢ |==> ∃ γ, ⌜I γ⌠∧ saved_prop_own γ P.
Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
Lemma saved_prop_alloc_cofinite `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
- (|==> ∃ γ, ⌜γ ∉ G⌠∧ saved_prop_own γ P)%I.
+ ⊢ |==> ∃ γ, ⌜γ ∉ G⌠∧ saved_prop_own γ P.
Proof. iApply saved_anything_alloc_cofinite. Qed.
Lemma saved_prop_alloc `{!savedPropG Σ} (P: iProp Σ) :
- (|==> ∃ γ, saved_prop_own γ P)%I.
+ ⊢ |==> ∃ γ, saved_prop_own γ P.
Proof. iApply saved_anything_alloc. Qed.
Lemma saved_prop_agree `{!savedPropG Σ} γ P Q :
@@ -114,15 +114,15 @@ Qed.
Lemma saved_pred_alloc_strong `{!savedPredG Σ A} (I : gname → Prop) (Φ : A → iProp Σ) :
pred_infinite I →
- (|==> ∃ γ, ⌜I γ⌠∧ saved_pred_own γ Φ)%I.
+ ⊢ |==> ∃ γ, ⌜I γ⌠∧ saved_pred_own γ Φ.
Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
Lemma saved_pred_alloc_cofinite `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
- (|==> ∃ γ, ⌜γ ∉ G⌠∧ saved_pred_own γ Φ)%I.
+ ⊢ |==> ∃ γ, ⌜γ ∉ G⌠∧ saved_pred_own γ Φ.
Proof. iApply saved_anything_alloc_cofinite. Qed.
Lemma saved_pred_alloc `{!savedPredG Σ A} (Φ : A → iProp Σ) :
- (|==> ∃ γ, saved_pred_own γ Φ)%I.
+ ⊢ |==> ∃ γ, saved_pred_own γ Φ.
Proof. iApply saved_anything_alloc. Qed.
(* We put the `x` on the outside to make this lemma easier to apply. *)
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 531638941..6e367b79e 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -39,9 +39,9 @@ Proof. by intros HP HQ; rewrite /vs -HP HQ. Qed.
Global Instance vs_mono' E1 E2 : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (vs E1 E2).
Proof. solve_proper. Qed.
-Lemma vs_false_elim E1 E2 P : False ={E1,E2}=> P.
+Lemma vs_false_elim E1 E2 P : ⊢ False ={E1,E2}=> P.
Proof. iIntros "!> []". Qed.
-Lemma vs_timeless E P : Timeless P → ▷ P ={E}=> P.
+Lemma vs_timeless E P : Timeless P → ⊢ ▷ P ={E}=> P.
Proof. by iIntros (?) "!> > ?". Qed.
Lemma vs_transitive E1 E2 E3 P Q R :
@@ -51,7 +51,7 @@ Proof.
iMod ("HvsP" with "HP") as "HQ". by iApply "HvsQ".
Qed.
-Lemma vs_reflexive E P : P ={E}=> P.
+Lemma vs_reflexive E P : ⊢ P ={E}=> P.
Proof. by iIntros "!> HP". Qed.
Lemma vs_impl E P Q : □ (P → Q) ⊢ P ={E}=> Q.
@@ -77,7 +77,7 @@ Proof.
by iApply "Hclose".
Qed.
-Lemma vs_alloc N P : ▷ P ={↑N}=> inv N P.
+Lemma vs_alloc N P : ⊢ ▷ P ={↑N}=> inv N P.
Proof. iIntros "!> HP". by iApply inv_alloc. Qed.
Lemma wand_fupd_alt E1 E2 P Q : (P ={E1,E2}=∗ Q) ⊣⊢ ∃ R, R ∗ (P ∗ R ={E1,E2}=> Q).
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index e63dbd9c1..0cc14c031 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -69,9 +69,9 @@ Proof. solve_contractive. Qed.
Global Instance ownI_persistent i P : Persistent (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
-Lemma ownE_empty : (|==> ownE ∅)%I.
+Lemma ownE_empty : ⊢ |==> ownE ∅.
Proof.
- rewrite /uPred_valid /bi_emp_valid.
+ rewrite /bi_emp_valid.
by rewrite (own_unit (coPset_disjUR) enabled_name).
Qed.
Lemma ownE_op E1 E2 : E1 ## E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
@@ -87,9 +87,9 @@ Qed.
Lemma ownE_singleton_twice i : ownE {[i]} ∗ ownE {[i]} ⊢ False.
Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
-Lemma ownD_empty : (|==> ownD ∅)%I.
+Lemma ownD_empty : ⊢ |==> ownD ∅.
Proof.
- rewrite /uPred_valid /bi_emp_valid.
+ rewrite /bi_emp_valid.
by rewrite (own_unit (gset_disjUR positive) disabled_name).
Qed.
Lemma ownD_op E1 E2 : E1 ## E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ∗ ownD E2.
@@ -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 ⊤.
Proof.
iIntros.
iMod (own_alloc (◠(∅ : gmap positive _))) as (γI) "HI";
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 215778047..8ce55d3ab 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -352,13 +352,13 @@ Proof. rewrite -{1}[P](left_id emp%I bi_sep). auto using sep_mono. Qed.
Lemma sep_True_2 P : P ⊢ P ∗ True.
Proof. by rewrite comm -True_sep_2. Qed.
-Lemma sep_intro_emp_valid_l P Q R : P → (R ⊢ Q) → R ⊢ P ∗ Q.
+Lemma sep_intro_emp_valid_l P Q R : (⊢ P) → (R ⊢ Q) → R ⊢ P ∗ Q.
Proof. intros ? ->. rewrite -{1}(left_id emp%I _ Q). by apply sep_mono. Qed.
-Lemma sep_intro_emp_valid_r P Q R : (R ⊢ P) → Q → R ⊢ P ∗ Q.
+Lemma sep_intro_emp_valid_r P Q R : (R ⊢ P) → (⊢ Q) → R ⊢ P ∗ Q.
Proof. intros -> ?. rewrite comm. by apply sep_intro_emp_valid_l. Qed.
-Lemma sep_elim_emp_valid_l P Q R : P → (P ∗ R ⊢ Q) → R ⊢ Q.
+Lemma sep_elim_emp_valid_l P Q R : (⊢ P) → (P ∗ R ⊢ Q) → R ⊢ Q.
Proof. intros <- <-. by rewrite left_id. Qed.
-Lemma sep_elim_emp_valid_r P Q R : P → (R ∗ P ⊢ Q) → R ⊢ Q.
+Lemma sep_elim_emp_valid_r P Q R : (⊢P) → (R ∗ P ⊢ Q) → R ⊢ Q.
Proof. intros <- <-. by rewrite right_id. Qed.
Lemma wand_intro_l P Q R : (Q ∗ P ⊢ R) → P ⊢ Q -∗ R.
@@ -435,30 +435,30 @@ Global Instance wand_iff_proper :
Lemma wand_iff_refl P : emp ⊢ P ∗-∗ P.
Proof. apply and_intro; apply wand_intro_l; by rewrite right_id. Qed.
-Lemma wand_entails P Q : (P -∗ Q)%I → P ⊢ Q.
+Lemma wand_entails P Q : (⊢ P -∗ Q) → P ⊢ Q.
Proof. intros. rewrite -[P]emp_sep. by apply wand_elim_l'. Qed.
-Lemma entails_wand P Q : (P ⊢ Q) → (P -∗ Q)%I.
+Lemma entails_wand P Q : (P ⊢ Q) → ⊢ P -∗ Q.
Proof. intros ->. apply wand_intro_r. by rewrite left_id. Qed.
(* A version that works with rewrite, in which bi_emp_valid is unfolded. *)
Lemma entails_wand' P Q : (P ⊢ Q) → emp ⊢ (P -∗ Q).
Proof. apply entails_wand. Qed.
-Lemma equiv_wand_iff P Q : (P ⊣⊢ Q) → (P ∗-∗ Q)%I.
+Lemma equiv_wand_iff P Q : (P ⊣⊢ Q) → ⊢ P ∗-∗ Q.
Proof. intros ->; apply wand_iff_refl. Qed.
-Lemma wand_iff_equiv P Q : (P ∗-∗ Q)%I → (P ⊣⊢ Q).
+Lemma wand_iff_equiv P Q : (⊢ P ∗-∗ Q) → (P ⊣⊢ Q).
Proof.
intros HPQ; apply (anti_symm (⊢));
apply wand_entails; rewrite /bi_emp_valid HPQ /bi_wand_iff; auto.
Qed.
-Lemma entails_impl P Q : (P ⊢ Q) → (P → Q)%I.
+Lemma entails_impl P Q : (P ⊢ Q) → (⊢ P → Q).
Proof. intros ->. apply impl_intro_l. auto. Qed.
-Lemma impl_entails P Q `{!Affine P} : (P → Q)%I → P ⊢ Q.
+Lemma impl_entails P Q `{!Affine P} : (⊢ P → Q) → P ⊢ Q.
Proof. intros HPQ. apply impl_elim with P=>//. by rewrite {1}(affine P). Qed.
-Lemma equiv_iff P Q : (P ⊣⊢ Q) → (P ↔ Q)%I.
+Lemma equiv_iff P Q : (P ⊣⊢ Q) → (⊢ P ↔ Q).
Proof. intros ->; apply iff_refl. Qed.
-Lemma iff_equiv P Q `{!Affine P, !Affine Q} : (P ↔ Q)%I → (P ⊣⊢ Q).
+Lemma iff_equiv P Q `{!Affine P, !Affine Q} : (⊢ P ↔ Q)%I → (P ⊣⊢ Q).
Proof.
intros HPQ; apply (anti_symm (⊢));
apply: impl_entails; rewrite /bi_emp_valid HPQ /bi_iff; auto.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index cd9fe751c..3eaa91784 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -84,7 +84,7 @@ Section embed_laws.
Proof. eapply bi_embed_mixin_ne, bi_embed_mixin. Qed.
Global Instance embed_mono : Proper ((⊢) ==> (⊢)) embed.
Proof. eapply bi_embed_mixin_mono, bi_embed_mixin. Qed.
- Lemma embed_emp_valid_inj P : (⎡P⎤ : PROP2)%I → P.
+ Lemma embed_emp_valid_inj P : (⊢@{PROP2} ⎡P⎤) → ⊢ P.
Proof. eapply bi_embed_mixin_emp_valid_inj, bi_embed_mixin. Qed.
Lemma embed_emp_2 : emp ⊢ ⎡emp⎤.
Proof. eapply bi_embed_mixin_emp_2, bi_embed_mixin. Qed.
@@ -123,7 +123,7 @@ Section embed.
intros P Q EQ. apply bi.equiv_spec, conj; apply (inj embed); rewrite EQ //.
Qed.
- Lemma embed_emp_valid (P : PROP1) : ⎡P⎤%I ↔ P.
+ Lemma embed_emp_valid (P : PROP1) : (⊢ ⎡P⎤) ↔ (⊢ P).
Proof.
rewrite /bi_emp_valid. split=> HP.
- by apply embed_emp_valid_inj.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index fd09f4c2f..1d0895ae6 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -292,12 +292,14 @@ Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
Infix "≡" := sbi_internal_eq : bi_scope.
Notation "â–· P" := (sbi_later P) : bi_scope.
-Coercion bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P.
-Coercion sbi_emp_valid {PROP : sbi} : PROP → Prop := bi_emp_valid.
+Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P.
Arguments bi_emp_valid {_} _%I : simpl never.
Typeclasses Opaque bi_emp_valid.
+Notation "⊢ Q" := (bi_emp_valid Q%I) : stdpp_scope.
+Notation "'⊢@{' PROP } Q" := (bi_emp_valid (PROP:=PROP) Q%I) (only parsing) : stdpp_scope.
+
Module bi.
Section bi_laws.
Context {PROP : bi}.
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 638287c9b..318f4fbab 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -306,9 +306,9 @@ Section lemmas.
Qed.
Lemma aacc_intro Eo Ei α P β Φ :
- Ei ⊆ Eo → (∀.. x, α x -∗
+ Ei ⊆ Eo → ⊢ (∀.. x, α x -∗
((α x ={Eo}=∗ P) ∧ (∀.. y, β x y ={Eo}=∗ Φ x y)) -∗
- atomic_acc Eo Ei α P β Φ)%I.
+ atomic_acc Eo Ei α P β Φ).
Proof.
iIntros (? x) "Hα Hclose".
iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first set_solver.
diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index ed3d464e9..1399d5fc1 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -21,11 +21,11 @@ Module savedprop. Section savedprop.
Context (ident : Type) (saved : ident → PROP → PROP).
Hypothesis sprop_persistent : ∀ i P, Persistent (saved i P).
Hypothesis sprop_alloc_dep :
- ∀ (P : ident → PROP), (|==> ∃ i, saved i (P i))%I.
+ ∀ (P : ident → PROP), ⊢ (|==> ∃ i, saved i (P i)).
Hypothesis sprop_agree : ∀ i P Q, saved i P ∧ saved i Q ⊢ □ (P ↔ Q).
(** We assume that we cannot update to false. *)
- Hypothesis consistency : ¬(|==> False)%I.
+ Hypothesis consistency : ¬(⊢ |==> False).
Instance bupd_mono' : Proper ((⊢) ==> (⊢)) bupd.
Proof. intros P Q ?. by apply bupd_mono. Qed.
@@ -38,7 +38,7 @@ Module savedprop. Section savedprop.
(** A bad recursive reference: "Assertion with name [i] does not hold" *)
Definition A (i : ident) : PROP := (∃ P, ¬ P ∗ saved i P)%I.
- Lemma A_alloc : (|==> ∃ i, saved i (A i))%I.
+ Lemma A_alloc : ⊢ |==> ∃ i, saved i (A i).
Proof. by apply sprop_alloc_dep. Qed.
Lemma saved_NA i : saved i (A i) ⊢ ¬ A i.
@@ -102,7 +102,7 @@ Module inv. Section inv.
Context (gname : Type).
Context (start finished : gname → PROP).
- Hypothesis sts_alloc : fupd M0 (∃ γ, start γ).
+ Hypothesis sts_alloc : ⊢ fupd M0 (∃ γ, start γ).
Hypotheses start_finish : ∀ γ, start γ ⊢ fupd M0 (finished γ).
Hypothesis finished_not_start : ∀ γ, start γ ∗ finished γ ⊢ False.
@@ -110,7 +110,7 @@ Module inv. Section inv.
Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ∗ finished γ.
(** We assume that we cannot update to false. *)
- Hypothesis consistency : ¬ (fupd M1 False).
+ Hypothesis consistency : ¬ (⊢ fupd M1 False).
(** Some general lemmas and proof mode compatibility. *)
Lemma inv_fupd' i P R : inv i P ∗ (P -∗ fupd M0 (P ∗ fupd M1 R)) ⊢ fupd M1 R.
@@ -156,7 +156,7 @@ Module inv. Section inv.
(∃ i, inv i (start γ ∨ (finished γ ∗ □ P)))%I.
Global Instance saved_persistent γ P : Persistent (saved γ P) := _.
- Lemma saved_alloc (P : gname → PROP) : fupd M1 (∃ γ, 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".
@@ -189,7 +189,7 @@ Module inv. Section inv.
Definition A i : PROP := (∃ P, ¬P ∗ saved i P)%I.
Global Instance A_persistent i : Persistent (A i) := _.
- Lemma A_alloc : fupd M1 (∃ i, saved i (A i)).
+ Lemma A_alloc : ⊢ fupd M1 (∃ i, saved i (A i)).
Proof. by apply saved_alloc. Qed.
Lemma saved_NA i : saved i (A i) ⊢ ¬A i.
@@ -239,7 +239,7 @@ Module linear1. Section linear1.
the [mask] type, but we do not need that either.) *)
Context (gname : Type) (cinv : gname → PROP → PROP) (cinv_own : gname → PROP).
Hypothesis cinv_alloc_open : ∀ P,
- (fupd M1 M0 (∃ γ, cinv γ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)))%I.
+ ⊢ fupd M1 M0 (∃ γ, cinv γ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)).
(** Some general lemmas and proof mode compatibility. *)
Instance fupd_mono' E1 E2 : Proper ((⊢) ==> (⊢)) (fupd E1 E2).
@@ -307,7 +307,7 @@ Module linear2. Section linear2.
the [mask] type, but we do not need that either.) *)
Context (gname : Type) (cinv : gname → PROP → PROP) (cinv_own : gname → PROP).
Hypothesis cinv_alloc : ∀ E,
- fupd E E (∃ γ, ∀ P, ▷ P -∗ fupd E E (cinv γ P ∗ cinv_own γ))%I.
+ ⊢ fupd E E (∃ γ, ∀ P, ▷ P -∗ fupd E E (cinv γ P ∗ cinv_own γ)).
Hypothesis cinv_acc : ∀ P γ,
cinv γ P -∗ cinv_own γ -∗ fupd M1 M0 (▷ P ∗ cinv_own γ ∗ (▷ P -∗ fupd M0 M1 emp)).
diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index 3dc7fd525..196d32b1d 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -6,7 +6,7 @@ Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *)
Class BiMonoPred {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) := {
- bi_mono_pred Φ Ψ : (<pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I;
+ bi_mono_pred Φ Ψ : ⊢ <pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x;
bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
}.
Arguments bi_mono_pred {_ _ _ _} _ _.
diff --git a/theories/bi/lib/relations.v b/theories/bi/lib/relations.v
index fcea297c9..924a9908c 100644
--- a/theories/bi/lib/relations.v
+++ b/theories/bi/lib/relations.v
@@ -67,7 +67,7 @@ Section bi_rtc.
by iApply (least_fixpoint_ind (bi_rtc_pre R x2) with "IH").
Qed.
- Lemma bi_rtc_refl x : bi_rtc R x x.
+ Lemma bi_rtc_refl x : ⊢ bi_rtc R x x.
Proof. rewrite bi_rtc_unfold. by iLeft. Qed.
Lemma bi_rtc_l x1 x2 x3 : R x1 x2 -∗ bi_rtc R x2 x3 -∗ bi_rtc R x1 x3.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 8b268c974..94a58c036 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -11,6 +11,9 @@ Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
Reserved Notation "(⊣⊢)".
Reserved Notation "('⊣⊢@{' PROP } )".
+Reserved Notation "⊢ Q" (at level 20, Q at level 200).
+Reserved Notation "'⊢@{' PROP } Q" (at level 20, Q at level 200).
+
(** BI connectives *)
Reserved Notation "'emp'".
Reserved Notation "'⌜' φ 'âŒ'" (at level 1, φ at level 200, format "⌜ φ âŒ").
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 1c3ecec3b..949ca07ed 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -225,7 +225,7 @@ Section fupd_derived.
Lemma fupd_intro E P : P ={E}=∗ P.
Proof. by rewrite {1}(fupd_intro_mask E E P) // fupd_trans. Qed.
- Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → (|={E1,E2}=> |={E2,E1}=> bi_emp (PROP:=PROP))%I.
+ Lemma fupd_intro_mask' E1 E2 : E2 ⊆ E1 → ⊢@{PROP} |={E1,E2}=> |={E2,E1}=> emp.
Proof. exact: fupd_intro_mask. Qed.
Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> ◇ P) ={E1,E2}=∗ P.
Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index da8ba0adc..2ed93d2c0 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -16,7 +16,7 @@ Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{!heapPreG Σ} s e σ φ :
- (∀ `{!heapG Σ}, WP e @ s; ⊤ {{ v, ⌜φ v⌠}}%I) →
+ (∀ `{!heapG Σ}, ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌠}}) →
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index e676c0150..611f5623b 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -67,7 +67,7 @@ Proof. by rewrite /Frame array_cons. Qed.
Lemma update_array l q vs off v :
vs !! off = Some v →
- l ↦∗{q} vs -∗ ((l +ₗ off) ↦{q} v ∗ ∀ v', (l +ₗ off) ↦{q} v' -∗ l ↦∗{q} <[off:=v']>vs).
+ ⊢ l ↦∗{q} vs -∗ ((l +ₗ off) ↦{q} v ∗ ∀ v', (l +ₗ off) ↦{q} v' -∗ l ↦∗{q} <[off:=v']>vs).
Proof.
iIntros (Hlookup) "Hl".
rewrite -[X in (l ↦∗{_} X)%I](take_drop_middle _ off v); last done.
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index c62373138..7e847e369 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -24,10 +24,10 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
alloc_spec (v : val) :
{{{ True }}} alloc v {{{ l, RET #l; mapsto l 1 v }}};
load_spec (l : loc) :
- <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
+ ⊢ <<< ∀ (v : val) q, mapsto l q v >>> load #l @ ⊤ <<< mapsto l q v, RET v >>>;
store_spec (l : loc) (w : val) :
- <<< ∀ v, mapsto l 1 v >>> store #l w @ ⊤
- <<< mapsto l 1 w, RET #() >>>;
+ ⊢ <<< ∀ v, mapsto l 1 v >>> store #l w @ ⊤
+ <<< mapsto l 1 w, RET #() >>>;
(* This spec is slightly weaker than it could be: It is sufficient for [w1]
*or* [v] to be unboxed. However, by writing it this way the [val_is_unboxed]
is outside the atomic triple, which makes it much easier to use -- and the
@@ -36,8 +36,8 @@ Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
[destruct (decide (a = b))] and it will simplify in both places. *)
cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 →
- <<< ∀ v, mapsto l 1 v >>> cmpxchg #l w1 w2 @ ⊤
- <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
+ ⊢ <<< ∀ v, mapsto l 1 v >>> cmpxchg #l w1 w2 @ ⊤
+ <<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET (v, #if decide (v = w1) then true else false) >>>;
}.
Arguments atomic_heap _ {_}.
@@ -67,7 +67,7 @@ Section derived.
Lemma cas_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 →
- <<< ∀ v, mapsto l 1 v >>> CAS #l w1 w2 @ ⊤
+ ⊢ <<< ∀ v, mapsto l 1 v >>> CAS #l w1 w2 @ ⊤
<<< if decide (v = w1) then mapsto l 1 w2 else mapsto l 1 v,
RET #if decide (v = w1) then true else false >>>.
Proof.
@@ -98,7 +98,7 @@ Section proof.
Qed.
Lemma primitive_load_spec (l : loc) :
- <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
+ ⊢ <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
<<< l ↦{q} v, RET v >>>.
Proof.
iIntros (Φ) "AU". wp_lam.
@@ -107,7 +107,7 @@ Section proof.
Qed.
Lemma primitive_store_spec (l : loc) (w : val) :
- <<< ∀ v, l ↦ v >>> primitive_store #l w @ ⊤
+ ⊢ <<< ∀ v, l ↦ v >>> primitive_store #l w @ ⊤
<<< l ↦ w, RET #() >>>.
Proof.
iIntros (Φ) "AU". wp_lam. wp_let.
@@ -117,7 +117,7 @@ Section proof.
Lemma primitive_cmpxchg_spec (l : loc) (w1 w2 : val) :
val_is_unboxed w1 →
- <<< ∀ (v : val), l ↦ v >>>
+ ⊢ <<< ∀ (v : val), l ↦ v >>>
primitive_cmpxchg #l w1 w2 @ ⊤
<<< if decide (v = w1) then l ↦ w2 else l ↦ v,
RET (v, #if decide (v = w1) then true else false) >>>.
diff --git a/theories/heap_lang/lib/diverge.v b/theories/heap_lang/lib/diverge.v
index 9f12d7234..1a34a029c 100644
--- a/theories/heap_lang/lib/diverge.v
+++ b/theories/heap_lang/lib/diverge.v
@@ -21,7 +21,7 @@ Definition diverge : val :=
rec: "diverge" "v" := "diverge" "v".
Lemma wp_diverge `{!heapG Σ} s E (Φ : val → iProp Σ) (v : val) :
- WP diverge v @ s;E {{ Φ }}%I.
+ ⊢ WP diverge v @ s;E {{ Φ }}.
Proof.
iLöb as "IH". wp_lam. iApply "IH".
Qed.
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 265570c95..b479bc96a 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -21,7 +21,7 @@ Section increment_physical.
else "incr" "l".
Lemma incr_phy_spec (l: loc) :
- <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
+ ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
Proof.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
@@ -53,7 +53,7 @@ Section increment.
of atomic accessors. Useful for introducing them as a concept,
but see below for a shorter proof. *)
Lemma incr_spec_direct (l: loc) :
- <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
+ ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
Proof.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
awp_apply load_spec.
@@ -78,7 +78,7 @@ Section increment.
(** A proof of the incr specification that uses lemmas to avoid reasining
with the definition of atomic accessors. *)
Lemma incr_spec (l: loc) :
- <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
+ ⊢ <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
Proof.
iIntros (Φ) "AU". iLöb as "IH". wp_lam.
awp_apply load_spec.
@@ -142,7 +142,7 @@ Section increment_client.
incr "l" ||| incr "l".
Lemma incr_client_safe (x: Z):
- WP incr_client #x {{ _, True }}%I.
+ ⊢ WP incr_client #x {{ _, True }}.
Proof using Type*.
wp_lam. wp_alloc l as "Hl".
iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto.
diff --git a/theories/heap_lang/total_adequacy.v b/theories/heap_lang/total_adequacy.v
index 8c2f6ffb5..2194d6df0 100644
--- a/theories/heap_lang/total_adequacy.v
+++ b/theories/heap_lang/total_adequacy.v
@@ -5,7 +5,7 @@ From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition heap_total Σ `{!heapPreG Σ} s e σ φ :
- (∀ `{!heapG Σ}, WP e @ s; ⊤ [{ v, ⌜φ v⌠}]%I) →
+ (∀ `{!heapG Σ}, ⊢ WP e @ s; ⊤ [{ v, ⌜φ v⌠}]) →
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 6d353035b..a0637add5 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -115,7 +115,7 @@ End adequacy.
(** Iris's generic adequacy result *)
Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e1 σ1 n κs t2 σ2 φ :
(∀ `{Hinv : !invG Σ},
- (|={⊤}=> ∃
+ ⊢ |={⊤}=> ∃
(s: stuckness)
(stateI : state Λ → list (observation Λ) → nat → iProp Σ)
(Φ fork_post : val Λ → iProp Σ),
@@ -138,7 +138,7 @@ Theorem wp_strong_adequacy Σ Λ `{!invPreG Σ} e1 σ1 n κs t2 σ2 φ :
can conclude [φ] in the logic. After opening all required invariants,
one can use [fupd_intro_mask'] or [fupd_mask_weaken] to introduce the
fancy update. *)
- |={⊤,∅}=> ⌜ φ âŒ))%I) →
+ |={⊤,∅}=> ⌜ φ âŒ)) →
nsteps n ([e1], σ1) κs (t2, σ2) →
(* Then we can conclude [φ] at the meta-level. *)
φ.
@@ -192,11 +192,11 @@ Qed.
Corollary wp_adequacy Σ Λ `{!invPreG Σ} s e σ φ :
(∀ `{Hinv : !invG Σ} κs,
- (|={⊤}=> ∃
+ ⊢ |={⊤}=> ∃
(stateI : state Λ → list (observation Λ) → iProp Σ)
(fork_post : val Λ → iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv (λ σ κs _, stateI σ κs) fork_post in
- stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌠}})%I) →
+ stateI σ κs ∗ WP e @ s; ⊤ {{ v, ⌜φ v⌠}}) →
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
@@ -210,12 +210,12 @@ Qed.
Corollary wp_invariance Σ Λ `{!invPreG Σ} s e1 σ1 t2 σ2 φ :
(∀ `{Hinv : !invG Σ} κs,
- (|={⊤}=> ∃
+ ⊢ |={⊤}=> ∃
(stateI : state Λ → list (observation Λ) → nat → iProp Σ)
(fork_post : val Λ → iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
stateI σ1 κs 0 ∗ WP e1 @ s; ⊤ {{ _, True }} ∗
- (stateI σ2 [] (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φâŒ))%I) →
+ (stateI σ2 [] (pred (length t2)) -∗ ∃ E, |={⊤,E}=> ⌜φâŒ)) →
rtc erased_step ([e1], σ1) (t2, σ2) →
φ.
Proof.
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 0404e9c90..401d690a2 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -41,7 +41,7 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v
)
(at level 20, Eo, α, β, v at level 200, x1 binder, xn binder, y1 binder, yn binder,
format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
- : stdpp_scope.
+ : bi_scope.
Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
(atomic_wp (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
@@ -61,7 +61,7 @@ Notation "'<<<' ∀ x1 .. xn , α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
)
(at level 20, Eo, α, β, v at level 200, x1 binder, xn binder,
format "'[hv' '<<<' ∀ x1 .. xn , α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
- : stdpp_scope.
+ : bi_scope.
Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
(atomic_wp (TA:=TeleO)
@@ -78,7 +78,7 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' ∃ y1 .. yn , β , 'RET' v '>>>'" :=
)
(at level 20, Eo, α, β, v at level 200, y1 binder, yn binder,
format "'[hv' '<<<' α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' ∃ y1 .. yn , β , '/' 'RET' v '>>>' ']' ']'")
- : stdpp_scope.
+ : bi_scope.
Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
(atomic_wp (TA:=TeleO)
@@ -91,7 +91,7 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
)
(at level 20, Eo, α, β, v at level 200,
format "'[hv' '<<<' α '>>>' '/ ' e @ Eo '/' '[ ' '<<<' β , '/' 'RET' v '>>>' ']' ']'")
- : stdpp_scope.
+ : bi_scope.
(** Theory *)
Section lemmas.
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index 075101768..1aa857791 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -59,7 +59,7 @@ Lemma wp_lift_pure_head_stuck E Φ e :
to_val e = None →
sub_redexes_are_values e →
(∀ σ, head_stuck e σ) →
- WP e @ E ?{{ Φ }}%I.
+ ⊢ WP e @ E ?{{ Φ }}.
Proof using Hinh.
iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
iIntros (σ κs n) "_". iMod (fupd_intro_mask' E ∅) as "_"; first set_solver.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index a8f5850ae..6eb2e36dc 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -64,10 +64,10 @@ Global Instance ht_mono' s E :
Proper (flip (⊢) ==> eq ==> pointwise_relation _ (⊢) ==> (⊢)) (ht s E).
Proof. solve_proper. Qed.
-Lemma ht_alt s E P Φ e : (P ⊢ WP e @ s; E {{ Φ }}) → {{ P }} e @ s; E {{ Φ }}.
+Lemma ht_alt s E P Φ e : (P ⊢ WP e @ s; E {{ Φ }}) → ⊢ {{ P }} e @ s; E {{ Φ }}.
Proof. iIntros (Hwp) "!> HP". by iApply Hwp. Qed.
-Lemma ht_val s E v : {{ True }} of_val v @ s; E {{ v', ⌜v = v'⌠}}.
+Lemma ht_val s E v : ⊢ {{ True }} of_val v @ s; E {{ v', ⌜v = v'⌠}}.
Proof. iIntros "!> _". by iApply wp_value'. Qed.
Lemma ht_vs s E P P' Φ Φ' e :
diff --git a/theories/program_logic/total_adequacy.v b/theories/program_logic/total_adequacy.v
index 1dbbd877b..c3d0235b9 100644
--- a/theories/program_logic/total_adequacy.v
+++ b/theories/program_logic/total_adequacy.v
@@ -15,8 +15,8 @@ Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
state_interp σ1 κs n ={⊤}=∗ ∃ n', ⌜κ = []⌠∗ state_interp σ2 κs n' ∗ twptp t2)%I.
Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
- (<pers> (∀ t, twptp1 t -∗ twptp2 t) →
- ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t)%I.
+ ⊢ <pers> (∀ t, twptp1 t -∗ twptp2 t) →
+ ∀ t, twptp_pre twptp1 t -∗ twptp_pre twptp2 t.
Proof.
iIntros "#H"; iIntros (t) "Hwp". rewrite /twptp_pre.
iIntros (t2 σ1 κ κs σ2 n1) "Hstep Hσ".
@@ -37,7 +37,7 @@ Lemma twptp_unfold t : twptp t ⊣⊢ twptp_pre twptp t.
Proof. by rewrite /twptp least_fixpoint_unfold. Qed.
Lemma twptp_ind Ψ :
- ((□ ∀ t, twptp_pre (λ t, Ψ t ∧ twptp t) t -∗ Ψ t) → ∀ t, twptp t -∗ Ψ t)%I.
+ ⊢ (□ ∀ t, twptp_pre (λ t, Ψ t ∧ twptp t) t -∗ Ψ t) → ∀ t, twptp t -∗ Ψ t.
Proof.
iIntros "#IH" (t) "H".
assert (NonExpansive Ψ).
@@ -116,11 +116,11 @@ End adequacy.
Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
(∀ `{Hinv : !invG Σ},
- (|={⊤}=> ∃
+ ⊢ |={⊤}=> ∃
(stateI : state Λ → list (observation Λ) → nat → iProp Σ)
(fork_post : val Λ → iProp Σ),
let _ : irisG Λ Σ := IrisG _ _ Hinv stateI fork_post in
- stateI σ [] 0 ∗ WP e @ s; ⊤ [{ Φ }])%I) →
+ stateI σ [] 0 ∗ WP e @ s; ⊤ [{ Φ }]) →
sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
Proof.
intros Hwp. apply (soundness (M:=iResUR Σ) _ 1); simpl.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 67ca8d4de..6b6b840be 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -27,8 +27,8 @@ Definition twp_pre `{!irisG Λ Σ} (s : stuckness)
monotone. The actual least fixpoint [twp_def] can be found below. *)
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.
+ ⊢ (□ ∀ E e Φ, wp1 E e Φ -∗ wp2 E e Φ) →
+ ∀ E e Φ, twp_pre s wp1 E e Φ -∗ twp_pre s wp2 E e Φ.
Proof.
iIntros "#H"; iIntros (E e1 Φ) "Hwp". rewrite /twp_pre.
destruct (to_val e1) as [v|]; first done.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index ef0c8d8c2..ccf395f4d 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -497,7 +497,7 @@ Proof. intros HP. apply HP. Defined.
checker, per https://gitlab.mpi-sws.org/iris/iris/issues/274; hence, it must
be done _outside_ [tac_pose_proof], so the latter can remain opaque. *)
Lemma tac_pose_proof Δ j P Q :
- P →
+ (⊢ P) →
match envs_app true (Esnoc Enil j P) Δ with
| None => False
| Some Δ' => envs_entails Δ' Q
diff --git a/theories/si_logic/bi.v b/theories/si_logic/bi.v
index 2efd1b8bf..d7d9f5aa3 100644
--- a/theories/si_logic/bi.v
+++ b/theories/si_logic/bi.v
@@ -125,8 +125,6 @@ Canonical Structure siPropSI : sbi :=
{| sbi_ofe_mixin := ofe_mixin_of siProp;
sbi_bi_mixin := siProp_bi_mixin; sbi_sbi_mixin := siProp_sbi_mixin |}.
-Coercion siProp_valid (P : siProp) : Prop := bi_emp_valid P.
-
Lemma siProp_plainly_mixin : BiPlainlyMixin siPropSI siProp_plainly.
Proof.
split; try done.
--
GitLab