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
Simon Spies
Iris
Commits
04f40730
Commit
04f40730
authored
Nov 17, 2015
by
Robbert Krebbers
Browse files
Sets over A as A -> bool.
parent
2c547961
Changes
2
Hide whitespace changes
Inline
Side-by-side
prelude/bsets.v
0 → 100644
View file @
04f40730
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This file implements bsets as functions into Prop. *)
Require
Export
prelude
.
prelude
.
Record
bset
(
A
:
Type
)
:
Type
:
=
mkBSet
{
bset_car
:
A
→
bool
}.
Arguments
mkBSet
{
_
}
_
.
Arguments
bset_car
{
_
}
_
_
.
Definition
bset_all
{
A
}
:
bset
A
:
=
mkBSet
(
λ
_
,
true
).
Instance
bset_empty
{
A
}
:
Empty
(
bset
A
)
:
=
mkBSet
(
λ
_
,
false
).
Instance
bset_singleton
{
A
}
`
{
∀
x
y
:
A
,
Decision
(
x
=
y
)}
:
Singleton
A
(
bset
A
)
:
=
λ
x
,
mkBSet
(
λ
y
,
bool_decide
(
y
=
x
)).
Instance
bset_elem_of
{
A
}
:
ElemOf
A
(
bset
A
)
:
=
λ
x
X
,
bset_car
X
x
.
Instance
bset_union
{
A
}
:
Union
(
bset
A
)
:
=
λ
X1
X2
,
mkBSet
(
λ
x
,
bset_car
X1
x
||
bset_car
X2
x
).
Instance
bset_intersection
{
A
}
:
Intersection
(
bset
A
)
:
=
λ
X1
X2
,
mkBSet
(
λ
x
,
bset_car
X1
x
&&
bset_car
X2
x
).
Instance
bset_difference
{
A
}
:
Difference
(
bset
A
)
:
=
λ
X1
X2
,
mkBSet
(
λ
x
,
bset_car
X1
x
&&
negb
(
bset_car
X2
x
)).
Instance
bset_collection
{
A
}
`
{
∀
x
y
:
A
,
Decision
(
x
=
y
)}
:
Collection
A
(
bset
A
).
Proof
.
split
;
[
split
|
|].
*
by
intros
x
?.
*
by
intros
x
y
;
rewrite
<-(
bool_decide_spec
(
x
=
y
)).
*
split
.
apply
orb_prop_elim
.
apply
orb_prop_intro
.
*
split
.
apply
andb_prop_elim
.
apply
andb_prop_intro
.
*
intros
X
Y
x
;
unfold
elem_of
,
bset_elem_of
;
simpl
.
destruct
(
bset_car
X
x
),
(
bset_car
Y
x
)
;
simpl
;
tauto
.
Qed
.
Instance
bset_elem_of_dec
{
A
}
x
(
X
:
bset
A
)
:
Decision
(
x
∈
X
)
:
=
_
.
Typeclasses
Opaque
bset_elem_of
.
Global
Opaque
bset_empty
bset_singleton
bset_union
bset_intersection
bset_difference
.
prelude/collections.v
View file @
04f40730
...
...
@@ -313,7 +313,7 @@ Section collection.
End
leibniz
.
Section
dec
.
Context
`
{
∀
X
Y
:
C
,
Decision
(
X
⊆
Y
)}.
Context
`
{
∀
(
x
:
A
)
(
X
:
C
)
,
Decision
(
x
∈
X
)}.
Lemma
not_elem_of_intersection
x
X
Y
:
x
∉
X
∩
Y
↔
x
∉
X
∨
x
∉
Y
.
Proof
.
rewrite
elem_of_intersection
.
destruct
(
decide
(
x
∈
X
))
;
tauto
.
Qed
.
Lemma
not_elem_of_difference
x
X
Y
:
x
∉
X
∖
Y
↔
x
∉
X
∨
x
∈
Y
.
...
...
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