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
Rice Wine
Iris
Commits
411de288
Commit
411de288
authored
Nov 11, 2015
by
Robbert Krebbers
Browse files
Now compiles with 8.5 beta 3.
parent
a123e160
Changes
6
Hide whitespace changes
Inline
Side-by-side
iris/logic.v
View file @
411de288
...
...
@@ -92,7 +92,7 @@ Solve Obligations with naive_solver eauto 2 using (dist_le (A:=B)).
Program
Definition
iprop_sep
{
A
}
(
P
Q
:
iProp
A
)
:
iProp
A
:
=
{|
iprop_holds
n
x
:
=
∃
x1
x2
,
x
={
n
}=
x1
⋅
x2
∧
P
n
x1
∧
Q
n
x2
|}.
Next
Obligation
.
by
intros
A
P
Q
x
y
n
(
x1
&
x2
&?&?&?)
Hxy
;
exists
x1
x2
;
rewrite
<-
Hxy
.
by
intros
A
P
Q
x
y
n
(
x1
&
x2
&?&?&?)
Hxy
;
exists
x1
,
x2
;
rewrite
<-
Hxy
.
Qed
.
Next
Obligation
.
intros
A
P
Q
x
y
n1
n2
Hxy
??
(
x1
&
x2
&
Hx
&?&?).
...
...
@@ -100,7 +100,7 @@ Next Obligation.
{
rewrite
ra_included_spec
in
Hxy
;
destruct
Hxy
as
[
z
Hy
].
exists
(
x2
⋅
z
)
;
split
;
eauto
using
ra_included_l
.
apply
dist_le
with
n1
;
auto
.
by
rewrite
(
associative
op
),
<-
Hx
,
Hy
.
}
exists
x1
x2'
;
split_ands
;
auto
.
exists
x1
,
x2'
;
split_ands
;
auto
.
*
apply
iprop_weaken
with
x1
n1
;
auto
.
by
apply
cmra_valid_op_l
with
x2'
;
rewrite
<-
Hy
.
*
apply
iprop_weaken
with
x2
n1
;
auto
.
...
...
@@ -194,7 +194,7 @@ Global Instance iprop_sep_ne n :
Proper
(
dist
n
==>
dist
n
==>
dist
n
)
(@
iprop_sep
A
).
Proof
.
intros
P
P'
HP
Q
Q'
HQ
x
n'
?
Hx'
;
split
;
intros
(
x1
&
x2
&
Hx
&?&?)
;
exists
x1
x2
;
rewrite
Hx
in
Hx'
;
split_ands
;
try
apply
HP
;
try
apply
HQ
;
exists
x1
,
x2
;
rewrite
Hx
in
Hx'
;
split_ands
;
try
apply
HP
;
try
apply
HQ
;
eauto
using
cmra_valid_op_l
,
cmra_valid_op_r
.
Qed
.
Global
Instance
iprop_wand_ne
n
:
...
...
@@ -262,27 +262,27 @@ Proof.
intros
P
x
n
Hvalid
;
split
.
*
intros
(
x1
&
x2
&
Hx
&
_
&?)
;
rewrite
Hx
in
Hvalid
|-
*.
apply
iprop_weaken
with
x2
n
;
auto
using
ra_included_r
.
*
by
intros
?
;
exists
(
unit
x
)
x
;
rewrite
ra_unit_l
.
*
by
intros
?
;
exists
(
unit
x
)
,
x
;
rewrite
ra_unit_l
.
Qed
.
Global
Instance
iprop_sep_commutative
:
Commutative
(
≡
)
(@
iprop_sep
A
).
Proof
.
by
intros
P
Q
x
n
?
;
split
;
intros
(
x1
&
x2
&?&?&?)
;
exists
x2
x1
;
rewrite
(
commutative
op
).
intros
(
x1
&
x2
&?&?&?)
;
exists
x2
,
x1
;
rewrite
(
commutative
op
).
Qed
.
Global
Instance
iprop_sep_associative
:
Associative
(
≡
)
(@
iprop_sep
A
).
Proof
.
intros
P
Q
R
x
n
?
;
split
.
*
intros
(
x1
&
x2
&
Hx
&?&
y1
&
y2
&
Hy
&?&?)
;
exists
(
x1
⋅
y1
)
y2
;
split_ands
;
auto
.
*
intros
(
x1
&
x2
&
Hx
&?&
y1
&
y2
&
Hy
&?&?)
;
exists
(
x1
⋅
y1
)
,
y2
;
split_ands
;
auto
.
+
by
rewrite
<-(
associative
op
),
<-
Hy
,
<-
Hx
.
+
by
exists
x1
y1
.
*
intros
(
x1
&
x2
&
Hx
&(
y1
&
y2
&
Hy
&?&?)&?)
;
exists
y1
(
y2
⋅
x2
)
;
split_ands
;
auto
.
+
by
exists
x1
,
y1
.
*
intros
(
x1
&
x2
&
Hx
&(
y1
&
y2
&
Hy
&?&?)&?)
;
exists
y1
,
(
y2
⋅
x2
)
;
split_ands
;
auto
.
+
by
rewrite
(
associative
op
),
<-
Hy
,
<-
Hx
.
+
by
exists
y2
x2
.
+
by
exists
y2
,
x2
.
Qed
.
Lemma
iprop_wand_intro
P
Q
R
:
(
R
★
P
)%
I
⊆
Q
→
R
⊆
(
P
-
★
Q
)%
I
.
Proof
.
intros
HPQ
x
n
??
x'
n'
???
;
apply
HPQ
;
auto
.
exists
x
x'
;
split_ands
;
auto
.
exists
x
,
x'
;
split_ands
;
auto
.
eapply
iprop_weaken
with
x
n
;
eauto
using
cmra_valid_op_l
.
Qed
.
Lemma
iprop_wand_elim
P
Q
:
((
P
-
★
Q
)
★
P
)%
I
⊆
Q
.
...
...
@@ -291,21 +291,21 @@ Proof.
Qed
.
Lemma
iprop_sep_or
P
Q
R
:
((
P
∨
Q
)
★
R
)%
I
≡
((
P
★
R
)
∨
(
Q
★
R
))%
I
.
Proof
.
split
;
[
by
intros
(
x1
&
x2
&
Hx
&[?|?]&?)
;
[
left
|
right
]
;
exists
x1
x2
|].
intros
[(
x1
&
x2
&
Hx
&?&?)|(
x1
&
x2
&
Hx
&?&?)]
;
exists
x1
x2
;
split_ands
;
split
;
[
by
intros
(
x1
&
x2
&
Hx
&[?|?]&?)
;
[
left
|
right
]
;
exists
x1
,
x2
|].
intros
[(
x1
&
x2
&
Hx
&?&?)|(
x1
&
x2
&
Hx
&?&?)]
;
exists
x1
,
x2
;
split_ands
;
first
[
by
left
|
by
right
|
done
].
Qed
.
Lemma
iprop_sep_and
P
Q
R
:
((
P
∧
Q
)
★
R
)%
I
⊆
((
P
★
R
)
∧
(
Q
★
R
))%
I
.
Proof
.
by
intros
x
n
?
(
x1
&
x2
&
Hx
&[??]&?)
;
split
;
exists
x1
x2
.
Qed
.
Proof
.
by
intros
x
n
?
(
x1
&
x2
&
Hx
&[??]&?)
;
split
;
exists
x1
,
x2
.
Qed
.
Lemma
iprop_sep_exist
{
B
}
(
P
:
B
→
iProp
A
)
Q
:
((
∃
b
,
P
b
)
★
Q
)%
I
≡
(
∃
b
,
P
b
★
Q
)%
I
.
Proof
.
split
;
[
by
intros
(
x1
&
x2
&
Hx
&[
b
?]&?)
;
exists
b
x1
x2
|].
intros
[
b
(
x1
&
x2
&
Hx
&?&?)]
;
exists
x1
x2
;
split_ands
;
by
try
exists
b
.
split
;
[
by
intros
(
x1
&
x2
&
Hx
&[
b
?]&?)
;
exists
b
,
x1
,
x2
|].
intros
[
b
(
x1
&
x2
&
Hx
&?&?)]
;
exists
x1
,
x2
;
split_ands
;
by
try
exists
b
.
Qed
.
Lemma
iprop_sep_forall
`
(
P
:
B
→
iProp
A
)
Q
:
((
∀
b
,
P
b
)
★
Q
)%
I
⊆
(
∀
b
,
P
b
★
Q
)%
I
.
Proof
.
by
intros
x
n
?
(
x1
&
x2
&
Hx
&?&?)
;
intros
b
;
exists
x1
x2
.
Qed
.
Proof
.
by
intros
x
n
?
(
x1
&
x2
&
Hx
&?&?)
;
intros
b
;
exists
x1
,
x2
.
Qed
.
(* Later *)
Global
Instance
iprop_later_contractive
:
Contractive
(@
iprop_later
A
).
...
...
@@ -345,12 +345,12 @@ Qed.
Lemma
iprop_later_sep
P
Q
:
(
▷
(
P
★
Q
))%
I
≡
(
▷
P
★
▷
Q
)%
I
.
Proof
.
intros
x
n
?
;
split
.
*
destruct
n
as
[|
n
]
;
simpl
;
[
by
exists
x
x
|
intros
(
x1
&
x2
&
Hx
&?&?)].
*
destruct
n
as
[|
n
]
;
simpl
;
[
by
exists
x
,
x
|
intros
(
x1
&
x2
&
Hx
&?&?)].
destruct
(
cmra_extend_op
x
x1
x2
n
)
as
([
y1
y2
]&
Hx'
&
Hy1
&
Hy2
)
;
auto
using
cmra_valid_S
;
simpl
in
*.
exists
y1
y2
;
split
;
[
by
rewrite
Hx'
|
by
rewrite
Hy1
,
Hy2
].
exists
y1
,
y2
;
split
;
[
by
rewrite
Hx'
|
by
rewrite
Hy1
,
Hy2
].
*
destruct
n
as
[|
n
]
;
simpl
;
[
done
|
intros
(
x1
&
x2
&
Hx
&?&?)].
exists
x1
x2
;
eauto
using
(
dist_S
(
A
:
=
A
)).
exists
x1
,
x2
;
eauto
using
(
dist_S
(
A
:
=
A
)).
Qed
.
(* Always *)
...
...
@@ -378,7 +378,7 @@ Lemma iprop_always_exist `(P : B → iProp A) : (□ ∃ b, P b)%I ≡ (∃ b,
Proof
.
done
.
Qed
.
Lemma
iprop_always_and_always_box
P
Q
:
(
□
P
∧
Q
)%
I
⊆
(
□
P
★
Q
)%
I
.
Proof
.
intros
x
n
?
[??]
;
exists
(
unit
x
)
x
;
simpl
in
*.
intros
x
n
?
[??]
;
exists
(
unit
x
)
,
x
;
simpl
in
*.
by
rewrite
ra_unit_l
,
ra_unit_idempotent
.
Qed
.
...
...
prelude/fin_maps.v
View file @
411de288
...
...
@@ -656,7 +656,7 @@ Lemma map_choose {A} (m : M A) : m ≠ ∅ → ∃ i x, m !! i = Some x.
Proof
.
intros
Hemp
.
destruct
(
map_to_list
m
)
as
[|[
i
x
]
l
]
eqn
:
Hm
.
{
destruct
Hemp
;
eauto
using
map_to_list_empty_inv
.
}
exists
i
x
.
rewrite
<-
elem_of_map_to_list
,
Hm
.
by
left
.
exists
i
,
x
.
rewrite
<-
elem_of_map_to_list
,
Hm
.
by
left
.
Qed
.
(** Properties of the imap function *)
...
...
@@ -777,7 +777,7 @@ Proof.
split
;
[|
intros
(
i
&
x
&?&?)
Hm
;
specialize
(
Hm
i
x
)
;
tauto
].
rewrite
map_Forall_to_list
.
intros
Hm
.
apply
(
not_Forall_Exists
_
),
Exists_exists
in
Hm
.
destruct
Hm
as
([
i
x
]&?&?).
exists
i
x
.
by
rewrite
<-
elem_of_map_to_list
.
destruct
Hm
as
([
i
x
]&?&?).
exists
i
,
x
.
by
rewrite
<-
elem_of_map_to_list
.
Qed
.
End
map_Forall
.
...
...
prelude/hashset.v
View file @
411de288
...
...
@@ -85,7 +85,7 @@ Proof.
rewrite
elem_of_list_intersection
in
Hx
;
naive_solver
.
}
intros
[(
l
&?&?)
(
k
&?&?)].
assert
(
x
∈
list_intersection
l
k
)
by
(
by
rewrite
elem_of_list_intersection
).
exists
(
list_intersection
l
k
)
;
split
;
[
exists
l
k
|]
;
split_ands
;
auto
.
exists
(
list_intersection
l
k
)
;
split
;
[
exists
l
,
k
|]
;
split_ands
;
auto
.
by
rewrite
option_guard_True
by
eauto
using
elem_of_not_nil
.
*
unfold
elem_of
,
hashset_elem_of
,
intersection
,
hashset_intersection
.
intros
[
m1
?]
[
m2
?]
x
;
simpl
.
...
...
@@ -95,7 +95,7 @@ Proof.
intros
[(
l
&?&?)
Hm2
]
;
destruct
(
m2
!!
hash
x
)
as
[
k
|]
eqn
:
?
;
eauto
.
destruct
(
decide
(
x
∈
k
))
;
[
destruct
Hm2
;
eauto
|].
assert
(
x
∈
list_difference
l
k
)
by
(
by
rewrite
elem_of_list_difference
).
exists
(
list_difference
l
k
)
;
split
;
[
right
;
exists
l
k
|]
;
split_ands
;
auto
.
exists
(
list_difference
l
k
)
;
split
;
[
right
;
exists
l
,
k
|]
;
split_ands
;
auto
.
by
rewrite
option_guard_True
by
eauto
using
elem_of_not_nil
.
*
unfold
elem_of
at
2
,
hashset_elem_of
,
elements
,
hashset_elems
.
intros
[
m
Hm
]
x
;
simpl
.
setoid_rewrite
elem_of_list_bind
.
split
.
...
...
prelude/list.v
View file @
411de288
...
...
@@ -487,8 +487,8 @@ Lemma list_lookup_other l i x :
length
l
≠
1
→
l
!!
i
=
Some
x
→
∃
j
y
,
j
≠
i
∧
l
!!
j
=
Some
y
.
Proof
.
intros
.
destruct
i
,
l
as
[|
x0
[|
x1
l
]]
;
simplify_equality'
.
*
by
exists
1
x1
.
*
by
exists
0
x0
.
*
by
exists
1
,
x1
.
*
by
exists
0
,
x0
.
Qed
.
Lemma
alter_app_l
f
l1
l2
i
:
i
<
length
l1
→
alter
f
i
(
l1
++
l2
)
=
alter
f
i
l1
++
l2
.
...
...
@@ -604,7 +604,7 @@ Proof. induction 1; rewrite ?elem_of_nil, ?elem_of_cons; intuition. Qed.
Lemma
elem_of_list_split
l
x
:
x
∈
l
→
∃
l1
l2
,
l
=
l1
++
x
::
l2
.
Proof
.
induction
1
as
[
x
l
|
x
y
l
?
[
l1
[
l2
->]]]
;
[
by
eexists
[],
l
|].
by
exists
(
y
::
l1
)
l2
.
by
exists
(
y
::
l1
)
,
l2
.
Qed
.
Lemma
elem_of_list_lookup_1
l
x
:
x
∈
l
→
∃
i
,
l
!!
i
=
Some
x
.
Proof
.
...
...
@@ -1621,7 +1621,7 @@ Proof.
split
.
*
intros
Hlk
.
induction
k
as
[|
y
k
IH
]
;
inversion
Hlk
.
+
eexists
[],
k
.
by
repeat
constructor
.
+
destruct
IH
as
(
k1
&
k2
&->&?)
;
auto
.
by
exists
(
y
::
k1
)
k2
.
+
destruct
IH
as
(
k1
&
k2
&->&?)
;
auto
.
by
exists
(
y
::
k1
)
,
k2
.
*
intros
(
k1
&
k2
&->&?).
by
apply
sublist_inserts_l
,
sublist_skip
.
Qed
.
Lemma
sublist_app_r
l
k1
k2
:
...
...
@@ -1633,9 +1633,9 @@ Proof.
{
eexists
[],
l
.
by
repeat
constructor
.
}
rewrite
sublist_cons_r
.
intros
[?|(
l'
&
?
&?)]
;
subst
.
+
destruct
(
IH
l
k2
)
as
(
l1
&
l2
&?&?&?)
;
trivial
;
subst
.
exists
l1
l2
.
auto
using
sublist_cons
.
exists
l1
,
l2
.
auto
using
sublist_cons
.
+
destruct
(
IH
l'
k2
)
as
(
l1
&
l2
&?&?&?)
;
trivial
;
subst
.
exists
(
y
::
l1
)
l2
.
auto
using
sublist_skip
.
exists
(
y
::
l1
)
,
l2
.
auto
using
sublist_skip
.
*
intros
(?&?&?&?&?)
;
subst
.
auto
using
sublist_app
.
Qed
.
Lemma
sublist_app_l
l1
l2
k
:
...
...
@@ -1647,7 +1647,7 @@ Proof.
{
eexists
[],
k
.
by
repeat
constructor
.
}
rewrite
sublist_cons_l
.
intros
(
k1
&
k2
&?&?)
;
subst
.
destruct
(
IH
l2
k2
)
as
(
h1
&
h2
&?&?&?)
;
trivial
;
subst
.
exists
(
k1
++
x
::
h1
)
h2
.
rewrite
<-(
associative_L
(++)).
exists
(
k1
++
x
::
h1
)
,
h2
.
rewrite
<-(
associative_L
(++)).
auto
using
sublist_inserts_l
,
sublist_skip
.
*
intros
(?&?&?&?&?)
;
subst
.
auto
using
sublist_app
.
Qed
.
...
...
@@ -1865,7 +1865,7 @@ Proof.
split
.
*
rewrite
contains_sublist_r
.
intros
(
l'
&
E
&
Hl'
).
rewrite
sublist_app_r
in
Hl'
.
destruct
Hl'
as
(
l1
&
l2
&?&?&?)
;
subst
.
exists
l1
l2
.
eauto
using
sublist_contains
.
exists
l1
,
l2
.
eauto
using
sublist_contains
.
*
intros
(?&?&
E
&?&?).
rewrite
E
.
eauto
using
contains_app
.
Qed
.
Lemma
contains_app_l
l1
l2
k
:
...
...
@@ -1875,7 +1875,7 @@ Proof.
split
.
*
rewrite
contains_sublist_l
.
intros
(
l'
&
Hl'
&
E
).
rewrite
sublist_app_l
in
Hl'
.
destruct
Hl'
as
(
k1
&
k2
&?&?&?)
;
subst
.
exists
k1
k2
.
split
.
done
.
eauto
using
sublist_contains
.
exists
k1
,
k2
.
split
.
done
.
eauto
using
sublist_contains
.
*
intros
(?&?&
E
&?&?).
rewrite
E
.
eauto
using
contains_app
.
Qed
.
Lemma
contains_app_inv_l
l1
l2
k
:
...
...
@@ -2578,7 +2578,7 @@ Section fmap.
Proof
.
revert
l
.
induction
k1
as
[|
y
k1
IH
]
;
simpl
;
[
intros
l
?
;
by
eexists
[],
l
|].
intros
[|
x
l
]
?
;
simplify_equality'
.
destruct
(
IH
l
)
as
(
l1
&
l2
&->&->&->)
;
[
done
|].
by
exists
(
x
::
l1
)
l2
.
destruct
(
IH
l
)
as
(
l1
&
l2
&->&->&->)
;
[
done
|].
by
exists
(
x
::
l1
)
,
l2
.
Qed
.
Lemma
fmap_length
l
:
length
(
f
<$>
l
)
=
length
l
.
Proof
.
by
induction
l
;
f_equal'
.
Qed
.
...
...
@@ -3006,7 +3006,7 @@ Section zip_with.
{
intros
l
k
?.
by
eexists
[],
[],
l
,
k
.
}
intros
[|
x
l
]
[|
y
k
]
?
;
simplify_equality'
.
destruct
(
IH
l
k
)
as
(
l1
&
k1
&
l2
&
k2
&->&->&->&->&?)
;
[
done
|].
exists
(
x
::
l1
)
(
y
::
k1
)
l2
k2
;
simpl
;
auto
with
congruence
.
exists
(
x
::
l1
)
,
(
y
::
k1
)
,
l2
,
k2
;
simpl
;
auto
with
congruence
.
Qed
.
Lemma
zip_with_inj
`
{!
Injective2
(=)
(=)
(=)
f
}
l1
l2
k1
k2
:
length
l1
=
length
k1
→
length
l2
=
length
k2
→
...
...
prelude/natmap.v
View file @
411de288
...
...
@@ -19,7 +19,7 @@ Lemma natmap_wf_lookup {A} (l : natmap_raw A) :
Proof
.
intros
Hwf
Hl
.
induction
l
as
[|[
x
|]
l
IH
]
;
simpl
;
[
done
|
|].
{
exists
0
.
simpl
.
eauto
.
}
destruct
IH
as
(
i
&
x
&?)
;
eauto
using
natmap_wf_inv
;
[|
by
exists
(
S
i
)
x
].
destruct
IH
as
(
i
&
x
&?)
;
eauto
using
natmap_wf_inv
;
[|
by
exists
(
S
i
)
,
x
].
intros
->.
by
destruct
Hwf
.
Qed
.
...
...
prelude/pmap.v
View file @
411de288
...
...
@@ -114,9 +114,9 @@ Proof. by destruct i. Qed.
Lemma
Pmap_ne_lookup
{
A
}
(
t
:
Pmap_raw
A
)
:
Pmap_ne
t
→
∃
i
x
,
t
!!
i
=
Some
x
.
Proof
.
induction
1
as
[?
x
?|
l
r
?
IHl
|
l
r
?
IHr
].
*
intros
.
by
exists
1
x
.
*
destruct
IHl
as
[
i
[
x
?]].
by
exists
(
i
~
0
)
x
.
*
destruct
IHr
as
[
i
[
x
?]].
by
exists
(
i
~
1
)
x
.
*
intros
.
by
exists
1
,
x
.
*
destruct
IHl
as
[
i
[
x
?]].
by
exists
(
i
~
0
)
,
x
.
*
destruct
IHr
as
[
i
[
x
?]].
by
exists
(
i
~
1
)
,
x
.
Qed
.
Lemma
Pmap_wf_eq_get
{
A
}
(
t1
t2
:
Pmap_raw
A
)
:
...
...
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