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
Iris
Fairis
Commits
0124939d
Commit
0124939d
authored
Mar 04, 2018
by
Joseph Tassarotti
Browse files
Bump opam version.
parent
cb9d659c
Changes
6
Hide whitespace changes
Inline
Side-by-side
opam
View file @
0124939d
...
...
@@ -7,5 +7,5 @@ remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/fri" ]
depends: [
"coq" { >= "8.7" }
"coq-stdpp" { (>= "1.1.0") | (>= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-0
2-27.1
") }
"coq-iris" { (= "branch.gen_proofmode.2018-0
3-04.7
") }
]
theories/algebra/upred.v
View file @
0124939d
...
...
@@ -417,9 +417,9 @@ Import iris.bi.derived_connectives.
Ltac
unfold_bi
:=
(
*
Coq
unfold
is
used
to
circumvent
bug
#
5699
in
rewrite
/
foo
*
)
unfold
bi_emp
;
simpl
;
unfold
(
*
uPred_emp
,
*
)
bi_pure
,
bi_and
,
bi_or
,
bi_impl
,
bi_forall
,
bi_exist
,
bi_sep
,
bi_wand
,
bi_plainly
,
bi_persistently
,
bi_affinely
,
sbi_later
;
simpl
;
bi_sep
,
bi_wand
,
bi_persistently
,
bi_affinely
,
sbi_later
;
simpl
;
unfold
sbi_emp
,
sbi_pure
,
sbi_and
,
sbi_or
,
sbi_impl
,
sbi_forall
,
sbi_exist
,
sbi_internal_eq
,
sbi_sep
,
sbi_wand
,
sbi_plainly
,
sbi_persistently
;
simpl
.
sbi_internal_eq
,
sbi_sep
,
sbi_wand
,
sbi_persistently
;
simpl
.
Ltac
unseal
:=
unfold_bi
;
rewrite
!
unseal_eqs
/=
.
Ltac
try_unseal
:=
unfold_bi
;
rewrite
?
unseal_eqs
/=
.
...
...
theories/algebra/upred_bi.v
View file @
0124939d
...
...
@@ -7,7 +7,7 @@ Import uPred.
Lemma
uPred_bi_mixin
(
M
:
ucmraT
)
:
BiMixin
uPred_entails
uPred_emp
uPred_pure
uPred_and
uPred_or
uPred_impl
(
@
uPred_forall
M
)
(
@
uPred_exist
M
)
uPred_sep
uPred_wand
uPred_plainly
uPred_persistent
.
uPred_sep
uPred_wand
uPred_persistent
.
Proof
.
split
;
try
apply
_
;
eauto
with
I
.
-
(
*
(
P
⊣⊢
Q
)
↔
(
P
⊢
Q
)
∧
(
Q
⊢
P
)
*
)
...
...
@@ -36,41 +36,16 @@ Proof.
-
intros
;
by
rewrite
assoc
.
-
intros
;
by
apply
wand_intro_r
.
-
intros
;
by
apply
wand_elim_l
'
.
-
unseal
.
intros
P
Q
HPQ
;
split
=>
n
x
y
??
HP
//=. apply HPQ => //=.
*
apply
ucmra_unit_validN
.
*
apply
ucmra_unit_validN
.
-
unseal
.
intros
P
.
split
=>
n
x
y
??
=>
//=. rewrite /uPred_holds //=.
intros
HP
.
eapply
uPred_mono
;
eauto
.
exists
(
core
x
).
rewrite
left_id
.
reflexivity
.
-
unseal
.
split
=>
n
x
y
??
=>
//=.
-
unseal
.
split
=>
n
x
y
??
=>
//=.
intros
HP
.
eapply
H
;
eauto
.
*
apply
cmra_core_validN
;
eauto
.
*
apply
ucmra_unit_validN
.
-
unseal
.
split
=>
n
x
y
??
=>
//=. rewrite /uPred_holds //= => H.
rewrite
/
uPred_holds
//=. rewrite cmra_core_idemp //.
-
unseal
.
split
=>
n
x
y
??
=>
//=.
do
2
rewrite
/
uPred_holds
//=.
intros
HPQ
n
'
x
'
????
HP
.
eapply
uPred_mono
;
first
eapply
HPQ
;
eauto
.
*
eapply
cmra_validN_le
;
eauto
.
*
eapply
cmra_validN_le
;
eauto
.
*
apply
cmra_included_includedN
;
auto
.
-
unseal
.
split
=>
n
x
y
??
=>
//=.
do
2
rewrite
/
uPred_holds
//=.
intros
HPQ
n
'
x
'
????
HP
.
eapply
uPred_mono
;
first
eapply
HPQ
;
eauto
.
*
eapply
cmra_validN_le
;
eauto
.
*
eapply
cmra_validN_le
;
eauto
.
*
apply
cmra_included_includedN
;
auto
.
-
unseal
.
split
=>
n
x
y
??
=>
//= HP.
repeat
rewrite
/
uPred_holds
//=.
-
unseal
.
split
=>
n
x
y
??
=>
//=. intros (x1&x2&y1&y2&Heqx&Heqy&HP&HQ).
apply
HP
.
-
intros
P
Q
.
unseal
=>
HPQ
.
split
=>
n
x
y
??
?
.
auto
.
apply
HPQ
;
simpl
;
auto
using
@
cmra_core_validN
,
@
ucmra_unit_validN
.
-
intros
P
.
by
apply
persistent_intro
'
.
-
intros
.
unseal
;
split
=>
n
x
y
??
.
simpl
;
try
naive_solver
.
-
intros
.
unseal
;
split
=>
n
x
y
??
.
simpl
;
try
naive_solver
.
-
unseal
.
split
=>
n
x
y
??
=>
//=.
-
intros
.
unseal
;
split
=>
n
x
y
??
.
intros
(
x1
&
x2
&
y1
&
y2
&
Heq1
&
Heq2
&
HP
&
HQ
).
...
...
@@ -86,10 +61,10 @@ Proof.
*
done
.
Qed
.
Lemma
uPred_sbi_mixin
(
M
:
ucmraT
)
:
SbiMixin
(
ofe_mixin_of
(
uPred
M
))
uPred_entails
uPred_pure
uPred_and
uPred_or
uPred_impl
Lemma
uPred_sbi_mixin
(
M
:
ucmraT
)
:
SbiMixin
uPred_entails
uPred_pure
uPred_or
uPred_impl
(
@
uPred_forall
M
)
(
@
uPred_exist
M
)
uPred_sep
uPred_wand
uPred_plainly
uPred_persistent
(
@
uPred_eq
M
)
uPred_sep
uPred_persistent
(
@
uPred_eq
M
)
uPred_later
.
Proof
.
split
;
try
apply
_
;
eauto
with
I
.
...
...
@@ -101,13 +76,6 @@ Proof.
-
by
unseal
.
-
(
*
Discrete
a
→
a
≡
b
⊣⊢
⌜
a
≡
b
⌝
*
)
intros
A
a
b
?
.
unseal
;
split
=>
n
x
y
??
;
by
apply
(
discrete_iff
n
).
-
unseal
;
split
=>
n
x
y
??
[
HPQ
HQP
].
rewrite
/
uPred_holds
//= in HPQ HQP.
split
=>
n
'
x
'
y
'
Hle1
Hvalidx
Hvalidy
;
split
.
*
intros
.
specialize
(
HPQ
n
'
x
'
y
'
Hle1
).
rewrite
?
left_id
in
HPQ
*
=>
HPQ
.
apply
HPQ
;
eauto
.
*
intros
.
specialize
(
HQP
n
'
x
'
y
'
Hle1
).
rewrite
?
left_id
in
HQP
*
=>
HQP
.
apply
HQP
;
eauto
.
-
by
unseal
.
-
by
unseal
.
-
apply
later_mono
.
...
...
@@ -121,8 +89,6 @@ Proof.
-
intros
;
by
rewrite
later_sep
.
-
by
unseal
.
-
by
unseal
.
-
by
unseal
.
-
by
unseal
.
-
(
*
▷
P
⊢
▷
False
∨
(
▷
False
→
P
)
*
)
intros
P
.
unseal
;
split
=>
-
[
|
n
]
x
y
??
/=
HP
;
[
by
left
|
right
].
intros
[
|
n
'
]
x
'
y
'
????
;
[
|
done
].
...
...
theories/chan_lang/refine_heap_proofmode.v
View file @
0124939d
...
...
@@ -638,7 +638,7 @@ Tactic Notation "refine_alloc" constr(dnew) ident(l) "as" constr(H) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
first
[
intros
l
|
fail
1
"refine_alloc:"
l
"not fresh"
];
eexists
;
split
;
...
...
@@ -664,7 +664,7 @@ Tactic Notation "refine_recv" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
case
cleft
;
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -684,7 +684,7 @@ Tactic Notation "refine_recv_miss" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
case
cleft
;
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -705,7 +705,7 @@ Tactic Notation "refine_send" constr(dnew) :=
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_send: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_send: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -726,7 +726,7 @@ Tactic Notation "refine_select" constr(dnew) :=
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_select: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_select: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -747,7 +747,7 @@ Tactic Notation "refine_rcase_left" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
case
cleft
;
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -768,7 +768,7 @@ Tactic Notation "refine_rcase_right" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
case
cleft
;
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -789,7 +789,7 @@ Tactic Notation "refine_rcase_miss" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
env_cbv
;
eauto
|
case
cleft
;
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -813,7 +813,7 @@ Tactic Notation "refine_rec" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_lam: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
...
...
@@ -838,7 +838,7 @@ Tactic Notation "refine_lam" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_lam: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
...
...
@@ -869,7 +869,7 @@ Tactic Notation "refine_letp" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
...
...
@@ -889,7 +889,7 @@ Tactic Notation "refine_delay" constr(dnew) :=
[
try
omega
|
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
eauto
|
]
...
...
@@ -920,7 +920,7 @@ Tactic Notation "refine_op" constr(dnew) :=
|
fail
1
"refine_op: cannot find 'BinOp' or 'UnOp' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_suc: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_suc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
rewrite
/=
?
to_of_val
;
fast_done
|
env_cbv
;
reflexivity
...
...
@@ -942,7 +942,7 @@ Tactic Notation "refine_fork" constr(dnew) ident(t) "as" constr(H) :=
|
fail
1
"refine_fork: cannot find 'Fork' in "
e0
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fork: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fork: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
first
[
intros
t
|
fail
1
"refine_fork:"
t
"not fresh"
];
eexists
;
split
;
...
...
@@ -959,7 +959,7 @@ Ltac refine_stopped :=
|
|-
context
[
Esnoc
_
_
(
ownT
?
i
?
e
?
K
?
d0
)]
=>
eapply
tac_refine_stopped
with
_
i
e
_
;
[
wp_done
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_stopped: non-affine ctxt"
]
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_stopped: non-affine ctxt"
]
end
.
Tactic
Notation
"refine_if_true"
constr
(
dnew
)
:=
...
...
@@ -974,7 +974,7 @@ Tactic Notation "refine_if_true" constr(dnew) :=
|
fail
1
"refine_if_true: cannot find 'If' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_if_true: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_if_true: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -993,7 +993,7 @@ Tactic Notation "refine_if_false" constr(dnew) :=
|
fail
1
"refine_if_false: cannot find 'If' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_if_true: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_if_true: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
theories/heap_lang/refine_proofmode.v
View file @
0124939d
...
...
@@ -511,7 +511,7 @@ Tactic Notation "refine_alloc" constr(dnew) ident(l) "as" constr(H) :=
|
wp_done
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_alloc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
first
[
intros
l
|
fail
1
"refine_alloc:"
l
"not fresh"
];
eexists
;
split
;
...
...
@@ -537,7 +537,7 @@ Tactic Notation "refine_load" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_load: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -558,7 +558,7 @@ Tactic Notation "refine_store" constr(dnew) :=
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_store: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_store: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -584,7 +584,7 @@ Tactic Notation "refine_cas_fail" constr(dnew) :=
|
iAssumptionCore
|
iAssumptionCore
|
try
congruence
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_fail: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_fail: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -610,7 +610,7 @@ Tactic Notation "refine_cas_suc" constr(dnew) :=
|
iAssumptionCore
|
iAssumptionCore
|
try
congruence
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_suc: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_cas_suc: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -631,7 +631,7 @@ Tactic Notation "refine_swap" constr(dnew) :=
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_swap: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_swap: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -652,7 +652,7 @@ Tactic Notation "refine_fai" constr(dnew) :=
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fai: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fai: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -676,7 +676,7 @@ Tactic Notation "refine_rec" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_rec: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
...
...
@@ -700,7 +700,7 @@ Tactic Notation "refine_lam" constr(dnew) :=
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_rec: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
...
...
@@ -722,7 +722,7 @@ Tactic Notation "refine_delay" constr(dnew) :=
[
try
omega
|
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_delay: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_delay: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
eauto
|
]
...
...
@@ -752,7 +752,7 @@ Tactic Notation "refine_op" constr(dnew) :=
|
fail
1
"refine_op: cannot find 'BinOp' or 'UnOp' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_op: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_op: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
|
env_cbv
;
reflexivity
...
...
@@ -776,7 +776,7 @@ Tactic Notation "refine_proj" constr(dnew) :=
|
fail
1
"refine_proj: cannot find 'Fst' or 'Snd' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_proj: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_proj: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
wp_done
|
wp_done
...
...
@@ -798,7 +798,7 @@ Tactic Notation "refine_fork" constr(dnew) ident(t) "as" constr(H) :=
|
fail
1
"refine_fork: cannot find 'Fork' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fork: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_fork: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
first
[
intros
t
|
fail
1
"refine_fork:"
t
"not fresh"
];
eexists
;
split
;
...
...
@@ -815,7 +815,7 @@ Ltac refine_stopped :=
|
|-
context
[
Esnoc
_
_
(
ownT
?
i
?
e
?
K
?
d0
)]
=>
eapply
tac_refine_stopped
with
_
i
e
_
;
[
wp_done
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_stopped: non-affine ctxt"
]
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine_stopped: non-affine ctxt"
]
end
.
Tactic
Notation
"refine_if_true"
constr
(
dnew
)
:=
...
...
@@ -830,7 +830,7 @@ Tactic Notation "refine_if_true" constr(dnew) :=
|
fail
1
"refine_if_true: cannot find 'If' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
@@ -849,7 +849,7 @@ Tactic Notation "refine_if_false" constr(dnew) :=
|
fail
1
"refine_if_false: cannot find 'If' in "
e
];
[
try
omega
|
try
omega
|
iAssumptionCore
||
fail
"cannot find sheap_ctx"
|
iAssumptionCore
|
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine: non-affine ctxt"
|
env_cbv
;
iAlways
;
by
apply
envs_entails_of_envs_refl
||
fail
"refine: non-affine ctxt"
|
done
||
eauto
with
ndisj
|
env_cbv
;
reflexivity
|
rewrite
-
ownT_fill
;
simpl
ectx_language
.
fill
]
...
...
theories/program_logic/pviewshifts.v
View file @
0124939d
...
...
@@ -326,8 +326,23 @@ Section proofmode_classes.
Global
Instance
is_except_0_pvs
E1
E2
P
:
IsExcept0
(
|={
E1
,
E2
}=>
P
).
Proof
.
rewrite
/
IsExcept0
.
apply
except_0_pvs
.
Qed
.
Global
Instance
from_modal_pvs
E
P
:
FromModal
(
|={
E
}=>
P
)
P
.
Proof
.
rewrite
/
FromModal
.
apply
pvs_intro
.
Qed
.
Lemma
modality_pvs_mixin
E
:
modality_mixin
(
@
pvs
Λ
Σ
E
E
)
MIEnvId
MIEnvId
.
Proof
.
split
.
-
intros
P
.
apply
pvs_intro
.
-
intros
P
.
apply
pvs_intro
.
-
apply
pvs_intro
.
-
intros
P
Q
?
.
by
apply
pvs_mono
.
-
intros
P
Q
.
by
apply
pvs_sep
.
Qed
.
Definition
modality_pvs
E
:=
Modality
_
(
modality_pvs_mixin
E
).
Global
Instance
from_modal_pvs
E
P
:
FromModal
(
modality_pvs
E
)
(
True
:
iProp
Λ
Σ
)
%
I
(
|={
E
}=>
P
)
%
I
P
.
Proof
.
rewrite
/
FromModal
=>
//=. Qed.
Global
Instance
elim_modal_pvs_pvs
E1
E2
E3
P
Q
:
ElimModal
(
E2
⊆
E1
∪
E3
)
(
|={
E1
,
E2
}=>
P
)
P
(
|={
E1
,
E3
}=>
Q
)
(
|={
E2
,
E3
}=>
Q
).
...
...
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