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
e0a45a07
Commit
e0a45a07
authored
Jan 22, 2017
by
Jacques-Henri Jourdan
Browse files
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
parents
5ffa64f9
626a2258
Changes
14
Hide whitespace changes
Inline
Side-by-side
theories/algebra/cmra.v
View file @
e0a45a07
...
...
@@ -130,10 +130,12 @@ Infix "⋅?" := opM (at level 50, left associativity) : C_scope.
(** * Persistent elements *)
Class
Persistent
{
A
:
cmraT
}
(
x
:
A
)
:
=
persistent
:
pcore
x
≡
Some
x
.
Arguments
persistent
{
_
}
_
{
_
}.
Hint
Mode
Persistent
+
!
:
typeclass_instances
.
(** * Exclusive elements (i.e., elements that cannot have a frame). *)
Class
Exclusive
{
A
:
cmraT
}
(
x
:
A
)
:
=
exclusive0_l
y
:
✓
{
0
}
(
x
⋅
y
)
→
False
.
Arguments
exclusive0_l
{
_
}
_
{
_
}
_
_
.
Hint
Mode
Exclusive
+
!
:
typeclass_instances
.
(** * CMRAs whose core is total *)
(** The function [core] may return a dummy when used on CMRAs without total
...
...
@@ -545,7 +547,7 @@ Section ucmra.
Global
Instance
cmra_unit_total
:
CMRATotal
A
.
Proof
.
intros
x
.
destruct
(
cmra_pcore_mono'
∅
x
∅
)
as
(
cx
&->&?)
;
eauto
using
ucmra_unit_least
,
(
persistent
∅
).
eauto
using
ucmra_unit_least
,
(
persistent
(
∅
:
A
)
).
Qed
.
End
ucmra
.
Hint
Immediate
cmra_unit_total
.
...
...
theories/algebra/ofe.v
View file @
e0a45a07
...
...
@@ -72,8 +72,10 @@ Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
(** Discrete OFEs and Timeless elements *)
(* TODO: On paper, We called these "discrete elements". I think that makes
more sense. *)
Class
Timeless
`
{
Equiv
A
,
Dist
A
}
(
x
:
A
)
:
=
timeless
y
:
x
≡
{
0
}
≡
y
→
x
≡
y
.
Arguments
timeless
{
_
_
_
}
_
{
_
}
_
_
.
Class
Timeless
{
A
:
ofeT
}
(
x
:
A
)
:
=
timeless
y
:
x
≡
{
0
}
≡
y
→
x
≡
y
.
Arguments
timeless
{
_
}
_
{
_
}
_
_
.
Hint
Mode
Timeless
+
!
:
typeclass_instances
.
Class
Discrete
(
A
:
ofeT
)
:
=
discrete_timeless
(
x
:
A
)
:
>
Timeless
x
.
(** OFEs with a completion *)
...
...
@@ -1029,12 +1031,13 @@ Section sigma.
Global
Instance
sig_timeless
(
x
:
sig
P
)
:
Timeless
(
proj1_sig
x
)
→
Timeless
x
.
Proof
.
intros
?
y
.
destruct
x
,
y
.
unfold
dist
,
sig_dist
,
equiv
,
sig_equiv
.
apply
(
timeless
_
).
Qed
.
Global
Instance
sig_discrete_cofe
:
Discrete
A
→
Discrete
sigC
.
Proof
.
intros
?
[??]
[??].
rewrite
/
dist
/
equiv
/
ofe_dist
/
ofe_equiv
/=.
rewrite
/
sig_dist
/
sig_equiv
/=.
apply
discrete_timeless
.
Qed
.
intros
?
[
b
?]
;
destruct
x
as
[
a
?].
rewrite
/
dist
/
ofe_dist
/=
/
sig_dist
/
equiv
/
ofe_equiv
/=
/
sig_equiv
/=.
apply
(
timeless
_
).
Qed
.
Global
Instance
sig_discrete_cofe
:
Discrete
A
→
Discrete
sigC
.
Proof
.
intros
??.
apply
_
.
Qed
.
End
sigma
.
Arguments
sigC
{
_
}
_
.
theories/algebra/vector.v
View file @
e0a45a07
...
...
@@ -12,10 +12,10 @@ Section ofe.
Definition
vec_ofe_mixin
m
:
OfeMixin
(
vec
A
m
).
Proof
.
split
.
-
intros
x
y
.
apply
(
equiv_dist
(
A
:
=
listC
A
)).
-
intros
v
w
.
apply
(
equiv_dist
(
A
:
=
listC
A
)).
-
unfold
dist
,
vec_dist
.
split
.
by
intros
?.
by
intros
??.
by
intros
?????
;
etrans
.
-
intros
.
by
apply
(
dist_S
(
A
:
=
listC
A
)).
-
intros
n
v
w
.
by
apply
(
dist_S
(
A
:
=
listC
A
)).
Qed
.
Canonical
Structure
vecC
m
:
ofeT
:
=
OfeT
(
vec
A
m
)
(
vec_ofe_mixin
m
).
...
...
@@ -48,22 +48,21 @@ Section proper.
Proper
(
dist
n
==>
eq
==>
dist
n
)
(@
Vector
.
nth
A
m
).
Proof
.
intros
v
.
induction
v
as
[|
x
m
v
IH
]
;
intros
v'
;
inv_vec
v'
.
-
intros
_
x
.
inversion
x
.
-
intros
x'
v'
EQ
i
?
<-.
inversion_clear
EQ
.
inv_fin
i
;
first
done
.
intros
i
.
by
apply
IH
.
-
intros
_
x
.
inv_fin
x
.
-
intros
x'
v'
EQ
i
?
<-.
inversion_clear
EQ
.
inv_fin
i
=>
//
i
.
by
apply
IH
.
Qed
.
Global
Instance
vlookup_proper
m
:
Proper
(
equiv
==>
eq
==>
equiv
)
(@
Vector
.
nth
A
m
).
Proof
.
intros
??????
.
apply
equiv_dist
=>
?.
subst
.
f_equiv
.
by
apply
equiv_dist
.
intros
v
v'
?
x
x'
->
.
apply
equiv_dist
=>
n
.
f_equiv
.
by
apply
equiv_dist
.
Qed
.
Global
Instance
vec_to_list_ne
n
m
:
Proper
(
dist
n
==>
dist
n
)
(@
vec_to_list
A
m
).
Proof
.
intros
??
H
.
apply
H
.
Qed
.
Proof
.
by
intros
v
v'
.
Qed
.
Global
Instance
vec_to_list_proper
m
:
Proper
(
equiv
==>
equiv
)
(@
vec_to_list
A
m
).
Proof
.
intros
??
H
.
apply
H
.
Qed
.
Proof
.
by
intros
v
v'
.
Qed
.
End
proper
.
Section
cofe
.
...
...
@@ -95,7 +94,7 @@ Instance vec_map_ne {A B : ofeT} m f n :
Proper
(
dist
n
==>
dist
n
)
f
→
Proper
(
dist
n
==>
dist
n
)
(@
vec_map
A
B
m
f
).
Proof
.
intros
?
??
H
.
eapply
list_fmap_ne
in
H
;
last
done
.
intros
?
v
v'
H
.
eapply
list_fmap_ne
in
H
;
last
done
.
by
rewrite
-!
vec_to_list_map
in
H
.
Qed
.
Definition
vecC_map
{
A
B
:
ofeT
}
m
(
f
:
A
-
n
>
B
)
:
vecC
A
m
-
n
>
vecC
B
m
:
=
...
...
theories/base_logic/big_op.v
View file @
e0a45a07
...
...
@@ -115,10 +115,12 @@ Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) X (λ x, P))
Class
PersistentL
{
M
}
(
Ps
:
list
(
uPred
M
))
:
=
persistentL
:
Forall
PersistentP
Ps
.
Arguments
persistentL
{
_
}
_
{
_
}.
Hint
Mode
PersistentL
+
!
:
typeclass_instances
.
Class
TimelessL
{
M
}
(
Ps
:
list
(
uPred
M
))
:
=
timelessL
:
Forall
TimelessP
Ps
.
Arguments
timelessL
{
_
}
_
{
_
}.
Hint
Mode
TimelessP
+
!
:
typeclass_instances
.
(** * Properties *)
Section
big_op
.
...
...
theories/base_logic/derived.v
View file @
e0a45a07
...
...
@@ -31,10 +31,12 @@ Typeclasses Opaque uPred_except_0.
Class
TimelessP
{
M
}
(
P
:
uPred
M
)
:
=
timelessP
:
▷
P
⊢
◇
P
.
Arguments
timelessP
{
_
}
_
{
_
}.
Hint
Mode
TimelessP
+
!
:
typeclass_instances
.
Class
PersistentP
{
M
}
(
P
:
uPred
M
)
:
=
persistentP
:
P
⊢
□
P
.
Hint
Mode
PersistentP
-
!
:
typeclass_instances
.
Arguments
persistentP
{
_
}
_
{
_
}.
Hint
Mode
PersistentP
+
!
:
typeclass_instances
.
Module
uPred
.
Section
derived
.
...
...
@@ -808,9 +810,43 @@ Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A)
(
∀
x
,
TimelessP
(
Ψ
x
))
→
TimelessP
P
→
TimelessP
(
from_option
Ψ
P
mx
).
Proof
.
destruct
mx
;
apply
_
.
Qed
.
(* Derived lemmas for persistence *)
Lemma
always_always
P
`
{!
PersistentP
P
}
:
□
P
⊣
⊢
P
.
Proof
.
apply
(
anti_symm
(
⊢
))
;
auto
using
always_elim
.
Qed
.
Lemma
always_if_always
p
P
`
{!
PersistentP
P
}
:
□
?p
P
⊣
⊢
P
.
Proof
.
destruct
p
;
simpl
;
auto
using
always_always
.
Qed
.
Lemma
always_intro
P
Q
`
{!
PersistentP
P
}
:
(
P
⊢
Q
)
→
P
⊢
□
Q
.
Proof
.
rewrite
-(
always_always
P
)
;
apply
always_intro'
.
Qed
.
Lemma
always_and_sep_l
P
Q
`
{!
PersistentP
P
}
:
P
∧
Q
⊣
⊢
P
∗
Q
.
Proof
.
by
rewrite
-(
always_always
P
)
always_and_sep_l'
.
Qed
.
Lemma
always_and_sep_r
P
Q
`
{!
PersistentP
Q
}
:
P
∧
Q
⊣
⊢
P
∗
Q
.
Proof
.
by
rewrite
-(
always_always
Q
)
always_and_sep_r'
.
Qed
.
Lemma
always_sep_dup
P
`
{!
PersistentP
P
}
:
P
⊣
⊢
P
∗
P
.
Proof
.
by
rewrite
-(
always_always
P
)
-
always_sep_dup'
.
Qed
.
Lemma
always_entails_l
P
Q
`
{!
PersistentP
Q
}
:
(
P
⊢
Q
)
→
P
⊢
Q
∗
P
.
Proof
.
by
rewrite
-(
always_always
Q
)
;
apply
always_entails_l'
.
Qed
.
Lemma
always_entails_r
P
Q
`
{!
PersistentP
Q
}
:
(
P
⊢
Q
)
→
P
⊢
P
∗
Q
.
Proof
.
by
rewrite
-(
always_always
Q
)
;
apply
always_entails_r'
.
Qed
.
Lemma
always_impl_wand
P
`
{!
PersistentP
P
}
Q
:
(
P
→
Q
)
⊣
⊢
(
P
-
∗
Q
).
Proof
.
apply
(
anti_symm
_
)
;
auto
using
impl_wand
.
apply
impl_intro_l
.
by
rewrite
always_and_sep_l
wand_elim_r
.
Qed
.
(* Persistence *)
Global
Instance
pure_persistent
φ
:
PersistentP
(
⌜φ⌝
:
uPred
M
)%
I
.
Proof
.
by
rewrite
/
PersistentP
always_pure
.
Qed
.
Global
Instance
pure_impl_persistent
φ
Q
:
PersistentP
Q
→
PersistentP
(
⌜φ⌝
→
Q
)%
I
.
Proof
.
rewrite
/
PersistentP
pure_impl_forall
always_forall
.
auto
using
forall_mono
.
Qed
.
Global
Instance
pure_wand_persistent
φ
Q
:
PersistentP
Q
→
PersistentP
(
⌜φ⌝
-
∗
Q
)%
I
.
Proof
.
rewrite
/
PersistentP
-
always_impl_wand
pure_impl_forall
always_forall
.
auto
using
forall_mono
.
Qed
.
Global
Instance
always_persistent
P
:
PersistentP
(
□
P
).
Proof
.
by
intros
;
apply
always_intro'
.
Qed
.
Global
Instance
and_persistent
P
Q
:
...
...
@@ -843,23 +879,5 @@ Proof. intros. by rewrite /PersistentP always_ownM. Qed.
Global
Instance
from_option_persistent
{
A
}
P
(
Ψ
:
A
→
uPred
M
)
(
mx
:
option
A
)
:
(
∀
x
,
PersistentP
(
Ψ
x
))
→
PersistentP
P
→
PersistentP
(
from_option
Ψ
P
mx
).
Proof
.
destruct
mx
;
apply
_
.
Qed
.
(* Derived lemmas for persistence *)
Lemma
always_always
P
`
{!
PersistentP
P
}
:
□
P
⊣
⊢
P
.
Proof
.
apply
(
anti_symm
(
⊢
))
;
auto
using
always_elim
.
Qed
.
Lemma
always_if_always
p
P
`
{!
PersistentP
P
}
:
□
?p
P
⊣
⊢
P
.
Proof
.
destruct
p
;
simpl
;
auto
using
always_always
.
Qed
.
Lemma
always_intro
P
Q
`
{!
PersistentP
P
}
:
(
P
⊢
Q
)
→
P
⊢
□
Q
.
Proof
.
rewrite
-(
always_always
P
)
;
apply
always_intro'
.
Qed
.
Lemma
always_and_sep_l
P
Q
`
{!
PersistentP
P
}
:
P
∧
Q
⊣
⊢
P
∗
Q
.
Proof
.
by
rewrite
-(
always_always
P
)
always_and_sep_l'
.
Qed
.
Lemma
always_and_sep_r
P
Q
`
{!
PersistentP
Q
}
:
P
∧
Q
⊣
⊢
P
∗
Q
.
Proof
.
by
rewrite
-(
always_always
Q
)
always_and_sep_r'
.
Qed
.
Lemma
always_sep_dup
P
`
{!
PersistentP
P
}
:
P
⊣
⊢
P
∗
P
.
Proof
.
by
rewrite
-(
always_always
P
)
-
always_sep_dup'
.
Qed
.
Lemma
always_entails_l
P
Q
`
{!
PersistentP
Q
}
:
(
P
⊢
Q
)
→
P
⊢
Q
∗
P
.
Proof
.
by
rewrite
-(
always_always
Q
)
;
apply
always_entails_l'
.
Qed
.
Lemma
always_entails_r
P
Q
`
{!
PersistentP
Q
}
:
(
P
⊢
Q
)
→
P
⊢
P
∗
Q
.
Proof
.
by
rewrite
-(
always_always
Q
)
;
apply
always_entails_r'
.
Qed
.
End
derived
.
End
uPred
.
theories/base_logic/lib/core.v
View file @
e0a45a07
...
...
@@ -8,7 +8,7 @@ Import uPred.
in the shallow embedding. *)
Definition
coreP
{
M
:
ucmraT
}
(
P
:
uPred
M
)
:
uPred
M
:
=
(
∀
`
(!
PersistentP
Q
,
P
⊢
Q
),
Q
)%
I
.
(
∀
`
(!
PersistentP
Q
)
,
⌜
P
⊢
Q
⌝
→
Q
)%
I
.
Instance
:
Params
(@
coreP
)
1
.
Typeclasses
Opaque
coreP
.
...
...
@@ -25,7 +25,7 @@ Section core.
Global
Instance
coreP_mono
:
Proper
((
⊢
)
==>
(
⊢
))
(@
coreP
M
).
Proof
.
rewrite
/
coreP
.
iIntros
(
P
P'
?)
"H"
;
iIntros
(
Q
??).
unshelve
iApply
(
"H"
$!
Q
).
by
etrans
.
iApply
(
"H"
$!
Q
with
"[%]"
).
by
etrans
.
Qed
.
Global
Instance
coreP_proper
:
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
coreP
M
).
...
...
theories/base_logic/lib/fancy_updates.v
View file @
e0a45a07
...
...
@@ -155,8 +155,10 @@ Section proofmode_classes.
Proof
.
rewrite
/
FromAssumption
=>->.
apply
bupd_fupd
.
Qed
.
Global
Instance
into_wand_fupd
E1
E2
R
P
Q
:
IntoWand
R
P
Q
→
IntoWand
R
(|={
E1
,
E2
}=>
P
)
(|={
E1
,
E2
}=>
Q
)
|
100
.
Proof
.
rewrite
/
IntoWand
=>->.
apply
wand_intro_l
.
by
rewrite
fupd_wand_r
.
Qed
.
IntoWand
R
P
Q
→
IntoWand'
R
(|={
E1
,
E2
}=>
P
)
(|={
E1
,
E2
}=>
Q
)
|
100
.
Proof
.
rewrite
/
IntoWand'
/
IntoWand
=>->.
apply
wand_intro_l
.
by
rewrite
fupd_wand_r
.
Qed
.
Global
Instance
from_sep_fupd
E
P
Q1
Q2
:
FromSep
P
Q1
Q2
→
FromSep
(|={
E
}=>
P
)
(|={
E
}=>
Q1
)
(|={
E
}=>
Q2
).
...
...
@@ -179,8 +181,8 @@ Section proofmode_classes.
Global
Instance
is_except_0_fupd
E1
E2
P
:
IsExcept0
(|={
E1
,
E2
}=>
P
).
Proof
.
by
rewrite
/
IsExcept0
except_0_fupd
.
Qed
.
Global
Instance
into
_modal_fupd
E
P
:
Into
Modal
P
(|={
E
}=>
P
).
Proof
.
rewrite
/
Into
Modal
.
apply
fupd_intro
.
Qed
.
Global
Instance
from
_modal_fupd
E
P
:
From
Modal
(|={
E
}=>
P
)
P
.
Proof
.
rewrite
/
From
Modal
.
apply
fupd_intro
.
Qed
.
(* Put a lower priority compared to [elim_modal_fupd_fupd], so that
it is not taken when the first parameter is not specified (in
...
...
theories/base_logic/lib/sts.v
View file @
e0a45a07
...
...
@@ -101,13 +101,13 @@ Section sts.
Proof
.
iIntros
"[Hinv Hγf]"
.
rewrite
/
sts_ownS
/
sts_inv
/
sts_own
.
iDestruct
"Hinv"
as
(
s
)
"[>Hγ Hφ]"
.
iCombine
"Hγ"
"Hγf"
as
"Hγ"
;
iDestruct
(
own_valid
with
"Hγ"
)
as
%
Hvalid
.
iDestruct
(
own_valid
_2
with
"Hγ
Hγf
"
)
as
%
Hvalid
.
assert
(
s
∈
S
)
by
eauto
using
sts_auth_frag_valid_inv
.
assert
(
✓
sts_frag
S
T
)
as
[??]
by
eauto
using
cmra_valid_op_r
.
rewrite
sts_op_auth_frag
//.
iModIntro
;
iExists
s
;
iSplit
;
[
done
|]
;
iFrame
"Hφ"
.
iIntros
(
s'
T'
)
"[% Hφ]"
.
iMod
(
own_update
with
"Hγ"
)
as
"Hγ"
;
first
eauto
using
sts_update_auth
.
iMod
(
own_update_2
with
"Hγ Hγf"
)
as
"Hγ"
.
{
rewrite
sts_op_auth_frag
;
[|
done
..].
by
apply
sts_update_auth
.
}
iRevert
"Hγ"
;
rewrite
-
sts_op_auth_frag_up
;
iIntros
"[Hγ $]"
.
iModIntro
.
iNext
.
iExists
s'
;
by
iFrame
.
Qed
.
...
...
theories/prelude/vector.v
View file @
e0a45a07
...
...
@@ -187,7 +187,8 @@ Proof.
Defined
.
Ltac
inv_vec
v
:
=
match
type
of
v
with
let
T
:
=
type
of
v
in
match
eval
hnf
in
T
with
|
vec
_
0
=>
revert
dependent
v
;
match
goal
with
|-
∀
v
,
@
?P
v
=>
apply
(
vec_0_inv
P
)
end
|
vec
_
(
S
?n
)
=>
...
...
theories/proofmode/class_instances.v
View file @
e0a45a07
...
...
@@ -219,15 +219,22 @@ Proof. apply and_elim_r', impl_wand. Qed.
Global
Instance
into_wand_always
R
P
Q
:
IntoWand
R
P
Q
→
IntoWand
(
□
R
)
P
Q
.
Proof
.
rewrite
/
IntoWand
=>
->.
apply
always_elim
.
Qed
.
Global
Instance
into_wand_later
(
R1
R2
P
Q
:
uPred
M
)
:
IntoLaterN
1
R1
R2
→
IntoWand
R2
P
Q
→
IntoWand
R1
(
▷
P
)
(
▷
Q
)
|
99
.
Proof
.
rewrite
/
IntoLaterN
/
IntoWand
=>
->
->.
by
rewrite
-
later_wand
.
Qed
.
IntoLaterN
1
R1
R2
→
IntoWand
R2
P
Q
→
IntoWand'
R1
(
▷
P
)
(
▷
Q
)
|
99
.
Proof
.
rewrite
/
IntoLaterN
/
IntoWand'
/
IntoWand
=>
->
->.
by
rewrite
-
later_wand
.
Qed
.
Global
Instance
into_wand_laterN
n
(
R1
R2
P
Q
:
uPred
M
)
:
IntoLaterN
n
R1
R2
→
IntoWand
R2
P
Q
→
IntoWand
R1
(
▷
^
n
P
)
(
▷
^
n
Q
)
|
100
.
Proof
.
rewrite
/
IntoLaterN
/
IntoWand
=>
->
->.
by
rewrite
-
laterN_wand
.
Qed
.
IntoLaterN
n
R1
R2
→
IntoWand
R2
P
Q
→
IntoWand'
R1
(
▷
^
n
P
)
(
▷
^
n
Q
)
|
100
.
Proof
.
rewrite
/
IntoLaterN
/
IntoWand'
/
IntoWand
=>
->
->.
by
rewrite
-
laterN_wand
.
Qed
.
Global
Instance
into_wand_bupd
R
P
Q
:
IntoWand
R
P
Q
→
IntoWand
R
(|==>
P
)
(|==>
Q
)
|
98
.
Proof
.
rewrite
/
IntoWand
=>->.
apply
wand_intro_l
.
by
rewrite
bupd_wand_r
.
Qed
.
IntoWand
R
P
Q
→
IntoWand'
R
(|==>
P
)
(|==>
Q
)
|
98
.
Proof
.
rewrite
/
IntoWand'
/
IntoWand
=>
->.
apply
wand_intro_l
.
by
rewrite
bupd_wand_r
.
Qed
.
(* FromAnd *)
Global
Instance
from_and_and
P1
P2
:
FromAnd
(
P1
∧
P2
)
P1
P2
.
...
...
@@ -564,12 +571,12 @@ Global Instance into_exist_laterN {A} n P (Φ : A → uPred M) :
IntoExist
P
Φ
→
Inhabited
A
→
IntoExist
(
▷
^
n
P
)
(
λ
a
,
▷
^
n
(
Φ
a
))%
I
.
Proof
.
rewrite
/
IntoExist
=>
HP
?.
by
rewrite
HP
laterN_exist
.
Qed
.
(*
Into
Modal *)
Global
Instance
into
_modal_later
P
:
Into
Modal
P
(
▷
P
).
(*
From
Modal *)
Global
Instance
from
_modal_later
P
:
From
Modal
(
▷
P
)
P
.
Proof
.
apply
later_intro
.
Qed
.
Global
Instance
into
_modal_bupd
P
:
Into
Modal
P
(|==>
P
).
Global
Instance
from
_modal_bupd
P
:
From
Modal
(|==>
P
)
P
.
Proof
.
apply
bupd_intro
.
Qed
.
Global
Instance
into
_modal_except_0
P
:
Into
Modal
P
(
◇
P
).
Global
Instance
from
_modal_except_0
P
:
From
Modal
(
◇
P
)
P
.
Proof
.
apply
except_0_intro
.
Qed
.
(* ElimModal *)
...
...
theories/proofmode/classes.v
View file @
e0a45a07
...
...
@@ -2,77 +2,102 @@ From iris.base_logic Require Export base_logic.
Set
Default
Proof
Using
"Type"
.
Import
uPred
.
Section
classes
.
Context
{
M
:
ucmraT
}.
Implicit
Types
P
Q
:
uPred
M
.
Class
FromAssumption
(
p
:
bool
)
(
P
Q
:
uPred
M
)
:
=
from_assumption
:
□
?p
P
⊢
Q
.
Global
Arguments
from_assumption
_
_
_
{
_
}.
Class
IntoPure
(
P
:
uPred
M
)
(
φ
:
Prop
)
:
=
into_pure
:
P
⊢
⌜φ⌝
.
Global
Arguments
into_pure
:
clear
implicits
.
Class
FromPure
(
P
:
uPred
M
)
(
φ
:
Prop
)
:
=
from_pure
:
⌜φ⌝
⊢
P
.
Global
Arguments
from_pure
:
clear
implicits
.
Class
IntoPersistentP
(
P
Q
:
uPred
M
)
:
=
into_persistentP
:
P
⊢
□
Q
.
Global
Arguments
into_persistentP
:
clear
implicits
.
Class
IntoLaterN
(
n
:
nat
)
(
P
Q
:
uPred
M
)
:
=
into_laterN
:
P
⊢
▷
^
n
Q
.
Global
Arguments
into_laterN
_
_
_
{
_
}.
Class
FromLaterN
(
n
:
nat
)
(
P
Q
:
uPred
M
)
:
=
from_laterN
:
▷
^
n
Q
⊢
P
.
Global
Arguments
from_laterN
_
_
_
{
_
}.
Class
IntoWand
(
R
P
Q
:
uPred
M
)
:
=
into_wand
:
R
⊢
P
-
∗
Q
.
Global
Arguments
into_wand
:
clear
implicits
.
Class
FromAnd
(
P
Q1
Q2
:
uPred
M
)
:
=
from_and
:
Q1
∧
Q2
⊢
P
.
Global
Arguments
from_and
:
clear
implicits
.
Class
FromSep
(
P
Q1
Q2
:
uPred
M
)
:
=
from_sep
:
Q1
∗
Q2
⊢
P
.
Global
Arguments
from_sep
:
clear
implicits
.
Class
IntoAnd
(
p
:
bool
)
(
P
Q1
Q2
:
uPred
M
)
:
=
Class
FromAssumption
{
M
}
(
p
:
bool
)
(
P
Q
:
uPred
M
)
:
=
from_assumption
:
□
?p
P
⊢
Q
.
Arguments
from_assumption
{
_
}
_
_
_
{
_
}.
Hint
Mode
FromAssumption
+
+
!
-
:
typeclass_instances
.
Class
IntoPure
{
M
}
(
P
:
uPred
M
)
(
φ
:
Prop
)
:
=
into_pure
:
P
⊢
⌜φ⌝
.
Arguments
into_pure
{
_
}
_
_
{
_
}.
Hint
Mode
IntoPure
+
!
-
:
typeclass_instances
.
Class
FromPure
{
M
}
(
P
:
uPred
M
)
(
φ
:
Prop
)
:
=
from_pure
:
⌜φ⌝
⊢
P
.
Arguments
from_pure
{
_
}
_
_
{
_
}.
Hint
Mode
FromPure
+
!
-
:
typeclass_instances
.
Class
IntoPersistentP
{
M
}
(
P
Q
:
uPred
M
)
:
=
into_persistentP
:
P
⊢
□
Q
.
Arguments
into_persistentP
{
_
}
_
_
{
_
}.
Hint
Mode
IntoPersistentP
+
!
-
:
typeclass_instances
.
Class
IntoLaterN
{
M
}
(
n
:
nat
)
(
P
Q
:
uPred
M
)
:
=
into_laterN
:
P
⊢
▷
^
n
Q
.
Arguments
into_laterN
{
_
}
_
_
_
{
_
}.
Hint
Mode
IntoLaterN
+
-
!
-
:
typeclass_instances
.
Class
FromLaterN
{
M
}
(
n
:
nat
)
(
P
Q
:
uPred
M
)
:
=
from_laterN
:
▷
^
n
Q
⊢
P
.
Arguments
from_laterN
{
_
}
_
_
_
{
_
}.
Hint
Mode
FromLaterN
+
-
!
-
:
typeclass_instances
.
Class
IntoWand
{
M
}
(
R
P
Q
:
uPred
M
)
:
=
into_wand
:
R
⊢
P
-
∗
Q
.
Arguments
into_wand
{
_
}
_
_
_
{
_
}.
Hint
Mode
IntoWand
+
!
-
-
:
typeclass_instances
.
Class
IntoWand'
{
M
}
(
R
P
Q
:
uPred
M
)
:
=
into_wand'
:
>
IntoWand
R
P
Q
.
Arguments
into_wand'
{
_
}
_
_
_
{
_
}.
Hint
Mode
IntoWand'
+
!
!
-
:
typeclass_instances
.
Hint
Mode
IntoWand'
+
!
-
!
:
typeclass_instances
.
Class
FromAnd
{
M
}
(
P
Q1
Q2
:
uPred
M
)
:
=
from_and
:
Q1
∧
Q2
⊢
P
.
Arguments
from_and
{
_
}
_
_
_
{
_
}.
Hint
Mode
FromAnd
+
!
-
-
:
typeclass_instances
.
Class
FromSep
{
M
}
(
P
Q1
Q2
:
uPred
M
)
:
=
from_sep
:
Q1
∗
Q2
⊢
P
.
Arguments
from_sep
{
_
}
_
_
_
{
_
}.
Hint
Mode
FromSep
+
!
-
-
:
typeclass_instances
.
Hint
Mode
FromSep
+
-
!
!
:
typeclass_instances
.
(* For iCombine *)
Class
IntoAnd
{
M
}
(
p
:
bool
)
(
P
Q1
Q2
:
uPred
M
)
:
=
into_and
:
P
⊢
if
p
then
Q1
∧
Q2
else
Q1
∗
Q2
.
Global
Arguments
into_and
:
clear
implicits
.
Lemma
mk_into_and_sep
p
P
Q1
Q2
:
(
P
⊢
Q1
∗
Q2
)
→
IntoAnd
p
P
Q1
Q2
.
Arguments
into_and
{
_
}
_
_
_
_
{
_
}.
Hint
Mode
IntoAnd
+
+
!
-
-
:
typeclass_instances
.
Lemma
mk_into_and_sep
{
M
}
p
(
P
Q1
Q2
:
uPred
M
)
:
(
P
⊢
Q1
∗
Q2
)
→
IntoAnd
p
P
Q1
Q2
.
Proof
.
rewrite
/
IntoAnd
=>->.
destruct
p
;
auto
using
sep_and
.
Qed
.
Class
FromOp
{
A
:
cmraT
}
(
a
b1
b2
:
A
)
:
=
from_op
:
b1
⋅
b2
≡
a
.
Global
Arguments
from_op
{
_
}
_
_
_
{
_
}.
Arguments
from_op
{
_
}
_
_
_
{
_
}.
Hint
Mode
FromOp
+
!
-
-
:
typeclass_instances
.
Hint
Mode
FromOp
+
-
!
!
:
typeclass_instances
.
(* For iCombine *)
Class
IntoOp
{
A
:
cmraT
}
(
a
b1
b2
:
A
)
:
=
into_op
:
a
≡
b1
⋅
b2
.
Global
Arguments
into_op
{
_
}
_
_
_
{
_
}.
Arguments
into_op
{
_
}
_
_
_
{
_
}.
(* No [Hint Mode] since we want to turn [?x] into [?x1 ⋅ ?x2], for example
when having [H : own ?x]. *)
Class
Frame
(
R
P
Q
:
uPred
M
)
:
=
frame
:
R
∗
Q
⊢
P
.
Global
Arguments
frame
:
clear
implicits
.
Class
Frame
{
M
}
(
R
P
Q
:
uPred
M
)
:
=
frame
:
R
∗
Q
⊢
P
.
Arguments
frame
{
_
}
_
_
_
{
_
}.
Hint
Mode
Frame
+
!
!
-
:
typeclass_instances
.
Class
FromOr
(
P
Q1
Q2
:
uPred
M
)
:
=
from_or
:
Q1
∨
Q2
⊢
P
.
Global
Arguments
from_or
:
clear
implicits
.
Class
FromOr
{
M
}
(
P
Q1
Q2
:
uPred
M
)
:
=
from_or
:
Q1
∨
Q2
⊢
P
.
Arguments
from_or
{
_
}
_
_
_
{
_
}.
Hint
Mode
FromOr
+
!
-
-
:
typeclass_instances
.
Class
IntoOr
P
Q1
Q2
:
=
into_or
:
P
⊢
Q1
∨
Q2
.
Global
Arguments
into_or
:
clear
implicits
.
Class
IntoOr
{
M
}
(
P
Q1
Q2
:
uPred
M
)
:
=
into_or
:
P
⊢
Q1
∨
Q2
.
Arguments
into_or
{
_
}
_
_
_
{
_
}.
Hint
Mode
IntoOr
+
!
-
-
:
typeclass_instances
.
Class
FromExist
{
A
}
(
P
:
uPred
M
)
(
Φ
:
A
→
uPred
M
)
:
=
Class
FromExist
{
M
A
}
(
P
:
uPred
M
)
(
Φ
:
A
→
uPred
M
)
:
=
from_exist
:
(
∃
x
,
Φ
x
)
⊢
P
.
Global
Arguments
from_exist
{
_
}
_
_
{
_
}.
Arguments
from_exist
{
_
_
}
_
_
{
_
}.
Hint
Mode
FromExist
+
-
!
-
:
typeclass_instances
.
Class
IntoExist
{
A
}
(
P
:
uPred
M
)
(
Φ
:
A
→
uPred
M
)
:
=
Class
IntoExist
{
M
A
}
(
P
:
uPred
M
)
(
Φ
:
A
→
uPred
M
)
:
=
into_exist
:
P
⊢
∃
x
,
Φ
x
.
Global
Arguments
into_exist
{
_
}
_
_
{
_
}.
Arguments
into_exist
{
_
_
}
_
_
{
_
}.
Hint
Mode
IntoExist
+
-
!
-
:
typeclass_instances
.
Class
IntoModal
(
P
Q
:
uPred
M
)
:
=
into_modal
:
P
⊢
Q
.
Global
Arguments
into_modal
:
clear
implicits
.
Class
FromModal
{
M
}
(
P
Q
:
uPred
M
)
:
=
from_modal
:
Q
⊢
P
.
Arguments
from_modal
{
_
}
_
_
{
_
}.
Hint
Mode
FromModal
+
!
-
:
typeclass_instances
.
Class
ElimModal
(
P
P'
:
uPred
M
)
(
Q
Q'
:
uPred
M
)
:
=
Class
ElimModal
{
M
}
(
P
P'
:
uPred
M
)
(
Q
Q'
:
uPred
M
)
:
=
elim_modal
:
P
∗
(
P'
-
∗
Q'
)
⊢
Q
.
Global
Arguments
elim_modal
_
_
_
_
{
_
}.
Arguments
elim_modal
{
_
}
_
_
_
_
{
_
}.
Hint
Mode
ElimModal
+
!
-
!
-
:
typeclass_instances
.
Hint
Mode
ElimModal
+
-
!
-
!
:
typeclass_instances
.
Lemma
elim_modal_dummy
P
Q
:
ElimModal
P
P
Q
Q
.
Lemma
elim_modal_dummy
{
M
}
(
P
Q
:
uPred
M
)
:
ElimModal
P
P
Q
Q
.
Proof
.
by
rewrite
/
ElimModal
wand_elim_r
.
Qed
.
Class
IsExcept0
(
Q
:
uPred
M
)
:
=
is_except_0
:
◇
Q
⊢
Q
.
Global
Arguments
is_except_0
:
clear
implicits
.
End
class
es
.
Class
IsExcept0
{
M
}
(
Q
:
uPred
M
)
:
=
is_except_0
:
◇
Q
⊢
Q
.
Arguments
is_except_0
{
_
}
_
{
_
}
.
Hint
Mode
IsExcept0
+
!
:
typeclass_instanc
es
.
theories/proofmode/coq_tactics.v
View file @
e0a45a07
...
...
@@ -832,8 +832,8 @@ Proof.
Qed
.
(** * Modalities *)
Lemma
tac_modal_intro
Δ
P
Q
:
Into
Modal
Q
P
→
(
Δ
⊢
Q
)
→
Δ
⊢
P
.
Proof
.
rewrite
/
Into
Modal
.
by
intros
<-
->.
Qed
.
Lemma
tac_modal_intro
Δ
P
Q
:
From
Modal
P
Q
→
(
Δ
⊢
Q
)
→
Δ
⊢
P
.
Proof
.
rewrite
/
From
Modal
.
by
intros
<-
->.
Qed
.
Lemma
tac_modal_elim
Δ
Δ
'
i
p
P'
P
Q
Q'
:
envs_lookup
i
Δ
=
Some
(
p
,
P
)
→
...
...
@@ -845,3 +845,5 @@ Proof.
rewrite
right_id
H
Δ
always_if_elim
.
by
apply
elim_modal
.
Qed
.
End
tactics
.
Hint
Mode
ForallSpecialize
+
-
-
!
-
:
typeclass_instances
.
theories/proofmode/tactics.v
View file @
e0a45a07
...
...
@@ -426,13 +426,14 @@ Tactic Notation "iApply" open_constr(lem) :=
|
ITrm
?t
?xs
?pat
=>
constr
:
(
ITrm
t
xs
(
"*"
+
:
+
pat
))
|
_
=>
constr
:
(
ITrm
lem
hnil
"*"
)
end
in
iPoseProofCore
lem
as
false
true
(
fun
H
=>
first
[
iExact
H
|
eapply
tac_apply
with
_
H
_
_
_;
let
rec
go
H
:
=
first
[
eapply
tac_apply
with
_
H
_
_
_;
[
env_cbv
;
reflexivity
|
let
P
:
=
match
goal
with
|-
IntoWand
?P
_
_
=>
P
end
in
apply
_
||
fail
1
"iApply: cannot apply"
P
|
lazy
beta
(* reduce betas created by instantiation *)
]]).
|
apply
_
|
lazy
beta
(* reduce betas created by instantiation *)
]
|
iSpecializePat
H
"[-]"
;
last
go
H
]
in
iPoseProofCore
lem
as
false
true
(
fun
H
=>
first
[
iExact
H
|
go
H
|
iTypeOf
H
(
fun
Q
=>
fail
1
"iApply: cannot apply"
Q
)]).
(** * Revert *)
Local
Tactic
Notation
"iForallRevert"
ident
(
x
)
:
=
...
...
@@ -642,7 +643,7 @@ Tactic Notation "iNext":= iNext _.
Tactic
Notation
"iModIntro"
:
=
iStartProof
;
eapply
tac_modal_intro
;
[
let
P
:
=
match
goal
with
|-
Into
Modal
_
?P
=>
P
end
in
[
let
P
:
=
match
goal
with
|-
From
Modal
?P
_
=>
P
end
in
apply
_
||
fail
"iModIntro:"
P
"not a modality"
|].