Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
David Swasey
coq-stdpp
Commits
10c2f692
Commit
10c2f692
authored
Feb 07, 2017
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Also support Coq 8.5pl3.
parent
e1762d72
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
13 additions
and
6 deletions
+13
-6
Makefile
Makefile
+8
-0
README.md
README.md
+2
-2
_CoqProject
_CoqProject
+0
-1
theories/fin_maps.v
theories/fin_maps.v
+2
-2
theories/gmap.v
theories/gmap.v
+1
-1
No files found.
Makefile
View file @
10c2f692
...
...
@@ -3,6 +3,14 @@ ifeq ($(Y), 1)
YFLAG
=
-y
endif
# Determine Coq version
COQ_VERSION
=
$(
shell
coqc
--version
| egrep
-o
'version 8.[0-9]'
| egrep
-o
'8.[0-9]'
)
COQ_MAKEFILE_FLAGS
?=
ifeq
($(COQ_VERSION), 8.6)
COQ_MAKEFILE_FLAGS
+=
-arg
-w
-arg
-notation-overridden
,-redundant-canonical-projection,-several-object-files
endif
# Forward most targets to Coq makefile (with some trick to make this phony)
%
:
Makefile.coq phony
+@make
-f
Makefile.coq
$@
...
...
README.md
View file @
10c2f692
...
...
@@ -20,7 +20,7 @@ The key features of this library are as follows:
`set_solver`
for goals involving set operations.
-
It is entirely axiom free.
# History
#
# History
Coq-std++ has originally been developed by Robbert Krebbers as part of his
formalization of the C programming language in his PhD thesis, called
...
...
@@ -32,7 +32,7 @@ developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.
This version is known to compile with:
-
Coq 8.6
-
Coq
8.5pl3 and Coq
8.6
## Building Instructions
...
...
_CoqProject
View file @
10c2f692
-Q theories stdpp
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
theories/option.v
theories/fin_map_dom.v
theories/bset.v
...
...
theories/fin_maps.v
View file @
10c2f692
...
...
@@ -792,8 +792,8 @@ Section map_of_to_collection.
Proof
.
intros
Hinj
.
assert
(
∀
x'
,
(
i
,
x
)
∈
f
<$>
elements
Y
→
(
i
,
x'
)
∈
f
<$>
elements
Y
→
x
=
x'
).
{
intros
x'
.
intros
(
y
&
Hx
&
?
%
elem_of_
elements
)%
elem_of_list_fmap
.
intros
(
y'
&
Hx'
&?%
elem_of_elements
)%
elem_of_list_fmap
.
{
intros
x'
.
intros
(
y
&
Hx
&
Hy
)
%
elem_of_
list_fmap
(
y'
&
Hx'
&
Hy'
)%
elem_of_list_fmap
.
rewrite
elem_of_elements
in
Hy
,
Hy'
.
cut
(
y
=
y'
)
;
[
congruence
|].
apply
Hinj
;
auto
.
by
rewrite
<-
Hx
,
<-
Hx'
.
}
unfold
map_of_collection
;
rewrite
<-
elem_of_map_of_list'
by
done
.
rewrite
elem_of_list_fmap
.
setoid_rewrite
elem_of_elements
;
naive_solver
.
...
...
theories/gmap.v
View file @
10c2f692
...
...
@@ -130,7 +130,7 @@ Definition gmap_curry `{Countable K1, Countable K2} {A} :
map_fold
(
λ
i2
x
,
<[(
i1
,
i2
)
:
=
x
]>)
macc
m'
)
∅
.
Definition
gmap_uncurry
`
{
Countable
K1
,
Countable
K2
}
{
A
}
:
gmap
(
K1
*
K2
)
A
→
gmap
K1
(
gmap
K2
A
)
:
=
map_fold
(
λ
'
(
i1
,
i2
)
x
,
map_fold
(
λ
ii
x
,
let
'
(
i1
,
i2
)
:
=
ii
in
partial_alter
(
Some
∘
<[
i2
:
=
x
]>
∘
from_option
id
∅
)
i1
)
∅
.
Section
curry_uncurry
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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