Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Janno
iris-coq
Commits
58bd4b02
Commit
58bd4b02
authored
Oct 21, 2016
by
Robbert Krebbers
Browse files
Rename except_last -> except_0.
parent
fc3ac148
Changes
8
Hide whitespace changes
Inline
Side-by-side
base_logic/derived.v
View file @
58bd4b02
...
...
@@ -12,11 +12,11 @@ Arguments uPred_always_if _ !_ _/.
Notation
"□? p P"
:
=
(
uPred_always_if
p
P
)
(
at
level
20
,
p
at
level
0
,
P
at
level
20
,
format
"□? p P"
).
Definition
uPred_except_
last
{
M
}
(
P
:
uPred
M
)
:
uPred
M
:
=
▷
False
∨
P
.
Notation
"◇ P"
:
=
(
uPred_except_
last
P
)
Definition
uPred_except_
0
{
M
}
(
P
:
uPred
M
)
:
uPred
M
:
=
▷
False
∨
P
.
Notation
"◇ P"
:
=
(
uPred_except_
0
P
)
(
at
level
20
,
right
associativity
)
:
uPred_scope
.
Instance
:
Params
(@
uPred_except_
last
)
1
.
Typeclasses
Opaque
uPred_except_
last
.
Instance
:
Params
(@
uPred_except_
0
)
1
.
Typeclasses
Opaque
uPred_except_
0
.
Class
TimelessP
{
M
}
(
P
:
uPred
M
)
:
=
timelessP
:
▷
P
⊢
◇
P
.
Arguments
timelessP
{
_
}
_
{
_
}.
...
...
@@ -547,50 +547,50 @@ Proof. destruct p; simpl; auto using always_later. Qed.
(* True now *)
Global
Instance
except_
last
_ne
n
:
Proper
(
dist
n
==>
dist
n
)
(@
uPred_except_
last
M
).
Global
Instance
except_
0
_ne
n
:
Proper
(
dist
n
==>
dist
n
)
(@
uPred_except_
0
M
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
except_
last
_proper
:
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
uPred_except_
last
M
).
Global
Instance
except_
0
_proper
:
Proper
((
⊣
⊢
)
==>
(
⊣
⊢
))
(@
uPred_except_
0
M
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
except_
last
_mono'
:
Proper
((
⊢
)
==>
(
⊢
))
(@
uPred_except_
last
M
).
Global
Instance
except_
0
_mono'
:
Proper
((
⊢
)
==>
(
⊢
))
(@
uPred_except_
0
M
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
except_
last
_flip_mono'
:
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
uPred_except_
last
M
).
Global
Instance
except_
0
_flip_mono'
:
Proper
(
flip
(
⊢
)
==>
flip
(
⊢
))
(@
uPred_except_
0
M
).
Proof
.
solve_proper
.
Qed
.
Lemma
except_
last
_intro
P
:
P
⊢
◇
P
.
Proof
.
rewrite
/
uPred_except_
last
;
auto
.
Qed
.
Lemma
except_
last
_mono
P
Q
:
(
P
⊢
Q
)
→
◇
P
⊢
◇
Q
.
Lemma
except_
0
_intro
P
:
P
⊢
◇
P
.
Proof
.
rewrite
/
uPred_except_
0
;
auto
.
Qed
.
Lemma
except_
0
_mono
P
Q
:
(
P
⊢
Q
)
→
◇
P
⊢
◇
Q
.
Proof
.
by
intros
->.
Qed
.
Lemma
except_
last
_idemp
P
:
◇
◇
P
⊢
◇
P
.
Proof
.
rewrite
/
uPred_except_
last
;
auto
.
Qed
.
Lemma
except_
last
_True
:
◇
True
⊣
⊢
True
.
Proof
.
rewrite
/
uPred_except_
last
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Lemma
except_
last
_or
P
Q
:
◇
(
P
∨
Q
)
⊣
⊢
◇
P
∨
◇
Q
.
Proof
.
rewrite
/
uPred_except_
last
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Lemma
except_
last
_and
P
Q
:
◇
(
P
∧
Q
)
⊣
⊢
◇
P
∧
◇
Q
.
Proof
.
by
rewrite
/
uPred_except_
last
or_and_l
.
Qed
.
Lemma
except_
last
_sep
P
Q
:
◇
(
P
★
Q
)
⊣
⊢
◇
P
★
◇
Q
.
Proof
.
rewrite
/
uPred_except_
last
.
apply
(
anti_symm
_
).
Lemma
except_
0
_idemp
P
:
◇
◇
P
⊢
◇
P
.
Proof
.
rewrite
/
uPred_except_
0
;
auto
.
Qed
.
Lemma
except_
0
_True
:
◇
True
⊣
⊢
True
.
Proof
.
rewrite
/
uPred_except_
0
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Lemma
except_
0
_or
P
Q
:
◇
(
P
∨
Q
)
⊣
⊢
◇
P
∨
◇
Q
.
Proof
.
rewrite
/
uPred_except_
0
.
apply
(
anti_symm
_
)
;
auto
.
Qed
.
Lemma
except_
0
_and
P
Q
:
◇
(
P
∧
Q
)
⊣
⊢
◇
P
∧
◇
Q
.
Proof
.
by
rewrite
/
uPred_except_
0
or_and_l
.
Qed
.
Lemma
except_
0
_sep
P
Q
:
◇
(
P
★
Q
)
⊣
⊢
◇
P
★
◇
Q
.
Proof
.
rewrite
/
uPred_except_
0
.
apply
(
anti_symm
_
).
-
apply
or_elim
;
last
by
auto
.
by
rewrite
-!
or_intro_l
-
always_pure
-
always_later
-
always_sep_dup'
.
-
rewrite
sep_or_r
sep_elim_l
sep_or_l
;
auto
.
Qed
.
Lemma
except_
last
_forall
{
A
}
(
Φ
:
A
→
uPred
M
)
:
◇
(
∀
a
,
Φ
a
)
⊢
∀
a
,
◇
Φ
a
.
Lemma
except_
0
_forall
{
A
}
(
Φ
:
A
→
uPred
M
)
:
◇
(
∀
a
,
Φ
a
)
⊢
∀
a
,
◇
Φ
a
.
Proof
.
apply
forall_intro
=>
a
.
by
rewrite
(
forall_elim
a
).
Qed
.
Lemma
except_
last
_exist
{
A
}
(
Φ
:
A
→
uPred
M
)
:
(
∃
a
,
◇
Φ
a
)
⊢
◇
∃
a
,
Φ
a
.
Lemma
except_
0
_exist
{
A
}
(
Φ
:
A
→
uPred
M
)
:
(
∃
a
,
◇
Φ
a
)
⊢
◇
∃
a
,
Φ
a
.
Proof
.
apply
exist_elim
=>
a
.
by
rewrite
(
exist_intro
a
).
Qed
.
Lemma
except_
last
_later
P
:
◇
▷
P
⊢
▷
P
.
Proof
.
by
rewrite
/
uPred_except_
last
-
later_or
False_or
.
Qed
.
Lemma
except_
last
_always
P
:
◇
□
P
⊣
⊢
□
◇
P
.
Proof
.
by
rewrite
/
uPred_except_
last
always_or
always_later
always_pure
.
Qed
.
Lemma
except_
last
_always_if
p
P
:
◇
□
?p
P
⊣
⊢
□
?p
◇
P
.
Proof
.
destruct
p
;
simpl
;
auto
using
except_
last
_always
.
Qed
.
Lemma
except_
last
_frame_l
P
Q
:
P
★
◇
Q
⊢
◇
(
P
★
Q
).
Proof
.
by
rewrite
{
1
}(
except_
last
_intro
P
)
except_
last
_sep
.
Qed
.
Lemma
except_
last
_frame_r
P
Q
:
◇
P
★
Q
⊢
◇
(
P
★
Q
).
Proof
.
by
rewrite
{
1
}(
except_
last
_intro
Q
)
except_
last
_sep
.
Qed
.
Lemma
except_
0
_later
P
:
◇
▷
P
⊢
▷
P
.
Proof
.
by
rewrite
/
uPred_except_
0
-
later_or
False_or
.
Qed
.
Lemma
except_
0
_always
P
:
◇
□
P
⊣
⊢
□
◇
P
.
Proof
.
by
rewrite
/
uPred_except_
0
always_or
always_later
always_pure
.
Qed
.
Lemma
except_
0
_always_if
p
P
:
◇
□
?p
P
⊣
⊢
□
?p
◇
P
.
Proof
.
destruct
p
;
simpl
;
auto
using
except_
0
_always
.
Qed
.
Lemma
except_
0
_frame_l
P
Q
:
P
★
◇
Q
⊢
◇
(
P
★
Q
).
Proof
.
by
rewrite
{
1
}(
except_
0
_intro
P
)
except_
0
_sep
.
Qed
.
Lemma
except_
0
_frame_r
P
Q
:
◇
P
★
Q
⊢
◇
(
P
★
Q
).
Proof
.
by
rewrite
{
1
}(
except_
0
_intro
Q
)
except_
0
_sep
.
Qed
.
(* Own and valid derived *)
Lemma
always_ownM
(
a
:
M
)
:
Persistent
a
→
□
uPred_ownM
a
⊣
⊢
uPred_ownM
a
.
...
...
@@ -628,9 +628,9 @@ Proof.
intros
;
rewrite
(
bupd_ownM_updateP
_
(
y
=))
;
last
by
apply
cmra_update_updateP
.
by
apply
bupd_mono
,
exist_elim
=>
y'
;
apply
pure_elim_l
=>
->.
Qed
.
Lemma
except_
last
_bupd
P
:
◇
(|==>
P
)
⊢
(|==>
◇
P
).
Lemma
except_
0
_bupd
P
:
◇
(|==>
P
)
⊢
(|==>
◇
P
).
Proof
.
rewrite
/
uPred_except_
last
.
apply
or_elim
;
auto
using
bupd_mono
.
rewrite
/
uPred_except_
0
.
apply
or_elim
;
auto
using
bupd_mono
.
by
rewrite
-
bupd_intro
-
or_intro_l
.
Qed
.
...
...
@@ -643,25 +643,25 @@ Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
TimelessP
(
✓
a
:
uPred
M
)%
I
.
Proof
.
rewrite
/
TimelessP
!
discrete_valid
.
apply
(
timelessP
_
).
Qed
.
Global
Instance
and_timeless
P
Q
:
TimelessP
P
→
TimelessP
Q
→
TimelessP
(
P
∧
Q
).
Proof
.
intros
;
rewrite
/
TimelessP
except_
last
_and
later_and
;
auto
.
Qed
.
Proof
.
intros
;
rewrite
/
TimelessP
except_
0
_and
later_and
;
auto
.
Qed
.
Global
Instance
or_timeless
P
Q
:
TimelessP
P
→
TimelessP
Q
→
TimelessP
(
P
∨
Q
).
Proof
.
intros
;
rewrite
/
TimelessP
except_
last
_or
later_or
;
auto
.
Qed
.
Proof
.
intros
;
rewrite
/
TimelessP
except_
0
_or
later_or
;
auto
.
Qed
.
Global
Instance
impl_timeless
P
Q
:
TimelessP
Q
→
TimelessP
(
P
→
Q
).
Proof
.
rewrite
/
TimelessP
=>
HQ
.
rewrite
later_false_excluded_middle
.
apply
or_mono
,
impl_intro_l
;
first
done
.
rewrite
-{
2
}(
l
ö
b
Q
)
;
apply
impl_intro_l
.
rewrite
HQ
/
uPred_except_
last
!
and_or_r
.
apply
or_elim
;
last
auto
.
rewrite
HQ
/
uPred_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
:
TimelessP
P
→
TimelessP
Q
→
TimelessP
(
P
★
Q
).
Proof
.
intros
;
rewrite
/
TimelessP
except_
last
_sep
later_sep
;
auto
.
Qed
.
Proof
.
intros
;
rewrite
/
TimelessP
except_
0
_sep
later_sep
;
auto
.
Qed
.
Global
Instance
wand_timeless
P
Q
:
TimelessP
Q
→
TimelessP
(
P
-
★
Q
).
Proof
.
rewrite
/
TimelessP
=>
HQ
.
rewrite
later_false_excluded_middle
.
apply
or_mono
,
wand_intro_l
;
first
done
.
rewrite
-{
2
}(
l
ö
b
Q
)
;
apply
impl_intro_l
.
rewrite
HQ
/
uPred_except_
last
!
and_or_r
.
apply
or_elim
;
last
auto
.
rewrite
HQ
/
uPred_except_
0
!
and_or_r
.
apply
or_elim
;
last
auto
.
rewrite
-(
always_pure
)
-
always_later
always_and_sep_l'
.
by
rewrite
assoc
(
comm
_
_
P
)
-
assoc
-
always_and_sep_l'
impl_elim_r
wand_elim_r
.
Qed
.
...
...
@@ -671,18 +671,18 @@ Proof.
rewrite
/
TimelessP
=>
HQ
.
rewrite
later_false_excluded_middle
.
apply
or_mono
;
first
done
.
apply
forall_intro
=>
x
.
rewrite
-(
l
ö
b
(
Ψ
x
))
;
apply
impl_intro_l
.
rewrite
HQ
/
uPred_except_
last
!
and_or_r
.
apply
or_elim
;
last
auto
.
rewrite
HQ
/
uPred_except_
0
!
and_or_r
.
apply
or_elim
;
last
auto
.
by
rewrite
impl_elim_r
(
forall_elim
x
).
Qed
.
Global
Instance
exist_timeless
{
A
}
(
Ψ
:
A
→
uPred
M
)
:
(
∀
x
,
TimelessP
(
Ψ
x
))
→
TimelessP
(
∃
x
,
Ψ
x
).
Proof
.
rewrite
/
TimelessP
=>
?.
rewrite
later_exist_false
.
apply
or_elim
.
-
rewrite
/
uPred_except_
last
;
auto
.
-
rewrite
/
uPred_except_
0
;
auto
.
-
apply
exist_elim
=>
x
.
rewrite
-(
exist_intro
x
)
;
auto
.
Qed
.
Global
Instance
always_timeless
P
:
TimelessP
P
→
TimelessP
(
□
P
).
Proof
.
intros
;
rewrite
/
TimelessP
except_
last
_always
-
always_later
;
auto
.
Qed
.
Proof
.
intros
;
rewrite
/
TimelessP
except_
0
_always
-
always_later
;
auto
.
Qed
.
Global
Instance
always_if_timeless
p
P
:
TimelessP
P
→
TimelessP
(
□
?p
P
).
Proof
.
destruct
p
;
apply
_
.
Qed
.
Global
Instance
eq_timeless
{
A
:
cofeT
}
(
a
b
:
A
)
:
...
...
@@ -691,8 +691,8 @@ Proof. intros. rewrite /TimelessP !timeless_eq. apply (timelessP _). Qed.
Global
Instance
ownM_timeless
(
a
:
M
)
:
Timeless
a
→
TimelessP
(
uPred_ownM
a
).
Proof
.
intros
?.
rewrite
/
TimelessP
later_ownM
.
apply
exist_elim
=>
b
.
rewrite
(
timelessP
(
a
≡
b
))
(
except_
last
_intro
(
uPred_ownM
b
))
-
except_
last
_and
.
apply
except_
last
_mono
.
rewrite
eq_sym
.
rewrite
(
timelessP
(
a
≡
b
))
(
except_
0
_intro
(
uPred_ownM
b
))
-
except_
0
_and
.
apply
except_
0
_mono
.
rewrite
eq_sym
.
apply
(
eq_rewrite
b
a
(
uPred_ownM
))
;
first
apply
_;
auto
.
Qed
.
...
...
program_logic/fancy_updates.v
View file @
58bd4b02
...
...
@@ -52,11 +52,11 @@ Lemma fupd_intro_mask E1 E2 P : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P.
Proof
.
intros
(
E1''
&->&?)%
subseteq_disjoint_union_L
.
rewrite
fupd_eq
/
fupd_def
ownE_op
//.
iIntros
"H ($ & $ & HE) !==>"
.
iApply
except_
last
_intro
.
iIntros
"[$ $] !==>"
.
iApply
except_
last
_intro
.
iApply
except_
0
_intro
.
iIntros
"[$ $] !==>"
.
iApply
except_
0
_intro
.
by
iFrame
.
Qed
.
Lemma
except_
last
_fupd
E1
E2
P
:
◇
(|={
E1
,
E2
}=>
P
)
={
E1
,
E2
}=
★
P
.
Lemma
except_
0
_fupd
E1
E2
P
:
◇
(|={
E1
,
E2
}=>
P
)
={
E1
,
E2
}=
★
P
.
Proof
.
rewrite
fupd_eq
.
iIntros
"H [Hw HE]"
.
iTimeless
"H"
.
iApply
"H"
;
by
iFrame
.
Qed
.
...
...
@@ -64,7 +64,7 @@ Qed.
Lemma
bupd_fupd
E
P
:
(|==>
P
)
={
E
}=
★
P
.
Proof
.
rewrite
fupd_eq
/
fupd_def
.
iIntros
"H [$ $]"
;
iUpd
"H"
.
iUpdIntro
.
by
iApply
except_
last
_intro
.
iUpdIntro
.
by
iApply
except_
0
_intro
.
Qed
.
Lemma
fupd_mono
E1
E2
P
Q
:
(
P
⊢
Q
)
→
(|={
E1
,
E2
}=>
P
)
={
E1
,
E2
}=
★
Q
.
...
...
@@ -85,7 +85,7 @@ Proof.
intros
.
rewrite
fupd_eq
/
fupd_def
ownE_op
//.
iIntros
"Hvs (Hw & HE1 &HEf)"
.
iUpd
(
"Hvs"
with
"[Hw HE1]"
)
as
">($ & HE2 & HP)"
;
first
by
iFrame
.
iDestruct
(
ownE_op'
with
"[HE2 HEf]"
)
as
"[? $]"
;
first
by
iFrame
.
iUpdIntro
;
iApply
except_
last
_intro
.
by
iApply
"HP"
.
iUpdIntro
;
iApply
except_
0
_intro
.
by
iApply
"HP"
.
Qed
.
Lemma
fupd_frame_r
E1
E2
P
Q
:
(|={
E1
,
E2
}=>
P
)
★
Q
={
E1
,
E2
}=
★
P
★
Q
.
...
...
@@ -102,8 +102,8 @@ Lemma fupd_intro E P : P ={E}=★ P.
Proof
.
iIntros
"HP"
.
by
iApply
bupd_fupd
.
Qed
.
Lemma
fupd_intro_mask'
E1
E2
:
E2
⊆
E1
→
True
⊢
|={
E1
,
E2
}=>
|={
E2
,
E1
}=>
True
.
Proof
.
exact
:
fupd_intro_mask
.
Qed
.
Lemma
fupd_except_
last
E1
E2
P
:
(|={
E1
,
E2
}=>
◇
P
)
={
E1
,
E2
}=
★
P
.
Proof
.
by
rewrite
{
1
}(
fupd_intro
E2
P
)
except_
last
_fupd
fupd_trans
.
Qed
.
Lemma
fupd_except_
0
E1
E2
P
:
(|={
E1
,
E2
}=>
◇
P
)
={
E1
,
E2
}=
★
P
.
Proof
.
by
rewrite
{
1
}(
fupd_intro
E2
P
)
except_
0
_fupd
fupd_trans
.
Qed
.
Lemma
fupd_frame_l
E1
E2
P
Q
:
(
P
★
|={
E1
,
E2
}=>
Q
)
={
E1
,
E2
}=
★
P
★
Q
.
Proof
.
rewrite
!(
comm
_
P
)
;
apply
fupd_frame_r
.
Qed
.
...
...
@@ -180,8 +180,8 @@ Section proofmode_classes.
Frame
R
P
Q
→
Frame
R
(|={
E1
,
E2
}=>
P
)
(|={
E1
,
E2
}=>
Q
).
Proof
.
rewrite
/
Frame
=><-.
by
rewrite
fupd_frame_l
.
Qed
.
Global
Instance
is_except_
last
_fupd
E1
E2
P
:
IsExcept
Last
(|={
E1
,
E2
}=>
P
).
Proof
.
by
rewrite
/
IsExcept
Last
except_
last
_fupd
.
Qed
.
Global
Instance
is_except_
0
_fupd
E1
E2
P
:
IsExcept
0
(|={
E1
,
E2
}=>
P
).
Proof
.
by
rewrite
/
IsExcept
0
except_
0
_fupd
.
Qed
.
Global
Instance
from_upd_fupd
E
P
:
FromUpd
(|={
E
}=>
P
)
P
.
Proof
.
by
rewrite
/
FromUpd
-
bupd_fupd
.
Qed
.
...
...
program_logic/invariants.v
View file @
58bd4b02
...
...
@@ -39,7 +39,7 @@ Proof.
eapply
nclose_infinite
,
(
difference_finite_inv
_
_
),
Hfin
.
apply
of_gset_finite
.
-
by
iFrame
.
-
rewrite
/
uPred_except_
last
;
eauto
.
-
rewrite
/
uPred_except_
0
;
eauto
.
Qed
.
Lemma
inv_open
E
N
P
:
...
...
@@ -49,9 +49,9 @@ Proof.
iDestruct
"Hi"
as
%
?%
elem_of_subseteq_singleton
.
rewrite
{
1
4
}(
union_difference_L
(
nclose
N
)
E
)
//
ownE_op
;
last
set_solver
.
rewrite
{
1
5
}(
union_difference_L
{[
i
]}
(
nclose
N
))
//
ownE_op
;
last
set_solver
.
iIntros
"(Hw & [HE $] & $)"
;
iUpdIntro
;
iApply
except_
last
_intro
.
iIntros
"(Hw & [HE $] & $)"
;
iUpdIntro
;
iApply
except_
0
_intro
.
iDestruct
(
ownI_open
i
P
with
"[Hw HE]"
)
as
"($ & $ & HD)"
;
first
by
iFrame
.
iIntros
"HP [Hw $] !==>"
;
iApply
except_
last
_intro
.
iApply
ownI_close
;
by
iFrame
.
iIntros
"HP [Hw $] !==>"
;
iApply
except_
0
_intro
.
iApply
ownI_close
;
by
iFrame
.
Qed
.
Lemma
inv_open_timeless
E
N
P
`
{!
TimelessP
P
}
:
...
...
program_logic/weakestpre.v
View file @
58bd4b02
...
...
@@ -222,8 +222,8 @@ Section proofmode_classes.
(
∀
v
,
Frame
R
(
Φ
v
)
(
Ψ
v
))
→
Frame
R
(
WP
e
@
E
{{
Φ
}})
(
WP
e
@
E
{{
Ψ
}}).
Proof
.
rewrite
/
Frame
=>
HR
.
rewrite
wp_frame_l
.
apply
wp_mono
,
HR
.
Qed
.
Global
Instance
is_except_
last
_wp
E
e
Φ
:
IsExcept
Last
(
WP
e
@
E
{{
Φ
}}).
Proof
.
by
rewrite
/
IsExcept
Last
-{
2
}
fupd_wp
-
except_
last
_fupd
-
fupd_intro
.
Qed
.
Global
Instance
is_except_
0
_wp
E
e
Φ
:
IsExcept
0
(
WP
e
@
E
{{
Φ
}}).
Proof
.
by
rewrite
/
IsExcept
0
-{
2
}
fupd_wp
-
except_
0
_fupd
-
fupd_intro
.
Qed
.
Global
Instance
elim_upd_bupd_wp
E
e
P
Φ
:
ElimUpd
(|==>
P
)
P
(
WP
e
@
E
{{
Φ
}})
(
WP
e
@
E
{{
Φ
}}).
...
...
proofmode/class_instances.v
View file @
58bd4b02
...
...
@@ -298,17 +298,17 @@ Proof.
rewrite
/
Frame
/
MakeLater
/
IntoLater
=>->
<-
<-.
by
rewrite
later_sep
.
Qed
.
Class
MakeExcept
Last
(
P
Q
:
uPred
M
)
:
=
make_except_
last
:
◇
P
⊣
⊢
Q
.
Global
Instance
make_except_
last
_True
:
MakeExcept
Last
True
True
.
Proof
.
by
rewrite
/
MakeExcept
Last
except_
last
_True
.
Qed
.
Global
Instance
make_except_
last
_default
P
:
MakeExcept
Last
P
(
◇
P
)
|
100
.
Class
MakeExcept
0
(
P
Q
:
uPred
M
)
:
=
make_except_
0
:
◇
P
⊣
⊢
Q
.
Global
Instance
make_except_
0
_True
:
MakeExcept
0
True
True
.
Proof
.
by
rewrite
/
MakeExcept
0
except_
0
_True
.
Qed
.
Global
Instance
make_except_
0
_default
P
:
MakeExcept
0
P
(
◇
P
)
|
100
.
Proof
.
done
.
Qed
.
Global
Instance
frame_except_
last
R
P
Q
Q'
:
Frame
R
P
Q
→
MakeExcept
Last
Q
Q'
→
Frame
R
(
◇
P
)
Q'
.
Global
Instance
frame_except_
0
R
P
Q
Q'
:
Frame
R
P
Q
→
MakeExcept
0
Q
Q'
→
Frame
R
(
◇
P
)
Q'
.
Proof
.
rewrite
/
Frame
/
MakeExcept
Last
=><-
<-.
by
rewrite
except_
last
_sep
-(
except_
last
_intro
R
).
rewrite
/
Frame
/
MakeExcept
0
=><-
<-.
by
rewrite
except_
0
_sep
-(
except_
0
_intro
R
).
Qed
.
Global
Instance
frame_exist
{
A
}
R
(
Φ
Ψ
:
A
→
uPred
M
)
:
...
...
@@ -357,21 +357,21 @@ Global Instance into_exist_always {A} P (Φ : A → uPred M) :
IntoExist
P
Φ
→
IntoExist
(
□
P
)
(
λ
a
,
□
(
Φ
a
))%
I
.
Proof
.
rewrite
/
IntoExist
=>
HP
.
by
rewrite
HP
always_exist
.
Qed
.
(* IntoExcept
Last
*)
Global
Instance
into_except_
last
_except_
last
P
:
IntoExcept
Last
(
◇
P
)
P
.
(* IntoExcept
0
*)
Global
Instance
into_except_
0
_except_
0
P
:
IntoExcept
0
(
◇
P
)
P
.
Proof
.
done
.
Qed
.
Global
Instance
into_except_
last
_timeless
P
:
TimelessP
P
→
IntoExcept
Last
(
▷
P
)
P
.
Global
Instance
into_except_
0
_timeless
P
:
TimelessP
P
→
IntoExcept
0
(
▷
P
)
P
.
Proof
.
done
.
Qed
.
(* IsExcept
Last
*)
Global
Instance
is_except_
last
_except_
last
P
:
IsExcept
Last
(
◇
P
).
Proof
.
by
rewrite
/
IsExcept
Last
except_
last
_idemp
.
Qed
.
Global
Instance
is_except_
last
_later
P
:
IsExcept
Last
(
▷
P
).
Proof
.
by
rewrite
/
IsExcept
Last
except_
last
_later
.
Qed
.
Global
Instance
is_except_
last
_bupd
P
:
IsExcept
Last
P
→
IsExcept
Last
(|==>
P
).
(* IsExcept
0
*)
Global
Instance
is_except_
0
_except_
0
P
:
IsExcept
0
(
◇
P
).
Proof
.
by
rewrite
/
IsExcept
0
except_
0
_idemp
.
Qed
.
Global
Instance
is_except_
0
_later
P
:
IsExcept
0
(
▷
P
).
Proof
.
by
rewrite
/
IsExcept
0
except_
0
_later
.
Qed
.
Global
Instance
is_except_
0
_bupd
P
:
IsExcept
0
P
→
IsExcept
0
(|==>
P
).
Proof
.
rewrite
/
IsExcept
Last
=>
HP
.
by
rewrite
-{
2
}
HP
-(
except_
last
_idemp
P
)
-
except_
last
_bupd
-(
except_
last
_intro
P
).
rewrite
/
IsExcept
0
=>
HP
.
by
rewrite
-{
2
}
HP
-(
except_
0
_idemp
P
)
-
except_
0
_bupd
-(
except_
0
_intro
P
).
Qed
.
(* FromUpd *)
...
...
proofmode/classes.v
View file @
58bd4b02
...
...
@@ -62,11 +62,11 @@ Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
into_exist
:
P
⊢
∃
x
,
Φ
x
.
Global
Arguments
into_exist
{
_
}
_
_
{
_
}.
Class
IntoExcept
Last
(
P
Q
:
uPred
M
)
:
=
into_except_
last
:
P
⊢
◇
Q
.
Global
Arguments
into_except_
last
:
clear
implicits
.
Class
IntoExcept
0
(
P
Q
:
uPred
M
)
:
=
into_except_
0
:
P
⊢
◇
Q
.
Global
Arguments
into_except_
0
:
clear
implicits
.
Class
IsExcept
Last
(
Q
:
uPred
M
)
:
=
is_except_
last
:
◇
Q
⊢
Q
.
Global
Arguments
is_except_
last
:
clear
implicits
.
Class
IsExcept
0
(
Q
:
uPred
M
)
:
=
is_except_
0
:
◇
Q
⊢
Q
.
Global
Arguments
is_except_
0
:
clear
implicits
.
Class
FromUpd
(
P
Q
:
uPred
M
)
:
=
from_upd
:
(|==>
Q
)
⊢
P
.
Global
Arguments
from_upd
:
clear
implicits
.
...
...
proofmode/coq_tactics.v
View file @
58bd4b02
...
...
@@ -446,14 +446,14 @@ Proof.
Qed
.
Lemma
tac_timeless
Δ
Δ
'
i
p
P
P'
Q
:
IsExcept
Last
Q
→
envs_lookup
i
Δ
=
Some
(
p
,
P
)
→
IntoExcept
Last
P
P'
→
IsExcept
0
Q
→
envs_lookup
i
Δ
=
Some
(
p
,
P
)
→
IntoExcept
0
P
P'
→
envs_simple_replace
i
p
(
Esnoc
Enil
i
P'
)
Δ
=
Some
Δ
'
→
(
Δ
'
⊢
Q
)
→
Δ
⊢
Q
.
Proof
.
intros
????
HQ
.
rewrite
envs_simple_replace_sound
//
;
simpl
.
rewrite
right_id
HQ
-{
2
}(
is_except_
last
Q
).
by
rewrite
(
into_except_
last
P
)
-
except_
last
_always_if
except_
last
_frame_r
wand_elim_r
.
rewrite
right_id
HQ
-{
2
}(
is_except_
0
Q
).
by
rewrite
(
into_except_
0
P
)
-
except_
0
_always_if
except_
0
_frame_r
wand_elim_r
.
Qed
.
(** * Always *)
...
...
proofmode/tactics.v
View file @
58bd4b02
...
...
@@ -612,10 +612,10 @@ Tactic Notation "iNext":=
Tactic
Notation
"iTimeless"
constr
(
H
)
:
=
eapply
tac_timeless
with
_
H
_
_
_;
[
let
Q
:
=
match
goal
with
|-
IsExcept
Last
?Q
=>
Q
end
in
[
let
Q
:
=
match
goal
with
|-
IsExcept
0
?Q
=>
Q
end
in
apply
_
||
fail
"iTimeless: cannot remove later when goal is"
Q
|
env_cbv
;
reflexivity
||
fail
"iTimeless:"
H
"not found"
|
let
P
:
=
match
goal
with
|-
IntoExcept
Last
?P
_
=>
P
end
in
|
let
P
:
=
match
goal
with
|-
IntoExcept
0
?P
_
=>
P
end
in
apply
_
||
fail
"iTimeless: cannot turn"
P
"into ◇"
|
env_cbv
;
reflexivity
|].
...
...
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