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
Lennard Gäher
Iris
Commits
ca0996a8
Commit
ca0996a8
authored
Dec 04, 2017
by
Jacques-Henri Jourdan
Browse files
Split bi/derived.v intro bi/derived_connectives.v and bi/derived_laws.v
parent
5524871e
Changes
7
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
ca0996a8
...
...
@@ -26,7 +26,8 @@ theories/algebra/coPset.v
theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
theories/bi/interface.v
theories/bi/derived.v
theories/bi/derived_connectives.v
theories/bi/derived_laws.v
theories/bi/big_op.v
theories/bi/bi.v
theories/bi/tactics.v
...
...
theories/base_logic/derived.v
View file @
ca0996a8
From
iris
.
base_logic
Require
Export
upred
.
From
iris
.
bi
Require
Export
interface
derived
.
From
iris
.
bi
Require
Export
derived
_laws
.
Set
Default
Proof
Using
"Type"
.
Import
upred
.
uPred
.
Import
interface
.
bi
derived
.
bi
.
Import
interface
.
bi
derived
_laws
.
bi
.
Module
uPred
.
Section
derived
.
...
...
theories/base_logic/upred.v
View file @
ca0996a8
From
iris
.
algebra
Require
Export
cmra
updates
.
From
iris
.
bi
Require
Export
interface
.
From
iris
.
bi
Require
Export
derived_connectives
.
From
stdpp
Require
Import
finite
.
Set
Default
Proof
Using
"Type"
.
Local
Hint
Extern
1
(
_
≼
_
)
=>
etrans
;
[
eassumption
|].
...
...
theories/bi/bi.v
View file @
ca0996a8
From
iris
.
bi
Require
Export
interface
derived
big_op
.
From
iris
.
bi
Require
Export
derived
_laws
big_op
.
Set
Default
Proof
Using
"Type"
.
Module
Import
bi
.
Export
bi
.
interface
.
bi
.
Export
bi
.
derived
.
bi
.
Export
bi
.
derived
_laws
.
bi
.
Export
bi
.
big_op
.
bi
.
End
bi
.
...
...
theories/bi/big_op.v
View file @
ca0996a8
From
iris
.
algebra
Require
Export
big_op
.
From
iris
.
bi
Require
Export
derived
.
From
iris
.
bi
Require
Export
derived
_laws
.
From
stdpp
Require
Import
countable
fin_collections
functions
.
Set
Default
Proof
Using
"Type"
.
...
...
@@ -41,7 +41,7 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
(** * Properties *)
Module
bi
.
Import
interface
.
bi
derived
.
bi
.
Import
interface
.
bi
derived
_laws
.
bi
.
Section
bi_big_op
.
Context
{
PROP
:
bi
}.
Implicit
Types
Ps
Qs
:
list
PROP
.
...
...
theories/bi/derived_connectives.v
0 → 100644
View file @
ca0996a8
From
iris
.
bi
Require
Export
interface
.
From
iris
.
algebra
Require
Import
monoid
.
From
stdpp
Require
Import
hlist
.
Definition
bi_iff
{
PROP
:
bi
}
(
P
Q
:
PROP
)
:
PROP
:
=
((
P
→
Q
)
∧
(
Q
→
P
))%
I
.
Arguments
bi_iff
{
_
}
_
%
I
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_iff
)
1
.
Infix
"↔"
:
=
bi_iff
:
bi_scope
.
Definition
bi_wand_iff
{
PROP
:
bi
}
(
P
Q
:
PROP
)
:
PROP
:
=
((
P
-
∗
Q
)
∧
(
Q
-
∗
P
))%
I
.
Arguments
bi_wand_iff
{
_
}
_
%
I
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_wand_iff
)
1
.
Infix
"∗-∗"
:
=
bi_wand_iff
(
at
level
95
,
no
associativity
)
:
bi_scope
.
Class
Plain
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
plain
:
P
⊢
bi_plainly
P
.
Arguments
Plain
{
_
}
_
%
I
:
simpl
never
.
Arguments
plain
{
_
}
_
%
I
{
_
}.
Hint
Mode
Plain
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Plain
)
1
.
Class
Persistent
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
persistent
:
P
⊢
bi_persistently
P
.
Arguments
Persistent
{
_
}
_
%
I
:
simpl
never
.
Arguments
persistent
{
_
}
_
%
I
{
_
}.
Hint
Mode
Persistent
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Persistent
)
1
.
Definition
bi_affinely
{
PROP
:
bi
}
(
P
:
PROP
)
:
PROP
:
=
(
emp
∧
P
)%
I
.
Arguments
bi_affinely
{
_
}
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_affinely
)
1
.
Typeclasses
Opaque
bi_affinely
.
Notation
"□ P"
:
=
(
bi_affinely
(
bi_persistently
P
))%
I
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Notation
"■ P"
:
=
(
bi_affinely
(
bi_plainly
P
))%
I
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Class
Affine
{
PROP
:
bi
}
(
Q
:
PROP
)
:
=
affine
:
Q
⊢
emp
.
Arguments
Affine
{
_
}
_
%
I
:
simpl
never
.
Arguments
affine
{
_
}
_
%
I
{
_
}.
Hint
Mode
Affine
+
!
:
typeclass_instances
.
Class
BiAffine
(
PROP
:
bi
)
:
=
absorbing_bi
(
Q
:
PROP
)
:
Affine
Q
.
Existing
Instance
absorbing_bi
|
0
.
Class
BiPositive
(
PROP
:
bi
)
:
=
bi_positive
(
P
Q
:
PROP
)
:
bi_affinely
(
P
∗
Q
)
⊢
bi_affinely
P
∗
Q
.
Definition
bi_absorbingly
{
PROP
:
bi
}
(
P
:
PROP
)
:
PROP
:
=
(
True
∗
P
)%
I
.
Arguments
bi_absorbingly
{
_
}
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_absorbingly
)
1
.
Typeclasses
Opaque
bi_absorbingly
.
Class
Absorbing
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
absorbing
:
bi_absorbingly
P
⊢
P
.
Arguments
Absorbing
{
_
}
_
%
I
:
simpl
never
.
Arguments
absorbing
{
_
}
_
%
I
.
Definition
bi_plainly_if
{
PROP
:
bi
}
(
p
:
bool
)
(
P
:
PROP
)
:
PROP
:
=
(
if
p
then
bi_plainly
P
else
P
)%
I
.
Arguments
bi_plainly_if
{
_
}
!
_
_
%
I
/.
Instance
:
Params
(@
bi_plainly_if
)
2
.
Typeclasses
Opaque
bi_plainly_if
.
Definition
bi_persistently_if
{
PROP
:
bi
}
(
p
:
bool
)
(
P
:
PROP
)
:
PROP
:
=
(
if
p
then
bi_persistently
P
else
P
)%
I
.
Arguments
bi_persistently_if
{
_
}
!
_
_
%
I
/.
Instance
:
Params
(@
bi_persistently_if
)
2
.
Typeclasses
Opaque
bi_persistently_if
.
Definition
bi_affinely_if
{
PROP
:
bi
}
(
p
:
bool
)
(
P
:
PROP
)
:
PROP
:
=
(
if
p
then
bi_affinely
P
else
P
)%
I
.
Arguments
bi_affinely_if
{
_
}
!
_
_
%
I
/.
Instance
:
Params
(@
bi_affinely_if
)
2
.
Typeclasses
Opaque
bi_affinely_if
.
Notation
"□? p P"
:
=
(
bi_affinely_if
p
(
bi_persistently_if
p
P
))%
I
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
right
associativity
,
format
"□? p P"
)
:
bi_scope
.
Notation
"■? p P"
:
=
(
bi_affinely_if
p
(
bi_plainly_if
p
P
))%
I
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
right
associativity
,
format
"■? p P"
)
:
bi_scope
.
Fixpoint
bi_hexist
{
PROP
:
bi
}
{
As
}
:
himpl
As
PROP
→
PROP
:
=
match
As
return
himpl
As
PROP
→
PROP
with
|
tnil
=>
id
|
tcons
A
As
=>
λ
Φ
,
∃
x
,
bi_hexist
(
Φ
x
)
end
%
I
.
Fixpoint
bi_hforall
{
PROP
:
bi
}
{
As
}
:
himpl
As
PROP
→
PROP
:
=
match
As
return
himpl
As
PROP
→
PROP
with
|
tnil
=>
id
|
tcons
A
As
=>
λ
Φ
,
∀
x
,
bi_hforall
(
Φ
x
)
end
%
I
.
Definition
bi_laterN
{
PROP
:
sbi
}
(
n
:
nat
)
(
P
:
PROP
)
:
PROP
:
=
Nat
.
iter
n
bi_later
P
.
Arguments
bi_laterN
{
_
}
!
_
%
nat_scope
_
%
I
.
Instance
:
Params
(@
bi_laterN
)
2
.
Notation
"▷^ n P"
:
=
(
bi_laterN
n
P
)
(
at
level
20
,
n
at
level
9
,
P
at
level
20
,
format
"▷^ n P"
)
:
bi_scope
.
Notation
"▷? p P"
:
=
(
bi_laterN
(
Nat
.
b2n
p
)
P
)
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
format
"▷? p P"
)
:
bi_scope
.
Definition
bi_except_0
{
PROP
:
sbi
}
(
P
:
PROP
)
:
PROP
:
=
(
▷
False
∨
P
)%
I
.
Arguments
bi_except_0
{
_
}
_
%
I
:
simpl
never
.
Notation
"◇ P"
:
=
(
bi_except_0
P
)
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Instance
:
Params
(@
bi_except_0
)
1
.
Typeclasses
Opaque
bi_except_0
.
Class
Timeless
{
PROP
:
sbi
}
(
P
:
PROP
)
:
=
timeless
:
▷
P
⊢
◇
P
.
Arguments
Timeless
{
_
}
_
%
I
:
simpl
never
.
Arguments
timeless
{
_
}
_
%
I
{
_
}.
Hint
Mode
Timeless
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Timeless
)
1
.
theories/bi/derived.v
→
theories/bi/derived
_laws
.v
View file @
ca0996a8
From
iris
.
bi
Require
Export
interface
.
From
iris
.
bi
Require
Export
derived_connectives
.
From
iris
.
algebra
Require
Import
monoid
.
From
stdpp
Require
Import
hlist
.
Definition
bi_iff
{
PROP
:
bi
}
(
P
Q
:
PROP
)
:
PROP
:
=
((
P
→
Q
)
∧
(
Q
→
P
))%
I
.
Arguments
bi_iff
{
_
}
_
%
I
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_iff
)
1
.
Infix
"↔"
:
=
bi_iff
:
bi_scope
.
Definition
bi_wand_iff
{
PROP
:
bi
}
(
P
Q
:
PROP
)
:
PROP
:
=
((
P
-
∗
Q
)
∧
(
Q
-
∗
P
))%
I
.
Arguments
bi_wand_iff
{
_
}
_
%
I
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_wand_iff
)
1
.
Infix
"∗-∗"
:
=
bi_wand_iff
(
at
level
95
,
no
associativity
)
:
bi_scope
.
Class
Plain
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
plain
:
P
⊢
bi_plainly
P
.
Arguments
Plain
{
_
}
_
%
I
:
simpl
never
.
Arguments
plain
{
_
}
_
%
I
{
_
}.
Hint
Mode
Plain
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Plain
)
1
.
Class
Persistent
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
persistent
:
P
⊢
bi_persistently
P
.
Arguments
Persistent
{
_
}
_
%
I
:
simpl
never
.
Arguments
persistent
{
_
}
_
%
I
{
_
}.
Hint
Mode
Persistent
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Persistent
)
1
.
Definition
bi_affinely
{
PROP
:
bi
}
(
P
:
PROP
)
:
PROP
:
=
(
emp
∧
P
)%
I
.
Arguments
bi_affinely
{
_
}
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_affinely
)
1
.
Typeclasses
Opaque
bi_affinely
.
Notation
"□ P"
:
=
(
bi_affinely
(
bi_persistently
P
))%
I
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Notation
"■ P"
:
=
(
bi_affinely
(
bi_plainly
P
))%
I
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Class
Affine
{
PROP
:
bi
}
(
Q
:
PROP
)
:
=
affine
:
Q
⊢
emp
.
Arguments
Affine
{
_
}
_
%
I
:
simpl
never
.
Arguments
affine
{
_
}
_
%
I
{
_
}.
Hint
Mode
Affine
+
!
:
typeclass_instances
.
Class
BiAffine
(
PROP
:
bi
)
:
=
absorbing_bi
(
Q
:
PROP
)
:
Affine
Q
.
Existing
Instance
absorbing_bi
|
0
.
Class
BiPositive
(
PROP
:
bi
)
:
=
bi_positive
(
P
Q
:
PROP
)
:
bi_affinely
(
P
∗
Q
)
⊢
bi_affinely
P
∗
Q
.
Definition
bi_absorbingly
{
PROP
:
bi
}
(
P
:
PROP
)
:
PROP
:
=
(
True
∗
P
)%
I
.
Arguments
bi_absorbingly
{
_
}
_
%
I
:
simpl
never
.
Instance
:
Params
(@
bi_absorbingly
)
1
.
Typeclasses
Opaque
bi_absorbingly
.
Class
Absorbing
{
PROP
:
bi
}
(
P
:
PROP
)
:
=
absorbing
:
bi_absorbingly
P
⊢
P
.
Arguments
Absorbing
{
_
}
_
%
I
:
simpl
never
.
Arguments
absorbing
{
_
}
_
%
I
.
Definition
bi_plainly_if
{
PROP
:
bi
}
(
p
:
bool
)
(
P
:
PROP
)
:
PROP
:
=
(
if
p
then
bi_plainly
P
else
P
)%
I
.
Arguments
bi_plainly_if
{
_
}
!
_
_
%
I
/.
Instance
:
Params
(@
bi_plainly_if
)
2
.
Typeclasses
Opaque
bi_plainly_if
.
Definition
bi_persistently_if
{
PROP
:
bi
}
(
p
:
bool
)
(
P
:
PROP
)
:
PROP
:
=
(
if
p
then
bi_persistently
P
else
P
)%
I
.
Arguments
bi_persistently_if
{
_
}
!
_
_
%
I
/.
Instance
:
Params
(@
bi_persistently_if
)
2
.
Typeclasses
Opaque
bi_persistently_if
.
Definition
bi_affinely_if
{
PROP
:
bi
}
(
p
:
bool
)
(
P
:
PROP
)
:
PROP
:
=
(
if
p
then
bi_affinely
P
else
P
)%
I
.
Arguments
bi_affinely_if
{
_
}
!
_
_
%
I
/.
Instance
:
Params
(@
bi_affinely_if
)
2
.
Typeclasses
Opaque
bi_affinely_if
.
Notation
"□? p P"
:
=
(
bi_affinely_if
p
(
bi_persistently_if
p
P
))%
I
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
right
associativity
,
format
"□? p P"
)
:
bi_scope
.
Notation
"■? p P"
:
=
(
bi_affinely_if
p
(
bi_plainly_if
p
P
))%
I
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
right
associativity
,
format
"■? p P"
)
:
bi_scope
.
Fixpoint
bi_hexist
{
PROP
:
bi
}
{
As
}
:
himpl
As
PROP
→
PROP
:
=
match
As
return
himpl
As
PROP
→
PROP
with
|
tnil
=>
id
|
tcons
A
As
=>
λ
Φ
,
∃
x
,
bi_hexist
(
Φ
x
)
end
%
I
.
Fixpoint
bi_hforall
{
PROP
:
bi
}
{
As
}
:
himpl
As
PROP
→
PROP
:
=
match
As
return
himpl
As
PROP
→
PROP
with
|
tnil
=>
id
|
tcons
A
As
=>
λ
Φ
,
∀
x
,
bi_hforall
(
Φ
x
)
end
%
I
.
Definition
bi_laterN
{
PROP
:
sbi
}
(
n
:
nat
)
(
P
:
PROP
)
:
PROP
:
=
Nat
.
iter
n
bi_later
P
.
Arguments
bi_laterN
{
_
}
!
_
%
nat_scope
_
%
I
.
Instance
:
Params
(@
bi_laterN
)
2
.
Notation
"▷^ n P"
:
=
(
bi_laterN
n
P
)
(
at
level
20
,
n
at
level
9
,
P
at
level
20
,
format
"▷^ n P"
)
:
bi_scope
.
Notation
"▷? p P"
:
=
(
bi_laterN
(
Nat
.
b2n
p
)
P
)
(
at
level
20
,
p
at
level
9
,
P
at
level
20
,
format
"▷? p P"
)
:
bi_scope
.
Definition
bi_except_0
{
PROP
:
sbi
}
(
P
:
PROP
)
:
PROP
:
=
(
▷
False
∨
P
)%
I
.
Arguments
bi_except_0
{
_
}
_
%
I
:
simpl
never
.
Notation
"◇ P"
:
=
(
bi_except_0
P
)
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Instance
:
Params
(@
bi_except_0
)
1
.
Typeclasses
Opaque
bi_except_0
.
Class
Timeless
{
PROP
:
sbi
}
(
P
:
PROP
)
:
=
timeless
:
▷
P
⊢
◇
P
.
Arguments
Timeless
{
_
}
_
%
I
:
simpl
never
.
Arguments
timeless
{
_
}
_
%
I
{
_
}.
Hint
Mode
Timeless
+
!
:
typeclass_instances
.
Instance
:
Params
(@
Timeless
)
1
.
Module
bi
.
Import
interface
.
bi
.
Section
bi_derived
.
...
...
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