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
Joshua Yanovski
iris-coq
Commits
1f8c4338
Commit
1f8c4338
authored
Nov 30, 2016
by
Ralf Jung
Browse files
Use primitive projections for sealing
This approach is originally by Robbert
parent
f6f511e6
Changes
9
Hide whitespace changes
Inline
Side-by-side
theories/algebra/ofe.v
View file @
1f8c4338
...
...
@@ -202,9 +202,9 @@ Qed.
Program
Definition
fixpoint_def
`
{
Cofe
A
,
Inhabited
A
}
(
f
:
A
→
A
)
`
{!
Contractive
f
}
:
A
:=
compl
(
fixpoint_chain
f
).
Definition
fixpoint_aux
:
{
x
|
x
=
@
fixpoint_def
}
.
by
eexists
.
Qed
.
Definition
fixpoint
{
A
AC
AiH
}
f
{
Hf
}
:=
proj1_sig
fixpoint_aux
A
AC
AiH
f
Hf
.
Definition
fixpoint_eq
:
@
fixpoint
=
@
fixpoint_def
:=
proj2_sig
fixpoint_aux
.
Definition
fixpoint_aux
:
seal
(
@
fixpoint_def
)
.
by
eexists
.
Qed
.
Definition
fixpoint
{
A
AC
AiH
}
f
{
Hf
}
:=
unseal
fixpoint_aux
A
AC
AiH
f
Hf
.
Definition
fixpoint_eq
:
@
fixpoint
=
@
fixpoint_def
:=
seal_eq
fixpoint_aux
.
Section
fixpoint
.
Context
`
{
Cofe
A
,
Inhabited
A
}
(
f
:
A
→
A
)
`
{!
Contractive
f
}
.
...
...
theories/base_logic/lib/fancy_updates.v
View file @
1f8c4338
...
...
@@ -11,9 +11,9 @@ Import uPred.
Program
Definition
fupd_def
`
{
invG
Σ
}
(
E1
E2
:
coPset
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:=
(
wsat
∗
ownE
E1
==
∗
◇
(
wsat
∗
ownE
E2
∗
P
))
%
I
.
Definition
fupd_aux
:
{
x
|
x
=
@
fupd_def
}
.
by
eexists
.
Qed
.
Definition
fupd
:=
proj1_sig
fupd_aux
.
Definition
fupd_eq
:
@
fupd
=
@
fupd_def
:=
proj2_sig
fupd_aux
.
Definition
fupd_aux
:
seal
(
@
fupd_def
)
.
by
eexists
.
Qed
.
Definition
fupd
:=
unseal
fupd_aux
.
Definition
fupd_eq
:
@
fupd
=
@
fupd_def
:=
seal_eq
fupd_aux
.
Arguments
fupd
{
_
_
}
_
_
_
%
I
.
Instance:
Params
(
@
fupd
)
4.
...
...
theories/base_logic/lib/gen_heap.v
View file @
1f8c4338
...
...
@@ -34,9 +34,9 @@ Section definitions.
Definition
mapsto_def
(
l
:
L
)
(
q
:
Qp
)
(
v
:
V
)
:
iProp
Σ
:=
own
gen_heap_name
(
◯
{
[
l
:=
(
q
,
to_agree
(
v
:
leibnizC
V
))
]
}
).
Definition
mapsto_aux
:
{
x
|
x
=
@
mapsto_def
}
.
by
eexists
.
Qed
.
Definition
mapsto
:=
proj1_sig
mapsto_aux
.
Definition
mapsto_eq
:
@
mapsto
=
@
mapsto_def
:=
proj2_sig
mapsto_aux
.
Definition
mapsto_aux
:
seal
(
@
mapsto_def
)
.
by
eexists
.
Qed
.
Definition
mapsto
:=
unseal
mapsto_aux
.
Definition
mapsto_eq
:
@
mapsto
=
@
mapsto_def
:=
seal_eq
mapsto_aux
.
End
definitions
.
Local
Notation
"l ↦{ q } v"
:=
(
mapsto
l
q
v
)
...
...
theories/base_logic/lib/invariants.v
View file @
1f8c4338
...
...
@@ -8,9 +8,9 @@ Import uPred.
(
**
Derived
forms
and
lemmas
about
them
.
*
)
Definition
inv_def
`
{
invG
Σ
}
(
N
:
namespace
)
(
P
:
iProp
Σ
)
:
iProp
Σ
:=
(
∃
i
,
⌜
i
∈
↑
N
⌝
∧
ownI
i
P
)
%
I
.
Definition
inv_aux
:
{
x
|
x
=
@
inv_def
}
.
by
eexists
.
Qed
.
Definition
inv
{
Σ
i
}
:=
proj1_sig
inv_aux
Σ
i
.
Definition
inv_eq
:
@
inv
=
@
inv_def
:=
proj2_sig
inv_aux
.
Definition
inv_aux
:
seal
(
@
inv_def
)
.
by
eexists
.
Qed
.
Definition
inv
{
Σ
i
}
:=
unseal
inv_aux
Σ
i
.
Definition
inv_eq
:
@
inv
=
@
inv_def
:=
seal_eq
inv_aux
.
Instance:
Params
(
@
inv
)
3.
Typeclasses
Opaque
inv
.
...
...
theories/base_logic/lib/namespaces.v
View file @
1f8c4338
...
...
@@ -11,14 +11,14 @@ Definition nroot : namespace := nil.
Definition
ndot_def
`
{
Countable
A
}
(
N
:
namespace
)
(
x
:
A
)
:
namespace
:=
encode
x
::
N
.
Definition
ndot_aux
:
{
x
|
x
=
@
ndot_def
}
.
by
eexists
.
Qed
.
Definition
ndot
{
A
A_dec
A_count
}:=
proj1_sig
ndot_aux
A
A_dec
A_count
.
Definition
ndot_eq
:
@
ndot
=
@
ndot_def
:=
proj2_sig
ndot_aux
.
Definition
ndot_aux
:
seal
(
@
ndot_def
)
.
by
eexists
.
Qed
.
Definition
ndot
{
A
A_dec
A_count
}:=
unseal
ndot_aux
A
A_dec
A_count
.
Definition
ndot_eq
:
@
ndot
=
@
ndot_def
:=
seal_eq
ndot_aux
.
Definition
nclose_def
(
N
:
namespace
)
:
coPset
:=
coPset_suffixes
(
encode
N
).
Definition
nclose_aux
:
{
x
|
x
=
@
nclose_def
}
.
by
eexists
.
Qed
.
Instance
nclose
:
UpClose
namespace
coPset
:=
proj1_sig
nclose_aux
.
Definition
nclose_eq
:
@
nclose
=
@
nclose_def
:=
proj2_sig
nclose_aux
.
Definition
nclose_aux
:
seal
(
@
nclose_def
)
.
by
eexists
.
Qed
.
Instance
nclose
:
UpClose
namespace
coPset
:=
unseal
nclose_aux
.
Definition
nclose_eq
:
@
nclose
=
@
nclose_def
:=
seal_eq
nclose_aux
.
Notation
"N .@ x"
:=
(
ndot
N
x
)
(
at
level
19
,
left
associativity
,
format
"N .@ x"
)
:
C_scope
.
...
...
theories/base_logic/lib/own.v
View file @
1f8c4338
...
...
@@ -54,9 +54,9 @@ Instance: Params (@iRes_singleton) 4.
Definition
own_def
`
{
inG
Σ
A
}
(
γ
:
gname
)
(
a
:
A
)
:
iProp
Σ
:=
uPred_ownM
(
iRes_singleton
γ
a
).
Definition
own_aux
:
{
x
|
x
=
@
own_def
}
.
by
eexists
.
Qed
.
Definition
own
{
Σ
A
i
}
:=
proj1_sig
own_aux
Σ
A
i
.
Definition
own_eq
:
@
own
=
@
own_def
:=
proj2_sig
own_aux
.
Definition
own_aux
:
seal
(
@
own_def
)
.
by
eexists
.
Qed
.
Definition
own
{
Σ
A
i
}
:=
unseal
own_aux
Σ
A
i
.
Definition
own_eq
:
@
own
=
@
own_def
:=
seal_eq
own_aux
.
Instance:
Params
(
@
own
)
4.
Typeclasses
Opaque
own
.
...
...
theories/base_logic/primitive.v
View file @
1f8c4338
...
...
@@ -9,26 +9,26 @@ Local Hint Extern 10 (_ ≤ _) => omega.
Program
Definition
uPred_pure_def
{
M
}
(
φ
:
Prop
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
φ
|}
.
Solve
Obligations
with
done
.
Definition
uPred_pure_aux
:
{
x
|
x
=
@
uPred_pure_def
}
.
by
eexists
.
Qed
.
Definition
uPred_pure
{
M
}
:=
proj1_sig
uPred_pure_aux
M
.
Definition
uPred_pure_aux
:
seal
(
@
uPred_pure_def
)
.
by
eexists
.
Qed
.
Definition
uPred_pure
{
M
}
:=
unseal
uPred_pure_aux
M
.
Definition
uPred_pure_eq
:
@
uPred_pure
=
@
uPred_pure_def
:=
proj2_sig
uPred_pure_aux
.
@
uPred_pure
=
@
uPred_pure_def
:=
seal_eq
uPred_pure_aux
.
Instance
uPred_inhabited
M
:
Inhabited
(
uPred
M
)
:=
populate
(
uPred_pure
True
).
Program
Definition
uPred_and_def
{
M
}
(
P
Q
:
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
P
n
x
∧
Q
n
x
|}
.
Solve
Obligations
with
naive_solver
eauto
2
with
uPred_def
.
Definition
uPred_and_aux
:
{
x
|
x
=
@
uPred_and_def
}
.
by
eexists
.
Qed
.
Definition
uPred_and
{
M
}
:=
proj1_sig
uPred_and_aux
M
.
Definition
uPred_and_eq
:
@
uPred_and
=
@
uPred_and_def
:=
proj2_sig
uPred_and_aux
.
Definition
uPred_and_aux
:
seal
(
@
uPred_and_def
)
.
by
eexists
.
Qed
.
Definition
uPred_and
{
M
}
:=
unseal
uPred_and_aux
M
.
Definition
uPred_and_eq
:
@
uPred_and
=
@
uPred_and_def
:=
seal_eq
uPred_and_aux
.
Program
Definition
uPred_or_def
{
M
}
(
P
Q
:
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
P
n
x
∨
Q
n
x
|}
.
Solve
Obligations
with
naive_solver
eauto
2
with
uPred_def
.
Definition
uPred_or_aux
:
{
x
|
x
=
@
uPred_or_def
}
.
by
eexists
.
Qed
.
Definition
uPred_or
{
M
}
:=
proj1_sig
uPred_or_aux
M
.
Definition
uPred_or_eq
:
@
uPred_or
=
@
uPred_or_def
:=
proj2_sig
uPred_or_aux
.
Definition
uPred_or_aux
:
seal
(
@
uPred_or_def
)
.
by
eexists
.
Qed
.
Definition
uPred_or
{
M
}
:=
unseal
uPred_or_aux
M
.
Definition
uPred_or_eq
:
@
uPred_or
=
@
uPred_or_def
:=
seal_eq
uPred_or_aux
.
Program
Definition
uPred_impl_def
{
M
}
(
P
Q
:
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
∀
n
'
x
'
,
...
...
@@ -39,33 +39,33 @@ Next Obligation.
eapply
HPQ
;
auto
.
exists
(
x2
⋅
x4
);
by
rewrite
assoc
.
Qed
.
Next
Obligation
.
intros
M
P
Q
[
|
n1
]
[
|
n2
]
x
;
auto
with
lia
.
Qed
.
Definition
uPred_impl_aux
:
{
x
|
x
=
@
uPred_impl_def
}
.
by
eexists
.
Qed
.
Definition
uPred_impl
{
M
}
:=
proj1_sig
uPred_impl_aux
M
.
Definition
uPred_impl_aux
:
seal
(
@
uPred_impl_def
)
.
by
eexists
.
Qed
.
Definition
uPred_impl
{
M
}
:=
unseal
uPred_impl_aux
M
.
Definition
uPred_impl_eq
:
@
uPred_impl
=
@
uPred_impl_def
:=
proj2_sig
uPred_impl_aux
.
@
uPred_impl
=
@
uPred_impl_def
:=
seal_eq
uPred_impl_aux
.
Program
Definition
uPred_forall_def
{
M
A
}
(
Ψ
:
A
→
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
∀
a
,
Ψ
a
n
x
|}
.
Solve
Obligations
with
naive_solver
eauto
2
with
uPred_def
.
Definition
uPred_forall_aux
:
{
x
|
x
=
@
uPred_forall_def
}
.
by
eexists
.
Qed
.
Definition
uPred_forall
{
M
A
}
:=
proj1_sig
uPred_forall_aux
M
A
.
Definition
uPred_forall_aux
:
seal
(
@
uPred_forall_def
)
.
by
eexists
.
Qed
.
Definition
uPred_forall
{
M
A
}
:=
unseal
uPred_forall_aux
M
A
.
Definition
uPred_forall_eq
:
@
uPred_forall
=
@
uPred_forall_def
:=
proj2_sig
uPred_forall_aux
.
@
uPred_forall
=
@
uPred_forall_def
:=
seal_eq
uPred_forall_aux
.
Program
Definition
uPred_exist_def
{
M
A
}
(
Ψ
:
A
→
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
∃
a
,
Ψ
a
n
x
|}
.
Solve
Obligations
with
naive_solver
eauto
2
with
uPred_def
.
Definition
uPred_exist_aux
:
{
x
|
x
=
@
uPred_exist_def
}
.
by
eexists
.
Qed
.
Definition
uPred_exist
{
M
A
}
:=
proj1_sig
uPred_exist_aux
M
A
.
Definition
uPred_exist_eq
:
@
uPred_exist
=
@
uPred_exist_def
:=
proj2_sig
uPred_exist_aux
.
Definition
uPred_exist_aux
:
seal
(
@
uPred_exist_def
)
.
by
eexists
.
Qed
.
Definition
uPred_exist
{
M
A
}
:=
unseal
uPred_exist_aux
M
A
.
Definition
uPred_exist_eq
:
@
uPred_exist
=
@
uPred_exist_def
:=
seal_eq
uPred_exist_aux
.
Program
Definition
uPred_internal_eq_def
{
M
}
{
A
:
ofeT
}
(
a1
a2
:
A
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
a1
≡
{
n
}
≡
a2
|}
.
Solve
Obligations
with
naive_solver
eauto
2
using
(
dist_le
(
A
:=
A
)).
Definition
uPred_internal_eq_aux
:
{
x
|
x
=
@
uPred_internal_eq_def
}
.
by
eexists
.
Qed
.
Definition
uPred_internal_eq
{
M
A
}
:=
proj1_sig
uPred_internal_eq_aux
M
A
.
Definition
uPred_internal_eq_aux
:
seal
(
@
uPred_internal_eq_def
)
.
by
eexists
.
Qed
.
Definition
uPred_internal_eq
{
M
A
}
:=
unseal
uPred_internal_eq_aux
M
A
.
Definition
uPred_internal_eq_eq
:
@
uPred_internal_eq
=
@
uPred_internal_eq_def
:=
proj2_sig
uPred_internal_eq_aux
.
@
uPred_internal_eq
=
@
uPred_internal_eq_def
:=
seal_eq
uPred_internal_eq_aux
.
Program
Definition
uPred_sep_def
{
M
}
(
P
Q
:
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
∃
x1
x2
,
x
≡
{
n
}
≡
x1
⋅
x2
∧
P
n
x1
∧
Q
n
x2
|}
.
...
...
@@ -79,9 +79,9 @@ Next Obligation.
exists
x1
,
x2
;
cofe_subst
;
split_and
!
;
eauto
using
dist_le
,
uPred_closed
,
cmra_validN_op_l
,
cmra_validN_op_r
.
Qed
.
Definition
uPred_sep_aux
:
{
x
|
x
=
@
uPred_sep_def
}
.
by
eexists
.
Qed
.
Definition
uPred_sep
{
M
}
:=
proj1_sig
uPred_sep_aux
M
.
Definition
uPred_sep_eq
:
@
uPred_sep
=
@
uPred_sep_def
:=
proj2_sig
uPred_sep_aux
.
Definition
uPred_sep_aux
:
seal
(
@
uPred_sep_def
)
.
by
eexists
.
Qed
.
Definition
uPred_sep
{
M
}
:=
unseal
uPred_sep_aux
M
.
Definition
uPred_sep_eq
:
@
uPred_sep
=
@
uPred_sep_def
:=
seal_eq
uPred_sep_aux
.
Program
Definition
uPred_wand_def
{
M
}
(
P
Q
:
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
∀
n
'
x
'
,
...
...
@@ -92,10 +92,10 @@ Next Obligation.
eauto
using
cmra_validN_includedN
,
cmra_monoN_r
,
cmra_includedN_le
.
Qed
.
Next
Obligation
.
naive_solver
.
Qed
.
Definition
uPred_wand_aux
:
{
x
|
x
=
@
uPred_wand_def
}
.
by
eexists
.
Qed
.
Definition
uPred_wand
{
M
}
:=
proj1_sig
uPred_wand_aux
M
.
Definition
uPred_wand_aux
:
seal
(
@
uPred_wand_def
)
.
by
eexists
.
Qed
.
Definition
uPred_wand
{
M
}
:=
unseal
uPred_wand_aux
M
.
Definition
uPred_wand_eq
:
@
uPred_wand
=
@
uPred_wand_def
:=
proj2_sig
uPred_wand_aux
.
@
uPred_wand
=
@
uPred_wand_def
:=
seal_eq
uPred_wand_aux
.
Program
Definition
uPred_always_def
{
M
}
(
P
:
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
P
n
(
core
x
)
|}
.
...
...
@@ -103,10 +103,10 @@ Next Obligation.
intros
M
;
naive_solver
eauto
using
uPred_mono
,
@
cmra_core_monoN
.
Qed
.
Next
Obligation
.
naive_solver
eauto
using
uPred_closed
,
@
cmra_core_validN
.
Qed
.
Definition
uPred_always_aux
:
{
x
|
x
=
@
uPred_always_def
}
.
by
eexists
.
Qed
.
Definition
uPred_always
{
M
}
:=
proj1_sig
uPred_always_aux
M
.
Definition
uPred_always_aux
:
seal
(
@
uPred_always_def
)
.
by
eexists
.
Qed
.
Definition
uPred_always
{
M
}
:=
unseal
uPred_always_aux
M
.
Definition
uPred_always_eq
:
@
uPred_always
=
@
uPred_always_def
:=
proj2_sig
uPred_always_aux
.
@
uPred_always
=
@
uPred_always_def
:=
seal_eq
uPred_always_aux
.
Program
Definition
uPred_later_def
{
M
}
(
P
:
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
match
n
return
_
with
0
=>
True
|
S
n
'
=>
P
n
'
x
end
|}
.
...
...
@@ -116,10 +116,10 @@ Qed.
Next
Obligation
.
intros
M
P
[
|
n1
]
[
|
n2
]
x
;
eauto
using
uPred_closed
,
cmra_validN_S
with
lia
.
Qed
.
Definition
uPred_later_aux
:
{
x
|
x
=
@
uPred_later_def
}
.
by
eexists
.
Qed
.
Definition
uPred_later
{
M
}
:=
proj1_sig
uPred_later_aux
M
.
Definition
uPred_later_aux
:
seal
(
@
uPred_later_def
)
.
by
eexists
.
Qed
.
Definition
uPred_later
{
M
}
:=
unseal
uPred_later_aux
M
.
Definition
uPred_later_eq
:
@
uPred_later
=
@
uPred_later_def
:=
proj2_sig
uPred_later_aux
.
@
uPred_later
=
@
uPred_later_def
:=
seal_eq
uPred_later_aux
.
Program
Definition
uPred_ownM_def
{
M
:
ucmraT
}
(
a
:
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
a
≼
{
n
}
x
|}
.
...
...
@@ -128,18 +128,18 @@ Next Obligation.
exists
(
a
'
⋅
x2
).
by
rewrite
(
assoc
op
)
Hx1
.
Qed
.
Next
Obligation
.
naive_solver
eauto
using
cmra_includedN_le
.
Qed
.
Definition
uPred_ownM_aux
:
{
x
|
x
=
@
uPred_ownM_def
}
.
by
eexists
.
Qed
.
Definition
uPred_ownM
{
M
}
:=
proj1_sig
uPred_ownM_aux
M
.
Definition
uPred_ownM_aux
:
seal
(
@
uPred_ownM_def
)
.
by
eexists
.
Qed
.
Definition
uPred_ownM
{
M
}
:=
unseal
uPred_ownM_aux
M
.
Definition
uPred_ownM_eq
:
@
uPred_ownM
=
@
uPred_ownM_def
:=
proj2_sig
uPred_ownM_aux
.
@
uPred_ownM
=
@
uPred_ownM_def
:=
seal_eq
uPred_ownM_aux
.
Program
Definition
uPred_cmra_valid_def
{
M
}
{
A
:
cmraT
}
(
a
:
A
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
✓
{
n
}
a
|}
.
Solve
Obligations
with
naive_solver
eauto
2
using
cmra_validN_le
.
Definition
uPred_cmra_valid_aux
:
{
x
|
x
=
@
uPred_cmra_valid_def
}
.
by
eexists
.
Qed
.
Definition
uPred_cmra_valid
{
M
A
}
:=
proj1_sig
uPred_cmra_valid_aux
M
A
.
Definition
uPred_cmra_valid_aux
:
seal
(
@
uPred_cmra_valid_def
)
.
by
eexists
.
Qed
.
Definition
uPred_cmra_valid
{
M
A
}
:=
unseal
uPred_cmra_valid_aux
M
A
.
Definition
uPred_cmra_valid_eq
:
@
uPred_cmra_valid
=
@
uPred_cmra_valid_def
:=
proj2_sig
uPred_cmra_valid_aux
.
@
uPred_cmra_valid
=
@
uPred_cmra_valid_def
:=
seal_eq
uPred_cmra_valid_aux
.
Program
Definition
uPred_bupd_def
{
M
}
(
Q
:
uPred
M
)
:
uPred
M
:=
{|
uPred_holds
n
x
:=
∀
k
yf
,
...
...
@@ -152,9 +152,9 @@ Next Obligation.
apply
uPred_mono
with
x
'
;
eauto
using
cmra_includedN_l
.
Qed
.
Next
Obligation
.
naive_solver
.
Qed
.
Definition
uPred_bupd_aux
:
{
x
|
x
=
@
uPred_bupd_def
}
.
by
eexists
.
Qed
.
Definition
uPred_bupd
{
M
}
:=
proj1_sig
uPred_bupd_aux
M
.
Definition
uPred_bupd_eq
:
@
uPred_bupd
=
@
uPred_bupd_def
:=
proj2_sig
uPred_bupd_aux
.
Definition
uPred_bupd_aux
:
seal
(
@
uPred_bupd_def
)
.
by
eexists
.
Qed
.
Definition
uPred_bupd
{
M
}
:=
unseal
uPred_bupd_aux
M
.
Definition
uPred_bupd_eq
:
@
uPred_bupd
=
@
uPred_bupd_def
:=
seal_eq
uPred_bupd_aux
.
(
*
Latest
notation
*
)
Notation
"'⌜' φ '⌝'"
:=
(
uPred_pure
φ
%
C
%
type
)
...
...
@@ -194,11 +194,11 @@ Notation "P -∗ Q" := (P ⊢ Q)
(
at
level
99
,
Q
at
level
200
,
right
associativity
)
:
C_scope
.
Module
uPred
.
Definition
unseal
:=
Definition
unseal
_eqs
:=
(
uPred_pure_eq
,
uPred_and_eq
,
uPred_or_eq
,
uPred_impl_eq
,
uPred_forall_eq
,
uPred_exist_eq
,
uPred_internal_eq_eq
,
uPred_sep_eq
,
uPred_wand_eq
,
uPred_always_eq
,
uPred_later_eq
,
uPred_ownM_eq
,
uPred_cmra_valid_eq
,
uPred_bupd_eq
).
Ltac
unseal
:=
rewrite
!
unseal
/=
.
Ltac
unseal
:=
rewrite
!
unseal
_eqs
/=
.
Section
primitive
.
Context
{
M
:
ucmraT
}
.
...
...
theories/prelude/base.v
View file @
1f8c4338
...
...
@@ -14,6 +14,13 @@ Export ListNotations.
From
Coq
.
Program
Require
Export
Basics
Syntax
.
Obligation
Tactic
:=
idtac
.
(
**
Sealing
off
definitions
*
)
Set
Primitive
Projections
.
Record
seal
{
A
}
(
f
:
A
)
:=
{
unseal
:
A
;
seal_eq
:
unseal
=
f
}
.
Arguments
unseal
{
_
_
}
_.
Arguments
seal_eq
{
_
_
}
_.
Unset
Primitive
Projections
.
(
**
Throughout
this
development
we
use
[
C_scope
]
for
all
general
purpose
notations
that
do
not
belong
to
a
more
specific
scope
.
*
)
Delimit
Scope
C_scope
with
C
.
...
...
theories/program_logic/weakestpre.v
View file @
1f8c4338
...
...
@@ -31,9 +31,9 @@ Qed.
Definition
wp_def
`
{
irisG
Λ
Σ
}
:
coPset
→
expr
Λ
→
(
val
Λ
→
iProp
Σ
)
→
iProp
Σ
:=
fixpoint
wp_pre
.
Definition
wp_aux
:
{
x
|
x
=
@
wp_def
}
.
by
eexists
.
Qed
.
Definition
wp
:=
proj1_sig
wp_aux
.
Definition
wp_eq
:
@
wp
=
@
wp_def
:=
proj2_sig
wp_aux
.
Definition
wp_aux
:
seal
(
@
wp_def
)
.
by
eexists
.
Qed
.
Definition
wp
:=
unseal
wp_aux
.
Definition
wp_eq
:
@
wp
=
@
wp_def
:=
seal_eq
wp_aux
.
Arguments
wp
{
_
_
_
}
_
_
%
E
_.
Instance:
Params
(
@
wp
)
5.
...
...
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