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
545eea68
Commit
545eea68
authored
May 29, 2018
by
Robbert Krebbers
Browse files
Revert `IntoWand` part of
ec4ac846
, and associated change in
9b14f90a
.
parent
9b14f90a
Pipeline
#9064
passed with stage
in 23 minutes and 52 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/class_instances_bi.v
View file @
545eea68
...
...
@@ -395,15 +395,9 @@ 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
.
Global
Instance
into_wand_embed
`
{
BiEmbed
PROP
PROP'
}
p
q
(
PP
QQ
RR
:
PROP
)
(
P
:
PROP'
)
:
IntoWand
p
q
RR
PP
QQ
→
IntoEmbed
P
PP
→
IntoWand
p
q
⎡
RR
⎤
P
⎡
QQ
⎤
.
Proof
.
rewrite
/
IntoEmbed
/
IntoWand
!
embed_intuitionistically_if_2
=>
->
->.
apply
bi
.
wand_intro_l
.
by
rewrite
embed_intuitionistically_if_2
-
embed_sep
bi
.
wand_elim_r
.
Qed
.
Global
Instance
into_wand_embed
`
{
BiEmbed
PROP
PROP'
}
p
q
R
P
Q
:
IntoWand
p
q
R
P
Q
→
IntoWand
p
q
⎡
R
⎤
⎡
P
⎤
⎡
Q
⎤
.
Proof
.
by
rewrite
/
IntoWand
!
embed_intuitionistically_if_2
-
embed_wand
=>
->.
Qed
.
(* FromWand *)
Global
Instance
from_wand_wand
P1
P2
:
FromWand
(
P1
-
∗
P2
)
P1
P2
.
...
...
theories/proofmode/classes.v
View file @
545eea68
...
...
@@ -482,14 +482,12 @@ Proof. apply _. Qed.
(** The class [IntoEmbed P Q] is used to transform hypotheses while introducing
embeddings using [iModIntro].
Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤].
Also used backwards, i.e. Input [Q] and output [P]. *)
Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
Class
IntoEmbed
{
PROP
PROP'
:
bi
}
`
{
BiEmbed
PROP
PROP'
}
(
P
:
PROP'
)
(
Q
:
PROP
)
:
=
into_embed
:
P
⊢
⎡
Q
⎤
.
Arguments
IntoEmbed
{
_
_
_
}
_
%
I
_
%
I
.
Arguments
into_embed
{
_
_
_
}
_
%
I
_
%
I
{
_
}.
Hint
Mode
IntoEmbed
+
+
+
!
-
:
typeclass_instances
.
Hint
Mode
IntoEmbed
+
+
+
-
!
:
typeclass_instances
.
(* We use two type classes for [AsEmpValid], in order to avoid loops in
typeclass search. Indeed, the [as_emp_valid_embed] instance would try
...
...
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