Acknowledgements
This material is taken verbatim from Software Foundations V4.0
Copyright (c) 2016
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
Assumed Knowledge:
* Inductively defined propositions in Coq
Learning Outcomes:
* TODO
Grab the Coq source file
Maps.v
Maps (or dictionaries) are ubiquitous data structures, both in
software construction generally and in the theory of programming
languages in particular; we're going to need them in many places
in the coming chapters. They also make a nice case study using
ideas we've seen in previous chapters, including building data
structures out of higher-order functions (from
Basics and
Poly) and the use of reflection to streamline proofs (from
IndProp).
We'll define two flavors of maps:
total maps, which include a
"default" element to be returned when a key being looked up
doesn't exist, and
partial maps, which return an
option to
indicate success or failure. The latter is defined in terms of
the former, using
None as the default element.
The Coq Standard Library
One small digression before we start.
Unlike the chapters we have seen so far, this one does not
Require Import the chapter before it (and, transitively, all the
earlier chapters). Instead, in this chapter and from now, on
we're going to import the definitions and theorems we need
directly from Coq's standard library stuff. You should not notice
much difference, though, because we've been careful to name our
own definitions and theorems the same as their counterparts in the
standard library, wherever they overlap.
Documentation for the standard library can be found at
http://coq.inria.fr/library/.
The
SearchAbout command is a good way to look for theorems
involving objects of specific types.
Identifiers
First, we need a type for the keys that we use to index into our
maps. For this purpose, we again use the type
id from the
Lists chapter. To make this chapter self contained, we repeat
its definition here, together with the equality comparison
function for
ids and its fundamental property.
The following useful property of beq_id follows from an
analogous lemma about numbers:
Similarly:
This useful variant follows just by rewriting:
Total Maps
Our main job in this chapter will be to build a definition of
partial maps that is similar in behavior to the one we saw in the
Lists chapter, plus accompanying lemmas about their behavior.
This time around, though, we're going to use
functions, rather
than lists of key-value pairs, to build maps. The advantage of
this representation is that it offers a more
extensional view of
maps, where two maps that respond to queries in the same way will
be represented as literally the same thing (the same function),
rather than just "equivalent" data structures. This, in turn,
simplifies proofs that use maps.
We build partial maps in two steps. First, we define a type of
total maps that return a default value when we look up a key
that is not present in the map.
Intuitively, a total map over an element type
A is just a
function that can be used to look up
ids, yielding
As.
The function
t_empty yields an empty total map, given a default
element; this map always returns the default element when applied
to any id.
More interesting is the update function, which (as before) takes
a map m, a key x, and a value v and returns a new map that
takes x to v and takes every other key to whatever m does.
This definition is a nice example of higher-order programming.
The
t_update function takes a
function m and yields a new
function
fun x' ⇒ ... that behaves like the desired map.
For example, we can build a map taking
ids to
bools, where
Id
3 is mapped to
true and every other key is mapped to
false,
like this:
This completes the definition of total maps. Note that we don't
need to define a find operation because it is just function
application!
To use maps in later chapters, we'll need several fundamental
facts about how they behave. Even if you don't work the following
exercises, make sure you thoroughly understand the statements of
the lemmas! (Some of the proofs require the functional
extensionality axiom, which is discussed in the
Logic
chapter and included in the Coq standard library.)
Exercise: 1 star, optional (t_apply_empty)
First, the empty map returns its default element for all keys:
☐
Exercise: 2 stars, optional (t_update_eq)
Next, if we update a map
m at a key
x with a new value
v
and then look up
x in the map resulting from the
update, we
get back
v:
☐
Exercise: 2 stars, optional (t_update_neq)
On the other hand, if we update a map
m at a key
x1 and then
look up a
different key
x2 in the resulting map, we get the
same result that
m would have given:
☐
Exercise: 2 stars, optional (t_update_shadow)
If we update a map
m at a key
x with a value
v1 and then
update again with the same key
x and another value
v2, the
resulting map behaves the same (gives the same result when applied
to any key) as the simpler map obtained by performing just
the second
update on
m:
☐
For the final two lemmas about total maps, it's convenient to use
the reflection idioms introduced in chapter
IndProp. We begin
by proving a fundamental
reflection lemma relating the equality
proposition on
ids with the boolean function
beq_id.
Exercise: 2 stars (beq_idP)
Use the proof of
beq_natP in chapter
IndProp as a template to
prove the following:
☐
Now, given
ids
x1 and
x2, we can use the
destruct (beq_idP
x1 x2) to simultaneously perform case analysis on the result of
beq_id x1 x2 and generate hypotheses about the equality (in the
sense of
=) of
x1 and
x2.
Exercise: 2 stars (t_update_same)
Using the example in chapter
IndProp as a template, use
beq_idP to prove the following theorem, which states that if we
update a map to assign key
x the same value as it already has in
m, then the result is equal to
m:
☐
Exercise: 3 stars, recommended (t_update_permute)
Use
beq_idP to prove one final property of the
update
function: If we update a map
m at two distinct keys, it doesn't
matter in which order we do the updates.
☐
Partial maps
Finally, we define
partial maps on top of total maps. A partial
map with elements of type
A is simply a total map with elements
of type
option A and default element
None.
We can now lift all of the basic lemmas about total maps to
partial maps.