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
Jonas Kastberg
iris
Commits
a928919c
Commit
a928919c
authored
Feb 15, 2017
by
Ralf Jung
Browse files
Merge branch 'janno/into-pure-instances' into 'master'
Add IntoPure instances for ∗, ∧, and ∨. See merge request !49
parents
84d78426
d9cad5bf
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/class_instances.v
View file @
a928919c
...
...
@@ -55,6 +55,15 @@ Global Instance into_pure_forall {X : Type} (Φ : X → uPred M) φ :
Proof
.
rewrite
/
IntoPure
=>
Hx
.
rewrite
-
pure_forall_2
.
by
setoid_rewrite
Hx
.
Qed
.
Global
Instance
into_pure_pure_conj
(
φ
1
φ
2
:
uPred
M
)
P1
P2
:
IntoPure
φ
1
P1
->
IntoPure
φ
2
P2
->
IntoPure
(
φ
1
∧
φ
2
)
(
P1
∧
P2
).
Proof
.
rewrite
/
IntoPure
pure_and
.
by
intros
->
->.
Qed
.
Global
Instance
into_pure_pure_sep
(
φ
1
φ
2
:
uPred
M
)
P1
P2
:
IntoPure
φ
1
P1
->
IntoPure
φ
2
P2
->
IntoPure
(
φ
1
∗
φ
2
)
(
P1
∧
P2
).
Proof
.
rewrite
/
IntoPure
sep_and
pure_and
.
by
intros
->
->.
Qed
.
Global
Instance
into_pure_pure_disj
(
φ
1
φ
2
:
uPred
M
)
P1
P2
:
IntoPure
φ
1
P1
->
IntoPure
φ
2
P2
->
IntoPure
(
φ
1
∨
φ
2
)
(
P1
∨
P2
).
Proof
.
rewrite
/
IntoPure
pure_or
.
by
intros
->
->.
Qed
.
(* FromPure *)
Global
Instance
from_pure_pure
φ
:
@
FromPure
M
⌜φ⌝
φ
.
...
...
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