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
1be17c0d
Commit
1be17c0d
authored
Jan 23, 2017
by
Robbert Krebbers
Browse files
Get rid of * specialization pattern and perform these automatically.
parent
f234569b
Changes
8
Hide whitespace changes
Inline
Side-by-side
ProofMode.md
View file @
1be17c0d
...
...
@@ -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 @
1be17c0d
...
...
@@ -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 @
1be17c0d
...
...
@@ -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 @
1be17c0d
...
...
@@ -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 @
1be17c0d
...
...
@@ -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 @
1be17c0d
...
...
@@ -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/spec_patterns.v
View file @
1be17c0d
...
...
@@ -12,8 +12,7 @@ Inductive spec_pat :=
|
SGoal
:
spec_goal
→
spec_pat
|
SGoalPersistent
:
spec_pat
|
SGoalPure
:
spec_pat
|
SName
:
string
→
spec_pat
|
SForall
:
spec_pat
.
|
SName
:
string
→
spec_pat
.
Module
spec_pat
.
Inductive
token
:
=
...
...
@@ -23,7 +22,6 @@ Inductive token :=
|
TBracketR
:
token
|
TPersistent
:
token
|
TPure
:
token
|
TForall
:
token
|
TModal
:
token
|
TFrame
:
token
.
...
...
@@ -37,7 +35,6 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
|
String
"]"
s
=>
tokenize_go
s
(
TBracketR
::
cons_name
kn
k
)
""
|
String
"#"
s
=>
tokenize_go
s
(
TPersistent
::
cons_name
kn
k
)
""
|
String
"%"
s
=>
tokenize_go
s
(
TPure
::
cons_name
kn
k
)
""
|
String
"*"
s
=>
tokenize_go
s
(
TForall
::
cons_name
kn
k
)
""
|
String
">"
s
=>
tokenize_go
s
(
TModal
::
cons_name
kn
k
)
""
|
String
"$"
s
=>
tokenize_go
s
(
TFrame
::
cons_name
kn
k
)
""
|
String
a
s
=>
...
...
@@ -60,7 +57,6 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
|
TBracketL
::
ts
=>
parse_goal
ts
(
SpecGoal
false
false
[]
[])
k
|
TModal
::
TBracketL
::
ts
=>
parse_goal
ts
(
SpecGoal
true
false
[]
[])
k
|
TModal
::
ts
=>
parse_go
ts
(
SGoal
(
SpecGoal
true
true
[]
[])
::
k
)
|
TForall
::
ts
=>
parse_go
ts
(
SForall
::
k
)
|
_
=>
None
end
with
parse_goal
(
ts
:
list
token
)
(
g
:
spec_goal
)
...
...
theories/proofmode/tactics.v
View file @
1be17c0d
...
...
@@ -285,7 +285,6 @@ 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
|
SName
?H2
::
?pats
=>
eapply
tac_specialize
with
_
_
H2
_
H1
_
_
_
_;
(* (j:=H1) (i:=H2) *)
[
env_cbv
;
reflexivity
||
fail
"iSpecialize:"
H2
"not found"
...
...
@@ -424,11 +423,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
...
...
@@ -971,7 +965,8 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
|
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
...
...
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