Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
71cd889a
Commit
71cd889a
authored
Oct 25, 2018
by
Robbert Krebbers
Browse files
Allow introduction of `∀` under `|={E1,E2}=>` in case the predicate is plain.
parent
84cd1f63
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/class_instances_sbi.v
View file @
71cd889a
...
...
@@ -321,6 +321,24 @@ Global Instance from_forall_plainly `{BiPlainly PROP} {A} P (Φ : A → PROP) :
FromForall
P
Φ
→
FromForall
(
■
P
)%
I
(
λ
a
,
■
(
Φ
a
))%
I
.
Proof
.
rewrite
/
FromForall
=>
<-.
by
rewrite
plainly_forall
.
Qed
.
Global
Instance
from_forall_fupd
`
{
BiFUpdPlainly
PROP
}
E1
E2
{
A
}
P
(
Φ
:
A
→
PROP
)
:
(* Some cases in which [E2 ⊆ E1] holds *)
TCOr
(
TCEq
E1
E2
)
(
TCOr
(
TCEq
E1
⊤
)
(
TCEq
E2
∅
))
→
FromForall
P
Φ
→
(
∀
x
,
Plain
(
Φ
x
))
→
FromForall
(|={
E1
,
E2
}=>
P
)%
I
(
λ
a
,
|={
E1
,
E2
}=>
(
Φ
a
))%
I
.
Proof
.
rewrite
/
FromForall
=>
-[->|[->|->]]
<-
?
;
rewrite
fupd_plain_forall
;
set_solver
.
Qed
.
Global
Instance
from_forall_step_fupd
`
{
BiFUpdPlainly
PROP
}
E1
E2
{
A
}
P
(
Φ
:
A
→
PROP
)
:
(* Some cases in which [E2 ⊆ E1] holds *)
TCOr
(
TCEq
E1
E2
)
(
TCOr
(
TCEq
E1
⊤
)
(
TCEq
E2
∅
))
→
FromForall
P
Φ
→
(
∀
x
,
Plain
(
Φ
x
))
→
FromForall
(|={
E1
,
E2
}
▷
=>
P
)%
I
(
λ
a
,
|={
E1
,
E2
}
▷
=>
(
Φ
a
))%
I
.
Proof
.
rewrite
/
FromForall
=>
-[->|[->|->]]
<-
?
;
rewrite
step_fupd_plain_forall
;
set_solver
.
Qed
.
(** IsExcept0 *)
Global
Instance
is_except_0_except_0
P
:
IsExcept0
(
◇
P
).
Proof
.
by
rewrite
/
IsExcept0
except_0_idemp
.
Qed
.
...
...
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