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
Fairis
Commits
39843c62
Commit
39843c62
authored
Jun 06, 2018
by
Ralf Jung
Browse files
bump Iris; fix for old eauto hint db being gone
parent
2b850ccc
Pipeline
#9796
failed with stage
in 6 minutes and 47 seconds
Changes
3
Pipelines
11
Hide whitespace changes
Inline
Side-by-side
opam
View file @
39843c62
...
...
@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-0
5-29.6.4417e093
") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-0
6-05.5.4946e270
") | (= "dev") }
]
theories/algebra/upred_bi.v
View file @
39843c62
...
...
@@ -220,11 +220,12 @@ Section ATimeless_sbi.
Global
Instance
and_atimeless
P
Q
:
ATimeless
P
→
ATimeless
Q
→
ATimeless
(
P
∧
Q
).
Proof
.
intros
;
rewrite
/
ATimeless
affinely_and
except_0_and
later_and
!
affinely_and
.
auto
with
*
.
auto
using
and_mono
.
Qed
.
Global
Instance
or_atimeless
P
Q
:
ATimeless
P
→
ATimeless
Q
→
ATimeless
(
P
∨
Q
).
Proof
.
intros
;
rewrite
/
ATimeless
affinely_or
except_0_or
later_or
affinely_or
;
auto
with
*
.
intros
;
rewrite
/
ATimeless
affinely_or
except_0_or
later_or
affinely_or
.
auto
using
or_mono
.
Qed
.
(
*
...
...
theories/program_logic/ownership.v
View file @
39843c62
...
...
@@ -59,7 +59,7 @@ Global Instance ownG_proper : Proper ((≡) ==> (⊣⊢)) (@ownG Λ Σ) := ne_pr
Lemma
ownG_op
m1
m2
:
ownG
(
m1
⋅
m2
)
⊣⊢
ownG
m1
∗
ownG
m2
.
Proof
.
by
rewrite
/
ownG
-
upred_bi
.
ownM_op
''
Res_op
!
left_id
.
Qed
.
Global
Instance
ownG_mono
:
Proper
(
flip
(
≼
)
==>
(
⊢
))
(
@
ownG
Λ
Σ
).
Proof
.
move
=>
a
b
[
c
H
].
rewrite
H
ownG_op
.
eauto
with
*
.
Qed
.
Proof
.
move
=>
a
b
[
c
H
].
rewrite
H
ownG_op
.
apply
:
sep_elim_l
.
Qed
.
Lemma
ownG_valid
m
:
ownG
m
⊢
⧆
(
✓
m
).
Proof
.
rewrite
/
ownG
uPred
.
ownM_valid
res_validI
/=
.
rewrite
!
affinely_and
;
auto
with
*
.
Qed
.
Lemma
ownG_empty
:
emp
⊢
(
ownG
∅
:
iProp
Λ
Σ
).
...
...
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