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
Iris
Iris
Commits
3a49be22
Commit
3a49be22
authored
Jan 04, 2016
by
Ralf Jung
Browse files
make it compile with Coq 8.5-rc1
parent
bb095111
Changes
1
Hide whitespace changes
Inline
Side-by-side
prelude/collections.v
View file @
3a49be22
...
...
@@ -599,7 +599,7 @@ Section finite.
Lemma
empty_finite
:
set_finite
∅
.
Proof
.
by
exists
[]
;
intros
?
;
rewrite
elem_of_empty
.
Qed
.
Lemma
singleton_finite
(
x
:
A
)
:
set_finite
{[
x
]}.
Proof
.
exists
[
x
]
;
intros
y
->
/
elem_of_singleton
;
left
.
Qed
.
Proof
.
exists
[
x
]
;
intros
y
->
%
elem_of_singleton
;
left
.
Qed
.
Lemma
union_finite
X
Y
:
set_finite
X
→
set_finite
Y
→
set_finite
(
X
∪
Y
).
Proof
.
intros
[
lX
?]
[
lY
?]
;
exists
(
lX
++
lY
)
;
intros
x
.
...
...
@@ -614,9 +614,9 @@ End finite.
Section
more_finite
.
Context
`
{
Collection
A
B
}.
Lemma
intersection_finite_l
X
Y
:
set_finite
X
→
set_finite
(
X
∩
Y
).
Proof
.
intros
[
l
?]
;
exists
l
;
intros
x
[??]
/
elem_of_intersection
;
auto
.
Qed
.
Proof
.
intros
[
l
?]
;
exists
l
;
intros
x
[??]
%
elem_of_intersection
;
auto
.
Qed
.
Lemma
intersection_finite_r
X
Y
:
set_finite
Y
→
set_finite
(
X
∩
Y
).
Proof
.
intros
[
l
?]
;
exists
l
;
intros
x
[??]
/
elem_of_intersection
;
auto
.
Qed
.
Proof
.
intros
[
l
?]
;
exists
l
;
intros
x
[??]
%
elem_of_intersection
;
auto
.
Qed
.
Lemma
difference_finite
X
Y
:
set_finite
X
→
set_finite
(
X
∖
Y
).
Proof
.
intros
[
l
?]
;
exists
l
;
intros
x
[??]
/
elem_of_difference
;
auto
.
Qed
.
Proof
.
intros
[
l
?]
;
exists
l
;
intros
x
[??]
%
elem_of_difference
;
auto
.
Qed
.
End
more_finite
.
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