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
George Pirlea
Iris
Commits
4763600e
Commit
4763600e
authored
Feb 18, 2016
by
Ralf Jung
Browse files
consistent name for exist_ne
parent
ab2b5816
Changes
2
Hide whitespace changes
Inline
Side-by-side
algebra/upred.v
View file @
4763600e
...
...
@@ -301,7 +301,7 @@ Proof. by intros n Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
Global
Instance
forall_proper
A
:
Proper
(
pointwise_relation
_
(
≡
)
==>
(
≡
))
(@
uPred_forall
M
A
).
Proof
.
by
intros
Ψ
1
Ψ
2
H
Ψ
n'
x
;
split
;
intros
HP
a
;
apply
H
Ψ
.
Qed
.
Global
Instance
exist
s
_ne
A
:
Global
Instance
exist_ne
A
:
Proper
(
pointwise_relation
_
(
dist
n
)
==>
dist
n
)
(@
uPred_exist
M
A
).
Proof
.
by
intros
n
P1
P2
HP
x
;
split
;
intros
[
a
?]
;
exists
a
;
apply
HP
.
Qed
.
Global
Instance
exist_proper
A
:
...
...
program_logic/invariants.v
View file @
4763600e
...
...
@@ -21,7 +21,7 @@ Implicit Types P Q R : iProp Λ Σ.
Implicit
Types
Φ
:
val
Λ
→
iProp
Λ
Σ
.
Global
Instance
inv_contractive
N
:
Contractive
(@
inv
Λ
Σ
N
).
Proof
.
intros
n
???.
apply
exist
s
_ne
=>
i
.
by
apply
and_ne
,
ownI_contractive
.
Qed
.
Proof
.
intros
n
???.
apply
exist_ne
=>
i
.
by
apply
and_ne
,
ownI_contractive
.
Qed
.
Global
Instance
inv_always_stable
N
P
:
AlwaysStable
(
inv
N
P
).
Proof
.
rewrite
/
inv
;
apply
_
.
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