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
d1fa8150
Commit
d1fa8150
authored
Jul 22, 2016
by
Robbert Krebbers
Browse files
Remove unused set_NoDup stuff.
parent
5b60a7fb
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/collections.v
View file @
d1fa8150
...
...
@@ -458,54 +458,6 @@ Section collection.
End
dec
.
End
collection
.
(** * Sets without duplicates up to an equivalence *)
Section
NoDup
.
Context
`
{
SimpleCollection
A
B
}
(
R
:
relation
A
)
`
{!
Equivalence
R
}.
Definition
elem_of_upto
(
x
:
A
)
(
X
:
B
)
:
=
∃
y
,
y
∈
X
∧
R
x
y
.
Definition
set_NoDup
(
X
:
B
)
:
=
∀
x
y
,
x
∈
X
→
y
∈
X
→
R
x
y
→
x
=
y
.
Global
Instance
:
Proper
((
≡
)
==>
iff
)
(
elem_of_upto
x
).
Proof
.
intros
???
E
.
unfold
elem_of_upto
.
by
setoid_rewrite
E
.
Qed
.
Global
Instance
:
Proper
(
R
==>
(
≡
)
==>
iff
)
elem_of_upto
.
Proof
.
intros
??
E1
??
E2
.
split
;
intros
[
z
[??]]
;
exists
z
.
-
rewrite
<-
E1
,
<-
E2
;
intuition
.
-
rewrite
E1
,
E2
;
intuition
.
Qed
.
Global
Instance
:
Proper
((
≡
)
==>
iff
)
set_NoDup
.
Proof
.
firstorder
.
Qed
.
Lemma
elem_of_upto_elem_of
x
X
:
x
∈
X
→
elem_of_upto
x
X
.
Proof
.
unfold
elem_of_upto
.
set_solver
.
Qed
.
Lemma
elem_of_upto_empty
x
:
¬
elem_of_upto
x
∅
.
Proof
.
unfold
elem_of_upto
.
set_solver
.
Qed
.
Lemma
elem_of_upto_singleton
x
y
:
elem_of_upto
x
{[
y
]}
↔
R
x
y
.
Proof
.
unfold
elem_of_upto
.
set_solver
.
Qed
.
Lemma
elem_of_upto_union
X
Y
x
:
elem_of_upto
x
(
X
∪
Y
)
↔
elem_of_upto
x
X
∨
elem_of_upto
x
Y
.
Proof
.
unfold
elem_of_upto
.
set_solver
.
Qed
.
Lemma
not_elem_of_upto
x
X
:
¬
elem_of_upto
x
X
→
∀
y
,
y
∈
X
→
¬
R
x
y
.
Proof
.
unfold
elem_of_upto
.
set_solver
.
Qed
.
Lemma
set_NoDup_empty
:
set_NoDup
∅
.
Proof
.
unfold
set_NoDup
.
set_solver
.
Qed
.
Lemma
set_NoDup_add
x
X
:
¬
elem_of_upto
x
X
→
set_NoDup
X
→
set_NoDup
({[
x
]}
∪
X
).
Proof
.
unfold
set_NoDup
,
elem_of_upto
.
set_solver
.
Qed
.
Lemma
set_NoDup_inv_add
x
X
:
x
∉
X
→
set_NoDup
({[
x
]}
∪
X
)
→
¬
elem_of_upto
x
X
.
Proof
.
intros
Hin
Hnodup
[
y
[??]].
rewrite
(
Hnodup
x
y
)
in
Hin
;
set_solver
.
Qed
.
Lemma
set_NoDup_inv_union_l
X
Y
:
set_NoDup
(
X
∪
Y
)
→
set_NoDup
X
.
Proof
.
unfold
set_NoDup
.
set_solver
.
Qed
.
Lemma
set_NoDup_inv_union_r
X
Y
:
set_NoDup
(
X
∪
Y
)
→
set_NoDup
Y
.
Proof
.
unfold
set_NoDup
.
set_solver
.
Qed
.
End
NoDup
.
(** * Quantifiers *)
Section
quantifiers
.
Context
`
{
SimpleCollection
A
B
}
(
P
:
A
→
Prop
).
...
...
theories/fin_collections.v
View file @
d1fa8150
...
...
@@ -185,6 +185,4 @@ Proof.
abstract
(
unfold
set_Exists
;
setoid_rewrite
<-
elem_of_elements
;
by
rewrite
<-
Exists_exists
).
Defined
.
Global
Instance
rel_elem_of_dec
`
{
∀
x
y
,
Decision
(
R
x
y
)}
x
X
:
Decision
(
elem_of_upto
R
x
X
)
|
100
:
=
decide
(
set_Exists
(
R
x
)
X
).
End
fin_collection
.
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