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
2523157b
Commit
2523157b
authored
Dec 11, 2015
by
Robbert Krebbers
Browse files
Iris namespaces.
parent
2420784d
Changes
1
Hide whitespace changes
Inline
Side-by-side
iris/namespace.v
0 → 100644
View file @
2523157b
Require
Export
prelude
.
countable
prelude
.
co_pset
.
Definition
namespace
:
=
list
positive
.
Definition
nnil
:
namespace
:
=
nil
.
Definition
ndot
`
{
Countable
A
}
(
I
:
namespace
)
(
x
:
A
)
:
namespace
:
=
encode
x
::
I
.
Definition
nclose
(
I
:
namespace
)
:
coPset
:
=
coPset_suffixes
(
encode
I
).
Instance
ndot_injective
`
{
Countable
A
}
:
Injective2
(=)
(=)
(=)
(@
ndot
A
_
_
).
Proof
.
by
intros
I1
x1
I2
x2
?
;
simplify_equality
.
Qed
.
Definition
nclose_nnil
:
nclose
nnil
=
coPset_all
.
Proof
.
by
apply
(
sig_eq_pi
_
).
Qed
.
Definition
nclose_subseteq
`
{
Countable
A
}
I
x
:
nclose
(
ndot
I
x
)
⊆
nclose
I
.
Proof
.
intros
p
;
unfold
nclose
;
rewrite
!
elem_coPset_suffixes
;
intros
[
q
->].
destruct
(
list_encode_suffix
I
(
ndot
I
x
))
as
[
q'
?]
;
[
by
exists
[
encode
x
]|].
by
exists
(
q
++
q'
)%
positive
;
rewrite
<-(
associative_L
_
)
;
f_equal
.
Qed
.
Definition
nclose_disjoint
`
{
Countable
A
}
I
(
x
y
:
A
)
:
x
≠
y
→
nclose
(
ndot
I
x
)
∩
nclose
(
ndot
I
y
)
=
∅
.
Proof
.
intros
Hxy
;
apply
elem_of_equiv_empty_L
;
intros
p
;
unfold
nclose
,
ndot
.
rewrite
elem_of_intersection
,
!
elem_coPset_suffixes
;
intros
[[
q
->]
[
q'
Hq
]].
apply
Hxy
,
(
injective
encode
),
(
injective
encode_nat
)
;
revert
Hq
.
rewrite
!(
list_encode_cons
(
encode
_
)).
rewrite
!(
associative_L
_
),
(
injective_iff
(++
_
)%
positive
)
;
simpl
.
generalize
(
encode_nat
(
encode
y
)).
induction
(
encode_nat
(
encode
x
))
;
intros
[|?]
?
;
f_equal'
;
naive_solver
.
Qed
.
\ No newline at end of file
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