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
Tej Chajed
stdpp
Commits
089f7cd8
Commit
089f7cd8
authored
Feb 27, 2016
by
Robbert Krebbers
Browse files
Hint Resolve for X ⊆ ⊤.
parent
7a965dfc
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/co_pset.v
View file @
089f7cd8
...
...
@@ -179,6 +179,9 @@ Proof.
apply
(
sig_eq_pi
_
),
coPset_eq
;
try
apply
proj2_sig
.
intros
p
;
apply
eq_bool_prop_intro
,
(
HXY
p
).
Qed
.
Lemma
coPset_top_subseteq
(
X
:
coPset
)
:
X
⊆
⊤
.
Proof
.
done
.
Qed
.
Hint
Resolve
coPset_top_subseteq
.
(** * Finite sets *)
Fixpoint
coPset_finite
(
t
:
coPset_raw
)
:
bool
:
=
...
...
theories/sets.v
View file @
089f7cd8
...
...
@@ -12,7 +12,7 @@ Notation "{[ x | P ]}" := (mkSet (λ x, P))
Instance
set_elem_of
{
A
}
:
ElemOf
A
(
set
A
)
:
=
λ
x
X
,
set_car
X
x
.
Instance
set_
all
{
A
}
:
Top
(
set
A
)
:
=
{[
_
|
True
]}.
Instance
set_
top
{
A
}
:
Top
(
set
A
)
:
=
{[
_
|
True
]}.
Instance
set_empty
{
A
}
:
Empty
(
set
A
)
:
=
{[
_
|
False
]}.
Instance
set_singleton
{
A
}
:
Singleton
A
(
set
A
)
:
=
λ
y
,
{[
x
|
y
=
x
]}.
Instance
set_union
{
A
}
:
Union
(
set
A
)
:
=
λ
X1
X2
,
{[
x
|
x
∈
X1
∨
x
∈
X2
]}.
...
...
@@ -23,12 +23,15 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
Instance
set_collection
:
Collection
A
(
set
A
).
Proof
.
split
;
[
split
|
|]
;
by
repeat
intro
.
Qed
.
Lemma
elem_of_
all
{
A
}
(
x
:
A
)
:
x
∈
⊤
↔
True
.
Lemma
elem_of_
top
{
A
}
(
x
:
A
)
:
x
∈
⊤
↔
True
.
Proof
.
done
.
Qed
.
Lemma
elem_of_mkSet
{
A
}
(
P
:
A
→
Prop
)
x
:
x
∈
{[
x
|
P
x
]}
↔
P
x
.
Proof
.
done
.
Qed
.
Lemma
not_elem_of_mkSet
{
A
}
(
P
:
A
→
Prop
)
x
:
x
∉
{[
x
|
P
x
]}
↔
¬
P
x
.
Proof
.
done
.
Qed
.
Lemma
top_subseteq
{
A
}
(
X
:
set
A
)
:
X
⊆
⊤
.
Proof
.
done
.
Qed
.
Hint
Resolve
top_subseteq
.
Instance
set_ret
:
MRet
set
:
=
λ
A
(
x
:
A
),
{[
x
]}.
Instance
set_bind
:
MBind
set
:
=
λ
A
B
(
f
:
A
→
set
B
)
(
X
:
set
A
),
...
...
@@ -46,6 +49,6 @@ Instance set_unfold_mkSet {A} (P : A → Prop) x Q :
SetUnfoldSimpl
(
P
x
)
Q
→
SetUnfold
(
x
∈
mkSet
P
)
Q
.
Proof
.
intros
HPQ
.
constructor
.
apply
HPQ
.
Qed
.
Global
Opaque
set_elem_of
set_
all
set_empty
set_singleton
.
Global
Opaque
set_elem_of
set_
top
set_empty
set_singleton
.
Global
Opaque
set_union
set_intersection
set_difference
.
Global
Opaque
set_ret
set_bind
set_fmap
set_join
.
\ 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