Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
S
stdpp
Project overview
Project overview
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Simon Spies
stdpp
Commits
6bc8803a
Commit
6bc8803a
authored
Jul 22, 2019
by
Paulo Emílio de Vilhena
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add new lemmas for list, set, and map operations.
parent
f9830af6
Changes
4
Hide whitespace changes
Inline
Sidebyside
Showing
4 changed files
with
65 additions
and
6 deletions
+65
6
CHANGELOG.md
CHANGELOG.md
+3
2
theories/fin_maps.v
theories/fin_maps.v
+19
4
theories/gmap.v
theories/gmap.v
+7
0
theories/list.v
theories/list.v
+36
0
No files found.
CHANGELOG.md
View file @
6bc8803a
...
@@ 4,7 +4,8 @@ APIbreaking change is listed.
...
@@ 4,7 +4,8 @@ APIbreaking change is listed.
## std++ 1.2.1 (unreleased)
## std++ 1.2.1 (unreleased)
This release of std++ received contributions by Michael Sammler, Paolo
This release of std++ received contributions by Michael Sammler, Paolo
G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies, and Rodolphe Lepigre.
G. Giarrusso, Ralf Jung, Robbert Krebbers, Simon Spies, Rodolphe Lepigre and
Paulo Emílio de Vilhena.
Noteworthy additions and changes:
Noteworthy additions and changes:
...
@@ 12,7 +13,7 @@ Noteworthy additions and changes:
...
@@ 12,7 +13,7 @@ Noteworthy additions and changes:

Make
`solve_ndisj`
tactic more powerful.

Make
`solve_ndisj`
tactic more powerful.

Add typeclass
`Involutive`
.

Add typeclass
`Involutive`
.

Improved
`naive_solver`
performance in case the goal is trivially solvable.

Improved
`naive_solver`
performance in case the goal is trivially solvable.

A bunch of new lemmas for list operations.

A bunch of new lemmas for list
, set, and map
operations.

`lookup_imap`
renamed into
`map_lookup_imap`
.

`lookup_imap`
renamed into
`map_lookup_imap`
.
## std++ 1.2.0 (released 20190426)
## std++ 1.2.0 (released 20190426)
...
...
theories/fin_maps.v
View file @
6bc8803a
...
@@ 1114,13 +1114,18 @@ Section map_filter.
...
@@ 1114,13 +1114,18 @@ Section map_filter.
naive_solver
.
naive_solver
.
Qed
.
Qed
.
Lemma
map_filter_insert_not
m
i
x
:
Lemma
map_filter_insert_not'
m
i
x
:
(
∀
y
,
¬
P
(
i
,
y
))
→
filter
P
(<[
i
:
=
x
]>
m
)
=
filter
P
m
.
¬
P
(
i
,
x
)
→
(
∀
y
,
m
!!
i
=
Some
y
→
¬
P
(
i
,
y
))
→
filter
P
(<[
i
:
=
x
]>
m
)
=
filter
P
m
.
Proof
.
Proof
.
intros
HP
.
apply
map_filter_lookup_eq
.
intros
j
y
Hy
.
intros
H
x
H
P
.
apply
map_filter_lookup_eq
.
intros
j
y
Hy
.
by
rewrite
lookup_insert_ne
by
naive_solver
.
rewrite
lookup_insert_Some
.
naive_solver
.
Qed
.
Qed
.
Lemma
map_filter_insert_not
m
i
x
:
(
∀
y
,
¬
P
(
i
,
y
))
→
filter
P
(<[
i
:
=
x
]>
m
)
=
filter
P
m
.
Proof
.
intros
HP
.
by
apply
map_filter_insert_not'
.
Qed
.
Lemma
map_filter_delete
m
i
:
filter
P
(
delete
i
m
)
=
delete
i
(
filter
P
m
).
Lemma
map_filter_delete
m
i
:
filter
P
(
delete
i
m
)
=
delete
i
(
filter
P
m
).
Proof
.
Proof
.
apply
map_eq
.
intros
j
.
apply
option_eq
;
intros
y
.
apply
map_eq
.
intros
j
.
apply
option_eq
;
intros
y
.
...
@@ 1139,6 +1144,16 @@ Section map_filter.
...
@@ 1139,6 +1144,16 @@ Section map_filter.
Lemma
map_filter_empty
:
filter
P
(
∅
:
M
A
)
=
∅
.
Lemma
map_filter_empty
:
filter
P
(
∅
:
M
A
)
=
∅
.
Proof
.
apply
map_fold_empty
.
Qed
.
Proof
.
apply
map_fold_empty
.
Qed
.
Lemma
map_filter_alt
m
:
filter
P
m
=
list_to_map
(
filter
P
(
map_to_list
m
)).
Proof
.
apply
list_to_map_flip
.
induction
m
as
[
k
x
m
?
IH
]
using
map_ind
.
{
by
rewrite
map_to_list_empty
,
map_filter_empty
,
map_to_list_empty
.
}
rewrite
map_to_list_insert
,
filter_cons
by
done
.
destruct
(
decide
(
P
_
)).

rewrite
map_filter_insert
by
done
.
by
rewrite
map_to_list_insert
,
IH
by
(
rewrite
map_filter_lookup_None
;
auto
).

by
rewrite
map_filter_insert_not'
by
naive_solver
.
Qed
.
End
map_filter
.
End
map_filter
.
(** ** Properties of the [map_Forall] predicate *)
(** ** Properties of the [map_Forall] predicate *)
...
...
theories/gmap.v
View file @
6bc8803a
...
@@ 279,6 +279,13 @@ Section gset.
...
@@ 279,6 +279,13 @@ Section gset.

by
rewrite
option_guard_True
by
(
rewrite
elem_of_dom
;
eauto
).

by
rewrite
option_guard_True
by
(
rewrite
elem_of_dom
;
eauto
).

by
rewrite
option_guard_False
by
(
rewrite
not_elem_of_dom
;
eauto
).

by
rewrite
option_guard_False
by
(
rewrite
not_elem_of_dom
;
eauto
).
Qed
.
Qed
.
Lemma
dom_gset_to_gmap
{
A
}
(
X
:
gset
K
)
(
x
:
A
)
:
dom
_
(
gset_to_gmap
x
X
)
=
X
.
Proof
.
induction
X
as
[
y
X
not_in
IH
]
using
set_ind_L
.

rewrite
gset_to_gmap_empty
,
dom_empty_L
;
done
.

rewrite
gset_to_gmap_union_singleton
,
dom_insert_L
,
IH
;
done
.
Qed
.
End
gset
.
End
gset
.
Typeclasses
Opaque
gset
.
Typeclasses
Opaque
gset
.
theories/list.v
View file @
6bc8803a
...
@@ 668,6 +668,42 @@ Proof.
...
@@ 668,6 +668,42 @@ Proof.
revert
i
j
.
induction
k
;
intros
i
j
?
;
simpl
;
revert
i
j
.
induction
k
;
intros
i
j
?
;
simpl
;
rewrite
1
?list_insert_commute
by
lia
;
auto
with
f_equal
.
rewrite
1
?list_insert_commute
by
lia
;
auto
with
f_equal
.
Qed
.
Qed
.
Lemma
list_inserts_app_l
l1
l2
l3
i
:
list_inserts
i
(
l1
++
l2
)
l3
=
list_inserts
(
length
l1
+
i
)
l2
(
list_inserts
i
l1
l3
).
Proof
.
revert
l1
i
;
induction
l1
as
[
x
l1
IH
]
;
[
done
].
intro
i
.
simpl
.
rewrite
IH
,
Nat
.
add_succ_r
.
apply
list_insert_inserts_lt
.
lia
.
Qed
.
Lemma
list_inserts_app_r
l1
l2
l3
i
:
list_inserts
(
length
l2
+
i
)
l1
(
l2
++
l3
)
=
l2
++
list_inserts
i
l1
l3
.
Proof
.
revert
l1
i
;
induction
l1
as
[
x
l1
IH
]
;
[
done
].
intros
i
.
simpl
.
by
rewrite
plus_n_Sm
,
IH
,
insert_app_r
.
Qed
.
Lemma
list_inserts_nil
l1
i
:
list_inserts
i
l1
[]
=
[].
Proof
.
revert
i
;
induction
l1
as
[
x
l1
IH
]
;
[
done
].
intro
i
.
simpl
.
by
rewrite
IH
.
Qed
.
Lemma
list_inserts_cons
l1
l2
i
x
:
list_inserts
(
S
i
)
l1
(
x
::
l2
)
=
x
::
list_inserts
i
l1
l2
.
Proof
.
revert
i
;
induction
l1
as
[
y
l1
IH
]
;
[
done
].
intro
i
.
simpl
.
by
rewrite
IH
.
Qed
.
Lemma
list_inserts_0_r
l1
l2
l3
:
length
l1
=
length
l2
→
list_inserts
0
l1
(
l2
++
l3
)
=
l1
++
l3
.
Proof
.
revert
l2
.
induction
l1
as
[
x
l1
IH
]
;
intros
[
y
l2
]
?
;
simplify_eq
/=
;
[
done
].
rewrite
list_inserts_cons
.
simpl
.
by
rewrite
IH
.
Qed
.
Lemma
list_inserts_0_l
l1
l2
l3
:
length
l1
=
length
l3
→
list_inserts
0
(
l1
++
l2
)
l3
=
l1
.
Proof
.
revert
l3
.
induction
l1
as
[
x
l1
IH
]
;
intros
[
z
l3
]
?
;
simplify_eq
/=.
{
by
rewrite
list_inserts_nil
.
}
rewrite
list_inserts_cons
.
simpl
.
by
rewrite
IH
.
Qed
.
(** ** Properties of the [elem_of] predicate *)
(** ** Properties of the [elem_of] predicate *)
Lemma
not_elem_of_nil
x
:
x
∉
[].
Lemma
not_elem_of_nil
x
:
x
∉
[].
...
...
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