Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
2d0e1f3e
Commit
2d0e1f3e
authored
Jun 08, 2018
by
Jacques-Henri Jourdan
Browse files
Change WP so that we have an fupd before the later, but after the quantification over next states.
parent
618c2767
Changes
5
Hide whitespace changes
Inline
Side-by-side
theories/program_logic/adequacy.v
View file @
2d0e1f3e
...
...
@@ -77,8 +77,8 @@ Proof.
rewrite
{
1
}
wp_unfold
/
wp_pre
.
iIntros
(?)
"[(Hw & HE & Hσ) H]"
.
rewrite
(
val_stuck
e1
σ
1 e2
σ
2
efs
)
//
uPred_fupd_eq
.
iMod
(
"H"
$!
σ
1
with
"Hσ [Hw HE]"
)
as
">(Hw & HE & _ & H)"
;
first
by
iFrame
.
iMod
Intro
;
iNext
.
i
Mod
(
"H"
$!
e2
σ
2
efs
with
"
[%]
[$Hw $HE]"
)
as
">($ & $ & $
& $)"
;
auto
.
iMod
(
"H"
$!
e2
σ
2
efs
with
"[//] [$Hw $HE]"
)
as
">(Hw & HE & H)"
.
i
Intros
"!> !>"
.
by
iMod
(
"H"
with
"[$Hw $HE]"
)
as
">($ & $ & $
)"
.
Qed
.
Lemma
wptp_step
s
e1
t1
t2
σ
1
σ
2
Φ
:
...
...
theories/program_logic/ectx_lifting.v
View file @
2d0e1f3e
...
...
@@ -14,20 +14,32 @@ Hint Resolve head_prim_reducible head_reducible_prim_step.
Hint
Resolve
(
reducible_not_val
_
inhabitant
).
Hint
Resolve
head_stuck_stuck
.
Lemma
wp_lift_head_step
{
s
E
Φ
}
e1
:
Lemma
wp_lift_head_step
_fupd
{
s
E
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
,
∅
}=
∗
⌜
head_reducible
e1
σ
1
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
,
E
}=
∗
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
}=
∗
▷
|
={
∅
,
E
}=
>
state_interp
σ
2
∗
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
wp_lift_step
=>//.
iIntros
(
σ
1
)
"Hσ"
.
iIntros
(?)
"H"
.
iApply
wp_lift_step
_fupd
=>//.
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
"H"
with
"Hσ"
)
as
"[% H]"
;
iModIntro
.
iSplit
;
first
by
destruct
s
;
eauto
.
iNext
.
iIntros
(
e2
σ
2
efs
)
"%"
.
iSplit
;
first
by
destruct
s
;
eauto
.
iIntros
(
e2
σ
2
efs
)
"%"
.
iApply
"H"
;
eauto
.
Qed
.
Lemma
wp_lift_head_step
{
s
E
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
,
∅
}=
∗
⌜
head_reducible
e1
σ
1
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
,
E
}=
∗
state_interp
σ
2
∗
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
wp_lift_head_step_fupd
;
[
done
|].
iIntros
(?)
"?"
.
iMod
(
"H"
with
"[$]"
)
as
"[$ H]"
.
iIntros
"!>"
(
e2
σ
2
efs
?)
"!> !>"
.
by
iApply
"H"
.
Qed
.
Lemma
wp_lift_head_stuck
E
Φ
e
:
to_val
e
=
None
→
sub_redexes_are_values
e
→
...
...
@@ -45,7 +57,7 @@ Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
using
Hinh
.
iIntros
(??)
"H"
.
iApply
wp_lift_pure_step
;
eauto
.
iIntros
(??)
"H"
.
iApply
wp_lift_pure_step
;
[|
by
eauto
|]
.
{
by
destruct
s
;
auto
.
}
iApply
(
step_fupd_wand
with
"H"
)
;
iIntros
"H"
.
iIntros
(????).
iApply
"H"
;
eauto
.
...
...
@@ -62,6 +74,21 @@ Proof using Hinh.
by
auto
.
Qed
.
Lemma
wp_lift_atomic_head_step_fupd
{
s
E1
E2
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E1
}=
∗
⌜
head_reducible
e1
σ
1
⌝
∗
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
={
E1
,
E2
}
▷
=
∗
state_interp
σ
2
∗
from_option
Φ
False
(
to_val
e2
)
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E1
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
wp_lift_atomic_step_fupd
;
[
done
|].
iIntros
(
σ
1
)
"Hσ1"
.
iMod
(
"H"
with
"Hσ1"
)
as
"[% H]"
;
iModIntro
.
iSplit
;
first
by
destruct
s
;
auto
.
iIntros
(
e2
σ
2
efs
)
"%"
.
iApply
"H"
;
auto
.
Qed
.
Lemma
wp_lift_atomic_head_step
{
s
E
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
}=
∗
...
...
@@ -77,6 +104,20 @@ Proof.
iApply
"H"
;
auto
.
Qed
.
Lemma
wp_lift_atomic_head_step_no_fork_fupd
{
s
E1
E2
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E1
}=
∗
⌜
head_reducible
e1
σ
1
⌝
∗
∀
e2
σ
2
efs
,
⌜
head_step
e1
σ
1 e2
σ
2
efs
⌝
={
E1
,
E2
}
▷
=
∗
⌜
efs
=
[]
⌝
∗
state_interp
σ
2
∗
from_option
Φ
False
(
to_val
e2
))
⊢
WP
e1
@
s
;
E1
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
wp_lift_atomic_head_step_fupd
;
[
done
|].
iIntros
(
σ
1
)
"Hσ1"
.
iMod
(
"H"
$!
σ
1
with
"Hσ1"
)
as
"[$ H]"
;
iModIntro
.
iIntros
(
v2
σ
2
efs
)
"%"
.
iMod
(
"H"
$!
v2
σ
2
efs
with
"[# //]"
)
as
"H"
.
iIntros
"!> !>"
.
iMod
"H"
as
"(% & $ & $)"
;
subst
;
auto
.
Qed
.
Lemma
wp_lift_atomic_head_step_no_fork
{
s
E
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
}=
∗
...
...
theories/program_logic/lifting.v
View file @
2d0e1f3e
...
...
@@ -11,16 +11,16 @@ Implicit Types σ : state Λ.
Implicit
Types
P
Q
:
iProp
Σ
.
Implicit
Types
Φ
:
val
Λ
→
iProp
Σ
.
Lemma
wp_lift_step
s
E
Φ
e1
:
Lemma
wp_lift_step
_fupd
s
E
Φ
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
,
∅
}=
∗
⌜
if
s
is
NotStuck
then
reducible
e1
σ
1
else
True
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
,
E
}=
∗
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
}=
∗
▷
|
={
∅
,
E
}=
>
state_interp
σ
2
∗
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
rewrite
wp_unfold
/
wp_pre
=>->.
iIntros
"H"
(
σ
1
)
"Hσ"
.
iMod
(
"H"
with
"Hσ"
)
as
"(%&
?
)"
.
iModIntro
.
iSplit
.
by
destruct
s
.
done
.
iMod
(
"H"
with
"Hσ"
)
as
"(%&
H
)"
.
iModIntro
.
iSplit
.
by
destruct
s
.
done
.
Qed
.
Lemma
wp_lift_stuck
E
Φ
e
:
...
...
@@ -30,10 +30,22 @@ Lemma wp_lift_stuck E Φ e :
Proof
.
rewrite
wp_unfold
/
wp_pre
=>->.
iIntros
"H"
(
σ
1
)
"Hσ"
.
iMod
(
"H"
with
"Hσ"
)
as
%[?
Hirr
].
iModIntro
.
iSplit
;
first
done
.
iIntros
"!>"
(
e2
σ
2
efs
)
"%"
.
by
case
:
(
Hirr
e2
σ
2
efs
).
iIntros
(
e2
σ
2
efs
)
"%
!> !>
"
.
by
case
:
(
Hirr
e2
σ
2
efs
).
Qed
.
(** Derived lifting lemmas. *)
Lemma
wp_lift_step
s
E
Φ
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
,
∅
}=
∗
⌜
if
s
is
NotStuck
then
reducible
e1
σ
1
else
True
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
,
E
}=
∗
state_interp
σ
2
∗
WP
e2
@
s
;
E
{{
Φ
}}
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
wp_lift_step_fupd
;
[
done
|].
iIntros
(?)
"Hσ"
.
iMod
(
"H"
with
"Hσ"
)
as
"[$ H]"
.
iIntros
"!> * % !>"
.
by
iApply
"H"
.
Qed
.
Lemma
wp_lift_pure_step
`
{
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
→
σ
1
=
σ
2
)
→
...
...
@@ -65,6 +77,26 @@ Qed.
(* Atomic steps don't need any mask-changing business here, one can
use the generic lemmas here. *)
Lemma
wp_lift_atomic_step_fupd
{
s
E1
E2
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E1
}=
∗
⌜
if
s
is
NotStuck
then
reducible
e1
σ
1
else
True
⌝
∗
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
E1
,
E2
}
▷
=
∗
state_interp
σ
2
∗
from_option
Φ
False
(
to_val
e2
)
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E1
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
(
wp_lift_step_fupd
s
E1
_
e1
)=>//
;
iIntros
(
σ
1
)
"Hσ1"
.
iMod
(
"H"
$!
σ
1
with
"Hσ1"
)
as
"[$ H]"
.
iMod
(
fupd_intro_mask'
E1
∅
)
as
"Hclose"
;
first
set_solver
.
iIntros
"!>"
(
e2
σ
2
efs
?).
iMod
"Hclose"
as
"_"
.
iMod
(
"H"
$!
e2
σ
2
efs
with
"[#]"
)
as
"H"
;
[
done
|].
iMod
(
fupd_intro_mask'
E2
∅
)
as
"Hclose"
;
[
set_solver
|].
iIntros
"!> !>"
.
iMod
"Hclose"
as
"_"
.
iMod
"H"
as
"($ & HΦ & $)"
.
destruct
(
to_val
e2
)
eqn
:
?
;
last
by
iExFalso
.
by
iApply
wp_value
.
Qed
.
Lemma
wp_lift_atomic_step
{
s
E
Φ
}
e1
:
to_val
e1
=
None
→
(
∀
σ
1
,
state_interp
σ
1
={
E
}=
∗
...
...
@@ -74,13 +106,9 @@ Lemma wp_lift_atomic_step {s E Φ} e1 :
from_option
Φ
False
(
to_val
e2
)
∗
[
∗
list
]
ef
∈
efs
,
WP
ef
@
s
;
⊤
{{
_
,
True
}})
⊢
WP
e1
@
s
;
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"H"
.
iApply
(
wp_lift_step
s
E
_
e1
)=>//
;
iIntros
(
σ
1
)
"Hσ1"
.
iMod
(
"H"
$!
σ
1
with
"Hσ1"
)
as
"[$ H]"
.
iMod
(
fupd_intro_mask'
E
∅
)
as
"Hclose"
;
first
set_solver
.
iModIntro
;
iNext
;
iIntros
(
e2
σ
2
efs
)
"%"
.
iMod
"Hclose"
as
"_"
.
iMod
(
"H"
$!
e2
σ
2
efs
with
"[#]"
)
as
"($ & HΦ & $)"
;
first
by
eauto
.
destruct
(
to_val
e2
)
eqn
:
?
;
last
by
iExFalso
.
by
iApply
wp_value
.
iIntros
(?)
"H"
.
iApply
wp_lift_atomic_step_fupd
;
[
done
|].
iIntros
(?)
"?"
.
iMod
(
"H"
with
"[$]"
)
as
"[$ H]"
.
iIntros
"!> * % !> !>"
.
by
iApply
"H"
.
Qed
.
Lemma
wp_lift_pure_det_step
`
{
Inhabited
(
state
Λ
)}
{
s
E
E'
Φ
}
e1
e2
efs
:
...
...
theories/program_logic/total_weakestpre.v
View file @
2d0e1f3e
...
...
@@ -315,9 +315,9 @@ Lemma twp_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
Proof
.
iIntros
"H"
.
iL
ö
b
as
"IH"
forall
(
E
e
Φ
).
rewrite
wp_unfold
twp_unfold
/
wp_pre
/
twp_pre
.
destruct
(
to_val
e
)
as
[
v
|]=>//.
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
"H"
with
"Hσ"
)
as
"[$ H]"
.
i
Mod
Intro
;
iNext
.
iIntros
(
e2
σ
2
efs
)
"Hstep"
.
i
Mod
(
"H"
with
"Hstep"
)
as
"($ & H & Hfork)"
;
iModIntro
.
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
"H"
with
"Hσ"
)
as
"[$ H]"
.
iIntro
s
"!>"
.
iIntros
(
e2
σ
2
efs
)
"Hstep"
.
iMod
(
"H"
with
"Hstep"
)
as
"($ & H & Hfork)"
.
i
Apply
step_fupd_intro
;
[
set_solver
+|].
iNext
.
iSplitL
"H"
.
by
iApply
"IH"
.
iApply
(@
big_sepL_impl
with
"[$Hfork]"
).
iIntros
"!#"
(
k
e'
_
)
"H"
.
by
iApply
"IH"
.
Qed
.
...
...
theories/program_logic/weakestpre.v
View file @
2d0e1f3e
...
...
@@ -32,7 +32,7 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
|
Some
v
=>
|={
E
}=>
Φ
v
|
None
=>
∀
σ
1
,
state_interp
σ
1
={
E
,
∅
}=
∗
⌜
if
s
is
NotStuck
then
reducible
e1
σ
1
else
True
⌝
∗
▷
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
,
E
}=
∗
∀
e2
σ
2
efs
,
⌜
prim_step
e1
σ
1 e2
σ
2
efs
⌝
={
∅
}=
∗
▷
|
={
∅
,
E
}=
>
state_interp
σ
2
∗
wp
E
e2
Φ
∗
[
∗
list
]
ef
∈
efs
,
wp
⊤
ef
(
λ
_
,
True
)
end
%
I
.
...
...
@@ -197,7 +197,7 @@ Proof.
(* FIXME: figure out a way to properly automate this proof *)
(* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
is very slow here *)
do
1
7
(
f_contractive
||
f_equiv
).
apply
IH
;
first
lia
.
do
1
8
(
f_contractive
||
f_equiv
).
apply
IH
;
first
lia
.
intros
v
.
eapply
dist_le
;
eauto
with
omega
.
Qed
.
Global
Instance
wp_proper
s
E
e
:
...
...
@@ -221,8 +221,8 @@ Proof.
{
iApply
(
"HΦ"
with
"[> -]"
).
by
iApply
(
fupd_mask_mono
E1
_
).
}
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
fupd_intro_mask'
E2
E1
)
as
"Hclose"
;
first
done
.
iMod
(
"H"
with
"[$]"
)
as
"[% H]"
.
iModIntro
.
iSplit
;
[
by
destruct
s1
,
s2
|].
iNext
.
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
with
"[//]"
)
as
"($ & H & Hefs)"
.
iModIntro
.
iSplit
;
[
by
destruct
s1
,
s2
|].
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
with
"[//]"
)
as
"H"
.
iIntros
"!> !>"
.
iMod
"H"
as
"($ & H & Hefs)"
.
iMod
"Hclose"
as
"_"
.
iModIntro
.
iSplitR
"Hefs"
.
-
iApply
(
"IH"
with
"[//] H HΦ"
).
-
iApply
(
big_sepL_impl
with
"[$Hefs]"
)
;
iIntros
"!#"
(
k
ef
_
)
"H"
.
...
...
@@ -245,8 +245,8 @@ Proof.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
He
.
{
by
iDestruct
"H"
as
">>> $"
.
}
iIntros
(
σ
1
)
"Hσ"
.
iMod
"H"
.
iMod
(
"H"
$!
σ
1
with
"Hσ"
)
as
"[$ H]"
.
iModIntro
.
iNext
.
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
with
"[//]"
)
as
"(Hphy & H & $)"
.
destruct
s
.
iModIntro
.
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
with
"[//]"
)
as
"H"
.
iIntros
"!>!>"
.
iMod
"H"
as
"(Hphy & H & $)"
.
destruct
s
.
-
rewrite
!
wp_unfold
/
wp_pre
.
destruct
(
to_val
e2
)
as
[
v2
|]
eqn
:
He2
.
+
iDestruct
"H"
as
">> $"
.
by
iFrame
.
+
iMod
(
"H"
with
"[$]"
)
as
"[H _]"
.
iDestruct
"H"
as
%(?
&
?
&
?
&
?).
...
...
@@ -261,8 +261,8 @@ Lemma wp_step_fupd s E1 E2 e P Φ :
Proof
.
rewrite
!
wp_unfold
/
wp_pre
.
iIntros
(->
?)
"HR H"
.
iIntros
(
σ
1
)
"Hσ"
.
iMod
"HR"
.
iMod
(
"H"
with
"[$]"
)
as
"[$ H]"
.
i
Mod
Intro
;
iNext
;
iIntros
(
e2
σ
2
efs
Hstep
)
.
i
Mod
(
"H"
$!
e2
σ
2
efs
with
"[% //]"
)
as
"($ & H & $)"
.
iIntro
s
"!>"
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
$!
e2
σ
2
efs
with
"[% //]"
)
as
"H"
.
i
Intros
"!>!>"
.
iMod
"H"
as
"($ & H & $)"
.
iMod
"HR"
.
iModIntro
.
iApply
(
wp_strong_mono
s
s
E2
with
"H"
)
;
[
done
..|].
iIntros
(
v
)
"H"
.
by
iApply
"H"
.
Qed
.
...
...
@@ -277,10 +277,10 @@ Proof.
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
"H"
with
"[$]"
)
as
"[% H]"
.
iModIntro
;
iSplit
.
{
iPureIntro
.
destruct
s
;
last
done
.
unfold
reducible
in
*.
naive_solver
eauto
using
fill_step
.
}
iNext
;
iIntros
(
e2
σ
2
efs
Hstep
).
iIntros
(
e2
σ
2
efs
Hstep
).
destruct
(
fill_step_inv
e
σ
1 e2
σ
2
efs
)
as
(
e2'
&->&?)
;
auto
.
iMod
(
"H"
$!
e2'
σ
2
efs
with
"[//]"
)
as
"
($ & H & $)
"
.
by
iApply
"IH"
.
iMod
(
"H"
$!
e2'
σ
2
efs
with
"[//]"
)
as
"
H"
.
iIntros
"!>!>
"
.
iMod
"H"
as
"($ & H & $)"
.
by
iApply
"IH"
.
Qed
.
Lemma
wp_bind_inv
K
`
{!
LanguageCtx
K
}
s
E
e
Φ
:
...
...
@@ -292,9 +292,9 @@ Proof.
rewrite
fill_not_val
//.
iIntros
(
σ
1
)
"Hσ"
.
iMod
(
"H"
with
"[$]"
)
as
"[% H]"
.
iModIntro
;
iSplit
.
{
destruct
s
;
eauto
using
reducible_fill
.
}
iNext
;
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
$!
(
K
e2
)
σ
2
efs
with
"[]"
)
as
"
($ & H & $)"
;
eauto
using
fill_step
.
by
iApply
"IH"
.
iIntros
(
e2
σ
2
efs
Hstep
).
iMod
(
"H"
$!
(
K
e2
)
σ
2
efs
with
"[]"
)
as
"
H"
;
[
by
eauto
using
fill_step
|]
.
iIntros
"!>!>"
.
iMod
"H"
as
"($ & H & $)"
.
by
iApply
"IH"
.
Qed
.
(** * Derived rules *)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment