# Maps: Total and Partial 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

Require Import Coq.Arith.Arith.

Require Import Coq.Bool.Bool.

Require Import Coq.Logic.FunctionalExtensionality.

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.

# Total Maps

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

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

*is*just a function that can be used to look up ids, yielding As.
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 : nat) (v : A) :=

fun x' => if beq_nat x x' then v else m x'.

This definition is a nice example of higher-order programming.
The t_update function takes a
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:

*function*m and yields a new function fun x' => ... that behaves like the desired map.
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 0 = false.

Proof. reflexivity. Qed.

Example update_example2 : examplemap 1 = false.

Proof. reflexivity. Qed.

Example update_example3 : examplemap 2 = false.

Proof. reflexivity. Qed.

Example update_example4 : examplemap 3 = true.

Proof. 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 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:Theorem t_update_neq : forall (X:Type) v x1 x2

(m : total_map X),

x1 <> x2 ->

(t_update m x1 v) x2 = m x2.

Proof.

Admitted.

☐

#### 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:Lemma t_update_shadow : forall A (m: total_map A) v1 v2 x,

t_update (t_update m x v1) x v2

= t_update m x v2.

Proof.

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 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.Theorem t_update_permute : forall (X:Type) v1 v2 x1 x2

(m : total_map X),

x2 <> x1 ->

(t_update (t_update m x2 v2) x1 v1)

= (t_update (t_update m x1 v1) x2 v2).

Proof.

Admitted.

☐

# Partial maps

*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 : nat) (v : A) :=

t_update m x (Some v).

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

Lemma apply_empty : forall A x, @empty A x = None.

Proof.

intros. unfold empty. rewrite t_apply_empty.

reflexivity.

Qed.

Lemma update_eq : forall A (m: partial_map A) x v,

(update m x v) x = Some v.

Proof.

intros. unfold update. rewrite t_update_eq.

reflexivity.

Qed.

Theorem update_neq : forall (X:Type) v x1 x2

(m : partial_map X),

x2 <> x1 ->

(update m x2 v) x1 = m x1.

Proof.

intros X v x1 x2 m H.

unfold update. rewrite t_update_neq. reflexivity.

apply H. Qed.

Lemma update_shadow : forall A (m: partial_map A) v1 v2 x,

update (update m x v1) x v2 = update m x v2.

Proof.

intros A m v1 v2 x1. unfold update. rewrite t_update_shadow.

reflexivity.

Qed.

Theorem update_same : forall X v x (m : partial_map X),

m x = Some v ->

update m x v = m.

Proof.

intros X v x m H. unfold update. rewrite <- H.

apply t_update_same.

Qed.

Theorem update_permute : forall (X:Type) v1 v2 x1 x2

(m : partial_map X),

x2 <> x1 ->

(update (update m x2 v2) x1 v1)

= (update (update m x1 v1) x2 v2).

Proof.

intros X v1 v2 x1 x2 m. unfold update.

apply t_update_permute.

Qed.