Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Rodolphe Lepigre
Iris
Commits
7b9acc61
Commit
7b9acc61
authored
Sep 19, 2019
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Nump std++.
parent
ca3f9d11
Changes
10
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
16 additions
and
16 deletions
+16
-16
opam
opam
+1
-1
theories/algebra/gmap.v
theories/algebra/gmap.v
+1
-1
theories/algebra/gmultiset.v
theories/algebra/gmultiset.v
+2
-2
theories/algebra/list.v
theories/algebra/list.v
+3
-3
theories/algebra/updates.v
theories/algebra/updates.v
+2
-2
theories/base_logic/derived.v
theories/base_logic/derived.v
+1
-1
theories/base_logic/lib/boxes.v
theories/base_logic/lib/boxes.v
+1
-1
theories/base_logic/lib/invariants.v
theories/base_logic/lib/invariants.v
+2
-2
theories/base_logic/lib/own.v
theories/base_logic/lib/own.v
+1
-1
theories/heap_lang/lang.v
theories/heap_lang/lang.v
+2
-2
No files found.
opam
View file @
7b9acc61
...
...
@@ -12,5 +12,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (= "8.7.2") | (= "8.8.2") | (>= "8.9" & < "8.11~") | (= "dev") }
"coq-stdpp" { (= "dev.2019-09-19.
0.b53cbe77
") | (= "dev") }
"coq-stdpp" { (= "dev.2019-09-19.
1.9041e6d8
") | (= "dev") }
]
theories/algebra/gmap.v
View file @
7b9acc61
...
...
@@ -195,7 +195,7 @@ Global Instance lookup_op_homomorphism :
MonoidHomomorphism
op
op
(
≡
)
(
lookup
i
:
gmap
K
A
→
option
A
).
Proof
.
split
;
[
split
|]
;
try
apply
_
.
intros
m1
m2
;
by
rewrite
lookup_op
.
done
.
Qed
.
Lemma
lookup_opM
m1
mm2
i
:
(
m1
⋅
?
mm2
)
!!
i
=
m1
!!
i
⋅
(
mm2
≫
=
(!!
i
)).
Lemma
lookup_opM
m1
mm2
i
:
(
m1
⋅
?
mm2
)
!!
i
=
m1
!!
i
⋅
(
mm2
≫
=
(
.
!!
i
)).
Proof
.
destruct
mm2
;
by
rewrite
/=
?lookup_op
?right_id_L
.
Qed
.
Lemma
lookup_validN_Some
n
m
i
x
:
✓
{
n
}
m
→
m
!!
i
≡
{
n
}
≡
Some
x
→
✓
{
n
}
x
.
...
...
theories/algebra/gmultiset.v
View file @
7b9acc61
...
...
@@ -52,7 +52,7 @@ Section gmultiset.
Global
Instance
gmultiset_cancelable
X
:
Cancelable
X
.
Proof
.
apply
:
discrete_cancelable
=>
Y
Z
_
?.
fold_leibniz
.
by
apply
(
inj
(
X
⊎
)).
apply
:
discrete_cancelable
=>
Y
Z
_
?.
fold_leibniz
.
by
apply
(
inj
(
X
⊎
.
)).
Qed
.
Lemma
gmultiset_opM
X
mY
:
X
⋅
?
mY
=
X
⊎
default
∅
mY
.
...
...
@@ -64,7 +64,7 @@ Section gmultiset.
Lemma
gmultiset_local_update
X
Y
X'
Y'
:
X
⊎
Y'
=
X'
⊎
Y
→
(
X
,
Y
)
~l
~>
(
X'
,
Y'
).
Proof
.
intros
HXY
.
rewrite
local_update_unital_discrete
=>
Z'
_
.
intros
->%
leibniz_equiv
.
split
;
first
done
.
apply
leibniz_equiv_iff
,
(
inj
(
⊎
Y
)).
split
;
first
done
.
apply
leibniz_equiv_iff
,
(
inj
(
.
⊎
Y
)).
rewrite
-
HXY
!
gmultiset_op_disj_union
.
by
rewrite
-(
comm_L
_
Y
)
(
comm_L
_
Y'
)
assoc_L
.
Qed
.
...
...
theories/algebra/list.v
View file @
7b9acc61
...
...
@@ -278,7 +278,7 @@ Section properties.
Local
Arguments
cmra_op
_
!
_
!
_
/
:
simpl
nomatch
.
Local
Arguments
ucmra_op
_
!
_
!
_
/
:
simpl
nomatch
.
Lemma
list_lookup_opM
l
mk
i
:
(
l
⋅
?
mk
)
!!
i
=
l
!!
i
⋅
(
mk
≫
=
(!!
i
)).
Lemma
list_lookup_opM
l
mk
i
:
(
l
⋅
?
mk
)
!!
i
=
l
!!
i
⋅
(
mk
≫
=
(
.
!!
i
)).
Proof
.
destruct
mk
;
by
rewrite
/=
?list_lookup_op
?right_id_L
.
Qed
.
Global
Instance
list_op_nil_l
:
LeftId
(=)
(@
nil
A
)
op
.
...
...
@@ -426,7 +426,7 @@ Section properties.
(* FIXME
Lemma list_middle_local_update l1 l2 x y ml :
x ~l~> y @ ml ≫= (!! length l1) →
x ~l~> y @ ml ≫= (
.
!! length l1) →
l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
Proof.
intros [Hxy Hxy']; split.
...
...
@@ -446,7 +446,7 @@ Section properties.
rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
Qed.
Lemma list_singleton_local_update i x y ml :
x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
x ~l~> y @ ml ≫= (
.
!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
*)
...
...
theories/algebra/updates.v
View file @
7b9acc61
...
...
@@ -32,7 +32,7 @@ Proof.
rewrite
/
cmra_update
=>
x
x'
Hx
y
y'
Hy
;
split
=>
?
n
mz
?
;
setoid_subst
;
auto
.
Qed
.
Lemma
cmra_update_updateP
x
y
:
x
~~>
y
↔
x
~~>
:
(
y
=).
Lemma
cmra_update_updateP
x
y
:
x
~~>
y
↔
x
~~>
:
(
y
=
.
).
Proof
.
split
=>
Hup
n
z
?
;
eauto
.
destruct
(
Hup
n
z
)
as
(?&<-&?)
;
auto
.
Qed
.
Lemma
cmra_updateP_id
(
P
:
A
→
Prop
)
x
:
P
x
→
x
~~>
:
P
.
Proof
.
intros
?
n
mz
?
;
eauto
.
Qed
.
...
...
@@ -42,7 +42,7 @@ Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed.
Lemma
cmra_updateP_compose_l
(
Q
:
A
→
Prop
)
x
y
:
x
~~>
y
→
y
~~>
:
Q
→
x
~~>
:
Q
.
Proof
.
rewrite
cmra_update_updateP
.
intros
;
apply
cmra_updateP_compose
with
(
y
=)
;
naive_solver
.
intros
;
apply
cmra_updateP_compose
with
(
y
=
.
)
;
naive_solver
.
Qed
.
Lemma
cmra_updateP_weaken
(
P
Q
:
A
→
Prop
)
x
:
x
~~>
:
P
→
(
∀
y
,
P
y
→
Q
y
)
→
x
~~>
:
Q
.
...
...
theories/base_logic/derived.v
View file @
7b9acc61
...
...
@@ -55,7 +55,7 @@ Proof.
Qed
.
Lemma
bupd_ownM_update
x
y
:
x
~~>
y
→
uPred_ownM
x
⊢
|==>
uPred_ownM
y
.
Proof
.
intros
;
rewrite
(
bupd_ownM_updateP
_
(
y
=))
;
last
by
apply
cmra_update_updateP
.
intros
;
rewrite
(
bupd_ownM_updateP
_
(
y
=
.
))
;
last
by
apply
cmra_update_updateP
.
by
apply
bupd_mono
,
exist_elim
=>
y'
;
apply
pure_elim_l
=>
->.
Qed
.
...
...
theories/base_logic/lib/boxes.v
View file @
7b9acc61
...
...
@@ -220,7 +220,7 @@ Qed.
Lemma
box_empty
E
f
P
:
↑
N
⊆
E
→
map_Forall
(
λ
_
,
(
true
=))
f
→
map_Forall
(
λ
_
,
(
true
=
.
))
f
→
box
N
f
P
={
E
}=
∗
▷
P
∗
box
N
(
const
false
<$>
f
)
P
.
Proof
.
iDestruct
1
as
(
Φ
)
"[#HeqP Hf]"
.
...
...
theories/base_logic/lib/invariants.v
View file @
7b9acc61
...
...
@@ -53,7 +53,7 @@ Qed.
Lemma
inv_alloc
N
E
P
:
▷
P
={
E
}=
∗
inv
N
P
.
Proof
.
rewrite
inv_eq
/
inv_def
uPred_fupd_eq
.
iIntros
"HP [Hw $]"
.
iMod
(
ownI_alloc
(
∈
(
↑
N
:
coPset
))
P
with
"[$HP $Hw]"
)
iMod
(
ownI_alloc
(
.
∈
(
↑
N
:
coPset
))
P
with
"[$HP $Hw]"
)
as
(
i
?)
"[$ ?]"
;
auto
using
fresh_inv_name
.
do
2
iModIntro
.
iExists
i
,
P
.
rewrite
-(
iff_refl
True
%
I
).
auto
.
Qed
.
...
...
@@ -62,7 +62,7 @@ Lemma inv_alloc_open N E P :
↑
N
⊆
E
→
(|={
E
,
E
∖↑
N
}=>
inv
N
P
∗
(
▷
P
={
E
∖↑
N
,
E
}=
∗
True
))%
I
.
Proof
.
rewrite
inv_eq
/
inv_def
uPred_fupd_eq
.
iIntros
(
Sub
)
"[Hw HE]"
.
iMod
(
ownI_alloc_open
(
∈
(
↑
N
:
coPset
))
P
with
"Hw"
)
iMod
(
ownI_alloc_open
(
.
∈
(
↑
N
:
coPset
))
P
with
"Hw"
)
as
(
i
?)
"(Hw & #Hi & HD)"
;
auto
using
fresh_inv_name
.
iAssert
(
ownE
{[
i
]}
∗
ownE
(
↑
N
∖
{[
i
]})
∗
ownE
(
E
∖
↑
N
))%
I
with
"[HE]"
as
"(HEi & HEN\i & HE\N)"
.
...
...
theories/base_logic/lib/own.v
View file @
7b9acc61
...
...
@@ -184,7 +184,7 @@ Qed.
Lemma
own_update
γ
a
a'
:
a
~~>
a'
→
own
γ
a
==
∗
own
γ
a'
.
Proof
.
intros
;
rewrite
(
own_updateP
(
a'
=))
;
last
by
apply
cmra_update_updateP
.
intros
;
rewrite
(
own_updateP
(
a'
=
.
))
;
last
by
apply
cmra_update_updateP
.
by
apply
bupd_mono
,
exist_elim
=>
a''
;
apply
pure_elim_l
=>
->.
Qed
.
Lemma
own_update_2
γ
a1
a2
a'
:
...
...
theories/heap_lang/lang.v
View file @
7b9acc61
...
...
@@ -657,7 +657,7 @@ Inductive head_step : expr → state → list observation → expr → state →
p
∉
σ
.(
used_proph_id
)
→
head_step
NewProph
σ
[]
(
Val
$
LitV
$
LitProphecy
p
)
(
state_upd_used_proph_id
({[
p
]}
∪
)
σ
)
(
Val
$
LitV
$
LitProphecy
p
)
(
state_upd_used_proph_id
({[
p
]}
∪
.
)
σ
)
[]
|
ResolveS
p
v
e
σ
w
σ
'
κ
s
ts
:
head_step
e
σ
κ
s
(
Val
v
)
σ
'
ts
→
...
...
@@ -698,7 +698,7 @@ Qed.
Lemma
new_proph_id_fresh
σ
:
let
p
:
=
fresh
σ
.(
used_proph_id
)
in
head_step
NewProph
σ
[]
(
Val
$
LitV
$
LitProphecy
p
)
(
state_upd_used_proph_id
({[
p
]}
∪
)
σ
)
[].
head_step
NewProph
σ
[]
(
Val
$
LitV
$
LitProphecy
p
)
(
state_upd_used_proph_id
({[
p
]}
∪
.
)
σ
)
[].
Proof
.
constructor
.
apply
is_fresh
.
Qed
.
Lemma
heap_lang_mixin
:
EctxiLanguageMixin
of_val
to_val
fill_item
head_step
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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