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
George Pirlea
Iris
Commits
bce1a24c
Commit
bce1a24c
authored
Mar 01, 2018
by
Jacques-Henri Jourdan
Browse files
Turn some MaybeLaterN instances into LaterN instances.
parent
741641e3
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/class_instances.v
View file @
bce1a24c
...
...
@@ -1609,24 +1609,20 @@ Proof.
Qed
.
Global
Instance
into_later_affinely
n
P
Q
:
MaybeIntoLaterN
false
n
P
Q
→
MaybeIntoLaterN
false
n
(
bi_affinely
P
)
(
bi_affinely
Q
).
Proof
.
rewrite
/
MaybeIntoLaterN
=>
->.
by
rewrite
laterN_affinely_2
.
Qed
.
IntoLaterN
false
n
P
Q
→
IntoLaterN
false
n
(
bi_affinely
P
)
(
bi_affinely
Q
).
Proof
.
rewrite
/
IntoLaterN
/
MaybeIntoLaterN
=>
->.
by
rewrite
laterN_affinely_2
.
Qed
.
Global
Instance
into_later_absorbingly
n
P
Q
:
MaybeIntoLaterN
false
n
P
Q
→
MaybeIntoLaterN
false
n
(
bi_absorbingly
P
)
(
bi_absorbingly
Q
).
Proof
.
rewrite
/
MaybeIntoLaterN
=>
->.
by
rewrite
laterN_absorbingly
.
Qed
.
IntoLaterN
false
n
P
Q
→
IntoLaterN
false
n
(
bi_absorbingly
P
)
(
bi_absorbingly
Q
).
Proof
.
rewrite
/
IntoLaterN
/
MaybeIntoLaterN
=>
->.
by
rewrite
laterN_absorbingly
.
Qed
.
Global
Instance
into_later_plainly
n
P
Q
:
MaybeIntoLaterN
false
n
P
Q
→
MaybeIntoLaterN
false
n
(
bi_plainly
P
)
(
bi_plainly
Q
).
Proof
.
rewrite
/
MaybeIntoLaterN
=>
->.
by
rewrite
laterN_plainly
.
Qed
.
IntoLaterN
false
n
P
Q
→
IntoLaterN
false
n
(
bi_plainly
P
)
(
bi_plainly
Q
).
Proof
.
rewrite
/
IntoLaterN
/
MaybeIntoLaterN
=>
->.
by
rewrite
laterN_plainly
.
Qed
.
Global
Instance
into_later_persistently
n
P
Q
:
MaybeIntoLaterN
false
n
P
Q
→
MaybeIntoLaterN
false
n
(
bi_persistently
P
)
(
bi_persistently
Q
).
Proof
.
rewrite
/
MaybeIntoLaterN
=>
->.
by
rewrite
laterN_persistently
.
Qed
.
IntoLaterN
false
n
P
Q
→
IntoLaterN
false
n
(
bi_persistently
P
)
(
bi_persistently
Q
).
Proof
.
rewrite
/
IntoLaterN
/
MaybeIntoLaterN
=>
->.
by
rewrite
laterN_persistently
.
Qed
.
Global
Instance
into_later_embed
`
{
SbiEmbedding
PROP
PROP'
}
n
P
Q
:
Maybe
IntoLaterN
false
n
P
Q
→
Maybe
IntoLaterN
false
n
⎡
P
⎤
⎡
Q
⎤
.
Proof
.
rewrite
/
MaybeIntoLaterN
=>
->.
by
rewrite
sbi_embed_laterN
.
Qed
.
IntoLaterN
false
n
P
Q
→
IntoLaterN
false
n
⎡
P
⎤
⎡
Q
⎤
.
Proof
.
rewrite
/
IntoLaterN
/
MaybeIntoLaterN
=>
->.
by
rewrite
sbi_embed_laterN
.
Qed
.
Global
Instance
into_laterN_sep_l
n
P1
P2
Q1
Q2
:
IntoLaterN
false
n
P1
Q1
→
MaybeIntoLaterN
false
n
P2
Q2
→
...
...
theories/proofmode/monpred.v
View file @
bce1a24c
...
...
@@ -426,10 +426,10 @@ Global Instance into_except_0_monPred_at_bwd i P 𝓟 Q :
Proof
.
rewrite
/
IntoExcept0
/
MakeMonPredAt
=>
H
<-.
by
rewrite
H
monPred_at_except_0
.
Qed
.
Global
Instance
maybe_into_later_monPred_at
i
n
P
Q
𝓠
:
Maybe
IntoLaterN
false
n
P
Q
→
MakeMonPredAt
i
Q
𝓠
→
Maybe
IntoLaterN
false
n
(
P
i
)
𝓠
.
IntoLaterN
false
n
P
Q
→
MakeMonPredAt
i
Q
𝓠
→
IntoLaterN
false
n
(
P
i
)
𝓠
.
Proof
.
rewrite
/
MaybeIntoLaterN
/
MakeMonPredAt
=>
->
<-.
elim
n
=>//=
?
<-.
rewrite
/
IntoLaterN
/
MaybeIntoLaterN
/
MakeMonPredAt
=>
->
<-.
elim
n
=>//=
?
<-.
by
rewrite
monPred_at_later
.
Qed
.
Global
Instance
from_later_monPred_at
i
n
P
Q
𝓠
:
...
...
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