Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Rodolphe Lepigre
Iris
Commits
89f354f0
Commit
89f354f0
authored
Jun 16, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Introduce iDestruct num tactic.
This introduces n hypotheses and destructs the nth one.
parent
8ca3fc9b
Changes
9
Hide whitespace changes
Inline
Side-by-side
Showing
9 changed files
with
74 additions
and
65 deletions
+74
-65
heap_lang/lib/barrier/proof.v
heap_lang/lib/barrier/proof.v
+1
-1
heap_lang/lib/lock.v
heap_lang/lib/lock.v
+1
-3
program_logic/auth.v
program_logic/auth.v
+1
-1
program_logic/boxes.v
program_logic/boxes.v
+3
-4
program_logic/invariants.v
program_logic/invariants.v
+1
-1
program_logic/sts.v
program_logic/sts.v
+1
-1
proofmode/tactics.v
proofmode/tactics.v
+62
-50
tests/barrier_client.v
tests/barrier_client.v
+2
-2
tests/joining_existentials.v
tests/joining_existentials.v
+2
-2
No files found.
heap_lang/lib/barrier/proof.v
View file @
89f354f0
...
...
@@ -171,7 +171,7 @@ Lemma recv_split E l P1 P2 :
nclose
N
⊆
E
→
recv
l
(
P1
★
P2
)
={
E
}=>
recv
l
P1
★
recv
l
P2
.
Proof
.
rename
P1
into
R1
;
rename
P2
into
R2
.
rewrite
{
1
}/
recv
/
barrier_ctx
.
iIntros
{?}
"Hr"
;
iDestruct
"Hr"
as
{
γ
P
Q
i
}
"(#(%&Hh&Hsts)&Hγ&#HQ&HQR)"
.
iIntros
{?}
.
iDestruct
1
as
{
γ
P
Q
i
}
"(#(%&Hh&Hsts)&Hγ&#HQ&HQR)"
.
iApply
pvs_trans'
.
iSts
γ
as
[
p
I
]
;
iDestruct
"Hγ"
as
"[Hl Hr]"
.
iPvs
(
saved_prop_alloc_strong
_
(
R1
:
∙
%
CF
iProp
)
I
)
as
{
i1
}
"[% #Hi1]"
.
...
...
heap_lang/lib/lock.v
View file @
89f354f0
...
...
@@ -44,9 +44,7 @@ Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof
.
apply
_
.
Qed
.
Lemma
locked_is_lock
l
R
:
locked
l
R
⊢
is_lock
l
R
.
Proof
.
rewrite
/
is_lock
.
iIntros
"Hl"
;
iDestruct
"Hl"
as
{
N
γ
}
"(?&?&?&_)"
.
eauto
.
Qed
.
Proof
.
rewrite
/
is_lock
.
iDestruct
1
as
{
N
γ
}
"(?&?&?&_)"
;
eauto
.
Qed
.
Lemma
newlock_spec
N
(
R
:
iProp
)
Φ
:
heapN
⊥
N
→
...
...
program_logic/auth.v
View file @
89f354f0
...
...
@@ -101,7 +101,7 @@ Section auth.
rewrite
->(
left_id
_
_
)
in
Ha'
;
setoid_subst
.
iApply
pvs_fsa_fsa
;
iApply
fsa_wand_r
;
iSplitL
"HΨ Hφ"
.
{
iApply
"HΨ"
;
by
iSplit
.
}
iIntros
{
v
}
"Ha"
.
iDestruct
"Ha"
as
{
b
}
"(% & Hφ & HΨ)"
.
iIntros
{
v
}
;
iDestruct
1
as
{
b
}
"(% & Hφ & HΨ)"
.
iPvs
(
own_update
_
with
"Hγ"
)
as
"[Hγ Hγf]"
;
first
eapply
auth_update
;
eauto
.
iPvsIntro
.
iSplitL
"Hφ Hγ"
;
last
by
iApply
"HΨ"
.
iNext
.
iExists
(
b
⋅
af
).
by
iFrame
.
...
...
program_logic/boxes.v
View file @
89f354f0
...
...
@@ -60,8 +60,7 @@ Lemma box_own_auth_agree γ b1 b2 :
box_own_auth
γ
(
●
Excl'
b1
)
★
box_own_auth
γ
(
◯
Excl'
b2
)
⊢
b1
=
b2
.
Proof
.
rewrite
/
box_own_prop
-
own_op
own_valid
prod_validI
/=
and_elim_l
.
iIntros
"Hb"
.
by
iDestruct
"Hb"
as
%
[[[]
[=]%
leibniz_equiv
]
?]%
auth_valid_discrete
.
by
iDestruct
1
as
%
[[[]
[=]%
leibniz_equiv
]
?]%
auth_valid_discrete
.
Qed
.
Lemma
box_own_auth_update
E
γ
b1
b2
b3
:
...
...
@@ -95,7 +94,7 @@ Lemma box_insert f P Q :
▷
box
N
f
P
={
N
}=>
∃
γ
,
f
!!
γ
=
None
★
slice
N
γ
Q
★
▷
box
N
(<[
γ
:
=
false
]>
f
)
(
Q
★
P
).
Proof
.
iIntros
"H"
;
iDestruct
"H"
as
{
Φ
}
"[#HeqP Hf]"
.
iDestruct
1
as
{
Φ
}
"[#HeqP Hf]"
.
iPvs
(
own_alloc_strong
(
●
Excl'
false
⋅
◯
Excl'
false
,
Some
(
to_agree
(
Next
(
iProp_unfold
Q
))))
_
(
dom
_
f
))
as
{
γ
}
"[Hdom Hγ]"
;
first
done
.
...
...
@@ -187,7 +186,7 @@ Lemma box_empty_all f P Q :
map_Forall
(
λ
_
,
(
true
=))
f
→
box
N
f
P
={
N
}=>
▷
P
★
box
N
(
const
false
<$>
f
)
P
.
Proof
.
iIntros
{?}
"H"
;
iDestruct
"H"
as
{
Φ
}
"[#HeqP Hf]"
.
iDestruct
1
as
{
Φ
}
"[#HeqP Hf]"
.
iAssert
([
★
map
]
γ↦
b
∈
f
,
▷
Φ
γ
★
box_own_auth
γ
(
◯
Excl'
false
)
★
box_own_prop
γ
(
Φ
γ
)
★
inv
N
(
slice_inv
γ
(
Φ
γ
)))%
I
with
"|==>[Hf]"
as
"[HΦ ?]"
.
{
iApply
(
pvs_big_sepM
_
_
f
)
;
iApply
(
big_sepM_impl
_
_
f
)
;
iFrame
"Hf"
.
...
...
program_logic/invariants.v
View file @
89f354f0
...
...
@@ -37,7 +37,7 @@ Lemma inv_open E N P :
inv
N
P
⊢
∃
E'
,
■
(
E
∖
nclose
N
⊆
E'
⊆
E
)
★
|={
E
,
E'
}=>
▷
P
★
(
▷
P
={
E'
,
E
}=
★
True
).
Proof
.
rewrite
/
inv
.
iIntros
{?}
"Hinv"
.
iDestruct
"Hinv"
as
{
i
}
"[% #Hi]"
.
rewrite
/
inv
.
iDestruct
1
as
{
i
}
"[% #Hi]"
.
iExists
(
E
∖
{[
i
]}).
iSplit
.
{
iPureIntro
.
set_solver
.
}
iPvs
(
pvs_openI'
with
"Hi"
)
as
"HP"
;
[
set_solver
..|].
iPvsIntro
.
iSplitL
"HP"
;
first
done
.
iIntros
"HP"
.
...
...
program_logic/sts.v
View file @
89f354f0
...
...
@@ -108,7 +108,7 @@ Section sts.
iRevert
"Hγ"
;
rewrite
sts_op_auth_frag
//
;
iIntros
"Hγ"
.
iApply
pvs_fsa_fsa
;
iApply
fsa_wand_r
;
iSplitL
"HΨ Hφ"
.
{
iApply
"HΨ"
;
by
iSplit
.
}
iIntros
{
a
}
"H"
;
iDestruct
"H"
as
{
s'
T'
}
"(% & Hφ & HΨ)"
.
iIntros
{
a
}
;
iDestruct
1
as
{
s'
T'
}
"(% & Hφ & HΨ)"
.
iPvs
(
own_update
with
"Hγ"
)
as
"Hγ"
;
first
eauto
using
sts_update_auth
.
iRevert
"Hγ"
;
rewrite
-
sts_op_auth_frag_up
;
iIntros
"[Hγ Hγf]"
.
iPvsIntro
;
iSplitL
"Hφ Hγ"
;
last
by
iApply
"HΨ"
.
...
...
proofmode/tactics.v
View file @
89f354f0
...
...
@@ -435,7 +435,7 @@ Local Tactic Notation "iExistDestruct" constr(H)
[
env_cbv
;
reflexivity
||
fail
"iExistDestruct:"
Hx
"not fresh"
|
revert
y
;
intros
x
].
(** *
D
estruct tactic *)
(** *
Basic d
estruct tactic *)
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
constr
(
pat
)
:
=
let
rec
go
Hz
pat
:
=
lazymatch
pat
with
...
...
@@ -485,55 +485,6 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" "{" simple_intropattern(x1)
simple_intropattern
(
x8
)
"}"
constr
(
pat
)
:
=
iExistDestruct
H
as
x1
H
;
iDestructHyp
H
as
{
x2
x3
x4
x5
x6
x7
x8
}
pat
.
Tactic
Notation
"iDestructHelp"
open_constr
(
lem
)
"as"
tactic
(
tac
)
:
=
lazymatch
type
of
lem
with
|
string
=>
tac
lem
|
iTrm
=>
lazymatch
lem
with
|
@
iTrm
string
?H
_
hnil
?pat
=>
iSpecializePat
H
pat
;
last
tac
H
|
_
=>
let
H
:
=
iFresh
in
iPoseProof
lem
as
H
;
last
tac
H
;
try
apply
_
end
|
_
=>
let
H
:
=
iFresh
in
iPoseProof
lem
as
H
;
last
tac
H
;
try
apply
_
end
.
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
x5
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
x5
x6
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
x5
x6
x7
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
x5
x6
x7
x8
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"%"
simple_intropattern
(
pat
)
:
=
let
Htmp
:
=
iFresh
in
iDestruct
H
as
Htmp
;
last
iPure
Htmp
as
pat
.
(** * Always *)
Tactic
Notation
"iAlways"
:
=
apply
tac_always_intro
;
...
...
@@ -676,6 +627,67 @@ Tactic Notation "iIntros" "{" simple_intropattern(x1) simple_intropattern(x2)
"}"
constr
(
p
)
:
=
iIntros
{
x1
x2
x3
x4
x5
x6
x7
x8
}
;
iIntros
p
.
(** * Destruct tactic *)
Tactic
Notation
"iDestructHelp"
open_constr
(
lem
)
"as"
tactic
(
tac
)
:
=
let
intro_destruct
n
:
=
let
rec
go
n'
:
=
lazymatch
n'
with
|
0
=>
fail
"iDestruct: cannot introduce"
n
"hypotheses"
|
1
=>
repeat
iIntroForall
;
let
H
:
=
iFresh
in
iIntro
H
;
tac
H
|
S
?n'
=>
repeat
iIntroForall
;
let
H
:
=
iFresh
in
iIntro
H
;
go
n'
end
in
intros
;
try
iProof
;
go
n
in
lazymatch
type
of
lem
with
|
nat
=>
intro_destruct
lem
|
Z
=>
(* to make it work in Z_scope. We should just be able to bind
tactic notation arguments to notation scopes. *)
let
n
:
=
eval
compute
in
(
Z
.
to_nat
lem
)
in
intro_destruct
n
|
string
=>
tac
lem
|
iTrm
=>
lazymatch
lem
with
|
@
iTrm
string
?H
_
hnil
?pat
=>
iSpecializePat
H
pat
;
last
tac
H
|
_
=>
let
H
:
=
iFresh
in
iPoseProof
lem
as
H
;
last
tac
H
;
try
apply
_
end
|
_
=>
let
H
:
=
iFresh
in
iPoseProof
lem
as
H
;
last
tac
H
;
try
apply
_
end
.
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
x5
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
x5
x6
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
x5
x6
x7
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"{"
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
"}"
constr
(
pat
)
:
=
iDestructHelp
H
as
(
fun
H
=>
iDestructHyp
H
as
{
x1
x2
x3
x4
x5
x6
x7
x8
}
pat
).
Tactic
Notation
"iDestruct"
open_constr
(
H
)
"as"
"%"
simple_intropattern
(
pat
)
:
=
let
Htmp
:
=
iFresh
in
iDestruct
H
as
Htmp
;
last
iPure
Htmp
as
pat
.
(* This is pretty ugly, but without Ltac support for manipulating lists of
idents I do not know how to do this better. *)
Local
Ltac
iL
ö
bHelp
IH
tac_before
tac_after
:
=
...
...
tests/barrier_client.v
View file @
89f354f0
...
...
@@ -22,7 +22,7 @@ Section client.
Lemma
y_inv_split
q
l
:
y_inv
q
l
⊢
(
y_inv
(
q
/
2
)
l
★
y_inv
(
q
/
2
)
l
).
Proof
.
iIntros
"Hl"
;
iDestruct
"Hl"
as
{
f
}
"[[Hl1 Hl2] #Hf]"
.
iDestruct
1
as
{
f
}
"[[Hl1 Hl2] #Hf]"
.
iSplitL
"Hl1"
;
iExists
f
;
by
iSplitL
;
try
iAlways
.
Qed
.
...
...
@@ -32,7 +32,7 @@ Section client.
Proof
.
iIntros
"[#Hh Hrecv]"
.
wp_lam
.
wp_let
.
wp_apply
wait_spec
;
iFrame
"Hrecv"
.
iIntros
"Hy"
;
iDestruct
"Hy"
as
{
f
}
"[Hy #Hf]"
.
iDestruct
1
as
{
f
}
"[Hy #Hf]"
.
wp_seq
.
wp_load
.
iApply
wp_wand_r
;
iSplitR
;
[
iApply
"Hf"
|
by
iIntros
{
v
}
"_"
].
Qed
.
...
...
tests/joining_existentials.v
View file @
89f354f0
...
...
@@ -34,7 +34,7 @@ Lemma worker_spec e γ l (Φ Ψ : X → iProp) :
⊢
WP
wait
#
l
;;
e
{{
_
,
barrier_res
γ
Ψ
}}.
Proof
.
iIntros
"[Hl #He]"
.
wp_apply
wait_spec
;
iFrame
"Hl"
.
iIntros
"Hγ"
;
iDestruct
"Hγ"
as
{
x
}
"[#Hγ Hx]"
.
iDestruct
1
as
{
x
}
"[#Hγ Hx]"
.
wp_seq
.
iApply
wp_wand_l
.
iSplitR
;
[|
by
iApply
"He"
].
iIntros
{
v
}
"?"
;
iExists
x
;
by
iSplit
.
Qed
.
...
...
@@ -45,7 +45,7 @@ Context {Ψ_join : ∀ x, (Ψ1 x ★ Ψ2 x) ⊢ Ψ x}.
Lemma
P_res_split
γ
:
barrier_res
γ
Φ
⊢
barrier_res
γ
Φ
1
★
barrier_res
γ
Φ
2
.
Proof
.
iIntros
"Hγ"
;
iDestruct
"Hγ"
as
{
x
}
"[#Hγ Hx]"
.
iDestruct
1
as
{
x
}
"[#Hγ Hx]"
.
iDestruct
(
Φ
_split
with
"Hx"
)
as
"[H1 H2]"
.
by
iSplitL
"H1"
;
iExists
x
;
iSplit
.
Qed
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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