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
dfa6603a
Commit
dfa6603a
authored
Sep 21, 2017
by
Robbert Krebbers
Browse files
Bump stdpp.
parent
e813387b
Changes
7
Hide whitespace changes
Inline
Side-by-side
opam
View file @
dfa6603a
...
...
@@ -12,5 +12,5 @@ remove: ["sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'"]
depends: [
"coq" { >= "8.6.1" & < "8.8~" }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq-stdpp" { (= "
dev.
2017-09-2
0
.2") | (= "dev") }
"coq-stdpp" { (= "2017-09-2
1
.2") | (= "dev") }
]
opam.pins
View file @
dfa6603a
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp
9b0f7c75a2387e0ad9fe5d16ec1083a0ece2bea3
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp
2f9f3d3f28aa568f5cbee1be5699f163800491c0
theories/algebra/big_op.v
View file @
dfa6603a
...
...
@@ -180,11 +180,11 @@ Section gmap.
Global
Instance
big_opM_ne
n
:
Proper
(
pointwise_relation
_
(
pointwise_relation
_
(
dist
n
))
==>
eq
==>
dist
n
)
(
big_opM
o
(
A
:
=
A
)).
(
big_opM
o
(
K
:
=
K
)
(
A
:
=
A
)).
Proof
.
intros
f
g
Hf
m
?
<-.
apply
big_opM_forall
;
apply
_
||
intros
;
apply
Hf
.
Qed
.
Global
Instance
big_opM_proper'
:
Proper
(
pointwise_relation
_
(
pointwise_relation
_
(
≡
))
==>
eq
==>
(
≡
))
(
big_opM
o
(
A
:
=
A
)).
(
big_opM
o
(
K
:
=
K
)
(
A
:
=
A
)).
Proof
.
intros
f
g
Hf
m
?
<-.
apply
big_opM_forall
;
apply
_
||
intros
;
apply
Hf
.
Qed
.
Lemma
big_opM_empty
f
:
([^
o
map
]
k
↦
x
∈
∅
,
f
k
x
)
=
monoid_unit
.
...
...
theories/algebra/gmap.v
View file @
dfa6603a
...
...
@@ -427,7 +427,7 @@ Lemma singleton_local_update m i x y x' y' :
(
m
,
{[
i
:
=
y
]})
~l
~>
(<[
i
:
=
x'
]>
m
,
{[
i
:
=
y'
]}).
Proof
.
intros
.
rewrite
/
singletonM
/
map_singleton
-(
insert_insert
∅
i
y'
y
).
eapply
insert_local_update
;
eauto
using
lookup_insert
.
by
eapply
insert_local_update
;
[|
eapply
lookup_insert
|]
.
Qed
.
Lemma
delete_local_update
m1
m2
i
x
`
{!
Exclusive
x
}
:
...
...
@@ -446,7 +446,7 @@ Lemma delete_singleton_local_update m i x `{!Exclusive x} :
(
m
,
{[
i
:
=
x
]})
~l
~>
(
delete
i
m
,
∅
).
Proof
.
rewrite
-(
delete_singleton
i
x
).
eapply
delete_local_update
;
eauto
using
lookup_singleton
.
by
eapply
delete_local_update
,
lookup_singleton
.
Qed
.
Lemma
delete_local_update_cancelable
m1
m2
i
mx
`
{!
Cancelable
mx
}
:
...
...
theories/base_logic/big_op.v
View file @
dfa6603a
...
...
@@ -213,7 +213,7 @@ Section gmap.
Global
Instance
big_sepM_mono'
:
Proper
(
pointwise_relation
_
(
pointwise_relation
_
(
⊢
))
==>
(=)
==>
(
⊢
))
(
big_opM
(@
uPred_sep
M
)
(
A
:
=
A
)).
(
big_opM
(@
uPred_sep
M
)
(
K
:
=
K
)
(
A
:
=
A
)).
Proof
.
intros
f
g
Hf
m
?
<-.
apply
big_opM_forall
;
apply
_
||
intros
;
apply
Hf
.
Qed
.
Lemma
big_sepM_empty
Φ
:
([
∗
map
]
k
↦
x
∈
∅
,
Φ
k
x
)
⊣
⊢
True
.
...
...
theories/base_logic/lib/gen_heap.v
View file @
dfa6603a
...
...
@@ -15,6 +15,7 @@ Class gen_heapG (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
gen_heap_inG
:
>
inG
Σ
(
authR
(
gen_heapUR
L
V
))
;
gen_heap_name
:
gname
}.
Arguments
gen_heap_name
{
_
_
_
_
_
}
_
:
assert
.
Class
gen_heapPreG
(
L
V
:
Type
)
(
Σ
:
gFunctors
)
`
{
Countable
L
}
:
=
{
gen_heap_preG_inG
:
>
inG
Σ
(
authR
(
gen_heapUR
L
V
))
}.
...
...
@@ -27,13 +28,13 @@ Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
Proof
.
solve_inG
.
Qed
.
Section
definitions
.
Context
`
{
gen_heapG
L
V
Σ
}.
Context
`
{
hG
:
gen_heapG
L
V
Σ
}.
Definition
gen_heap_ctx
(
σ
:
gmap
L
V
)
:
iProp
Σ
:
=
own
gen_heap_name
(
●
to_gen_heap
σ
).
own
(
gen_heap_name
hG
)
(
●
(
to_gen_heap
σ
)
)
.
Definition
mapsto_def
(
l
:
L
)
(
q
:
Qp
)
(
v
:
V
)
:
iProp
Σ
:
=
own
gen_heap_name
(
◯
{[
l
:
=
(
q
,
to_agree
(
v
:
leibnizC
V
))
]}).
own
(
gen_heap_name
hG
)
(
◯
{[
l
:
=
(
q
,
to_agree
(
v
:
leibnizC
V
))
]}).
Definition
mapsto_aux
:
seal
(@
mapsto_def
).
by
eexists
.
Qed
.
Definition
mapsto
:
=
unseal
mapsto_aux
.
Definition
mapsto_eq
:
@
mapsto
=
@
mapsto_def
:
=
seal_eq
mapsto_aux
.
...
...
@@ -77,6 +78,8 @@ Section gen_heap.
Implicit
Types
Φ
:
V
→
iProp
Σ
.
Implicit
Types
σ
:
gmap
L
V
.
Implicit
Types
h
g
:
gen_heapUR
L
V
.
Implicit
Types
l
:
L
.
Implicit
Types
v
:
V
.
(** General properties of mapsto *)
Global
Instance
mapsto_timeless
l
q
v
:
TimelessP
(
l
↦
{
q
}
v
).
...
...
theories/heap_lang/lang.v
View file @
dfa6603a
...
...
@@ -394,7 +394,7 @@ Qed.
Lemma
alloc_fresh
e
v
σ
:
let
l
:
=
fresh
(
dom
(
gset
loc
)
σ
)
in
to_val
e
=
Some
v
→
head_step
(
Alloc
e
)
σ
(
Lit
(
LitLoc
l
))
(<[
l
:
=
v
]>
σ
)
[].
Proof
.
by
intros
;
apply
AllocS
,
(
not_elem_of_dom
(
D
:
=
gset
_
)),
is_fresh
.
Qed
.
Proof
.
by
intros
;
apply
AllocS
,
(
not_elem_of_dom
(
D
:
=
gset
loc
)),
is_fresh
.
Qed
.
(* Misc *)
Lemma
to_val_rec
f
x
e
`
{!
Closed
(
f
:
b
:
x
:
b
:
[])
e
}
:
...
...
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