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
George Pirlea
Iris
Commits
2cfaecf6
Commit
2cfaecf6
authored
Mar 03, 2018
by
Jacques-Henri Jourdan
Browse files
Get rid of KnownFrame and iFrame automatically instantiating evars.
parent
1ac24719
Changes
6
Hide whitespace changes
Inline
Side-by-side
theories/program_logic/total_weakestpre.v
View file @
2cfaecf6
...
...
@@ -378,8 +378,8 @@ Section proofmode_classes.
Global
Instance
frame_twp
p
s
E
e
R
Φ
Ψ
:
(
∀
v
,
Frame
p
R
(
Φ
v
)
(
Ψ
v
))
→
Known
Frame
p
R
(
WP
e
@
s
;
E
[{
Φ
}])
(
WP
e
@
s
;
E
[{
Ψ
}]).
Proof
.
rewrite
/
KnownFrame
/
Frame
=>
HR
.
rewrite
twp_frame_l
.
apply
twp_mono
,
HR
.
Qed
.
Frame
p
R
(
WP
e
@
s
;
E
[{
Φ
}])
(
WP
e
@
s
;
E
[{
Ψ
}]).
Proof
.
rewrite
/
Frame
=>
HR
.
rewrite
twp_frame_l
.
apply
twp_mono
,
HR
.
Qed
.
Global
Instance
is_except_0_wp
s
E
e
Φ
:
IsExcept0
(
WP
e
@
s
;
E
[{
Φ
}]).
Proof
.
by
rewrite
/
IsExcept0
-{
2
}
fupd_twp
-
except_0_fupd
-
fupd_intro
.
Qed
.
...
...
theories/program_logic/weakestpre.v
View file @
2cfaecf6
...
...
@@ -372,8 +372,8 @@ Section proofmode_classes.
Global
Instance
frame_wp
p
s
E
e
R
Φ
Ψ
:
(
∀
v
,
Frame
p
R
(
Φ
v
)
(
Ψ
v
))
→
Known
Frame
p
R
(
WP
e
@
s
;
E
{{
Φ
}})
(
WP
e
@
s
;
E
{{
Ψ
}}).
Proof
.
rewrite
/
KnownFrame
/
Frame
=>
HR
.
rewrite
wp_frame_l
.
apply
wp_mono
,
HR
.
Qed
.
Frame
p
R
(
WP
e
@
s
;
E
{{
Φ
}})
(
WP
e
@
s
;
E
{{
Ψ
}}).
Proof
.
rewrite
/
Frame
=>
HR
.
rewrite
wp_frame_l
.
apply
wp_mono
,
HR
.
Qed
.
Global
Instance
is_except_0_wp
s
E
e
Φ
:
IsExcept0
(
WP
e
@
s
;
E
{{
Φ
}}).
Proof
.
by
rewrite
/
IsExcept0
-{
2
}
fupd_wp
-
except_0_fupd
-
fupd_intro
.
Qed
.
...
...
theories/proofmode/class_instances.v
View file @
2cfaecf6
...
...
@@ -716,25 +716,25 @@ Proof.
Qed
.
(* Frame *)
Global
Instance
frame_here_absorbing
p
R
:
Absorbing
R
→
Known
Frame
p
R
R
True
|
0
.
Proof
.
intros
.
by
rewrite
/
KnownFrame
/
Frame
affinely_persistently_if_elim
sep_elim_l
.
Qed
.
Global
Instance
frame_here
p
R
:
Known
Frame
p
R
R
emp
|
1
.
Proof
.
intros
.
by
rewrite
/
KnownFrame
/
Frame
affinely_persistently_if_elim
sep_elim_l
.
Qed
.
Global
Instance
frame_here_absorbing
p
R
:
Absorbing
R
→
Frame
p
R
R
True
|
0
.
Proof
.
intros
.
by
rewrite
/
Frame
affinely_persistently_if_elim
sep_elim_l
.
Qed
.
Global
Instance
frame_here
p
R
:
Frame
p
R
R
emp
|
1
.
Proof
.
intros
.
by
rewrite
/
Frame
affinely_persistently_if_elim
sep_elim_l
.
Qed
.
Global
Instance
frame_affinely_here_absorbing
p
R
:
Absorbing
R
→
Known
Frame
p
(
bi_affinely
R
)
R
True
|
0
.
Absorbing
R
→
Frame
p
(
bi_affinely
R
)
R
True
|
0
.
Proof
.
intros
.
rewrite
/
KnownFrame
/
Frame
affinely_persistently_if_elim
affinely_elim
.
intros
.
rewrite
/
Frame
affinely_persistently_if_elim
affinely_elim
.
apply
sep_elim_l
,
_
.
Qed
.
Global
Instance
frame_affinely_here
p
R
:
Known
Frame
p
(
bi_affinely
R
)
R
emp
|
1
.
Global
Instance
frame_affinely_here
p
R
:
Frame
p
(
bi_affinely
R
)
R
emp
|
1
.
Proof
.
intros
.
rewrite
/
KnownFrame
/
Frame
affinely_persistently_if_elim
affinely_elim
.
intros
.
rewrite
/
Frame
affinely_persistently_if_elim
affinely_elim
.
apply
sep_elim_l
,
_
.
Qed
.
Global
Instance
frame_here_pure
p
φ
Q
:
FromPure
false
Q
φ
→
Known
Frame
p
⌜φ⌝
Q
True
.
Global
Instance
frame_here_pure
p
φ
Q
:
FromPure
false
Q
φ
→
Frame
p
⌜φ⌝
Q
True
.
Proof
.
rewrite
/
FromPure
/
KnownFrame
/
Frame
=>
<-.
rewrite
/
FromPure
/
Frame
=>
<-.
by
rewrite
affinely_persistently_if_elim
sep_elim_l
.
Qed
.
...
...
@@ -749,16 +749,14 @@ Global Instance make_embed_default `{BiEmbed PROP PROP'} P :
Proof
.
by
rewrite
/
MakeEmbed
.
Qed
.
Global
Instance
frame_embed
`
{
BiEmbed
PROP
PROP'
}
p
P
Q
(
Q'
:
PROP'
)
R
:
Frame
p
R
P
Q
→
MakeEmbed
Q
Q'
→
Known
Frame
p
⎡
R
⎤
⎡
P
⎤
Q'
.
Frame
p
R
P
Q
→
MakeEmbed
Q
Q'
→
Frame
p
⎡
R
⎤
⎡
P
⎤
Q'
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeEmbed
=>
<-
<-.
rewrite
/
Frame
/
MakeEmbed
=>
<-
<-.
rewrite
embed_sep
embed_affinely_if
embed_persistently_if
=>
//.
Qed
.
Global
Instance
frame_pure_embed
`
{
BiEmbed
PROP
PROP'
}
p
P
Q
(
Q'
:
PROP'
)
φ
:
Frame
p
⌜φ⌝
P
Q
→
MakeEmbed
Q
Q'
→
KnownFrame
p
⌜φ⌝
⎡
P
⎤
Q'
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeEmbed
-
embed_pure
.
apply
(
frame_embed
p
P
Q
).
Qed
.
Frame
p
⌜φ⌝
P
Q
→
MakeEmbed
Q
Q'
→
Frame
p
⌜φ⌝
⎡
P
⎤
Q'
.
Proof
.
rewrite
/
Frame
/
MakeEmbed
-
embed_pure
.
apply
(
frame_embed
p
P
Q
).
Qed
.
Global
Instance
make_sep_emp_l
P
:
KnownLMakeSep
emp
P
P
.
Proof
.
apply
left_id
,
_
.
Qed
.
...
...
@@ -777,31 +775,31 @@ Proof. by rewrite /MakeSep. Qed.
Global
Instance
frame_sep_persistent_l
progress
R
P1
P2
Q1
Q2
Q'
:
Frame
true
R
P1
Q1
→
MaybeFrame
true
R
P2
Q2
progress
→
MakeSep
Q1
Q2
Q'
→
Known
Frame
true
R
(
P1
∗
P2
)
Q'
|
9
.
Frame
true
R
(
P1
∗
P2
)
Q'
|
9
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MaybeFrame
/
MakeSep
/=
=>
<-
<-
<-.
rewrite
/
Frame
/
MaybeFrame
/
MakeSep
/=
=>
<-
<-
<-.
rewrite
{
1
}(
affinely_persistently_sep_dup
R
).
solve_sep_entails
.
Qed
.
Global
Instance
frame_sep_l
R
P1
P2
Q
Q'
:
Frame
false
R
P1
Q
→
MakeSep
Q
P2
Q'
→
Known
Frame
false
R
(
P1
∗
P2
)
Q'
|
9
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeSep
=>
<-
<-.
by
rewrite
assoc
.
Qed
.
Frame
false
R
P1
Q
→
MakeSep
Q
P2
Q'
→
Frame
false
R
(
P1
∗
P2
)
Q'
|
9
.
Proof
.
rewrite
/
Frame
/
MakeSep
=>
<-
<-.
by
rewrite
assoc
.
Qed
.
Global
Instance
frame_sep_r
p
R
P1
P2
Q
Q'
:
Frame
p
R
P2
Q
→
MakeSep
P1
Q
Q'
→
Known
Frame
p
R
(
P1
∗
P2
)
Q'
|
10
.
Frame
p
R
P2
Q
→
MakeSep
P1
Q
Q'
→
Frame
p
R
(
P1
∗
P2
)
Q'
|
10
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeSep
=>
<-
<-.
by
rewrite
assoc
-(
comm
_
P1
)
assoc
.
rewrite
/
Frame
/
MakeSep
=>
<-
<-.
by
rewrite
assoc
-(
comm
_
P1
)
assoc
.
Qed
.
Global
Instance
frame_big_sepL_cons
{
A
}
p
(
Φ
:
nat
→
A
→
PROP
)
R
Q
l
x
l'
:
IsCons
l
x
l'
→
Frame
p
R
(
Φ
0
x
∗
[
∗
list
]
k
↦
y
∈
l'
,
Φ
(
S
k
)
y
)
Q
→
Known
Frame
p
R
([
∗
list
]
k
↦
y
∈
l
,
Φ
k
y
)
Q
.
Proof
.
rewrite
/
IsCons
=>->.
by
rewrite
/
KnownFrame
/
Frame
big_sepL_cons
.
Qed
.
Frame
p
R
([
∗
list
]
k
↦
y
∈
l
,
Φ
k
y
)
Q
.
Proof
.
rewrite
/
IsCons
=>->.
by
rewrite
/
Frame
big_sepL_cons
.
Qed
.
Global
Instance
frame_big_sepL_app
{
A
}
p
(
Φ
:
nat
→
A
→
PROP
)
R
Q
l
l1
l2
:
IsApp
l
l1
l2
→
Frame
p
R
(([
∗
list
]
k
↦
y
∈
l1
,
Φ
k
y
)
∗
[
∗
list
]
k
↦
y
∈
l2
,
Φ
(
length
l1
+
k
)
y
)
Q
→
Known
Frame
p
R
([
∗
list
]
k
↦
y
∈
l
,
Φ
k
y
)
Q
.
Proof
.
rewrite
/
IsApp
=>->.
by
rewrite
/
KnownFrame
/
Frame
big_opL_app
.
Qed
.
Frame
p
R
([
∗
list
]
k
↦
y
∈
l
,
Φ
k
y
)
Q
.
Proof
.
rewrite
/
IsApp
=>->.
by
rewrite
/
Frame
big_opL_app
.
Qed
.
Global
Instance
make_and_true_l
P
:
KnownLMakeAnd
True
P
P
.
Proof
.
apply
left_id
,
_
.
Qed
.
...
...
@@ -823,9 +821,9 @@ Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
MaybeFrame
p
R
P2
Q2
progress2
→
TCEq
(
progress1
||
progress2
)
true
→
MakeAnd
Q1
Q2
Q'
→
Known
Frame
p
R
(
P1
∧
P2
)
Q'
|
9
.
Frame
p
R
(
P1
∧
P2
)
Q'
|
9
.
Proof
.
rewrite
/
MaybeFrame
/
KnownFrame
/
Frame
/
MakeAnd
=>
<-
<-
_
<-.
apply
and_intro
;
rewrite
/
MaybeFrame
/
Frame
/
MakeAnd
=>
<-
<-
_
<-.
apply
and_intro
;
[
rewrite
and_elim_l
|
rewrite
and_elim_r
]
;
done
.
Qed
.
...
...
@@ -843,9 +841,9 @@ Proof. by rewrite /MakeOr. Qed.
(* We could in principle write the instance [frame_or_spatial] by a bunch of
instances, i.e. (omitting the parameter [p = false]):
Frame R P1 Q1 → Frame R P2 Q2 →
Known
Frame R (P1 ∨ P2) (Q1 ∨ Q2)
Frame R P1 True →
Known
Frame R (P1 ∨ P2) P2
Frame R P2 True →
Known
Frame R (P1 ∨ P2) P1
Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2)
Frame R P1 True → Frame R (P1 ∨ P2) P2
Frame R P2 True → Frame R (P1 ∨ P2) P1
The problem here is that Coq will try to infer [Frame R P1 ?] and [Frame R P2 ?]
multiple times, whereas the current solution makes sure that said inference
...
...
@@ -859,19 +857,19 @@ Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
(
TCAnd
(
TCEq
progress1
true
)
(
TCEq
Q1
True
%
I
))
(
TCAnd
(
TCEq
progress2
true
)
(
TCEq
Q2
True
%
I
)))
→
MakeOr
Q1
Q2
Q
→
Known
Frame
false
R
(
P1
∨
P2
)
Q
|
9
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeOr
=>
<-
<-
_
<-.
by
rewrite
-
sep_or_l
.
Qed
.
Frame
false
R
(
P1
∨
P2
)
Q
|
9
.
Proof
.
rewrite
/
Frame
/
MakeOr
=>
<-
<-
_
<-.
by
rewrite
-
sep_or_l
.
Qed
.
Global
Instance
frame_or_persistent
progress1
progress2
R
P1
P2
Q1
Q2
Q
:
MaybeFrame
true
R
P1
Q1
progress1
→
MaybeFrame
true
R
P2
Q2
progress2
→
TCEq
(
progress1
||
progress2
)
true
→
MakeOr
Q1
Q2
Q
→
Known
Frame
true
R
(
P1
∨
P2
)
Q
|
9
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeOr
=>
<-
<-
_
<-.
by
rewrite
-
sep_or_l
.
Qed
.
MakeOr
Q1
Q2
Q
→
Frame
true
R
(
P1
∨
P2
)
Q
|
9
.
Proof
.
rewrite
/
Frame
/
MakeOr
=>
<-
<-
_
<-.
by
rewrite
-
sep_or_l
.
Qed
.
Global
Instance
frame_wand
p
R
P1
P2
Q2
:
Frame
p
R
P2
Q2
→
Known
Frame
p
R
(
P1
-
∗
P2
)
(
P1
-
∗
Q2
).
Frame
p
R
P2
Q2
→
Frame
p
R
(
P1
-
∗
P2
)
(
P1
-
∗
Q2
).
Proof
.
rewrite
/
KnownFrame
/
Frame
=>
?.
apply
wand_intro_l
.
rewrite
/
Frame
=>
?.
apply
wand_intro_l
.
by
rewrite
assoc
(
comm
_
P1
)
-
assoc
wand_elim_r
.
Qed
.
...
...
@@ -883,9 +881,9 @@ Global Instance make_affinely_default P : MakeAffinely P (bi_affinely P) | 100.
Proof
.
by
rewrite
/
MakeAffinely
.
Qed
.
Global
Instance
frame_affinely
R
P
Q
Q'
:
Frame
true
R
P
Q
→
MakeAffinely
Q
Q'
→
Known
Frame
true
R
(
bi_affinely
P
)
Q'
.
Frame
true
R
P
Q
→
MakeAffinely
Q
Q'
→
Frame
true
R
(
bi_affinely
P
)
Q'
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeAffinely
=>
<-
<-
/=.
rewrite
/
Frame
/
MakeAffinely
=>
<-
<-
/=.
by
rewrite
-{
1
}
affinely_idemp
affinely_sep_2
.
Qed
.
...
...
@@ -901,9 +899,9 @@ Global Instance make_absorbingly_default P : MakeAbsorbingly P (bi_absorbingly P
Proof
.
by
rewrite
/
MakeAbsorbingly
.
Qed
.
Global
Instance
frame_absorbingly
p
R
P
Q
Q'
:
Frame
p
R
P
Q
→
MakeAbsorbingly
Q
Q'
→
Known
Frame
p
R
(
bi_absorbingly
P
)
Q'
.
Frame
p
R
P
Q
→
MakeAbsorbingly
Q
Q'
→
Frame
p
R
(
bi_absorbingly
P
)
Q'
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeAbsorbingly
=>
<-
<-
/=.
by
rewrite
absorbingly_sep_r
.
rewrite
/
Frame
/
MakeAbsorbingly
=>
<-
<-
/=.
by
rewrite
absorbingly_sep_r
.
Qed
.
Global
Instance
make_persistently_true
:
@
KnownMakePersistently
PROP
True
True
.
...
...
@@ -918,45 +916,38 @@ Global Instance make_persistently_default P :
Proof
.
by
rewrite
/
MakePersistently
.
Qed
.
Global
Instance
frame_persistently
R
P
Q
Q'
:
Frame
true
R
P
Q
→
MakePersistently
Q
Q'
→
Known
Frame
true
R
(
bi_persistently
P
)
Q'
.
Frame
true
R
P
Q
→
MakePersistently
Q
Q'
→
Frame
true
R
(
bi_persistently
P
)
Q'
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakePersistently
=>
<-
<-
/=.
rewrite
/
Frame
/
MakePersistently
=>
<-
<-
/=.
rewrite
-
persistently_and_affinely_sep_l
.
by
rewrite
-
persistently_sep_2
-
persistently_and_sep_l_1
persistently_affinely
persistently_idemp
.
Qed
.
Global
Instance
frame_exist
{
A
}
p
R
(
Φ
Ψ
:
A
→
PROP
)
:
(
∀
a
,
Frame
p
R
(
Φ
a
)
(
Ψ
a
))
→
Known
Frame
p
R
(
∃
x
,
Φ
x
)
(
∃
x
,
Ψ
x
).
Proof
.
rewrite
/
KnownFrame
/
Frame
=>
?.
by
rewrite
sep_exist_l
;
apply
exist_mono
.
Qed
.
(
∀
a
,
Frame
p
R
(
Φ
a
)
(
Ψ
a
))
→
Frame
p
R
(
∃
x
,
Φ
x
)
(
∃
x
,
Ψ
x
).
Proof
.
rewrite
/
Frame
=>
?.
by
rewrite
sep_exist_l
;
apply
exist_mono
.
Qed
.
Global
Instance
frame_forall
{
A
}
p
R
(
Φ
Ψ
:
A
→
PROP
)
:
(
∀
a
,
Frame
p
R
(
Φ
a
)
(
Ψ
a
))
→
Known
Frame
p
R
(
∀
x
,
Φ
x
)
(
∀
x
,
Ψ
x
).
Proof
.
rewrite
/
KnownFrame
/
Frame
=>
?.
by
rewrite
sep_forall_l
;
apply
forall_mono
.
Qed
.
(
∀
a
,
Frame
p
R
(
Φ
a
)
(
Ψ
a
))
→
Frame
p
R
(
∀
x
,
Φ
x
)
(
∀
x
,
Ψ
x
).
Proof
.
rewrite
/
Frame
=>
?.
by
rewrite
sep_forall_l
;
apply
forall_mono
.
Qed
.
Global
Instance
frame_impl_persistent
R
P1
P2
Q2
:
Frame
true
R
P2
Q2
→
Known
Frame
true
R
(
P1
→
P2
)
(
P1
→
Q2
).
Frame
true
R
P2
Q2
→
Frame
true
R
(
P1
→
P2
)
(
P1
→
Q2
).
Proof
.
rewrite
/
KnownFrame
/
Frame
/=
=>
?.
apply
impl_intro_l
.
rewrite
/
Frame
/=
=>
?.
apply
impl_intro_l
.
by
rewrite
-
persistently_and_affinely_sep_l
assoc
(
comm
_
P1
)
-
assoc
impl_elim_r
persistently_and_affinely_sep_l
.
Qed
.
Global
Instance
frame_impl
R
P1
P2
Q2
:
Persistent
P1
→
Absorbing
P1
→
Frame
false
R
P2
Q2
→
Known
Frame
false
R
(
P1
→
P2
)
(
P1
→
Q2
).
Frame
false
R
P2
Q2
→
Frame
false
R
(
P1
→
P2
)
(
P1
→
Q2
).
Proof
.
rewrite
/
KnownFrame
/
Frame
/==>
???.
apply
impl_intro_l
.
rewrite
/
Frame
/==>
???.
apply
impl_intro_l
.
rewrite
{
1
}(
persistent
P1
)
persistently_and_affinely_sep_l
assoc
.
rewrite
(
comm
_
(
□
P1
)%
I
)
-
assoc
-
persistently_and_affinely_sep_l
.
rewrite
persistently_elim
impl_elim_r
//.
Qed
.
(* In the case nothing else suceeded, then we try to instantiate the
evar [P] with [R ∗ Q]. This only does so in non-persistent mode:
The idea is that persistent assumptions will still be available
when [P] will be used, so there is no need to keep it in [P]. *)
Global
Instance
frame_sep_instantiate
R
Q
:
Frame
false
R
(
R
∗
Q
)
Q
|
100
.
Proof
.
by
rewrite
/
Frame
.
Qed
.
(* IntoEmbed *)
Global
Instance
into_embed_embed
{
PROP'
:
bi
}
`
{
BiEmbed
PROP
PROP'
}
P
:
IntoEmbed
⎡
P
⎤
P
.
...
...
@@ -1054,7 +1045,7 @@ Global Instance into_wand_later p q R P Q :
IntoWand
p
q
R
P
Q
→
IntoWand
p
q
(
▷
R
)
(
▷
P
)
(
▷
Q
).
Proof
.
rewrite
/
IntoWand
/=
=>
HR
.
by
rewrite
!
later_affinely_persistently_if_2
-
later_wand
HR
.
by
rewrite
!
later_affinely_persistently_if_2
-
later_wand
HR
.
Qed
.
Global
Instance
into_wand_later_args
p
q
R
P
Q
:
IntoWand
p
q
R
P
Q
→
IntoWand'
p
q
R
(
▷
P
)
(
▷
Q
).
...
...
@@ -1067,7 +1058,7 @@ Global Instance into_wand_laterN n p q R P Q :
IntoWand
p
q
R
P
Q
→
IntoWand
p
q
(
▷
^
n
R
)
(
▷
^
n
P
)
(
▷
^
n
Q
).
Proof
.
rewrite
/
IntoWand
/=
=>
HR
.
by
rewrite
!
laterN_affinely_persistently_if_2
-
laterN_wand
HR
.
by
rewrite
!
laterN_affinely_persistently_if_2
-
laterN_wand
HR
.
Qed
.
Global
Instance
into_wand_laterN_args
n
p
q
R
P
Q
:
IntoWand
p
q
R
P
Q
→
IntoWand'
p
q
R
(
▷
^
n
P
)
(
▷
^
n
Q
).
...
...
@@ -1506,8 +1497,8 @@ Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
(* Frame *)
Global
Instance
frame_eq_embed
`
{
SbiEmbed
PROP
PROP'
}
p
P
Q
(
Q'
:
PROP'
)
{
A
:
ofeT
}
(
a
b
:
A
)
:
Frame
p
(
a
≡
b
)
P
Q
→
MakeEmbed
Q
Q'
→
Known
Frame
p
(
a
≡
b
)
⎡
P
⎤
Q'
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeEmbed
-
embed_internal_eq
.
apply
(
frame_embed
p
P
Q
).
Qed
.
Frame
p
(
a
≡
b
)
P
Q
→
MakeEmbed
Q
Q'
→
Frame
p
(
a
≡
b
)
⎡
P
⎤
Q'
.
Proof
.
rewrite
/
Frame
/
MakeEmbed
-
embed_internal_eq
.
apply
(
frame_embed
p
P
Q
).
Qed
.
Global
Instance
make_laterN_true
n
:
@
KnownMakeLaterN
PROP
n
True
True
|
0
.
Proof
.
by
rewrite
/
KnownMakeLaterN
/
MakeLaterN
laterN_True
.
Qed
.
...
...
@@ -1520,25 +1511,25 @@ Proof. by rewrite /MakeLaterN. Qed.
Global
Instance
frame_later
p
R
R'
P
Q
Q'
:
NoBackTrack
(
MaybeIntoLaterN
true
1
R'
R
)
→
Frame
p
R
P
Q
→
MakeLaterN
1
Q
Q'
→
Known
Frame
p
R'
(
▷
P
)
Q'
.
Frame
p
R
P
Q
→
MakeLaterN
1
Q
Q'
→
Frame
p
R'
(
▷
P
)
Q'
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeLaterN
/
MaybeIntoLaterN
=>-[->]
<-
<-.
rewrite
/
Frame
/
MakeLaterN
/
MaybeIntoLaterN
=>-[->]
<-
<-.
by
rewrite
later_affinely_persistently_if_2
later_sep
.
Qed
.
Global
Instance
frame_laterN
p
n
R
R'
P
Q
Q'
:
NoBackTrack
(
MaybeIntoLaterN
true
n
R'
R
)
→
Frame
p
R
P
Q
→
MakeLaterN
n
Q
Q'
→
Known
Frame
p
R'
(
▷
^
n
P
)
Q'
.
Frame
p
R
P
Q
→
MakeLaterN
n
Q
Q'
→
Frame
p
R'
(
▷
^
n
P
)
Q'
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeLaterN
/
MaybeIntoLaterN
=>-[->]
<-
<-.
rewrite
/
Frame
/
MakeLaterN
/
MaybeIntoLaterN
=>-[->]
<-
<-.
by
rewrite
laterN_affinely_persistently_if_2
laterN_sep
.
Qed
.
Global
Instance
frame_bupd
`
{
BiBUpd
PROP
}
p
R
P
Q
:
Frame
p
R
P
Q
→
Known
Frame
p
R
(|==>
P
)
(|==>
Q
).
Proof
.
rewrite
/
KnownFrame
/
Frame
=><-.
by
rewrite
bupd_frame_l
.
Qed
.
Frame
p
R
P
Q
→
Frame
p
R
(|==>
P
)
(|==>
Q
).
Proof
.
rewrite
/
Frame
=><-.
by
rewrite
bupd_frame_l
.
Qed
.
Global
Instance
frame_fupd
`
{
BiFUpd
PROP
}
p
E1
E2
R
P
Q
:
Frame
p
R
P
Q
→
Known
Frame
p
R
(|={
E1
,
E2
}=>
P
)
(|={
E1
,
E2
}=>
Q
).
Proof
.
rewrite
/
KnownFrame
/
Frame
=><-.
by
rewrite
fupd_frame_l
.
Qed
.
Frame
p
R
P
Q
→
Frame
p
R
(|={
E1
,
E2
}=>
P
)
(|={
E1
,
E2
}=>
Q
).
Proof
.
rewrite
/
Frame
=><-.
by
rewrite
fupd_frame_l
.
Qed
.
Global
Instance
make_except_0_True
:
@
KnownMakeExcept0
PROP
True
True
.
Proof
.
by
rewrite
/
KnownMakeExcept0
/
MakeExcept0
except_0_True
.
Qed
.
...
...
@@ -1546,9 +1537,9 @@ Global Instance make_except_0_default P : MakeExcept0 P (◇ P) | 100.
Proof
.
by
rewrite
/
MakeExcept0
.
Qed
.
Global
Instance
frame_except_0
p
R
P
Q
Q'
:
Frame
p
R
P
Q
→
MakeExcept0
Q
Q'
→
Known
Frame
p
R
(
◇
P
)
Q'
.
Frame
p
R
P
Q
→
MakeExcept0
Q
Q'
→
Frame
p
R
(
◇
P
)
Q'
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeExcept0
=><-
<-.
rewrite
/
Frame
/
MakeExcept0
=><-
<-.
by
rewrite
except_0_sep
-(
except_0_intro
(
□
?p
R
)%
I
).
Qed
.
...
...
theories/proofmode/classes.v
View file @
2cfaecf6
...
...
@@ -254,19 +254,7 @@ Proof. done. Qed.
Class
Frame
{
PROP
:
bi
}
(
p
:
bool
)
(
R
P
Q
:
PROP
)
:
=
frame
:
□
?p
R
∗
Q
⊢
P
.
Arguments
Frame
{
_
}
_
_
%
I
_
%
I
_
%
I
.
Arguments
frame
{
_
_
}
_
%
I
_
%
I
_
%
I
{
_
}.
(* [P] has - hint mode even though it is morally an input. In the case
P is an evar, it will be instantiated with [R * ?P'], where [?P']
is a new evar. This mechanism should be the only instance able to
instanciate [P] when it is an evar. *)
Hint
Mode
Frame
+
+
!
-
-
:
typeclass_instances
.
(* [KnownFrame] is like [Frame], but with an [Hint Mode] that make
sure we do not instantiate [P]. *)
Class
KnownFrame
{
PROP
:
bi
}
(
p
:
bool
)
(
R
P
Q
:
PROP
)
:
=
known_frame
:
>
Frame
p
R
P
Q
.
Arguments
KnownFrame
{
_
}
_
_
%
I
_
%
I
_
%
I
.
Arguments
known_frame
{
_
_
}
_
%
I
_
%
I
_
%
I
{
_
}.
Hint
Mode
KnownFrame
+
+
!
!
-
:
typeclass_instances
.
Hint
Mode
Frame
+
+
!
!
-
:
typeclass_instances
.
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
...
...
theories/proofmode/monpred.v
View file @
2cfaecf6
...
...
@@ -332,16 +332,16 @@ Qed.
search, and hence performance issues. *)
Global
Instance
frame_monPred_at
p
P
Q
𝓠
R
i
j
:
IsBiIndexRel
i
j
→
Frame
p
R
P
Q
→
MakeMonPredAt
j
Q
𝓠
→
Known
Frame
p
(
R
i
)
(
P
j
)
𝓠
.
Frame
p
(
R
i
)
(
P
j
)
𝓠
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeMonPredAt
/
bi_affinely_if
/
bi_persistently_if
rewrite
/
Frame
/
MakeMonPredAt
/
bi_affinely_if
/
bi_persistently_if
/
IsBiIndexRel
=>
Hij
<-
<-.
destruct
p
;
by
rewrite
Hij
monPred_at_sep
?monPred_at_affinely
?monPred_at_persistently
.
Qed
.
Global
Instance
frame_monPred_at_embed
i
p
P
Q
𝓠
𝓡
:
Frame
p
⎡𝓡⎤
P
Q
→
MakeMonPredAt
i
Q
𝓠
→
Known
Frame
p
𝓡
(
P
i
)
𝓠
.
Frame
p
⎡𝓡⎤
P
Q
→
MakeMonPredAt
i
Q
𝓠
→
Frame
p
𝓡
(
P
i
)
𝓠
.
Proof
.
rewrite
/
KnownFrame
/
Frame
/
MakeMonPredAt
/
bi_affinely_if
/
bi_persistently_if
=>
<-
<-.
rewrite
/
Frame
/
MakeMonPredAt
/
bi_affinely_if
/
bi_persistently_if
=>
<-
<-.
destruct
p
;
by
rewrite
monPred_at_sep
?monPred_at_affinely
?monPred_at_persistently
monPred_at_embed
.
Qed
.
...
...
theories/tests/proofmode.v
View file @
2cfaecf6
...
...
@@ -370,15 +370,15 @@ Proof.
Qed
.
Lemma
iFrame_with_evar_r
P
Q
:
∃
R
,
(
P
-
∗
Q
-
∗
P
∗
R
)
∧
R
=
(
Q
∗
emp
)%
I
.
∃
R
,
(
P
-
∗
Q
-
∗
P
∗
R
)
∧
R
=
Q
.
Proof
.
eexists
.
split
.
iIntros
"HP HQ"
.
iFrame
.
i
EmpIntro
.
done
.
eexists
.
split
.
iIntros
"HP HQ"
.
iFrame
.
i
Apply
"HQ"
.
done
.
Qed
.
Lemma
iFrame_with_evar_l
P
Q
:
∃
R
,
(
P
-
∗
Q
-
∗
R
∗
P
)
∧
R
=
(
Q
∗
emp
)%
I
.
∃
R
,
(
P
-
∗
Q
-
∗
R
∗
P
)
∧
R
=
Q
.
Proof
.
eexists
.
split
.
iIntros
"HP HQ"
.
iFrame
"HQ"
.
iSplitR
.
iEmpIntro
.
done
.
done
.
eexists
.
split
.
iIntros
"HP HQ"
.
Fail
iFrame
"HQ"
.
by
iSplitR
"HP"
.
done
.
Qed
.
Lemma
iFrame_with_evar_persistent
P
Q
:
∃
R
,
(
P
-
∗
□
Q
-
∗
P
∗
R
∗
Q
)
∧
R
=
emp
%
I
.
...
...
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