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
Rodolphe Lepigre
Iris
Commits
10a2b0f3
Commit
10a2b0f3
authored
Jan 24, 2017
by
Robbert Krebbers
Browse files
Merge branch 'no_star_specpat'
parents
f234569b
6a3c7402
Changes
7
Hide whitespace changes
Inline
Side-by-side
ProofMode.md
View file @
10a2b0f3
...
...
@@ -251,7 +251,6 @@ _specification patterns_ to express splitting of hypotheses:
`P`
, as well the remaining goal.
-
`[%]`
: This pattern can be used when eliminating
`P -★ Q`
when
`P`
is pure.
It will generate a Coq goal for
`P`
and does not consume any hypotheses.
-
`*`
: instantiate all top-level universal quantifiers with meta variables.
For example, given:
...
...
theories/heap_lang/lib/par.v
View file @
10a2b0f3
...
...
@@ -33,7 +33,7 @@ Proof.
iIntros
(
l
)
"Hl"
.
wp_let
.
wp_proj
.
wp_bind
(
f2
_
).
iApply
(
wp_wand
with
"Hf2"
)
;
iIntros
(
v
)
"H2"
.
wp_let
.
wp_apply
(
join_spec
with
"[$Hl]"
).
iIntros
(
w
)
"H1"
.
iSpecialize
(
"HΦ"
with
"
*
[-]"
)
;
first
by
iSplitL
"H1"
.
by
wp_let
.
iSpecialize
(
"HΦ"
with
"[-]"
)
;
first
by
iSplitL
"H1"
.
by
wp_let
.
Qed
.
Lemma
wp_par
(
Ψ
1
Ψ
2
:
val
→
iProp
Σ
)
...
...
theories/program_logic/adequacy.v
View file @
10a2b0f3
...
...
@@ -134,7 +134,7 @@ Lemma wp_safe e σ Φ :
Proof
.
rewrite
wp_unfold
/
wp_pre
.
iIntros
"[(Hw&HE&Hσ) H]"
.
destruct
(
to_val
e
)
as
[
v
|]
eqn
:
?
;
[
eauto
10
|].
rewrite
fupd_eq
.
iMod
(
"H"
with
"
*
Hσ [-]"
)
as
">(?&?&%&?)"
;
first
by
iFrame
.
rewrite
fupd_eq
.
iMod
(
"H"
with
"Hσ [-]"
)
as
">(?&?&%&?)"
;
first
by
iFrame
.
eauto
10
.
Qed
.
...
...
theories/program_logic/ownp.v
View file @
10a2b0f3
...
...
@@ -96,7 +96,7 @@ Section lifting.
iMod
(
own_update_2
with
"Hσ Hσf"
)
as
"[Hσ Hσf]"
.
{
by
apply
auth_update
,
option_local_update
,
(
exclusive_local_update
_
(
Excl
σ
2
)).
}
iFrame
"Hσ"
.
iApply
(
"H"
with
"
*
[]"
)
;
eauto
.
iFrame
"Hσ"
.
iApply
(
"H"
with
"[]"
)
;
eauto
.
Qed
.
Lemma
ownP_lift_pure_step
`
{
Inhabited
(
state
Λ
)}
E
Φ
e1
:
...
...
@@ -171,7 +171,7 @@ Section ectx_lifting.
iIntros
"H"
.
iApply
(
ownP_lift_step
E
)
;
try
done
.
iMod
"H"
as
(
σ
1
)
"(%&Hσ1&Hwp)"
.
iModIntro
.
iExists
σ
1
.
iSplit
;
first
by
eauto
.
iFrame
.
iNext
.
iIntros
(
e2
σ
2
efs
)
"% ?"
.
iApply
(
"Hwp"
with
"
*
[]"
)
;
by
eauto
.
iApply
(
"Hwp"
with
"[]"
)
;
eauto
.
Qed
.
Lemma
ownP_lift_pure_head_step
E
Φ
e1
:
...
...
@@ -193,7 +193,7 @@ Section ectx_lifting.
⊢
WP
e1
@
E
{{
Φ
}}.
Proof
.
iIntros
(?)
"[? H]"
.
iApply
ownP_lift_atomic_step
;
eauto
.
iFrame
.
iNext
.
iIntros
(???)
"% ?"
.
iApply
(
"H"
with
"
*
[]"
)
;
eauto
.
iIntros
(???)
"% ?"
.
iApply
(
"H"
with
"[]"
)
;
eauto
.
Qed
.
Lemma
ownP_lift_atomic_det_head_step
{
E
Φ
e1
}
σ
1
v2
σ
2
efs
:
...
...
theories/program_logic/weakestpre.v
View file @
10a2b0f3
...
...
@@ -155,10 +155,10 @@ Proof.
{
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 & $)"
;
first
done
.
iMod
(
"H"
with
"[]"
)
as
"(Hphy & H & $)"
;
first
done
.
rewrite
!
wp_unfold
/
wp_pre
.
destruct
(
to_val
e2
)
as
[
v2
|]
eqn
:
He2
.
-
iDestruct
"H"
as
">> $"
.
iFrame
.
eauto
.
-
iMod
(
"H"
with
"
*
Hphy"
)
as
"[H _]"
.
-
iMod
(
"H"
with
"Hphy"
)
as
"[H _]"
.
iDestruct
"H"
as
%(?
&
?
&
?
&
?).
by
edestruct
(
Hatomic
_
_
_
_
Hstep
).
Qed
.
...
...
theories/proofmode/class_instances.v
View file @
10a2b0f3
...
...
@@ -21,6 +21,9 @@ Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
Global
Instance
from_assumption_bupd
p
P
Q
:
FromAssumption
p
P
Q
→
FromAssumption
p
P
(|==>
Q
)%
I
.
Proof
.
rewrite
/
FromAssumption
=>->.
apply
bupd_intro
.
Qed
.
Global
Instance
from_assumption_forall
{
A
}
p
(
Φ
:
A
→
uPred
M
)
Q
x
:
FromAssumption
p
(
Φ
x
)
Q
→
FromAssumption
p
(
∀
x
,
Φ
x
)
Q
.
Proof
.
rewrite
/
FromAssumption
=>
<-.
by
rewrite
forall_elim
.
Qed
.
(* IntoPure *)
Global
Instance
into_pure_pure
φ
:
@
IntoPure
M
⌜φ⌝
φ
.
...
...
@@ -217,6 +220,9 @@ Proof. by apply and_elim_l', impl_wand. Qed.
Global
Instance
into_wand_iff_r
P
Q
:
IntoWand
(
P
↔
Q
)
Q
P
.
Proof
.
apply
and_elim_r'
,
impl_wand
.
Qed
.
Global
Instance
into_wand_forall
{
A
}
(
Φ
:
A
→
uPred
M
)
P
Q
x
:
IntoWand
(
Φ
x
)
P
Q
→
IntoWand
(
∀
x
,
Φ
x
)
P
Q
.
Proof
.
rewrite
/
IntoWand
=>
<-.
apply
forall_elim
.
Qed
.
Global
Instance
into_wand_always
R
P
Q
:
IntoWand
R
P
Q
→
IntoWand
(
□
R
)
P
Q
.
Proof
.
rewrite
/
IntoWand
=>
->.
apply
always_elim
.
Qed
.
...
...
theories/proofmode/tactics.v
View file @
10a2b0f3
...
...
@@ -285,7 +285,9 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
let
rec
go
H1
pats
:
=
lazymatch
pats
with
|
[]
=>
idtac
|
SForall
::
?pats
=>
try
(
iSpecializeArgs
H1
(
hcons
_
_
))
;
go
H1
pats
|
SForall
::
?pats
=>
idtac
"the * specialization pattern is deprecated because it is applied implicitly"
;
go
H1
pats
|
SName
?H2
::
?pats
=>
eapply
tac_specialize
with
_
_
H2
_
H1
_
_
_
_;
(* (j:=H1) (i:=H2) *)
[
env_cbv
;
reflexivity
||
fail
"iSpecialize:"
H2
"not found"
...
...
@@ -424,11 +426,6 @@ Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
(** * Apply *)
Tactic
Notation
"iApply"
open_constr
(
lem
)
:
=
let
lem
:
=
(* add a `*` to specialize all top-level foralls *)
lazymatch
lem
with
|
ITrm
?t
?xs
?pat
=>
constr
:
(
ITrm
t
xs
(
"*"
+
:
+
pat
))
|
_
=>
constr
:
(
ITrm
lem
hnil
"*"
)
end
in
let
rec
go
H
:
=
first
[
eapply
tac_apply
with
_
H
_
_
_;
[
env_cbv
;
reflexivity
...
...
@@ -964,27 +961,59 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
tac
.
(** * Destruct tactic *)
Class
CopyDestruct
{
M
}
(
P
:
uPred
M
).
Hint
Mode
CopyDestruct
+
!
:
typeclass_instances
.
Instance
copy_destruct_forall
{
M
A
}
(
Φ
:
A
→
uPred
M
)
:
CopyDestruct
(
∀
x
,
Φ
x
).
Instance
copy_destruct_impl
{
M
}
(
P
Q
:
uPred
M
)
:
CopyDestruct
Q
→
CopyDestruct
(
P
→
Q
).
Instance
copy_destruct_wand
{
M
}
(
P
Q
:
uPred
M
)
:
CopyDestruct
Q
→
CopyDestruct
(
P
-
∗
Q
).
Instance
copy_destruct_always
{
M
}
(
P
:
uPred
M
)
:
CopyDestruct
P
→
CopyDestruct
(
□
P
).
Tactic
Notation
"iDestructCore"
open_constr
(
lem
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
let
hyp_name
:
=
lazymatch
type
of
lem
with
|
string
=>
constr
:
(
Some
lem
)
|
iTrm
=>
lazymatch
lem
with
|
@
iTrm
string
?H
_
_
=>
constr
:
(
Some
H
)
|
_
=>
constr
:
(@
None
string
)
end
|
_
=>
constr
:
(@
None
string
)
end
in
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
;
iStartProof
;
go
n
in
end
in
intros
;
iStartProof
;
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
=>
(* only copy the hypothesis when universal quantifiers are instantiated *)
lazymatch
lem
with
|
@
iTrm
string
?H
_
hnil
?pat
=>
iSpecializeCore
lem
as
p
;
last
tac
|
_
=>
iPoseProofCore
lem
as
p
false
tac
|
_
=>
(* Only copy the hypothesis in case there is a [CopyDestruct] instance.
Also, rule out cases in which it does not make sense to copy, namely when
destructing a lemma (instead of a hypothesis) or a spatial hyopthesis
(which cannot be kept). *)
lazymatch
hyp_name
with
|
None
=>
iPoseProofCore
lem
as
p
false
tac
|
Some
?H
=>
iTypeOf
H
(
fun
q
P
=>
lazymatch
q
with
|
true
=>
(* persistent hypothesis, check for a CopyDestruct instance *)
tryif
(
let
dummy
:
=
constr
:
(
_
:
CopyDestruct
P
)
in
idtac
)
then
(
iPoseProofCore
lem
as
p
false
tac
)
else
(
iSpecializeCore
lem
as
p
;
last
(
tac
H
))
|
false
=>
(* spatial hypothesis, cannot copy *)
iSpecializeCore
lem
as
p
;
last
(
tac
H
)
end
)
end
|
_
=>
iPoseProofCore
lem
as
p
false
tac
end
.
Tactic
Notation
"iDestruct"
open_constr
(
lem
)
"as"
constr
(
pat
)
:
=
...
...
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