Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Maps: Total and Partial Maps

Maps (or dictionaries) are ubiquitous data structures both 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 begin...

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.

From Coq Require Import Arith.Arith.
From Coq Require Import Bool.Bool.
Require Export Coq.Strings.String.
From Coq Require Import Logic.FunctionalExtensionality.
From Coq Require Import Lists.List.
Import ListNotations.

Documentation for the standard library can be found at http://coq.inria.fr/library/.

The Search command is a good way to look for theorems involving objects of specific types. Take a minute now to experiment with it.

(* ################################################################# *)

Identifiers

First, we need a type for the keys that we use to index into our maps. In Lists.v we introduced a fresh type id for a similar purpose; here and for the rest of Software Foundations we will use the string type from Coq's standard library.

To compare strings, we define the function eqb_string, which internally uses the function string_dec from Coq's string library.

Definition eqb_string (x y : string) : bool :=
  if string_dec x y then true else false.

(The function string_dec comes from Coq's string library. If you check the result type of string_dec, you'll see that it does not actually return a bool, but rather a type that looks like {x = y} + {x ≠ y}, called a sumbool, which can be thought of as an "evidence-carrying boolean." Formally, an element of sumbool is either a proof that two things are equal or a proof that they are unequal, together with a tag indicating which. But for present purposes you can think of it as just a fancy bool.)

Now we need a few basic properties of string equality...

Theorem eqb_string_refl : forall s : string, true = eqb_string s s.forall s : string, true = eqb_string s s
Proof.forall s : string, true = eqb_string s s intros s.s:string
true = eqb_string s s unfold eqb_string.s:string
true = (if string_dec s s then true else false) destruct (string_dec s s) as [|Hs].s:string
e:s = s
true = true
s:string
Hs:s <> s
true = false
  -s:string
e:s = s
true = true reflexivity.
  -s:string
Hs:s <> s
true = false destruct Hs.s:string
s = s reflexivity.
Qed.

The following useful property follows from an analogous lemma about strings:

Theorem eqb_string_true_iff : forall x y : string,
    eqb_string x y = true <-> x = y.forall x y : string, eqb_string x y = true <-> x = y
Proof.forall x y : string, eqb_string x y = true <-> x = y
   intros x y.x, y:string
eqb_string x y = true <-> x = y
   unfold eqb_string.x, y:string
(if string_dec x y then true else false) = true <->
x = y
   destruct (string_dec x y) as [|Hs].x, y:string
e:x = y
true = true <-> x = y
x, y:string
Hs:x <> y
false = true <-> x = y
   -x, y:string
e:x = y
true = true <-> x = y subst.y:string
true = true <-> y = y split.y:string
true = true -> y = y
y:string
y = y -> true = true reflexivity.y:string
y = y -> true = true reflexivity.
   -x, y:string
Hs:x <> y
false = true <-> x = y split.x, y:string
Hs:x <> y
false = true -> x = y
x, y:string
Hs:x <> y
x = y -> false = true
     +x, y:string
Hs:x <> y
false = true -> x = y intros contra.x, y:string
Hs:x <> y
contra:false = true
x = y discriminate contra.
     +x, y:string
Hs:x <> y
x = y -> false = true intros H.x, y:string
Hs:x <> y
H:x = y
false = true rewrite H in Hs.x, y:string
Hs:y <> y
H:x = y
false = true destruct Hs.x, y:string
H:x = y
y = y reflexivity.
Qed.

Similarly:

Theorem eqb_string_false_iff : forall x y : string,
    eqb_string x y = false <-> x <> y.forall x y : string, eqb_string x y = false <-> x <> y
Proof.forall x y : string, eqb_string x y = false <-> x <> y
  intros x y.x, y:string
eqb_string x y = false <-> x <> y rewrite <- eqb_string_true_iff.x, y:string
eqb_string x y = false <-> eqb_string x y <> true
  rewrite not_true_iff_false.x, y:string
eqb_string x y = false <-> eqb_string x y = false reflexivity. Qed.

This handy variant follows just by rewriting:

Theorem false_eqb_string : forall x y : string,
   x <> y -> eqb_string x y = false.forall x y : string, x <> y -> eqb_string x y = false
Proof.forall x y : string, x <> y -> eqb_string x y = false
  intros x y.x, y:string
x <> y -> eqb_string x y = false rewrite eqb_string_false_iff.x, y:string
x <> y -> x <> y
  intros H.x, y:string
H:x <> y
x <> y apply H. Qed.

(* ################################################################# *)

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 its 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 very 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.

Definition total_map (A : Type) := string -> A.

Intuitively, a total map over an element type A is just a function that can be used to look up strings, 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 string.

Definition t_empty {A : Type} (v : A) : total_map A :=
  (fun _ => v).

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.

Definition t_update {A : Type} (m : total_map A)
                    (x : string) (v : A) :=
  fun x' => if eqb_string x x' then v else m x'.

This definition is a nice example of higher-order programming: t_update 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 strings to bools, where "foo" and "bar" are mapped to true and every other key is mapped to false, like this:

Definition examplemap :=
  t_update (t_update (t_empty false) "foo" true)
           "bar" true.

Next, let's introduce some new notations to facilitate working with maps.

First, we will use the following notation to create an empty total map with a default value.

Notation "'_' '!->' v" := (t_empty v)
  (at level 100, right associativity).

Example example_empty := (_ !-> false).

We then introduce a convenient notation for extending an existing map with some bindings.

Notation "x '!->' v ';' m" := (t_update m x v)
                              (at level 100, v at next level, right associativity).

The examplemap above can now be defined as follows:

Definition examplemap' :=
  ( "bar" !-> true;
    "foo" !-> true;
    _     !-> false
  ).

This completes the definition of total maps. Note that we don't need to define a find operation because it is just function application!

Example update_example1 : examplemap' "baz" = false.examplemap' "baz" = false
Proof.examplemap' "baz" = false reflexivity. Qed.

Example update_example2 : examplemap' "foo" = true.examplemap' "foo" = true
Proof.examplemap' "foo" = true reflexivity. Qed.

Example update_example3 : examplemap' "quux" = false.examplemap' "quux" = false
Proof.examplemap' "quux" = false reflexivity. Qed.

Example update_example4 : examplemap' "bar" = true.examplemap' "bar" = true
Proof.examplemap' "bar" = true reflexivity. Qed.

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.)

Exercise: 1 star, standard, optional (t_apply_empty)

First, the empty map returns its default element for all keys:

Lemma t_apply_empty : forall (A : Type) (x : string) (v : A),
    (_ !-> v) x = v.forall (A : Type) (x : string) (v : A),
(_ !-> v) x = v
Proof.forall (A : Type) (x : string) (v : A),
(_ !-> v) x = v
  (* FILL IN HERE *) Admitted.

☐

Exercise: 2 stars, standard, 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:

Lemma t_update_eq : forall (A : Type) (m : total_map A) x v,
    (x !-> v ; m) x = v.forall (A : Type) (m : total_map A) (x : string)
  (v : A), (x !-> v; m) x = v
Proof.forall (A : Type) (m : total_map A) (x : string)
  (v : A), (x !-> v; m) x = v
  (* FILL IN HERE *) Admitted.

☐

Exercise: 2 stars, standard, 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:

Theorem t_update_neq : forall (A : Type) (m : total_map A) x1 x2 v,
    x1 <> x2 ->
    (x1 !-> v ; m) x2 = m x2.forall (A : Type) (m : total_map A) (x1 x2 : string)
  (v : A), x1 <> x2 -> (x1 !-> v; m) x2 = m x2
Proof.forall (A : Type) (m : total_map A) (x1 x2 : string)
  (v : A), x1 <> x2 -> (x1 !-> v; m) x2 = m x2
  (* FILL IN HERE *) Admitted.

☐

Exercise: 2 stars, standard, 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:

Lemma t_update_shadow : forall (A : Type) (m : total_map A) x v1 v2,
    (x !-> v2 ; x !-> v1 ; m) = (x !-> v2 ; m).forall (A : Type) (m : total_map A) (x : string)
  (v1 v2 : A), (x !-> v2; x !-> v1; m) = (x !-> v2; m)
Proof.forall (A : Type) (m : total_map A) (x : string)
  (v1 v2 : A), (x !-> v2; x !-> v1; m) = (x !-> v2; m)
  (* FILL IN HERE *) Admitted.

☐

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 eqb_id.

Exercise: 2 stars, standard, optional (eqb_stringP)

Use the proof of eqbP in chapter IndProp as a template to prove the following:

Lemma eqb_stringP : forall x y : string,
    reflect (x = y) (eqb_string x y).forall x y : string, reflect (x = y) (eqb_string x y)
Proof.forall x y : string, reflect (x = y) (eqb_string x y)
  (* FILL IN HERE *) Admitted.

☐

Now, given strings x1 and x2, we can use the tactic destruct (eqb_stringP x1 x2) to simultaneously perform case analysis on the result of eqb_string x1 x2 and generate hypotheses about the equality (in the sense of =) of x1 and x2.

Exercise: 2 stars, standard (t_update_same)

With the example in chapter IndProp as a template, use eqb_stringP 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:

Theorem t_update_same : forall (A : Type) (m : total_map A) x,
    (x !-> m x ; m) = m.forall (A : Type) (m : total_map A) (x : string),
(x !-> m x; m) = m
Proof.forall (A : Type) (m : total_map A) (x : string),
(x !-> m x; m) = m
  (* FILL IN HERE *) Admitted.

☐

Exercise: 3 stars, standard, recommended (t_update_permute)

Use eqb_stringP 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.

Theorem t_update_permute : forall (A : Type) (m : total_map A)
                                  v1 v2 x1 x2,
    x2 <> x1 ->
    (x1 !-> v1 ; x2 !-> v2 ; m)
    =
    (x2 !-> v2 ; x1 !-> v1 ; m).forall (A : Type) (m : total_map A) (v1 v2 : A)
  (x1 x2 : string),
x2 <> x1 ->
(x1 !-> v1; x2 !-> v2; m) = (x2 !-> v2; x1 !-> v1; m)
Proof.forall (A : Type) (m : total_map A) (v1 v2 : A)
  (x1 x2 : string),
x2 <> x1 ->
(x1 !-> v1; x2 !-> v2; m) = (x2 !-> v2; x1 !-> v1; m)
  (* FILL IN HERE *) Admitted.

☐

(* ################################################################# *)

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.

Definition partial_map (A : Type) := total_map (option A).

Definition empty {A : Type} : partial_map A :=
  t_empty None.

Definition update {A : Type} (m : partial_map A)
           (x : string) (v : A) :=
  (x !-> Some v ; m).

We introduce a similar notation for partial maps:

Notation "x '|->' v ';' m" := (update m x v)
  (at level 100, v at next level, right associativity).

We can also hide the last case when it is empty.

Notation "x '|->' v" := (update empty x v)
  (at level 100).

Example examplepmap :=
  ("Church" |-> true ; "Turing" |-> false).

We now straightforwardly lift all of the basic lemmas about total maps to partial maps.

Lemma apply_empty : forall (A : Type) (x : string),
    @empty A x = None.forall (A : Type) (x : string), empty x = None
Proof.forall (A : Type) (x : string), empty x = None
  intros.A:Type
x:string
empty x = None unfold empty.A:Type
x:string
(_ !-> None) x = None rewrite t_apply_empty.A:Type
x:string
None = None
  reflexivity.
Qed.

Lemma update_eq : forall (A : Type) (m : partial_map A) x v,
    (x |-> v ; m) x = Some v.forall (A : Type) (m : partial_map A) (x : string)
  (v : A), (x |-> v; m) x = Some v
Proof.forall (A : Type) (m : partial_map A) (x : string)
  (v : A), (x |-> v; m) x = Some v
  intros.A:Type
m:partial_map A
x:string
v:A
(x |-> v; m) x = Some v unfold update.A:Type
m:partial_map A
x:string
v:A
(x !-> Some v; m) x = Some v rewrite t_update_eq.A:Type
m:partial_map A
x:string
v:A
Some v = Some v
  reflexivity.
Qed.

Theorem update_neq : forall (A : Type) (m : partial_map A) x1 x2 v,
    x2 <> x1 ->
    (x2 |-> v ; m) x1 = m x1.forall (A : Type) (m : partial_map A) (x1 x2 : string)
  (v : A), x2 <> x1 -> (x2 |-> v; m) x1 = m x1
Proof.forall (A : Type) (m : partial_map A) (x1 x2 : string)
  (v : A), x2 <> x1 -> (x2 |-> v; m) x1 = m x1
  intros A m x1 x2 v H.A:Type
m:partial_map A
x1, x2:string
v:A
H:x2 <> x1
(x2 |-> v; m) x1 = m x1
  unfold update.A:Type
m:partial_map A
x1, x2:string
v:A
H:x2 <> x1
(x2 !-> Some v; m) x1 = m x1 rewrite t_update_neq.A:Type
m:partial_map A
x1, x2:string
v:A
H:x2 <> x1
m x1 = m x1
A:Type
m:partial_map A
x1, x2:string
v:A
H:x2 <> x1
x2 <> x1 reflexivity.A:Type
m:partial_map A
x1, x2:string
v:A
H:x2 <> x1
x2 <> x1
  apply H. Qed.

Lemma update_shadow : forall (A : Type) (m : partial_map A) x v1 v2,
    (x |-> v2 ; x |-> v1 ; m) = (x |-> v2 ; m).forall (A : Type) (m : partial_map A) (x : string)
  (v1 v2 : A), (x |-> v2; x |-> v1; m) = (x |-> v2; m)
Proof.forall (A : Type) (m : partial_map A) (x : string)
  (v1 v2 : A), (x |-> v2; x |-> v1; m) = (x |-> v2; m)
  intros A m x v1 v2.A:Type
m:partial_map A
x:string
v1, v2:A
(x |-> v2; x |-> v1; m) = (x |-> v2; m) unfold update.A:Type
m:partial_map A
x:string
v1, v2:A
(x !-> Some v2; x !-> Some v1; m) = (x !-> Some v2; m) rewrite t_update_shadow.A:Type
m:partial_map A
x:string
v1, v2:A
(x !-> Some v2; m) = (x !-> Some v2; m)
  reflexivity.
Qed.

Theorem update_same : forall (A : Type) (m : partial_map A) x v,
    m x = Some v ->
    (x |-> v ; m) = m.forall (A : Type) (m : partial_map A) (x : string)
  (v : A), m x = Some v -> (x |-> v; m) = m
Proof.forall (A : Type) (m : partial_map A) (x : string)
  (v : A), m x = Some v -> (x |-> v; m) = m
  intros A m x v H.A:Type
m:partial_map A
x:string
v:A
H:m x = Some v
(x |-> v; m) = m unfold update.A:Type
m:partial_map A
x:string
v:A
H:m x = Some v
(x !-> Some v; m) = m rewrite <- H.A:Type
m:partial_map A
x:string
v:A
H:m x = Some v
(x !-> m x; m) = m
  apply t_update_same.
Qed.

Theorem update_permute : forall (A : Type) (m : partial_map A)
                                x1 x2 v1 v2,
    x2 <> x1 ->
    (x1 |-> v1 ; x2 |-> v2 ; m) = (x2 |-> v2 ; x1 |-> v1 ; m).forall (A : Type) (m : partial_map A) (x1 x2 : string)
  (v1 v2 : A),
x2 <> x1 ->
(x1 |-> v1; x2 |-> v2; m) = (x2 |-> v2; x1 |-> v1; m)
Proof.forall (A : Type) (m : partial_map A) (x1 x2 : string)
  (v1 v2 : A),
x2 <> x1 ->
(x1 |-> v1; x2 |-> v2; m) = (x2 |-> v2; x1 |-> v1; m)
  intros A m x1 x2 v1 v2.A:Type
m:partial_map A
x1, x2:string
v1, v2:A
x2 <> x1 ->
(x1 |-> v1; x2 |-> v2; m) = (x2 |-> v2; x1 |-> v1; m) unfold update.A:Type
m:partial_map A
x1, x2:string
v1, v2:A
x2 <> x1 ->
(x1 !-> Some v1; x2 !-> Some v2; m) =
(x2 !-> Some v2; x1 !-> Some v1; m)
  apply t_update_permute.
Qed.

(* Wed Jan 9 12:02:45 EST 2019 *)