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
Rodolphe Lepigre
Iris
Commits
f610d6ff
Commit
f610d6ff
authored
Dec 20, 2017
by
Ralf Jung
Browse files
BI -> Bi, to match our convention
parent
1a1aa388
Changes
3
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/upred.v
View file @
f610d6ff
...
...
@@ -351,7 +351,7 @@ Import uPred_unseal.
Local
Arguments
uPred_holds
{
_
}
!
_
_
_
/.
Lemma
uPred_bi_mixin
(
M
:
ucmraT
)
:
B
I
Mixin
(
ofe_mixin_of
(
uPred
M
))
Lemma
uPred_bi_mixin
(
M
:
ucmraT
)
:
B
i
Mixin
(
ofe_mixin_of
(
uPred
M
))
uPred_entails
uPred_emp
uPred_pure
uPred_and
uPred_or
uPred_impl
(@
uPred_forall
M
)
(@
uPred_exist
M
)
(@
uPred_internal_eq
M
)
uPred_sep
uPred_wand
uPred_plainly
uPred_persistently
.
...
...
@@ -511,7 +511,7 @@ Proof.
exists
(
core
x
),
x
;
rewrite
?cmra_core_l
;
auto
.
Qed
.
Lemma
uPred_sbi_mixin
(
M
:
ucmraT
)
:
S
BI
Mixin
Lemma
uPred_sbi_mixin
(
M
:
ucmraT
)
:
S
bi
Mixin
uPred_entails
uPred_pure
uPred_or
uPred_impl
(@
uPred_forall
M
)
(@
uPred_exist
M
)
(@
uPred_internal_eq
M
)
uPred_sep
uPred_plainly
uPred_persistently
uPred_later
.
...
...
theories/bi/fixpoint.v
View file @
f610d6ff
...
...
@@ -5,7 +5,7 @@ Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *)
Class
B
I
MonoPred
{
PROP
:
bi
}
{
A
:
ofeT
}
(
F
:
(
A
→
PROP
)
→
(
A
→
PROP
))
:
=
{
Class
B
i
MonoPred
{
PROP
:
bi
}
{
A
:
ofeT
}
(
F
:
(
A
→
PROP
)
→
(
A
→
PROP
))
:
=
{
bi_mono_pred
Φ
Ψ
:
((
bi_persistently
(
∀
x
,
Φ
x
-
∗
Ψ
x
))
→
∀
x
,
F
Φ
x
-
∗
F
Ψ
x
)%
I
;
bi_mono_pred_ne
Φ
:
NonExpansive
Φ
→
NonExpansive
(
F
Φ
)
}.
...
...
@@ -21,7 +21,7 @@ Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
(
∃
Φ
:
A
-
n
>
PROP
,
bi_persistently
(
∀
x
,
Φ
x
-
∗
F
Φ
x
)
∧
Φ
x
)%
I
.
Section
least
.
Context
{
PROP
:
bi
}
{
A
:
ofeT
}
(
F
:
(
A
→
PROP
)
→
(
A
→
PROP
))
`
{!
B
I
MonoPred
F
}.
Context
{
PROP
:
bi
}
{
A
:
ofeT
}
(
F
:
(
A
→
PROP
)
→
(
A
→
PROP
))
`
{!
B
i
MonoPred
F
}.
Global
Instance
least_fixpoint_ne
:
NonExpansive
(
bi_least_fixpoint
F
).
Proof
.
solve_proper
.
Qed
.
...
...
theories/bi/interface.v
View file @
f610d6ff
...
...
@@ -42,7 +42,7 @@ Section bi_mixin.
Local
Infix
"-∗"
:
=
bi_wand
.
Local
Notation
"▷ P"
:
=
(
sbi_later
P
).
Record
B
I
Mixin
:
=
{
Record
B
i
Mixin
:
=
{
bi_mixin_entails_po
:
PreOrder
bi_entails
;
bi_mixin_equiv_spec
P
Q
:
equiv
P
Q
↔
(
P
⊢
Q
)
∧
(
Q
⊢
P
)
;
...
...
@@ -141,7 +141,7 @@ Section bi_mixin.
bi_persistently
P
∧
Q
⊢
(
emp
∧
P
)
∗
Q
;
}.
Record
S
BI
Mixin
:
=
{
Record
S
bi
Mixin
:
=
{
sbi_mixin_later_contractive
:
Contractive
sbi_later
;
sbi_mixin_later_eq_1
{
A
:
ofeT
}
(
x
y
:
A
)
:
Next
x
≡
Next
y
⊢
▷
(
x
≡
y
)
;
...
...
@@ -166,7 +166,7 @@ Section bi_mixin.
}.
End
bi_mixin
.
Structure
bi
:
=
B
I
{
Structure
bi
:
=
B
i
{
bi_car
:
>
Type
;
bi_dist
:
Dist
bi_car
;
bi_equiv
:
Equiv
bi_car
;
...
...
@@ -184,7 +184,7 @@ Structure bi := BI {
bi_plainly
:
bi_car
→
bi_car
;
bi_persistently
:
bi_car
→
bi_car
;
bi_ofe_mixin
:
OfeMixin
bi_car
;
bi_bi_mixin
:
B
I
Mixin
bi_ofe_mixin
bi_entails
bi_emp
bi_pure
bi_and
bi_or
bi_bi_mixin
:
B
i
Mixin
bi_ofe_mixin
bi_entails
bi_emp
bi_pure
bi_and
bi_or
bi_impl
bi_forall
bi_exist
bi_internal_eq
bi_sep
bi_wand
bi_plainly
bi_persistently
;
}.
...
...
@@ -224,7 +224,7 @@ Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
Arguments
bi_plainly
{
PROP
}
_
%
I
:
simpl
never
,
rename
.
Arguments
bi_persistently
{
PROP
}
_
%
I
:
simpl
never
,
rename
.
Structure
sbi
:
=
S
BI
{
Structure
sbi
:
=
S
bi
{
sbi_car
:
>
Type
;
sbi_dist
:
Dist
sbi_car
;
sbi_equiv
:
Equiv
sbi_car
;
...
...
@@ -243,10 +243,10 @@ Structure sbi := SBI {
sbi_persistently
:
sbi_car
→
sbi_car
;
sbi_later
:
sbi_car
→
sbi_car
;
sbi_ofe_mixin
:
OfeMixin
sbi_car
;
sbi_bi_mixin
:
B
I
Mixin
sbi_ofe_mixin
sbi_entails
sbi_emp
sbi_pure
sbi_and
sbi_bi_mixin
:
B
i
Mixin
sbi_ofe_mixin
sbi_entails
sbi_emp
sbi_pure
sbi_and
sbi_or
sbi_impl
sbi_forall
sbi_exist
sbi_internal_eq
sbi_sep
sbi_wand
sbi_plainly
sbi_persistently
;
sbi_sbi_mixin
:
S
BI
Mixin
sbi_entails
sbi_pure
sbi_or
sbi_impl
sbi_sbi_mixin
:
S
bi
Mixin
sbi_entails
sbi_pure
sbi_or
sbi_impl
sbi_forall
sbi_exist
sbi_internal_eq
sbi_sep
sbi_plainly
sbi_persistently
sbi_later
;
}.
...
...
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