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
5d6b3364
Commit
5d6b3364
authored
Dec 04, 2017
by
Jacques-Henri Jourdan
Browse files
bi_later->sbi_later.
parent
56dcb30c
Changes
7
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/derived.v
View file @
5d6b3364
...
...
@@ -77,7 +77,7 @@ Proof.
Qed
.
Lemma
except_0_bupd
P
:
◇
(|==>
P
)
⊢
(|==>
◇
P
).
Proof
.
rewrite
/
bi_except_0
.
apply
or_elim
;
auto
using
bupd_mono
,
or_intro_r
.
rewrite
/
s
bi_except_0
.
apply
or_elim
;
auto
using
bupd_mono
,
or_intro_r
.
by
rewrite
-
bupd_intro
-
or_intro_l
.
Qed
.
...
...
theories/base_logic/soundness.v
View file @
5d6b3364
...
...
@@ -10,7 +10,7 @@ Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
Proof
.
cut
((
▷
^
n
⌜
φ
⌝
:
uPred
M
)%
I
n
ε
→
φ
).
{
intros
help
H
.
eapply
help
,
H
;
eauto
using
ucmra_unit_validN
.
by
unseal
.
}
rewrite
/
bi_laterN
;
unseal
.
induction
n
as
[|
n
IH
]=>
H
;
auto
.
rewrite
/
s
bi_laterN
;
unseal
.
induction
n
as
[|
n
IH
]=>
H
;
auto
.
Qed
.
Corollary
consistency_modal
n
:
¬
(
▷
^
n
False
:
uPred
M
)%
I
.
...
...
theories/base_logic/upred.v
View file @
5d6b3364
...
...
@@ -341,7 +341,7 @@ Definition unseal_eqs :=
Ltac
unseal
:
=
(* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold
bi_emp
;
simpl
;
unfold
uPred_emp
,
bi_pure
,
bi_and
,
bi_or
,
bi_impl
,
bi_forall
,
bi_exist
,
bi_internal_eq
,
bi_sep
,
bi_wand
,
bi_plainly
,
bi_persistently
,
bi_later
;
simpl
;
bi_internal_eq
,
bi_sep
,
bi_wand
,
bi_plainly
,
bi_persistently
,
s
bi_later
;
simpl
;
unfold
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
;
simpl
;
rewrite
!
unseal_eqs
/=.
...
...
@@ -516,7 +516,7 @@ Lemma uPred_sbi_mixin (M : ucmraT) : SBIMixin
uPred_sep
uPred_plainly
uPred_persistently
uPred_later
.
Proof
.
split
.
-
(* Contractive bi_later *)
-
(* Contractive
s
bi_later *)
unseal
;
intros
[|
n
]
P
Q
HPQ
;
split
=>
-[|
n'
]
x
??
//=
;
try
omega
.
apply
HPQ
;
eauto
using
cmra_validN_S
.
-
(* Next x ≡ Next y ⊢ ▷ (x ≡ y) *)
...
...
@@ -645,7 +645,7 @@ Lemma ownM_unit : bi_valid (uPred_ownM (ε:M)).
Proof
.
unseal
;
split
=>
n
x
??
;
by
exists
x
;
rewrite
left_id
.
Qed
.
Lemma
later_ownM
(
a
:
M
)
:
▷
uPred_ownM
a
⊢
∃
b
,
uPred_ownM
b
∧
▷
(
a
≡
b
).
Proof
.
rewrite
/
bi_and
/
bi_later
/
bi_exist
/
bi_internal_eq
/=
;
unseal
.
rewrite
/
bi_and
/
s
bi_later
/
bi_exist
/
bi_internal_eq
/=
;
unseal
.
split
=>
-[|
n
]
x
/=
?
Hax
;
first
by
eauto
using
ucmra_unit_leastN
.
destruct
Hax
as
[
y
?].
destruct
(
cmra_extend
n
x
a
y
)
as
(
a'
&
y'
&
Hx
&?&?)
;
auto
using
cmra_validN_S
.
...
...
theories/bi/derived_connectives.v
View file @
5d6b3364
...
...
@@ -94,20 +94,20 @@ Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP :=
|
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
)
Definition
s
bi_laterN
{
PROP
:
sbi
}
(
n
:
nat
)
(
P
:
PROP
)
:
PROP
:
=
Nat
.
iter
n
s
bi_later
P
.
Arguments
s
bi_laterN
{
_
}
!
_
%
nat_scope
_
%
I
.
Instance
:
Params
(@
s
bi_laterN
)
2
.
Notation
"▷^ n P"
:
=
(
s
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
)
Notation
"▷? p P"
:
=
(
s
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
.
Definition
s
bi_except_0
{
PROP
:
sbi
}
(
P
:
PROP
)
:
PROP
:
=
(
▷
False
∨
P
)%
I
.
Arguments
s
bi_except_0
{
_
}
_
%
I
:
simpl
never
.
Notation
"◇ P"
:
=
(
s
bi_except_0
P
)
(
at
level
20
,
right
associativity
)
:
bi_scope
.
Instance
:
Params
(@
s
bi_except_0
)
1
.
Typeclasses
Opaque
s
bi_except_0
.
Class
Timeless
{
PROP
:
sbi
}
(
P
:
PROP
)
:
=
timeless
:
▷
P
⊢
◇
P
.
Arguments
Timeless
{
_
}
_
%
I
:
simpl
never
.
...
...
theories/bi/derived_laws.v
View file @
5d6b3364
...
...
@@ -1857,7 +1857,7 @@ Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim.
Hint
Resolve
and_elim_l'
and_elim_r'
and_intro
forall_intro
.
Global
Instance
later_proper
:
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
bi_later
PROP
)
:
=
ne_proper
_
.
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
s
bi_later
PROP
)
:
=
ne_proper
_
.
(* Equality *)
Lemma
internal_eq_rewrite_contractive
{
A
:
ofeT
}
a
b
(
Ψ
:
A
→
PROP
)
...
...
@@ -1878,10 +1878,10 @@ Proof. apply (anti_symm _); auto using later_eq_1, later_eq_2. Qed.
(* Later derived *)
Hint
Resolve
later_mono
.
Global
Instance
later_mono'
:
Proper
((
⊢
)
==>
(
⊢
))
(@
bi_later
PROP
).
Global
Instance
later_mono'
:
Proper
((
⊢
)
==>
(
⊢
))
(@
s
bi_later
PROP
).
Proof
.
intros
P
Q
;
apply
later_mono
.
Qed
.
Global
Instance
later_flip_mono'
:
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
bi_later
PROP
).
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
s
bi_later
PROP
).
Proof
.
intros
P
Q
;
apply
later_mono
.
Qed
.
Lemma
later_intro
P
:
P
⊢
▷
P
.
...
...
@@ -1944,10 +1944,10 @@ Global Instance later_absorbing P : Absorbing P → Absorbing (▷ P).
Proof
.
intros
?.
by
rewrite
/
Absorbing
-
later_absorbingly
absorbing
.
Qed
.
(* Iterated later modality *)
Global
Instance
laterN_ne
m
:
NonExpansive
(@
bi_laterN
PROP
m
).
Global
Instance
laterN_ne
m
:
NonExpansive
(@
s
bi_laterN
PROP
m
).
Proof
.
induction
m
;
simpl
.
by
intros
???.
solve_proper
.
Qed
.
Global
Instance
laterN_proper
m
:
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
bi_laterN
PROP
m
)
:
=
ne_proper
_
.
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
s
bi_laterN
PROP
m
)
:
=
ne_proper
_
.
Lemma
laterN_0
P
:
▷
^
0
P
⊣
⊢
P
.
Proof
.
done
.
Qed
.
...
...
@@ -1962,10 +1962,10 @@ Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
Lemma
laterN_mono
n
P
Q
:
(
P
⊢
Q
)
→
▷
^
n
P
⊢
▷
^
n
Q
.
Proof
.
induction
n
;
simpl
;
auto
.
Qed
.
Global
Instance
laterN_mono'
n
:
Proper
((
⊢
)
==>
(
⊢
))
(@
bi_laterN
PROP
n
).
Global
Instance
laterN_mono'
n
:
Proper
((
⊢
)
==>
(
⊢
))
(@
s
bi_laterN
PROP
n
).
Proof
.
intros
P
Q
;
apply
laterN_mono
.
Qed
.
Global
Instance
laterN_flip_mono'
n
:
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
bi_laterN
PROP
n
).
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
s
bi_laterN
PROP
n
).
Proof
.
intros
P
Q
;
apply
laterN_mono
.
Qed
.
Lemma
laterN_intro
n
P
:
P
⊢
▷
^
n
P
.
...
...
@@ -2019,34 +2019,34 @@ Global Instance laterN_absorbing n P : Absorbing P → Absorbing (▷^n P).
Proof
.
induction
n
;
apply
_
.
Qed
.
(* Except-0 *)
Global
Instance
except_0_ne
:
NonExpansive
(@
bi_except_0
PROP
).
Global
Instance
except_0_ne
:
NonExpansive
(@
s
bi_except_0
PROP
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
except_0_proper
:
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
bi_except_0
PROP
).
Global
Instance
except_0_proper
:
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
s
bi_except_0
PROP
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
except_0_mono'
:
Proper
((
⊢
)
==>
(
⊢
))
(@
bi_except_0
PROP
).
Global
Instance
except_0_mono'
:
Proper
((
⊢
)
==>
(
⊢
))
(@
s
bi_except_0
PROP
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
except_0_flip_mono'
:
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
bi_except_0
PROP
).
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
s
bi_except_0
PROP
).
Proof
.
solve_proper
.
Qed
.
Lemma
except_0_intro
P
:
P
⊢
◇
P
.
Proof
.
rewrite
/
bi_except_0
;
auto
.
Qed
.
Proof
.
rewrite
/
s
bi_except_0
;
auto
.
Qed
.
Lemma
except_0_mono
P
Q
:
(
P
⊢
Q
)
→
◇
P
⊢
◇
Q
.
Proof
.
by
intros
->.
Qed
.
Lemma
except_0_idemp
P
:
◇
◇
P
⊣
⊢
◇
P
.
Proof
.
apply
(
anti_symm
_
)
;
rewrite
/
bi_except_0
;
auto
.
Qed
.
Proof
.
apply
(
anti_symm
_
)
;
rewrite
/
s
bi_except_0
;
auto
.
Qed
.
Lemma
except_0_True
:
◇
True
⊣
⊢
True
.
Proof
.
rewrite
/
bi_except_0
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Proof
.
rewrite
/
s
bi_except_0
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Lemma
except_0_emp
`
{!
BiAffine
PROP
}
:
◇
emp
⊣
⊢
emp
.
Proof
.
by
rewrite
-
True_emp
except_0_True
.
Qed
.
Lemma
except_0_or
P
Q
:
◇
(
P
∨
Q
)
⊣
⊢
◇
P
∨
◇
Q
.
Proof
.
rewrite
/
bi_except_0
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Proof
.
rewrite
/
s
bi_except_0
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Lemma
except_0_and
P
Q
:
◇
(
P
∧
Q
)
⊣
⊢
◇
P
∧
◇
Q
.
Proof
.
by
rewrite
/
bi_except_0
or_and_l
.
Qed
.
Proof
.
by
rewrite
/
s
bi_except_0
or_and_l
.
Qed
.
Lemma
except_0_sep
P
Q
:
◇
(
P
∗
Q
)
⊣
⊢
◇
P
∗
◇
Q
.
Proof
.
rewrite
/
bi_except_0
.
apply
(
anti_symm
_
).
rewrite
/
s
bi_except_0
.
apply
(
anti_symm
_
).
-
apply
or_elim
;
last
by
auto
using
sep_mono
.
by
rewrite
-!
or_intro_l
-
persistently_pure
-
later_sep
-
persistently_sep_dup
.
-
rewrite
sep_or_r
!
sep_or_l
{
1
}(
later_intro
P
)
{
1
}(
later_intro
Q
).
...
...
@@ -2074,15 +2074,15 @@ Proof.
-
apply
exist_mono
=>
a
.
apply
except_0_intro
.
Qed
.
Lemma
except_0_later
P
:
◇
▷
P
⊢
▷
P
.
Proof
.
by
rewrite
/
bi_except_0
-
later_or
False_or
.
Qed
.
Proof
.
by
rewrite
/
s
bi_except_0
-
later_or
False_or
.
Qed
.
Lemma
except_0_plainly_1
P
:
◇
bi_plainly
P
⊢
bi_plainly
(
◇
P
).
Proof
.
by
rewrite
/
bi_except_0
-
plainly_or_2
-
later_plainly
plainly_pure
.
Qed
.
Proof
.
by
rewrite
/
s
bi_except_0
-
plainly_or_2
-
later_plainly
plainly_pure
.
Qed
.
Lemma
except_0_plainly
`
{
BiPlainlyExist
PROP
}
P
:
◇
bi_plainly
P
⊣
⊢
bi_plainly
(
◇
P
).
Proof
.
by
rewrite
/
bi_except_0
plainly_or
-
later_plainly
plainly_pure
.
Qed
.
Proof
.
by
rewrite
/
s
bi_except_0
plainly_or
-
later_plainly
plainly_pure
.
Qed
.
Lemma
except_0_persistently
P
:
◇
bi_persistently
P
⊣
⊢
bi_persistently
(
◇
P
).
Proof
.
by
rewrite
/
bi_except_0
persistently_or
-
later_persistently
persistently_pure
.
by
rewrite
/
s
bi_except_0
persistently_or
-
later_persistently
persistently_pure
.
Qed
.
Lemma
except_0_affinely_2
P
:
bi_affinely
(
◇
P
)
⊢
◇
bi_affinely
P
.
Proof
.
rewrite
/
bi_affinely
except_0_and
.
auto
using
except_0_intro
.
Qed
.
...
...
@@ -2111,11 +2111,11 @@ Proof.
Qed
.
Global
Instance
except_0_plain
P
:
Plain
P
→
Plain
(
◇
P
).
Proof
.
rewrite
/
bi_except_0
;
apply
_
.
Qed
.
Proof
.
rewrite
/
s
bi_except_0
;
apply
_
.
Qed
.
Global
Instance
except_0_persistent
P
:
Persistent
P
→
Persistent
(
◇
P
).
Proof
.
rewrite
/
bi_except_0
;
apply
_
.
Qed
.
Proof
.
rewrite
/
s
bi_except_0
;
apply
_
.
Qed
.
Global
Instance
except_0_absorbing
P
:
Absorbing
P
→
Absorbing
(
◇
P
).
Proof
.
rewrite
/
bi_except_0
;
apply
_
.
Qed
.
Proof
.
rewrite
/
s
bi_except_0
;
apply
_
.
Qed
.
(* Timeless instances *)
Global
Instance
Timeless_proper
:
Proper
((
≡
)
==>
iff
)
(@
Timeless
PROP
).
...
...
@@ -2123,7 +2123,7 @@ Proof. solve_proper. Qed.
Global
Instance
pure_timeless
φ
:
Timeless
(
⌜φ⌝
:
PROP
)%
I
.
Proof
.
rewrite
/
Timeless
/
bi_except_0
pure_alt
later_exist_false
.
rewrite
/
Timeless
/
s
bi_except_0
pure_alt
later_exist_false
.
apply
or_elim
,
exist_elim
;
[
auto
|]=>
H
φ
.
rewrite
-(
exist_intro
H
φ
).
auto
.
Qed
.
Global
Instance
emp_timeless
`
{
BiAffine
PROP
}
:
Timeless
(
emp
:
PROP
)%
I
.
...
...
@@ -2139,7 +2139,7 @@ Proof.
rewrite
/
Timeless
=>
HQ
.
rewrite
later_false_em
.
apply
or_mono
,
impl_intro_l
;
first
done
.
rewrite
-{
2
}(
l
ö
b
Q
)
;
apply
impl_intro_l
.
rewrite
HQ
/
bi_except_0
!
and_or_r
.
apply
or_elim
;
last
auto
.
rewrite
HQ
/
s
bi_except_0
!
and_or_r
.
apply
or_elim
;
last
auto
.
by
rewrite
assoc
(
comm
_
_
P
)
-
assoc
!
impl_elim_r
.
Qed
.
Global
Instance
sep_timeless
P
Q
:
Timeless
P
→
Timeless
Q
→
Timeless
(
P
∗
Q
).
...
...
@@ -2152,7 +2152,7 @@ Proof.
rewrite
/
Timeless
=>
HQ
.
rewrite
later_false_em
.
apply
or_mono
,
wand_intro_l
;
first
done
.
rewrite
-{
2
}(
l
ö
b
Q
)
;
apply
impl_intro_l
.
rewrite
HQ
/
bi_except_0
!
and_or_r
.
apply
or_elim
;
last
auto
.
rewrite
HQ
/
s
bi_except_0
!
and_or_r
.
apply
or_elim
;
last
auto
.
by
rewrite
(
comm
_
P
)
persistent_and_sep_assoc
impl_elim_r
wand_elim_l
.
Qed
.
Global
Instance
forall_timeless
{
A
}
(
Ψ
:
A
→
PROP
)
:
...
...
@@ -2165,19 +2165,19 @@ Global Instance exist_timeless {A} (Ψ : A → PROP) :
(
∀
x
,
Timeless
(
Ψ
x
))
→
Timeless
(
∃
x
,
Ψ
x
).
Proof
.
rewrite
/
Timeless
=>
?.
rewrite
later_exist_false
.
apply
or_elim
.
-
rewrite
/
bi_except_0
;
auto
.
-
rewrite
/
s
bi_except_0
;
auto
.
-
apply
exist_elim
=>
x
.
rewrite
-(
exist_intro
x
)
;
auto
.
Qed
.
Global
Instance
plainly_timeless
P
`
{
BiPlainlyExist
PROP
}
:
Timeless
P
→
Timeless
(
bi_plainly
P
).
Proof
.
intros
.
rewrite
/
Timeless
/
bi_except_0
later_plainly_1
.
by
rewrite
(
timeless
P
)
/
bi_except_0
plainly_or
{
1
}
plainly_elim
.
intros
.
rewrite
/
Timeless
/
s
bi_except_0
later_plainly_1
.
by
rewrite
(
timeless
P
)
/
s
bi_except_0
plainly_or
{
1
}
plainly_elim
.
Qed
.
Global
Instance
persistently_timeless
P
:
Timeless
P
→
Timeless
(
bi_persistently
P
).
Proof
.
intros
.
rewrite
/
Timeless
/
bi_except_0
later_persistently_1
.
by
rewrite
(
timeless
P
)
/
bi_except_0
persistently_or
{
1
}
persistently_elim
.
intros
.
rewrite
/
Timeless
/
s
bi_except_0
later_persistently_1
.
by
rewrite
(
timeless
P
)
/
s
bi_except_0
persistently_or
{
1
}
persistently_elim
.
Qed
.
Global
Instance
affinely_timeless
P
:
...
...
@@ -2194,64 +2194,64 @@ Global Instance from_option_timeless {A} P (Ψ : A → PROP) (mx : option A) :
Proof
.
destruct
mx
;
apply
_
.
Qed
.
(* Big op stuff *)
Global
Instance
bi_later_monoid_and_homomorphism
:
MonoidHomomorphism
bi_and
bi_and
(
≡
)
(@
bi_later
PROP
).
Global
Instance
s
bi_later_monoid_and_homomorphism
:
MonoidHomomorphism
bi_and
bi_and
(
≡
)
(@
s
bi_later
PROP
).
Proof
.
split
;
[
split
|]
;
try
apply
_
.
apply
later_and
.
apply
later_True
.
Qed
.
Global
Instance
bi_laterN_and_homomorphism
n
:
MonoidHomomorphism
bi_and
bi_and
(
≡
)
(@
bi_laterN
PROP
n
).
Global
Instance
s
bi_laterN_and_homomorphism
n
:
MonoidHomomorphism
bi_and
bi_and
(
≡
)
(@
s
bi_laterN
PROP
n
).
Proof
.
split
;
[
split
|]
;
try
apply
_
.
apply
laterN_and
.
apply
laterN_True
.
Qed
.
Global
Instance
bi_except_0_and_homomorphism
:
MonoidHomomorphism
bi_and
bi_and
(
≡
)
(@
bi_except_0
PROP
).
Global
Instance
s
bi_except_0_and_homomorphism
:
MonoidHomomorphism
bi_and
bi_and
(
≡
)
(@
s
bi_except_0
PROP
).
Proof
.
split
;
[
split
|]
;
try
apply
_
.
apply
except_0_and
.
apply
except_0_True
.
Qed
.
Global
Instance
bi_later_monoid_or_homomorphism
:
WeakMonoidHomomorphism
bi_or
bi_or
(
≡
)
(@
bi_later
PROP
).
Global
Instance
s
bi_later_monoid_or_homomorphism
:
WeakMonoidHomomorphism
bi_or
bi_or
(
≡
)
(@
s
bi_later
PROP
).
Proof
.
split
;
try
apply
_
.
apply
later_or
.
Qed
.
Global
Instance
bi_laterN_or_homomorphism
n
:
WeakMonoidHomomorphism
bi_or
bi_or
(
≡
)
(@
bi_laterN
PROP
n
).
Global
Instance
s
bi_laterN_or_homomorphism
n
:
WeakMonoidHomomorphism
bi_or
bi_or
(
≡
)
(@
s
bi_laterN
PROP
n
).
Proof
.
split
;
try
apply
_
.
apply
laterN_or
.
Qed
.
Global
Instance
bi_except_0_or_homomorphism
:
WeakMonoidHomomorphism
bi_or
bi_or
(
≡
)
(@
bi_except_0
PROP
).
Global
Instance
s
bi_except_0_or_homomorphism
:
WeakMonoidHomomorphism
bi_or
bi_or
(
≡
)
(@
s
bi_except_0
PROP
).
Proof
.
split
;
try
apply
_
.
apply
except_0_or
.
Qed
.
Global
Instance
bi_later_monoid_sep_weak_homomorphism
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_later
PROP
).
Global
Instance
s
bi_later_monoid_sep_weak_homomorphism
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
s
bi_later
PROP
).
Proof
.
split
;
try
apply
_
.
apply
later_sep
.
Qed
.
Global
Instance
bi_laterN_sep_weak_homomorphism
n
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_laterN
PROP
n
).
Global
Instance
s
bi_laterN_sep_weak_homomorphism
n
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
s
bi_laterN
PROP
n
).
Proof
.
split
;
try
apply
_
.
apply
laterN_sep
.
Qed
.
Global
Instance
bi_except_0_sep_weak_homomorphism
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_except_0
PROP
).
Global
Instance
s
bi_except_0_sep_weak_homomorphism
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
s
bi_except_0
PROP
).
Proof
.
split
;
try
apply
_
.
apply
except_0_sep
.
Qed
.
Global
Instance
bi_later_monoid_sep_homomorphism
`
{!
BiAffine
PROP
}
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_later
PROP
).
Global
Instance
s
bi_later_monoid_sep_homomorphism
`
{!
BiAffine
PROP
}
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
s
bi_later
PROP
).
Proof
.
split
;
try
apply
_
.
apply
later_emp
.
Qed
.
Global
Instance
bi_laterN_sep_homomorphism
`
{!
BiAffine
PROP
}
n
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_laterN
PROP
n
).
Global
Instance
s
bi_laterN_sep_homomorphism
`
{!
BiAffine
PROP
}
n
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
s
bi_laterN
PROP
n
).
Proof
.
split
;
try
apply
_
.
apply
laterN_emp
.
Qed
.
Global
Instance
bi_except_0_sep_homomorphism
`
{!
BiAffine
PROP
}
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
bi_except_0
PROP
).
Global
Instance
s
bi_except_0_sep_homomorphism
`
{!
BiAffine
PROP
}
:
MonoidHomomorphism
bi_sep
bi_sep
(
≡
)
(@
s
bi_except_0
PROP
).
Proof
.
split
;
try
apply
_
.
apply
except_0_emp
.
Qed
.
Global
Instance
bi_later_monoid_sep_entails_weak_homomorphism
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
bi_later
PROP
).
Global
Instance
s
bi_later_monoid_sep_entails_weak_homomorphism
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
s
bi_later
PROP
).
Proof
.
split
;
try
apply
_
.
intros
P
Q
.
by
rewrite
later_sep
.
Qed
.
Global
Instance
bi_laterN_sep_entails_weak_homomorphism
n
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
bi_laterN
PROP
n
).
Global
Instance
s
bi_laterN_sep_entails_weak_homomorphism
n
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
s
bi_laterN
PROP
n
).
Proof
.
split
;
try
apply
_
.
intros
P
Q
.
by
rewrite
laterN_sep
.
Qed
.
Global
Instance
bi_except_0_sep_entails_weak_homomorphism
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
bi_except_0
PROP
).
Global
Instance
s
bi_except_0_sep_entails_weak_homomorphism
:
WeakMonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
s
bi_except_0
PROP
).
Proof
.
split
;
try
apply
_
.
intros
P
Q
.
by
rewrite
except_0_sep
.
Qed
.
Global
Instance
bi_later_monoid_sep_entails_homomorphism
:
MonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
bi_later
PROP
).
Global
Instance
s
bi_later_monoid_sep_entails_homomorphism
:
MonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
s
bi_later
PROP
).
Proof
.
split
;
try
apply
_
.
apply
later_intro
.
Qed
.
Global
Instance
bi_laterN_sep_entails_homomorphism
n
:
MonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
bi_laterN
PROP
n
).
Global
Instance
s
bi_laterN_sep_entails_homomorphism
n
:
MonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
s
bi_laterN
PROP
n
).
Proof
.
split
;
try
apply
_
.
apply
laterN_intro
.
Qed
.
Global
Instance
bi_except_0_sep_entails_homomorphism
:
MonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
bi_except_0
PROP
).
Global
Instance
s
bi_except_0_sep_entails_homomorphism
:
MonoidHomomorphism
bi_sep
bi_sep
(
flip
(
⊢
))
(@
s
bi_except_0
PROP
).
Proof
.
split
;
try
apply
_
.
apply
except_0_intro
.
Qed
.
End
sbi_derived
.
End
bi
.
...
...
theories/bi/interface.v
View file @
5d6b3364
...
...
@@ -23,7 +23,7 @@ Section bi_mixin.
Context
(
bi_wand
:
PROP
→
PROP
→
PROP
).
Context
(
bi_plainly
:
PROP
→
PROP
).
Context
(
bi_persistently
:
PROP
→
PROP
).
Context
(
bi_later
:
PROP
→
PROP
).
Context
(
s
bi_later
:
PROP
→
PROP
).
Local
Infix
"⊢"
:
=
bi_entails
.
Local
Notation
"'emp'"
:
=
bi_emp
.
...
...
@@ -40,7 +40,7 @@ Section bi_mixin.
Local
Notation
"x ≡ y"
:
=
(
bi_internal_eq
_
x
y
).
Local
Infix
"∗"
:
=
bi_sep
.
Local
Infix
"-∗"
:
=
bi_wand
.
Local
Notation
"▷ P"
:
=
(
bi_later
P
).
Local
Notation
"▷ P"
:
=
(
s
bi_later
P
).
Record
BIMixin
:
=
{
bi_mixin_entails_po
:
PreOrder
bi_entails
;
...
...
@@ -142,7 +142,7 @@ Section bi_mixin.
}.
Record
SBIMixin
:
=
{
sbi_mixin_later_contractive
:
Contractive
bi_later
;
sbi_mixin_later_contractive
:
Contractive
s
bi_later
;
sbi_mixin_later_eq_1
{
A
:
ofeT
}
(
x
y
:
A
)
:
Next
x
≡
Next
y
⊢
▷
(
x
≡
y
)
;
sbi_mixin_later_eq_2
{
A
:
ofeT
}
(
x
y
:
A
)
:
▷
(
x
≡
y
)
⊢
Next
x
≡
Next
y
;
...
...
@@ -241,14 +241,14 @@ Structure sbi := SBI {
sbi_wand
:
sbi_car
→
sbi_car
→
sbi_car
;
sbi_plainly
:
sbi_car
→
sbi_car
;
sbi_persistently
:
sbi_car
→
sbi_car
;
bi_later
:
sbi_car
→
sbi_car
;
s
bi_later
:
sbi_car
→
sbi_car
;
sbi_ofe_mixin
:
OfeMixin
sbi_car
;
sbi_bi_mixin
:
BIMixin
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
:
SBIMixin
sbi_entails
sbi_pure
sbi_or
sbi_impl
sbi_forall
sbi_exist
sbi_internal_eq
sbi_sep
sbi_plainly
sbi_persistently
bi_later
;
sbi_sep
sbi_plainly
sbi_persistently
s
bi_later
;
}.
Arguments
sbi_car
:
simpl
never
.
...
...
@@ -288,7 +288,7 @@ Arguments sbi_sep {PROP} _%I _%I : simpl never, rename.
Arguments
sbi_wand
{
PROP
}
_
%
I
_
%
I
:
simpl
never
,
rename
.
Arguments
sbi_plainly
{
PROP
}
_
%
I
:
simpl
never
,
rename
.
Arguments
sbi_persistently
{
PROP
}
_
%
I
:
simpl
never
,
rename
.
Arguments
bi_later
{
PROP
}
_
%
I
:
simpl
never
,
rename
.
Arguments
s
bi_later
{
PROP
}
_
%
I
:
simpl
never
,
rename
.
Hint
Extern
0
(
bi_entails
_
_
)
=>
reflexivity
.
Instance
bi_rewrite_relation
(
PROP
:
bi
)
:
RewriteRelation
(@
bi_entails
PROP
).
...
...
@@ -321,7 +321,7 @@ Notation "∃ x .. y , P" :=
(
bi_exist
(
λ
x
,
..
(
bi_exist
(
λ
y
,
P
))
..)%
I
)
:
bi_scope
.
Infix
"≡"
:
=
bi_internal_eq
:
bi_scope
.
Notation
"▷ P"
:
=
(
bi_later
P
)
:
bi_scope
.
Notation
"▷ P"
:
=
(
s
bi_later
P
)
:
bi_scope
.
Coercion
bi_valid
{
PROP
:
bi
}
(
P
:
PROP
)
:
Prop
:
=
emp
⊢
P
.
Coercion
sbi_valid
{
PROP
:
sbi
}
:
PROP
→
Prop
:
=
bi_valid
.
...
...
@@ -488,7 +488,7 @@ Context {PROP : sbi}.
Implicit
Types
φ
:
Prop
.
Implicit
Types
P
Q
R
:
PROP
.
Global
Instance
later_contractive
:
Contractive
(@
bi_later
PROP
).
Global
Instance
later_contractive
:
Contractive
(@
s
bi_later
PROP
).
Proof
.
eapply
sbi_mixin_later_contractive
,
sbi_sbi_mixin
.
Qed
.
Lemma
later_eq_1
{
A
:
ofeT
}
(
x
y
:
A
)
:
Next
x
≡
Next
y
⊢
▷
(
x
≡
y
:
PROP
).
...
...
theories/proofmode/class_instances.v
View file @
5d6b3364
...
...
@@ -956,7 +956,7 @@ Global Instance into_sep_affinely_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
Proof
.
rewrite
/
IntoSep
/=
=>
??
->.
rewrite
-{
1
}(
affine_affinely
Q1
)
-{
1
}(
affine_affinely
Q2
)
later_sep
!
later_affinely_1
.
rewrite
-
except_0_sep
/
bi_except_0
affinely_or
.
apply
or_elim
,
affinely_elim
.
rewrite
-
except_0_sep
/
s
bi_except_0
affinely_or
.
apply
or_elim
,
affinely_elim
.
rewrite
-(
idemp
bi_and
(
bi_affinely
(
▷
False
))%
I
)
persistent_and_sep_1
.
by
rewrite
-(
False_elim
Q1
)
-(
False_elim
Q2
).
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