Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Dan Frumin
iris-coq
Commits
0d6031e4
Commit
0d6031e4
authored
Dec 30, 2017
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Rename `timelessP` into `timelessP`.
This was an oversight in !63.
parent
88e93595
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
6 additions
and
6 deletions
+6
-6
theories/base_logic/derived.v
theories/base_logic/derived.v
+5
-5
theories/proofmode/class_instances.v
theories/proofmode/class_instances.v
+1
-1
No files found.
theories/base_logic/derived.v
View file @
0d6031e4
...
...
@@ -29,8 +29,8 @@ Notation "◇ P" := (uPred_except_0 P)
Instance:
Params
(
@
uPred_except_0
)
1.
Typeclasses
Opaque
uPred_except_0
.
Class
Timeless
{
M
}
(
P
:
uPred
M
)
:=
timeless
P
:
▷
P
⊢
◇
P
.
Arguments
timeless
P
{
_
}
_
{
_
}
.
Class
Timeless
{
M
}
(
P
:
uPred
M
)
:=
timeless
:
▷
P
⊢
◇
P
.
Arguments
timeless
{
_
}
_
{
_
}
.
Hint
Mode
Timeless
+
!
:
typeclass_instances
.
Instance:
Params
(
@
Timeless
)
1.
...
...
@@ -908,7 +908,7 @@ Proof.
Qed
.
Global
Instance
valid_timeless
{
A
:
cmraT
}
`
{
CmraDiscrete
A
}
(
a
:
A
)
:
Timeless
(
✓
a
:
uPred
M
)
%
I
.
Proof
.
rewrite
/
Timeless
!
discrete_valid
.
apply
(
timeless
P
_
).
Qed
.
Proof
.
rewrite
/
Timeless
!
discrete_valid
.
apply
(
timeless
_
).
Qed
.
Global
Instance
and_timeless
P
Q
:
Timeless
P
→
Timeless
Q
→
Timeless
(
P
∧
Q
).
Proof
.
intros
;
rewrite
/
Timeless
except_0_and
later_and
;
auto
.
Qed
.
Global
Instance
or_timeless
P
Q
:
Timeless
P
→
Timeless
Q
→
Timeless
(
P
∨
Q
).
...
...
@@ -951,11 +951,11 @@ Global Instance persistently_if_timeless p P : Timeless P → Timeless (□?p P)
Proof
.
destruct
p
;
apply
_.
Qed
.
Global
Instance
eq_timeless
{
A
:
ofeT
}
(
a
b
:
A
)
:
Discrete
a
→
Timeless
(
a
≡
b
:
uPred
M
)
%
I
.
Proof
.
intros
.
rewrite
/
Timeless
!
discrete_eq
.
apply
(
timeless
P
_
).
Qed
.
Proof
.
intros
.
rewrite
/
Timeless
!
discrete_eq
.
apply
(
timeless
_
).
Qed
.
Global
Instance
ownM_timeless
(
a
:
M
)
:
Discrete
a
→
Timeless
(
uPred_ownM
a
).
Proof
.
intros
?
.
rewrite
/
Timeless
later_ownM
.
apply
exist_elim
=>
b
.
rewrite
(
timeless
P
(
a
≡
b
))
(
except_0_intro
(
uPred_ownM
b
))
-
except_0_and
.
rewrite
(
timeless
(
a
≡
b
))
(
except_0_intro
(
uPred_ownM
b
))
-
except_0_and
.
apply
except_0_mono
.
rewrite
internal_eq_sym
.
apply
impl_elim_r
'
.
apply:
internal_eq_rewrite
.
Qed
.
...
...
theories/proofmode/class_instances.v
View file @
0d6031e4
...
...
@@ -871,7 +871,7 @@ Qed.
Global
Instance
elim_modal_timeless_bupd
P
Q
:
Timeless
P
→
IsExcept0
Q
→
ElimModal
(
▷
P
)
P
Q
Q
.
Proof
.
intros
.
rewrite
/
ElimModal
(
except_0_intro
(
_
-
∗
_
))
(
timeless
P
P
).
intros
.
rewrite
/
ElimModal
(
except_0_intro
(
_
-
∗
_
))
(
timeless
P
).
by
rewrite
-
except_0_sep
wand_elim_r
.
Qed
.
Global
Instance
elim_modal_timeless_bupd
'
p
P
Q
:
...
...
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