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

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

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.

If you want to find out how or where a notation is defined, the
Locate command is useful. For example, where is the natural
addition operation defined in the standard library?

Locate "+".

There are several uses for that notation, but only one for
naturals.

Print Init.Nat.add.

# Identifiers

*Software Foundations*we will use the string type from Coq's standard library.

Definition eqb_string (x y : string) : bool :=

if string_dec x y then true else false.

Theorem eqb_string_refl : ∀ s : string, true = eqb_string s s.

Theorem eqb_string_true_iff : ∀ x y : string,

eqb_string x y = true ↔ x = y.

Theorem eqb_string_false_iff : ∀ x y : string,

eqb_string x y = false ↔ x ≠ y.

Theorem eqb_string_true_iff : ∀ x y : string,

eqb_string x y = true ↔ x = y.

Theorem eqb_string_false_iff : ∀ x y : string,

eqb_string x y = false ↔ x ≠ y.

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

Notation "'_' '!->' v" := (t_empty v)

(at level 100, right associativity).

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

(at level 100, right associativity).

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

Notation "x '!->' v ';' m" := (t_update m x v)

(at level 100, v at next level, right associativity).

(at level 100, v at next level, right associativity).

Definition examplemap' :=

( "bar" !-> true;

"foo" !-> true;

_ !-> false

).

### To use maps in later chapters, we'll need several fundamental facts about how they behave.

Lemma t_apply_empty : ∀ (A : Type) (x : string) (v : A),

(_ !-> v) x = v.

Proof.

(* FILL IN HERE *) Admitted.

(* FILL IN HERE *) Admitted.

Lemma t_update_eq : ∀ (A : Type) (m : total_map A) x v,

(x !-> v ; m) x = v.

Proof.

(* FILL IN HERE *) Admitted.

(* FILL IN HERE *) Admitted.

Theorem t_update_neq : ∀ (A : Type) (m : total_map A) x

_{1}x

_{2}v,

x

_{1}≠ x

_{2}→

(x

_{1}!-> v ; m) x

_{2}= m x

_{2}.

Proof.

(* FILL IN HERE *) Admitted.

(* FILL IN HERE *) Admitted.

Lemma t_update_shadow : ∀ (A : Type) (m : total_map A) x v

_{1}v

_{2},

(x !-> v

_{2}; x !-> v

_{1}; m) = (x !-> v

_{2}; m).

Proof.

(* FILL IN HERE *) Admitted.

(* 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 strings with the boolean function eqb_string.

Lemma eqb_stringP : ∀ x y : string,

reflect (x = y) (eqb_string x y).

Proof.

(* FILL IN HERE *) Admitted.

(* FILL IN HERE *) Admitted.

### Now, given strings x

_{1}and x

_{2}, we can use the tactic destruct (eqb_stringP x

_{1}x

_{2}) to simultaneously perform case analysis on the result of eqb_string x

_{1}x

_{2}and generate hypotheses about the equality (in the sense of =) of x

_{1}and x

_{2}.

Theorem t_update_same : ∀ (A : Type) (m : total_map A) x,

(x !-> m x ; m) = m.

Proof.

(* FILL IN HERE *) Admitted.

(* FILL IN HERE *) Admitted.

Theorem t_update_permute : ∀ (A : Type) (m : total_map A)

v

_{1}v

_{2}x

_{1}x

_{2},

x

_{2}≠ x

_{1}→

(x

_{1}!-> v

_{1}; x

_{2}!-> v

_{2}; m)

=

(x

_{2}!-> v

_{2}; x

_{1}!-> v

_{1}; m).

Proof.

(* FILL IN HERE *) Admitted.

(* FILL IN HERE *) 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 : string) (v : A) :=

(x !-> Some v ; m).

Notation "x '⊢>' v ';' m" := (update m x v)

(at level 100, v at next level, right associativity).

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

(at level 100).

Example examplepmap :=

("Church" ⊢> true ; "Turing" ⊢> false).

Lemma apply_empty : ∀ (A : Type) (x : string),

@empty A x = None.

Lemma update_eq : ∀ (A : Type) (m : partial_map A) x v,

(x ⊢> v ; m) x = Some v.

Theorem update_neq : ∀ (A : Type) (m : partial_map A) x

_{1}x

_{2}v,

x

_{2}≠ x

_{1}→

(x

_{2}⊢> v ; m) x

_{1}= m x

_{1}.

Lemma update_shadow : ∀ (A : Type) (m : partial_map A) x v

_{1}v

_{2},

(x ⊢> v

_{2}; x ⊢> v

_{1}; m) = (x ⊢> v

_{2}; m).

Theorem update_same : ∀ (A : Type) (m : partial_map A) x v,

m x = Some v →

(x ⊢> v ; m) = m.

Theorem update_permute : ∀ (A : Type) (m : partial_map A)

x

_{1}x

_{2}v

_{1}v

_{2},

x

_{2}≠ x

_{1}→

(x

_{1}⊢> v

_{1}; x

_{2}⊢> v

_{2}; m) = (x

_{2}⊢> v

_{2}; x

_{1}⊢> v

_{1}; m).