Skip to content

GitLab

Commit 31bb46c5 authored by Gregory Malecha's avatar Gregory Malecha Committed by Robbert Krebbers
Browse files

CLEAN cleanup 

- remove "odd" comment
- move atomic triples to bi_scope
parent ad82d138
Hide whitespace changes
Inline Side-by-side
Showing with 130 additions and 138 deletions
tests/atomic.ref
View file @ 31bb46c5
......@@ -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
......
tests/atomic.v
View file @ 31bb46c5
......@@ -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.
......
tests/heap_lang.v
View file @ 31bb46c5
......@@ -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.
......
tests/ipm_paper.v
View file @ 31bb46c5
......@@ -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.
......
tests/one_shot.v
View file @ 31bb46c5
......@@ -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.
......
tests/one_shot_once.v
View file @ 31bb46c5
......@@ -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]").
......
tests/proofmode.v
View file @ 31bb46c5
......@@ -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.