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
Iris
Iris
Commits
f49a7f18
Commit
f49a7f18
authored
Nov 30, 2016
by
Jacques-Henri Jourdan
Browse files
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
parents
9ae19ed5
38d61951
Pipeline
#3186
passed with stage
in 10 minutes and 40 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
base_logic/big_op.v
View file @
f49a7f18
...
...
@@ -526,6 +526,17 @@ Section gset.
by
rewrite
!
big_sepS_insert
//
IH
pure_False
//
False_impl
left_id
.
Qed
.
Lemma
big_sepS_filter_acc
(
P
:
A
→
Prop
)
`
{
∀
y
,
Decision
(
P
y
)}
Φ
X
Y
:
(
∀
y
,
y
∈
Y
→
P
y
→
y
∈
X
)
→
([
∗
set
]
y
∈
X
,
Φ
y
)
-
∗
([
∗
set
]
y
∈
Y
,
⌜
P
y
⌝
→
Φ
y
)
∗
(([
∗
set
]
y
∈
Y
,
⌜
P
y
⌝
→
Φ
y
)
-
∗
[
∗
set
]
y
∈
X
,
Φ
y
).
Proof
.
intros
?.
destruct
(
proj1
(
subseteq_disjoint_union_L
(
filter
P
Y
)
X
))
as
(
Z
&->&?)
;
first
set_solver
.
rewrite
big_sepS_union
//
big_sepS_filter
.
by
apply
sep_mono_r
,
wand_intro_l
.
Qed
.
Lemma
big_sepS_sepS
Φ
Ψ
X
:
([
∗
set
]
y
∈
X
,
Φ
y
∗
Ψ
y
)
⊣
⊢
([
∗
set
]
y
∈
X
,
Φ
y
)
∗
([
∗
set
]
y
∈
X
,
Ψ
y
).
Proof
.
apply
:
big_opS_opS
.
Qed
.
...
...
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