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
Iris
Iris
Commits
ee3b01dd
Commit
ee3b01dd
authored
Feb 11, 2016
by
Ralf Jung
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
parents
2b80e398
cd41721d
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
32 additions
and
10 deletions
+32
-10
algebra/upred.v
algebra/upred.v
+32
-10
No files found.
algebra/upred.v
View file @
ee3b01dd
...
@@ -230,6 +230,10 @@ Arguments timelessP {_} _ {_} _ _ _ _.
...
@@ -230,6 +230,10 @@ Arguments timelessP {_} _ {_} _ _ _ _.
Class
AlwaysStable
{
M
}
(
P
:
uPred
M
)
:
=
always_stable
:
P
⊑
□
P
.
Class
AlwaysStable
{
M
}
(
P
:
uPred
M
)
:
=
always_stable
:
P
⊑
□
P
.
Arguments
always_stable
{
_
}
_
{
_
}
_
_
_
_
.
Arguments
always_stable
{
_
}
_
{
_
}
_
_
_
_
.
Class
AlwaysStableL
{
M
}
(
Ps
:
list
(
uPred
M
))
:
=
always_stableL
:
Forall
AlwaysStable
Ps
.
Arguments
always_stableL
{
_
}
_
{
_
}.
Module
uPred
.
Section
uPred_logic
.
Module
uPred
.
Section
uPred_logic
.
Context
{
M
:
cmraT
}.
Context
{
M
:
cmraT
}.
Implicit
Types
φ
:
Prop
.
Implicit
Types
φ
:
Prop
.
...
@@ -823,33 +827,33 @@ Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
...
@@ -823,33 +827,33 @@ Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
Proof
.
by
intros
;
rewrite
ownM_valid
valid_elim
.
Qed
.
Proof
.
by
intros
;
rewrite
ownM_valid
valid_elim
.
Qed
.
(* Big ops *)
(* Big ops *)
Global
Instance
uPred_
big_and_proper
:
Proper
((
≡
)
==>
(
≡
))
(@
uPred_big_and
M
).
Global
Instance
big_and_proper
:
Proper
((
≡
)
==>
(
≡
))
(@
uPred_big_and
M
).
Proof
.
by
induction
1
as
[|
P
Q
Ps
Qs
HPQ
?
IH
]
;
rewrite
/=
?HPQ
?IH
.
Qed
.
Proof
.
by
induction
1
as
[|
P
Q
Ps
Qs
HPQ
?
IH
]
;
rewrite
/=
?HPQ
?IH
.
Qed
.
Global
Instance
uPred_
big_sep_proper
:
Proper
((
≡
)
==>
(
≡
))
(@
uPred_big_sep
M
).
Global
Instance
big_sep_proper
:
Proper
((
≡
)
==>
(
≡
))
(@
uPred_big_sep
M
).
Proof
.
by
induction
1
as
[|
P
Q
Ps
Qs
HPQ
?
IH
]
;
rewrite
/=
?HPQ
?IH
.
Qed
.
Proof
.
by
induction
1
as
[|
P
Q
Ps
Qs
HPQ
?
IH
]
;
rewrite
/=
?HPQ
?IH
.
Qed
.
Global
Instance
uPred_
big_and_perm
:
Proper
((
≡
ₚ
)
==>
(
≡
))
(@
uPred_big_and
M
).
Global
Instance
big_and_perm
:
Proper
((
≡
ₚ
)
==>
(
≡
))
(@
uPred_big_and
M
).
Proof
.
Proof
.
induction
1
as
[|
P
Ps
Qs
?
IH
|
P
Q
Ps
|]
;
simpl
;
auto
.
induction
1
as
[|
P
Ps
Qs
?
IH
|
P
Q
Ps
|]
;
simpl
;
auto
.
*
by
rewrite
IH
.
*
by
rewrite
IH
.
*
by
rewrite
!
associative
(
commutative
_
P
).
*
by
rewrite
!
associative
(
commutative
_
P
).
*
etransitivity
;
eauto
.
*
etransitivity
;
eauto
.
Qed
.
Qed
.
Global
Instance
uPred_
big_sep_perm
:
Proper
((
≡
ₚ
)
==>
(
≡
))
(@
uPred_big_sep
M
).
Global
Instance
big_sep_perm
:
Proper
((
≡
ₚ
)
==>
(
≡
))
(@
uPred_big_sep
M
).
Proof
.
Proof
.
induction
1
as
[|
P
Ps
Qs
?
IH
|
P
Q
Ps
|]
;
simpl
;
auto
.
induction
1
as
[|
P
Ps
Qs
?
IH
|
P
Q
Ps
|]
;
simpl
;
auto
.
*
by
rewrite
IH
.
*
by
rewrite
IH
.
*
by
rewrite
!
associative
(
commutative
_
P
).
*
by
rewrite
!
associative
(
commutative
_
P
).
*
etransitivity
;
eauto
.
*
etransitivity
;
eauto
.
Qed
.
Qed
.
Lemma
uPred_
big_and_app
Ps
Qs
:
(
Π
∧
(
Ps
++
Qs
))%
I
≡
(
Π
∧
Ps
∧
Π
∧
Qs
)%
I
.
Lemma
big_and_app
Ps
Qs
:
(
Π
∧
(
Ps
++
Qs
))%
I
≡
(
Π
∧
Ps
∧
Π
∧
Qs
)%
I
.
Proof
.
by
induction
Ps
as
[|??
IH
]
;
rewrite
/=
?left_id
-
?associative
?IH
.
Qed
.
Proof
.
by
induction
Ps
as
[|??
IH
]
;
rewrite
/=
?left_id
-
?associative
?IH
.
Qed
.
Lemma
uPred_
big_sep_app
Ps
Qs
:
(
Π★
(
Ps
++
Qs
))%
I
≡
(
Π★
Ps
★
Π★
Qs
)%
I
.
Lemma
big_sep_app
Ps
Qs
:
(
Π★
(
Ps
++
Qs
))%
I
≡
(
Π★
Ps
★
Π★
Qs
)%
I
.
Proof
.
by
induction
Ps
as
[|??
IH
]
;
rewrite
/=
?left_id
-
?associative
?IH
.
Qed
.
Proof
.
by
induction
Ps
as
[|??
IH
]
;
rewrite
/=
?left_id
-
?associative
?IH
.
Qed
.
Lemma
uPred_
big_sep_and
Ps
:
(
Π★
Ps
)
⊑
(
Π
∧
Ps
).
Lemma
big_sep_and
Ps
:
(
Π★
Ps
)
⊑
(
Π
∧
Ps
).
Proof
.
by
induction
Ps
as
[|
P
Ps
IH
]
;
simpl
;
auto
.
Qed
.
Proof
.
by
induction
Ps
as
[|
P
Ps
IH
]
;
simpl
;
auto
.
Qed
.
Lemma
uPred_
big_and_elem_of
Ps
P
:
P
∈
Ps
→
(
Π
∧
Ps
)
⊑
P
.
Lemma
big_and_elem_of
Ps
P
:
P
∈
Ps
→
(
Π
∧
Ps
)
⊑
P
.
Proof
.
induction
1
;
simpl
;
auto
.
Qed
.
Proof
.
induction
1
;
simpl
;
auto
.
Qed
.
Lemma
uPred_
big_sep_elem_of
Ps
P
:
P
∈
Ps
→
(
Π★
Ps
)
⊑
P
.
Lemma
big_sep_elem_of
Ps
P
:
P
∈
Ps
→
(
Π★
Ps
)
⊑
P
.
Proof
.
induction
1
;
simpl
;
auto
.
Qed
.
Proof
.
induction
1
;
simpl
;
auto
.
Qed
.
(* Timeless *)
(* Timeless *)
...
@@ -911,7 +915,7 @@ Proof.
...
@@ -911,7 +915,7 @@ Proof.
Qed
.
Qed
.
(* Always stable *)
(* Always stable *)
Notation
AS
:
=
AlwaysStable
.
Local
Notation
AS
:
=
AlwaysStable
.
Global
Instance
const_always_stable
φ
:
AS
(
■
φ
:
uPred
M
)%
I
.
Global
Instance
const_always_stable
φ
:
AS
(
■
φ
:
uPred
M
)%
I
.
Proof
.
by
rewrite
/
AlwaysStable
always_const
.
Qed
.
Proof
.
by
rewrite
/
AlwaysStable
always_const
.
Qed
.
Global
Instance
always_always_stable
P
:
AS
(
□
P
).
Global
Instance
always_always_stable
P
:
AS
(
□
P
).
...
@@ -940,6 +944,24 @@ Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A)
...
@@ -940,6 +944,24 @@ Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A)
AS
P
→
(
∀
x
,
AS
(
Q
x
))
→
AS
(
default
P
mx
Q
).
AS
P
→
(
∀
x
,
AS
(
Q
x
))
→
AS
(
default
P
mx
Q
).
Proof
.
destruct
mx
;
apply
_
.
Qed
.
Proof
.
destruct
mx
;
apply
_
.
Qed
.
(* Always stable for lists *)
Local
Notation
ASL
:
=
AlwaysStableL
.
Global
Instance
big_and_always_stable
Ps
:
ASL
Ps
→
AS
(
Π
∧
Ps
).
Proof
.
induction
1
;
apply
_
.
Qed
.
Global
Instance
big_sep_always_stable
Ps
:
ASL
Ps
→
AS
(
Π★
Ps
).
Proof
.
induction
1
;
apply
_
.
Qed
.
Global
Instance
nil_always_stable
:
ASL
(@
nil
(
uPred
M
)).
Proof
.
constructor
.
Qed
.
Global
Instance
cons_always_stable
P
Ps
:
AS
P
→
ASL
Ps
→
ASL
(
P
::
Ps
).
Proof
.
by
constructor
.
Qed
.
Global
Instance
app_always_stable
Ps
Ps'
:
ASL
Ps
→
ASL
Ps'
→
ASL
(
Ps
++
Ps'
).
Proof
.
apply
Forall_app_2
.
Qed
.
Global
Instance
zip_with_always_stable
{
A
B
}
(
f
:
A
→
B
→
uPred
M
)
xs
ys
:
(
∀
x
y
,
AS
(
f
x
y
))
→
ASL
(
zip_with
f
xs
ys
).
Proof
.
unfold
ASL
=>
?
;
revert
ys
;
induction
xs
=>
-[|??]
;
constructor
;
auto
.
Qed
.
(* Derived lemmas for always stable *)
Lemma
always_always
P
`
{!
AlwaysStable
P
}
:
(
□
P
)%
I
≡
P
.
Lemma
always_always
P
`
{!
AlwaysStable
P
}
:
(
□
P
)%
I
≡
P
.
Proof
.
apply
(
anti_symmetric
(
⊑
))
;
auto
using
always_elim
.
Qed
.
Proof
.
apply
(
anti_symmetric
(
⊑
))
;
auto
using
always_elim
.
Qed
.
Lemma
always_intro'
P
Q
`
{!
AlwaysStable
P
}
:
P
⊑
Q
→
P
⊑
□
Q
.
Lemma
always_intro'
P
Q
`
{!
AlwaysStable
P
}
:
P
⊑
Q
→
P
⊑
□
Q
.
...
...
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