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
Rodolphe Lepigre
Iris
Commits
f42a673b
Commit
f42a673b
authored
Aug 08, 2016
by
Jacques-Henri Jourdan
Browse files
Inhabited instance for any Empty instance.
parent
340afd90
Changes
3
Hide whitespace changes
Inline
Side-by-side
algebra/cmra.v
View file @
f42a673b
...
...
@@ -504,8 +504,6 @@ Section ucmra.
Context
{
A
:
ucmraT
}.
Implicit
Types
x
y
z
:
A
.
Global
Instance
ucmra_unit_inhabited
:
Inhabited
A
:
=
populate
∅
.
Lemma
ucmra_unit_validN
n
:
✓
{
n
}
(
∅
:
A
).
Proof
.
apply
cmra_valid_validN
,
ucmra_unit_valid
.
Qed
.
Lemma
ucmra_unit_leastN
n
x
:
∅
≼
{
n
}
x
.
...
...
prelude/base.v
View file @
f42a673b
...
...
@@ -567,6 +567,8 @@ intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
Class
Empty
A
:
=
empty
:
A
.
Notation
"∅"
:
=
empty
:
C_scope
.
Instance
empty_inhabited
`
(
Empty
A
)
:
Inhabited
A
:
=
populate
∅
.
Class
Top
A
:
=
top
:
A
.
Notation
"⊤"
:
=
top
:
C_scope
.
...
...
proofmode/weakestpre.v
View file @
f42a673b
...
...
@@ -30,7 +30,7 @@ Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
(* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)
Global
Instance
elim_vs_pvs_wp_atomic
E1
E2
e
P
Φ
:
atomic
e
→
ElimVs
(|={
E1
,
E2
}=>
P
)
P
ElimVs
(|={
E1
,
E2
}=>
P
)
P
(
WP
e
@
E1
{{
Φ
}})
(
WP
e
@
E2
{{
v
,
|={
E2
,
E1
}=>
Φ
v
}})%
I
|
100
.
Proof
.
intros
.
by
rewrite
/
ElimVs
pvs_frame_r
wand_elim_r
wp_atomic
.
Qed
.
End
weakestpre
.
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