Commit 278515b8 authored by Ralf Jung's avatar Ralf Jung

tests/ipm_paper: show goals where they were shown in the paper

parent 8fd3233e
1 subgoal
M : ucmraT
A : Type
P, R : iProp
Ψ : A → iProp
x : A
============================
"HP" : P
"HΨ" : Ψ x
"HR" : R
--------------------------------------∗
Ψ x ∗ P
2 subgoals
M : ucmraT
A : Type
P, R : iProp
Ψ : A → iProp
x : A
============================
"HΨ" : Ψ x
--------------------------------------∗
Ψ x
subgoal 2 is:
"HP" : P
"HR" : R
--------------------------------------∗
P
1 subgoal
M : ucmraT
A : Type
P, R : iProp
Ψ : A → iProp
x : A
============================
"HP" : P
"HR" : R
--------------------------------------∗
P
1 subgoal
M : ucmraT
A : Type
P, R : iProp
Ψ : A → iProp
============================
"HP" : P
"HΨ" : ∃ a : A, Ψ a
"HR" : R
--------------------------------------∗
∃ a : A, Ψ a ∗ P
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
counterG0 : counterG Σ
l : loc
n : nat
N : namespace
γ : gname
============================
"Hinv" : inv N (I γ l)
--------------------------------------□
"Hγf" : own γ (Frag n)
--------------------------------------∗
WP ! #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
counterG0 : counterG Σ
l : loc
n : nat
N : namespace
γ : gname
c : nat
============================
"Hinv" : inv N (I γ l)
--------------------------------------□
"Hγf" : own γ (Frag n)
"Hl" : l ↦ #c
"Hγ" : own γ (Auth c)
--------------------------------------∗
▷ I γ l ∗ (∃ m : nat, ⌜#c = #m ∧ n ≤ m⌝ ∧ C l m)
......@@ -30,14 +30,14 @@ Section demo.
Proof.
iIntros "[HP [HΨ HR]]".
iDestruct "HΨ" as (x) "HΨ".
iExists x.
iSplitL "HΨ". iAssumption. iAssumption.
iExists x. Show.
iSplitL "HΨ". Show. iAssumption. Show. iAssumption.
Qed.
(* The short version in IPM, as in the paper *)
Lemma sep_exist_short A (P R: iProp) (Ψ: A iProp) :
P ( a, Ψ a) R a, Ψ a P.
Proof. iIntros "[HP [HΨ HR]]". iFrame "HP". iAssumption. Qed.
Proof. iIntros "[HP [HΨ HR]]". Show. iFrame "HP". iAssumption. Qed.
(* An even shorter version in IPM, using the frame introduction pattern `$` *)
Lemma sep_exist_shorter A (P R: iProp) (Ψ: A iProp) :
......@@ -239,8 +239,8 @@ Section counter_proof.
{{ 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_let. iApply wp_inv_open; last iFrame "Hinv"; auto.
iDestruct 1 as (c) "[Hl Hγ]". wp_load.
rewrite /read /=. wp_let. Show. iApply wp_inv_open; last iFrame "Hinv"; auto.
iDestruct 1 as (c) "[Hl Hγ]". wp_load. Show.
iDestruct (own_valid γ (Frag n Auth c) with "[-]") as % ?%auth_frag_valid.
{ iApply own_op. by iFrame. }
rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']".
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment