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
Iris
Iris
Commits
0c4a3e1b
Commit
0c4a3e1b
authored
Mar 22, 2018
by
Ralf Jung
Browse files
more consistent lemma naming
Fixes
#177
parent
9ca430f6
Changes
7
Hide whitespace changes
Inline
Side-by-side
theories/bi/derived_laws_bi.v
View file @
0c4a3e1b
...
...
@@ -2,6 +2,13 @@ From iris.bi Require Export derived_connectives.
From
iris
.
algebra
Require
Import
monoid
.
From
stdpp
Require
Import
hlist
.
(** Naming schema for lemmas about modalities:
M1_into_M2: M1 P ⊢ M2 P
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
*)
Module
bi
.
Import
interface
.
bi
.
Section
bi_derived
.
...
...
@@ -605,7 +612,7 @@ Proof. by rewrite /bi_absorbingly !assoc (comm _ P). Qed.
Lemma
absorbingly_sep_lr
P
Q
:
<
absorb
>
P
∗
Q
⊣
⊢
P
∗
<
absorb
>
Q
.
Proof
.
by
rewrite
absorbingly_sep_l
absorbingly_sep_r
.
Qed
.
Lemma
affinely_absorbingly
`
{!
BiPositive
PROP
}
P
:
<
affine
>
<
absorb
>
P
⊣
⊢
<
affine
>
P
.
Lemma
affinely_absorbingly
_elim
`
{!
BiPositive
PROP
}
P
:
<
affine
>
<
absorb
>
P
⊣
⊢
<
affine
>
P
.
Proof
.
apply
(
anti_symm
_
),
affinely_mono
,
absorbingly_intro
.
by
rewrite
/
bi_absorbingly
affinely_sep
affinely_True_emp
affinely_emp
left_id
.
...
...
@@ -714,7 +721,7 @@ Global Instance persistently_flip_mono' :
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
bi_persistently
PROP
).
Proof
.
intros
P
Q
;
apply
persistently_mono
.
Qed
.
Lemma
absorbingly_persistently
P
:
<
absorb
>
<
pers
>
P
⊣
⊢
<
pers
>
P
.
Lemma
absorbingly_
elim_
persistently
P
:
<
absorb
>
<
pers
>
P
⊣
⊢
<
pers
>
P
.
Proof
.
apply
(
anti_symm
_
),
absorbingly_intro
.
by
rewrite
/
bi_absorbingly
comm
persistently_absorbing
.
...
...
@@ -776,16 +783,16 @@ Proof.
Qed
.
Lemma
persistently_and_emp_elim
P
:
emp
∧
<
pers
>
P
⊢
P
.
Proof
.
by
rewrite
comm
persistently_and_sep_elim_emp
right_id
and_elim_r
.
Qed
.
Lemma
persistently_
elim
_absorbingly
P
:
<
pers
>
P
⊢
<
absorb
>
P
.
Lemma
persistently_
into
_absorbingly
P
:
<
pers
>
P
⊢
<
absorb
>
P
.
Proof
.
rewrite
-(
right_id
True
%
I
_
(<
pers
>
_
)%
I
)
-{
1
}(
left_id
emp
%
I
_
True
%
I
).
by
rewrite
persistently_and_sep_assoc
(
comm
bi_and
)
persistently_and_emp_elim
comm
.
Qed
.
Lemma
persistently_elim
P
`
{!
Absorbing
P
}
:
<
pers
>
P
⊢
P
.
Proof
.
by
rewrite
persistently_
elim
_absorbingly
absorbing_absorbingly
.
Qed
.
Proof
.
by
rewrite
persistently_
into
_absorbingly
absorbing_absorbingly
.
Qed
.
Lemma
persistently_idemp_1
P
:
<
pers
>
<
pers
>
P
⊢
<
pers
>
P
.
Proof
.
by
rewrite
persistently_
elim
_absorbingly
absorbingly_persistently
.
Qed
.
Proof
.
by
rewrite
persistently_
into
_absorbingly
absorbingly_
elim_
persistently
.
Qed
.
Lemma
persistently_idemp
P
:
<
pers
>
<
pers
>
P
⊣
⊢
<
pers
>
P
.
Proof
.
apply
(
anti_symm
_
)
;
auto
using
persistently_idemp_1
,
persistently_idemp_2
.
Qed
.
...
...
@@ -795,7 +802,7 @@ Proof. intros <-. apply persistently_idemp_2. Qed.
Lemma
persistently_pure
φ
:
<
pers
>
⌜φ⌝
⊣
⊢
⌜φ⌝
.
Proof
.
apply
(
anti_symm
_
).
{
by
rewrite
persistently_
elim
_absorbingly
absorbingly_pure
.
}
{
by
rewrite
persistently_
into
_absorbingly
absorbingly_pure
.
}
apply
pure_elim'
=>
H
φ
.
trans
(
∀
x
:
False
,
<
pers
>
True
:
PROP
)%
I
;
[
by
apply
forall_intro
|].
rewrite
persistently_forall_2
.
auto
using
persistently_mono
,
pure_intro
.
...
...
@@ -824,7 +831,7 @@ Proof.
by
rewrite
persistently_and_sep_assoc
(
comm
bi_and
)
persistently_and_emp_elim
.
Qed
.
Lemma
persistently_affinely
P
:
<
pers
>
<
affine
>
P
⊣
⊢
<
pers
>
P
.
Lemma
persistently_affinely
_elim
P
:
<
pers
>
<
affine
>
P
⊣
⊢
<
pers
>
P
.
Proof
.
by
rewrite
/
bi_affinely
persistently_and
-
persistently_True_emp
persistently_pure
left_id
.
...
...
@@ -842,7 +849,7 @@ Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently.
Lemma
persistently_sep
`
{
BiPositive
PROP
}
P
Q
:
<
pers
>
(
P
∗
Q
)
⊣
⊢
<
pers
>
P
∗
<
pers
>
Q
.
Proof
.
apply
(
anti_symm
_
)
;
auto
using
persistently_sep_2
.
rewrite
-
persistently_affinely
affinely_sep
-
and_sep_persistently
.
apply
and_intro
.
rewrite
-
persistently_affinely
_elim
affinely_sep
-
and_sep_persistently
.
apply
and_intro
.
-
by
rewrite
(
affinely_elim_emp
Q
)
right_id
affinely_elim
.
-
by
rewrite
(
affinely_elim_emp
P
)
left_id
affinely_elim
.
Qed
.
...
...
@@ -858,7 +865,8 @@ Qed.
Lemma
persistently_alt_fixpoint'
P
:
<
pers
>
P
⊣
⊢
<
affine
>
P
∗
<
pers
>
P
.
Proof
.
rewrite
-{
1
}
persistently_affinely
{
1
}
persistently_alt_fixpoint
persistently_affinely
//.
rewrite
-{
1
}
persistently_affinely_elim
{
1
}
persistently_alt_fixpoint
persistently_affinely_elim
//.
Qed
.
Lemma
persistently_wand
P
Q
:
<
pers
>
(
P
-
∗
Q
)
⊢
<
pers
>
P
-
∗
<
pers
>
Q
.
...
...
@@ -946,7 +954,7 @@ Proof. rewrite /bi_intuitionistically affinely_elim_emp //. Qed.
Lemma
intuitionistically_intro'
P
Q
:
(
□
P
⊢
Q
)
→
□
P
⊢
□
Q
.
Proof
.
intros
<-.
by
rewrite
/
bi_intuitionistically
persistently_affinely
persistently_idemp
.
by
rewrite
/
bi_intuitionistically
persistently_affinely
_elim
persistently_idemp
.
Qed
.
Lemma
intuitionistically_emp
:
□
emp
⊣
⊢
emp
.
...
...
@@ -973,11 +981,11 @@ Lemma intuitionistically_sep `{BiPositive PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P
Proof
.
by
rewrite
/
bi_intuitionistically
-
affinely_sep
-
persistently_sep
.
Qed
.
Lemma
intuitionistically_idemp
P
:
□
□
P
⊣
⊢
□
P
.
Proof
.
by
rewrite
/
bi_intuitionistically
persistently_affinely
persistently_idemp
.
Qed
.
Proof
.
by
rewrite
/
bi_intuitionistically
persistently_affinely
_elim
persistently_idemp
.
Qed
.
Lemma
intuitionistically_persistently_1
P
:
□
P
⊢
<
pers
>
P
.
Lemma
intuitionistically_
into_
persistently_1
P
:
□
P
⊢
<
pers
>
P
.
Proof
.
rewrite
/
bi_intuitionistically
affinely_elim
//.
Qed
.
Lemma
intuitionistically_persistently_
persistently
P
:
□
<
pers
>
P
⊣
⊢
□
P
.
Lemma
intuitionistically_persistently_
elim
P
:
□
<
pers
>
P
⊣
⊢
□
P
.
Proof
.
rewrite
/
bi_intuitionistically
persistently_idemp
//.
Qed
.
Lemma
intuitionistic_intuitionistically
P
:
...
...
@@ -992,8 +1000,8 @@ Proof.
-
rewrite
and_elim_l
//.
-
apply
persistently_and_emp_elim
.
Qed
.
Lemma
intuitionistically_affinely_
affinely
P
:
□
<
affine
>
P
⊣
⊢
□
P
.
Proof
.
rewrite
/
bi_intuitionistically
persistently_affinely
//.
Qed
.
Lemma
intuitionistically_affinely_
elim
P
:
□
<
affine
>
P
⊣
⊢
□
P
.
Proof
.
rewrite
/
bi_intuitionistically
persistently_affinely
_elim
//.
Qed
.
Lemma
persistently_and_intuitionistically_sep_l
P
Q
:
<
pers
>
P
∧
Q
⊣
⊢
□
P
∗
Q
.
Proof
.
...
...
@@ -1038,7 +1046,7 @@ Qed.
Section
bi_affine_intuitionistically
.
Context
`
{
BiAffine
PROP
}.
Lemma
intuitionistically_persistently
P
:
□
P
⊣
⊢
<
pers
>
P
.
Lemma
intuitionistically_
into_
persistently
P
:
□
P
⊣
⊢
<
pers
>
P
.
Proof
.
rewrite
/
bi_intuitionistically
affine_affinely
//.
Qed
.
End
bi_affine_intuitionistically
.
...
...
@@ -1205,10 +1213,11 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
Lemma
persistent_entails_r
P
Q
`
{!
Persistent
Q
}
:
(
P
⊢
Q
)
→
P
⊢
P
∗
Q
.
Proof
.
intros
.
rewrite
-
persistent_and_sep_1
;
auto
.
Qed
.
Lemma
absorbingly_intuitionistically
P
:
<
absorb
>
□
P
⊣
⊢
<
pers
>
P
.
Lemma
absorbingly_intuitionistically_into_persistently
P
:
<
absorb
>
□
P
⊣
⊢
<
pers
>
P
.
Proof
.
apply
(
anti_symm
_
).
-
by
rewrite
intuitionistically_persistently_1
absorbingly_persistently
.
-
by
rewrite
intuitionistically_
into_
persistently_1
absorbingly_
elim_
persistently
.
-
rewrite
-{
1
}(
idemp
bi_and
(<
pers
>
_
)%
I
)
persistently_and_intuitionistically_sep_r
.
by
rewrite
{
1
}
(
True_intro
(<
pers
>
_
)%
I
).
Qed
.
...
...
@@ -1216,13 +1225,13 @@ Qed.
Lemma
persistent_absorbingly_affinely_2
P
`
{!
Persistent
P
}
:
P
⊢
<
absorb
>
<
affine
>
P
.
Proof
.
rewrite
{
1
}(
persistent
P
)
-
absorbingly_intuitionistically
.
rewrite
{
1
}(
persistent
P
)
-
absorbingly_intuitionistically
_into_persistently
.
by
rewrite
intuitionistically_affinely
.
Qed
.
Lemma
persistent_absorbingly_affinely
P
`
{!
Persistent
P
,
!
Absorbing
P
}
:
<
absorb
>
<
affine
>
P
⊣
⊢
P
.
Proof
.
by
rewrite
-(
persistent_persistently
P
)
absorbingly_intuitionistically
.
by
rewrite
-(
persistent_persistently
P
)
absorbingly_intuitionistically
_into_persistently
.
Qed
.
Lemma
persistent_and_sep_assoc
P
`
{!
Persistent
P
,
!
Absorbing
P
}
Q
R
:
...
...
@@ -1309,7 +1318,7 @@ Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_in
Global
Instance
absorbingly_absorbing
P
:
Absorbing
(<
absorb
>
P
).
Proof
.
rewrite
/
bi_absorbingly
.
apply
_
.
Qed
.
Global
Instance
persistently_absorbing
P
:
Absorbing
(<
pers
>
P
).
Proof
.
by
rewrite
/
Absorbing
absorbingly_persistently
.
Qed
.
Proof
.
by
rewrite
/
Absorbing
absorbingly_
elim_
persistently
.
Qed
.
Global
Instance
persistently_if_absorbing
P
p
:
Absorbing
P
→
Absorbing
(<
pers
>
?p
P
).
Proof
.
intros
;
destruct
p
;
simpl
;
apply
_
.
Qed
.
...
...
theories/bi/derived_laws_sbi.v
View file @
0c4a3e1b
...
...
@@ -121,7 +121,7 @@ Qed.
Lemma
persistently_internal_eq
{
A
:
ofeT
}
(
a
b
:
A
)
:
<
pers
>
(
a
≡
b
)
⊣
⊢
a
≡
b
.
Proof
.
apply
(
anti_symm
(
⊢
)).
{
by
rewrite
persistently_
elim
_absorbingly
absorbingly_internal_eq
.
}
{
by
rewrite
persistently_
into
_absorbingly
absorbingly_internal_eq
.
}
apply
(
internal_eq_rewrite'
a
b
(
λ
b
,
<
pers
>
(
a
≡
b
))%
I
)
;
auto
.
rewrite
-(
internal_eq_refl
emp
%
I
a
).
apply
persistently_emp_intro
.
Qed
.
...
...
theories/bi/plainly.v
View file @
0c4a3e1b
...
...
@@ -121,16 +121,16 @@ Proof. intros P Q; apply plainly_mono. Qed.
Lemma
affinely_plainly_elim
P
:
<
affine
>
■
P
⊢
P
.
Proof
.
by
rewrite
plainly_elim_persistently
/
bi_affinely
persistently_and_emp_elim
.
Qed
.
Lemma
persistently_plainly
P
:
<
pers
>
■
P
⊣
⊢
■
P
.
Lemma
persistently_
elim_
plainly
P
:
<
pers
>
■
P
⊣
⊢
■
P
.
Proof
.
apply
(
anti_symm
_
).
-
by
rewrite
persistently_
elim
_absorbingly
/
bi_absorbingly
comm
plainly_absorb
.
-
by
rewrite
persistently_
into
_absorbingly
/
bi_absorbingly
comm
plainly_absorb
.
-
by
rewrite
{
1
}
plainly_idemp_2
plainly_elim_persistently
.
Qed
.
Lemma
persistently_if_plainly
P
p
:
<
pers
>
?p
■
P
⊣
⊢
■
P
.
Proof
.
destruct
p
;
last
done
.
exact
:
persistently_plainly
.
Qed
.
Lemma
persistently_if_
elim_
plainly
P
p
:
<
pers
>
?p
■
P
⊣
⊢
■
P
.
Proof
.
destruct
p
;
last
done
.
exact
:
persistently_
elim_
plainly
.
Qed
.
Lemma
plainly_persistently
P
:
■
<
pers
>
P
⊣
⊢
■
P
.
Lemma
plainly_persistently
_elim
P
:
■
<
pers
>
P
⊣
⊢
■
P
.
Proof
.
apply
(
anti_symm
_
).
-
rewrite
-{
1
}(
left_id
True
%
I
bi_and
(
■
_
)%
I
)
(
plainly_emp_intro
True
%
I
).
...
...
@@ -139,22 +139,22 @@ Proof.
-
by
rewrite
{
1
}
plainly_idemp_2
(
plainly_elim_persistently
P
).
Qed
.
Lemma
absorbingly_plainly
P
:
<
absorb
>
■
P
⊣
⊢
■
P
.
Proof
.
by
rewrite
-(
persistently_plainly
P
)
absorbingly_persistently
.
Qed
.
Lemma
absorbingly_
elim_
plainly
P
:
<
absorb
>
■
P
⊣
⊢
■
P
.
Proof
.
by
rewrite
-(
persistently_
elim_
plainly
P
)
absorbingly_
elim_
persistently
.
Qed
.
Lemma
plainly_and_sep_elim
P
Q
:
■
P
∧
Q
-
∗
(
emp
∧
P
)
∗
Q
.
Proof
.
by
rewrite
plainly_elim_persistently
persistently_and_sep_elim_emp
.
Qed
.
Lemma
plainly_and_sep_assoc
P
Q
R
:
■
P
∧
(
Q
∗
R
)
⊣
⊢
(
■
P
∧
Q
)
∗
R
.
Proof
.
by
rewrite
-(
persistently_plainly
P
)
persistently_and_sep_assoc
.
Qed
.
Proof
.
by
rewrite
-(
persistently_
elim_
plainly
P
)
persistently_and_sep_assoc
.
Qed
.
Lemma
plainly_and_emp_elim
P
:
emp
∧
■
P
⊢
P
.
Proof
.
by
rewrite
plainly_elim_persistently
persistently_and_emp_elim
.
Qed
.
Lemma
plainly_
elim
_absorbingly
P
:
■
P
⊢
<
absorb
>
P
.
Proof
.
by
rewrite
plainly_elim_persistently
persistently_
elim
_absorbingly
.
Qed
.
Lemma
plainly_
into
_absorbingly
P
:
■
P
⊢
<
absorb
>
P
.
Proof
.
by
rewrite
plainly_elim_persistently
persistently_
into
_absorbingly
.
Qed
.
Lemma
plainly_elim
P
`
{!
Absorbing
P
}
:
■
P
⊢
P
.
Proof
.
by
rewrite
plainly_elim_persistently
persistently_elim
.
Qed
.
Lemma
plainly_idemp_1
P
:
■
■
P
⊢
■
P
.
Proof
.
by
rewrite
plainly_
elim
_absorbingly
absorbingly_plainly
.
Qed
.
Proof
.
by
rewrite
plainly_
into
_absorbingly
absorbingly_
elim_
plainly
.
Qed
.
Lemma
plainly_idemp
P
:
■
■
P
⊣
⊢
■
P
.
Proof
.
apply
(
anti_symm
_
)
;
auto
using
plainly_idemp_1
,
plainly_idemp_2
.
Qed
.
...
...
@@ -213,15 +213,15 @@ Proof.
by
rewrite
plainly_and_sep_assoc
(
comm
bi_and
)
plainly_and_emp_elim
.
Qed
.
Lemma
plainly_affinely
P
:
■
<
affine
>
P
⊣
⊢
■
P
.
Lemma
plainly_affinely
_elim
P
:
■
<
affine
>
P
⊣
⊢
■
P
.
Proof
.
by
rewrite
/
bi_affinely
plainly_and
-
plainly_True_emp
plainly_pure
left_id
.
Qed
.
Lemma
intuitionistically_plainly_elim
P
:
□
■
P
-
∗
□
P
.
Proof
.
rewrite
intuitionistically_affinely
plainly_elim_persistently
//.
Qed
.
Lemma
intuitionistically_plainly
P
:
□
■
P
-
∗
■
□
P
.
Proof
.
rewrite
/
bi_intuitionistically
plainly_affinely
affinely_elim
.
rewrite
persistently_plainly
plainly_persistently
.
done
.
rewrite
/
bi_intuitionistically
plainly_affinely
_elim
affinely_elim
.
rewrite
persistently_
elim_
plainly
plainly_persistently
_elim
.
done
.
Qed
.
Lemma
and_sep_plainly
P
Q
:
■
P
∧
■
Q
⊣
⊢
■
P
∗
■
Q
.
...
...
@@ -236,7 +236,7 @@ Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
Lemma
plainly_sep
`
{
BiPositive
PROP
}
P
Q
:
■
(
P
∗
Q
)
⊣
⊢
■
P
∗
■
Q
.
Proof
.
apply
(
anti_symm
_
)
;
auto
using
plainly_sep_2
.
rewrite
-(
plainly_affinely
(
_
∗
_
)%
I
)
affinely_sep
-
and_sep_plainly
.
apply
and_intro
.
rewrite
-(
plainly_affinely
_elim
(
_
∗
_
)%
I
)
affinely_sep
-
and_sep_plainly
.
apply
and_intro
.
-
by
rewrite
(
affinely_elim_emp
Q
)
right_id
affinely_elim
.
-
by
rewrite
(
affinely_elim_emp
P
)
left_id
affinely_elim
.
Qed
.
...
...
@@ -260,7 +260,7 @@ Lemma impl_wand_plainly_2 P Q : (■ P -∗ Q) ⊢ (■ P → Q).
Proof
.
apply
impl_intro_l
.
by
rewrite
plainly_and_sep_l_1
wand_elim_r
.
Qed
.
Lemma
impl_wand_affinely_plainly
P
Q
:
(
■
P
→
Q
)
⊣
⊢
(<
affine
>
■
P
-
∗
Q
).
Proof
.
by
rewrite
-(
persistently_plainly
P
)
impl_wand_intuitionistically
.
Qed
.
Proof
.
by
rewrite
-(
persistently_
elim_
plainly
P
)
impl_wand_intuitionistically
.
Qed
.
Lemma
persistently_wand_affinely_plainly
P
Q
:
(<
affine
>
■
P
-
∗
<
pers
>
Q
)
⊢
<
pers
>
(<
affine
>
■
P
-
∗
Q
).
...
...
@@ -357,11 +357,11 @@ Lemma impl_persistent P Q :
Absorbing
P
→
Plain
P
→
Persistent
Q
→
Persistent
(
P
→
Q
).
Proof
.
intros
.
by
rewrite
/
Persistent
{
2
}(
plain
P
)
-
persistently_impl_plainly
-(
persistent
Q
)
(
plainly_
elim
_absorbingly
P
)
absorbing
.
-(
persistent
Q
)
(
plainly_
into
_absorbingly
P
)
absorbing
.
Qed
.
Global
Instance
plainly_persistent
P
:
Persistent
(
■
P
).
Proof
.
by
rewrite
/
Persistent
persistently_plainly
.
Qed
.
Proof
.
by
rewrite
/
Persistent
persistently_
elim_
plainly
.
Qed
.
Global
Instance
wand_persistent
P
Q
:
Plain
P
→
Persistent
Q
→
Absorbing
Q
→
Persistent
(
P
-
∗
Q
).
...
...
@@ -428,7 +428,7 @@ Qed.
Global
Instance
impl_plain
P
Q
:
Absorbing
P
→
Plain
P
→
Plain
Q
→
Plain
(
P
→
Q
).
Proof
.
intros
.
by
rewrite
/
Plain
{
2
}(
plain
P
)
-
plainly_impl_plainly
-(
plain
Q
)
(
plainly_
elim
_absorbingly
P
)
absorbing
.
(
plainly_
into
_absorbingly
P
)
absorbing
.
Qed
.
Global
Instance
wand_plain
P
Q
:
Plain
P
→
Plain
Q
→
Absorbing
Q
→
Plain
(
P
-
∗
Q
).
...
...
@@ -445,7 +445,7 @@ Global Instance plainly_plain P : Plain (■ P).
Proof
.
by
rewrite
/
Plain
plainly_idemp
.
Qed
.
Global
Instance
persistently_plain
P
:
Plain
P
→
Plain
(<
pers
>
P
).
Proof
.
rewrite
/
Plain
=>
HP
.
rewrite
{
1
}
HP
plainly_persistently
persistently_plainly
//.
rewrite
/
Plain
=>
HP
.
rewrite
{
1
}
HP
plainly_persistently
_elim
persistently_
elim_
plainly
//.
Qed
.
Global
Instance
affinely_plain
P
:
Plain
P
→
Plain
(<
affine
>
P
).
Proof
.
rewrite
/
bi_affinely
.
apply
_
.
Qed
.
...
...
@@ -468,7 +468,7 @@ Qed.
Lemma
plainly_alt
P
:
■
P
⊣
⊢
<
affine
>
P
≡
emp
.
Proof
.
rewrite
-
plainly_affinely
.
apply
(
anti_symm
(
⊢
)).
rewrite
-
plainly_affinely
_elim
.
apply
(
anti_symm
(
⊢
)).
-
rewrite
-
prop_ext
.
apply
plainly_mono
,
and_intro
;
apply
wand_intro_l
.
+
by
rewrite
affinely_elim_emp
left_id
.
+
by
rewrite
left_id
.
...
...
theories/proofmode/class_instances_bi.v
View file @
0c4a3e1b
...
...
@@ -64,13 +64,13 @@ Global Instance from_assumption_persistently_l_true P Q :
FromAssumption
true
P
Q
→
KnownLFromAssumption
true
(<
pers
>
P
)
Q
.
Proof
.
rewrite
/
KnownLFromAssumption
/
FromAssumption
/=
=><-.
rewrite
intuitionistically_persistently_
persistently
//.
rewrite
intuitionistically_persistently_
elim
//.
Qed
.
Global
Instance
from_assumption_persistently_l_false
`
{
BiAffine
PROP
}
P
Q
:
FromAssumption
true
P
Q
→
KnownLFromAssumption
false
(<
pers
>
P
)
Q
.
Proof
.
rewrite
/
KnownLFromAssumption
/
FromAssumption
/=
=><-.
by
rewrite
intuitionistically_persistently
.
by
rewrite
intuitionistically_
into_
persistently
.
Qed
.
Global
Instance
from_assumption_affinely_l_true
p
P
Q
:
FromAssumption
p
P
Q
→
KnownLFromAssumption
p
(<
affine
>
P
)
Q
.
...
...
@@ -195,7 +195,7 @@ Global Instance from_pure_persistently P a φ :
FromPure
true
P
φ
→
FromPure
a
(<
pers
>
P
)
φ
.
Proof
.
rewrite
/
FromPure
=>
<-
/=.
by
rewrite
persistently_affinely
affinely_if_elim
persistently_pure
.
by
rewrite
persistently_affinely
_elim
affinely_if_elim
persistently_pure
.
Qed
.
Global
Instance
from_pure_affinely_true
P
φ
:
FromPure
true
P
φ
→
FromPure
true
(<
affine
>
P
)
φ
.
...
...
@@ -206,7 +206,7 @@ Proof. rewrite /FromPure /= affine_affinely //. Qed.
Global
Instance
from_pure_intuitionistically_true
P
φ
:
FromPure
true
P
φ
→
FromPure
true
(
□
P
)
φ
.
Proof
.
rewrite
/
FromPure
=><-
/=.
rewrite
intuitionistically_affinely_
affinely
.
rewrite
/
FromPure
=><-
/=.
rewrite
intuitionistically_affinely_
elim
.
rewrite
{
1
}(
persistent
⌜φ⌝
%
I
)
//.
Qed
.
...
...
@@ -233,7 +233,7 @@ Proof.
rewrite
/
IntoPersistent
/=
=><-.
destruct
p
;
simpl
;
eauto
using
persistently_mono
,
intuitionistically_elim
,
intuitionistically_persistently_1
.
intuitionistically_
into_
persistently_1
.
Qed
.
Global
Instance
into_persistent_embed
`
{
BiEmbed
PROP
PROP'
}
p
P
Q
:
IntoPersistent
p
P
Q
→
IntoPersistent
p
⎡
P
⎤
⎡
Q
⎤
|
0
.
...
...
@@ -259,7 +259,9 @@ Global Instance from_modal_intuitionistically P :
Proof
.
by
rewrite
/
FromModal
.
Qed
.
Global
Instance
from_modal_intuitionistically_affine_bi
P
:
BiAffine
PROP
→
FromModal
modality_persistently
(
□
P
)
(
□
P
)
P
|
0
.
Proof
.
intros
.
by
rewrite
/
FromModal
/=
intuitionistically_persistently
.
Qed
.
Proof
.
intros
.
by
rewrite
/
FromModal
/=
intuitionistically_into_persistently
.
Qed
.
Global
Instance
from_modal_absorbingly
P
:
FromModal
modality_id
(<
absorb
>
P
)
(<
absorb
>
P
)
P
.
...
...
@@ -356,7 +358,7 @@ Global Instance into_wand_intuitionistically p q R P Q :
Proof
.
by
rewrite
/
IntoWand
intuitionistically_elim
.
Qed
.
Global
Instance
into_wand_persistently_true
q
R
P
Q
:
IntoWand
true
q
R
P
Q
→
IntoWand
true
q
(<
pers
>
R
)
P
Q
.
Proof
.
by
rewrite
/
IntoWand
/=
intuitionistically_persistently_
persistently
.
Qed
.
Proof
.
by
rewrite
/
IntoWand
/=
intuitionistically_persistently_
elim
.
Qed
.
Global
Instance
into_wand_persistently_false
q
R
P
Q
:
Absorbing
R
→
IntoWand
false
q
R
P
Q
→
IntoWand
false
q
(<
pers
>
R
)
P
Q
.
Proof
.
intros
?.
by
rewrite
/
IntoWand
persistently_elim
.
Qed
.
...
...
@@ -494,7 +496,7 @@ Global Instance into_and_affinely p P Q1 Q2 :
IntoAnd
p
P
Q1
Q2
→
IntoAnd
p
(<
affine
>
P
)
(<
affine
>
Q1
)
(<
affine
>
Q2
).
Proof
.
rewrite
/
IntoAnd
.
destruct
p
;
simpl
.
-
rewrite
-
affinely_and
!
intuitionistically_affinely_
affinely
//.
-
rewrite
-
affinely_and
!
intuitionistically_affinely_
elim
//.
-
intros
->.
by
rewrite
affinely_and
.
Qed
.
Global
Instance
into_and_intuitionistically
p
P
Q1
Q2
:
...
...
@@ -509,7 +511,7 @@ Global Instance into_and_persistently p P Q1 Q2 :
IntoAnd
p
(<
pers
>
P
)
(<
pers
>
Q1
)
(<
pers
>
Q2
).
Proof
.
rewrite
/
IntoAnd
/=.
destruct
p
;
simpl
.
-
rewrite
-
persistently_and
!
intuitionistically_persistently_
persistently
//.
-
rewrite
-
persistently_and
!
intuitionistically_persistently_
elim
//.
-
intros
->.
by
rewrite
persistently_and
.
Qed
.
Global
Instance
into_and_embed
`
{
BiEmbed
PROP
PROP'
}
p
P
Q1
Q2
:
...
...
@@ -746,7 +748,7 @@ Qed.
Global
Instance
from_forall_intuitionistically
`
{
BiAffine
PROP
}
{
A
}
P
(
Φ
:
A
→
PROP
)
:
FromForall
P
Φ
→
FromForall
(
□
P
)
(
λ
a
,
□
(
Φ
a
))%
I
.
Proof
.
rewrite
/
FromForall
=>
<-.
setoid_rewrite
intuitionistically_persistently
.
rewrite
/
FromForall
=>
<-.
setoid_rewrite
intuitionistically_
into_
persistently
.
by
rewrite
persistently_forall
.
Qed
.
Global
Instance
from_forall_persistently
{
A
}
P
(
Φ
:
A
→
PROP
)
:
...
...
theories/proofmode/class_instances_sbi.v
View file @
0c4a3e1b
...
...
@@ -36,7 +36,7 @@ Global Instance from_assumption_plainly_l_false `{BiPlainly PROP, BiAffine PROP}
FromAssumption
true
P
Q
→
KnownLFromAssumption
false
(
■
P
)
Q
.
Proof
.
rewrite
/
KnownLFromAssumption
/
FromAssumption
/=
=><-.
rewrite
plainly_elim_persistently
intuitionistically_persistently
//.
rewrite
plainly_elim_persistently
intuitionistically_
into_
persistently
//.
Qed
.
(* FromPure *)
...
...
theories/proofmode/coq_tactics.v
View file @
0c4a3e1b
...
...
@@ -375,7 +375,7 @@ Lemma env_spatial_is_nil_intuitionistically Δ :
Proof
.
intros
.
unfold
of_envs
;
destruct
Δ
as
[?
[]]
;
simplify_eq
/=.
rewrite
!
right_id
/
bi_intuitionistically
{
1
}
affinely_and_r
persistently_and
.
by
rewrite
persistently_affinely
persistently_idemp
persistently_pure
.
by
rewrite
persistently_affinely
_elim
persistently_idemp
persistently_pure
.
Qed
.
Lemma
envs_lookup_envs_delete
Δ
i
p
P
:
...
...
@@ -616,7 +616,7 @@ Proof.
+
rewrite
-(
affine_affinely
P
)
(
_
:
P
=
<
pers
>
?false
P
)%
I
//
(
into_persistent
_
P
)
wand_elim_r
//.
+
rewrite
(
_
:
P
=
<
pers
>
?false
P
)%
I
//
(
into_persistent
_
P
).
by
rewrite
-{
1
}
absorbingly_intuitionistically
by
rewrite
-{
1
}
absorbingly_intuitionistically
_into_persistently
absorbingly_sep_l
wand_elim_r
HQ
.
Qed
.
...
...
@@ -673,7 +673,7 @@ Proof.
-
rewrite
-(
affine_affinely
P
)
(
_
:
P
=
<
pers
>
?false
P
)%
I
//
(
into_persistent
_
P
)
wand_elim_r
//.
-
rewrite
(
_
:
P
=
<
pers
>
?false
P
)%
I
//
(
into_persistent
_
P
).
by
rewrite
-{
1
}
absorbingly_intuitionistically
by
rewrite
-{
1
}
absorbingly_intuitionistically
_into_persistently
absorbingly_sep_l
wand_elim_r
HQ
.
Qed
.
Lemma
tac_wand_intro_pure
Δ
P
φ
Q
R
:
...
...
@@ -769,7 +769,7 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
Proof
.
rewrite
envs_entails_eq
=>
?????
<-.
rewrite
envs_simple_replace_singleton_sound
//=.
rewrite
-
intuitionistically_if_idemp
into_wand
/=
-(
from_pure
_
P1
)
/
bi_intuitionistically
.
rewrite
pure_True
//=
persistently_affinely
persistently_pure
rewrite
pure_True
//=
persistently_affinely
_elim
persistently_pure
affinely_True_emp
affinely_emp
.
by
rewrite
emp_wand
wand_elim_r
.
Qed
.
...
...
@@ -787,7 +787,7 @@ Proof.
rewrite
-(
idemp
bi_and
(
of_envs
(
envs_delete
_
_
_
_
))).
rewrite
{
2
}
envs_simple_replace_singleton_sound'
//
;
simpl
.
rewrite
{
1
}
HP1
(
into_absorbingly
P1'
)
(
persistent_persistently_2
P1
).
rewrite
absorbingly_persistently
persistently_and_intuitionistically_sep_l
assoc
.
rewrite
absorbingly_
elim_
persistently
persistently_and_intuitionistically_sep_l
assoc
.
rewrite
-
intuitionistically_if_idemp
-
intuitionistically_idemp
.
rewrite
(
intuitionistically_intuitionistically_if
q
).
by
rewrite
intuitionistically_if_sep_2
into_wand
wand_elim_l
wand_elim_r
.
...
...
@@ -804,7 +804,7 @@ Proof.
rewrite
envs_entails_eq
=>
?
HR
?
Hpos
?
<-.
rewrite
-(
idemp
bi_and
(
of_envs
Δ
))
{
1
}
HR
.
rewrite
envs_replace_singleton_sound
//
;
destruct
q
;
simpl
.
-
by
rewrite
(
_
:
R
=
<
pers
>
?false
R
)%
I
//
(
into_persistent
_
R
)
absorbingly_persistently
sep_elim_r
persistently_and_intuitionistically_sep_l
wand_elim_r
.
absorbingly_
elim_
persistently
sep_elim_r
persistently_and_intuitionistically_sep_l
wand_elim_r
.
-
by
rewrite
(
absorbing_absorbingly
R
)
(
_
:
R
=
<
pers
>
?false
R
)%
I
//
(
into_persistent
_
R
)
sep_elim_r
persistently_and_intuitionistically_sep_l
wand_elim_r
.
Qed
.
...
...
@@ -848,7 +848,7 @@ Proof.
rewrite
/
IntoIH
envs_entails_eq
.
intros
HP
?
HPQ
.
rewrite
(
env_spatial_is_nil_intuitionistically
Δ
)
//.
rewrite
-(
idemp
bi_and
(
□
(
of_envs
Δ
))%
I
)
{
1
}
HP
//
HPQ
.
rewrite
{
1
}
intuitionistically_persistently_1
intuitionistically_elim
impl_elim_r
//.
rewrite
{
1
}
intuitionistically_
into_
persistently_1
intuitionistically_elim
impl_elim_r
//.
Qed
.
Lemma
tac_assert
Δ
Δ
'
j
P
Q
:
...
...
@@ -1407,6 +1407,6 @@ Proof.
rewrite
-(
l
ö
b
(<
pers
>
Q
)%
I
)
later_persistently
.
apply
impl_intro_l
.
rewrite
envs_app_singleton_sound
//
;
simpl
;
rewrite
HQ
.
rewrite
persistently_and_intuitionistically_sep_l
-{
1
}
intuitionistically_idemp
.
rewrite
intuitionistically_sep_2
wand_elim_r
intuitionistically_persistently_1
//.
rewrite
intuitionistically_sep_2
wand_elim_r
intuitionistically_
into_
persistently_1
//.
Qed
.
End
sbi_tactics
.
theories/proofmode/frame_instances.v
View file @
0c4a3e1b
...
...
@@ -229,8 +229,8 @@ Global Instance frame_persistently R P Q Q' :
Proof
.
rewrite
/
Frame
/
MakePersistently
=>
<-
<-
/=.
rewrite
-
persistently_and_intuitionistically_sep_l
.
by
rewrite
-
persistently_sep_2
-
persistently_and_sep_l_1
persistently_affinely
persistently_idemp
.
by
rewrite
-
persistently_sep_2
-
persistently_and_sep_l_1
persistently_affinely_elim
persistently_idemp
.
Qed
.
Global
Instance
frame_exist
{
A
}
p
R
(
Φ
Ψ
:
A
→
PROP
)
:
...
...
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