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

# The Coq Standard Library

Require Import Coq.Arith.Arith.

Require Import Coq.Bool.Bool.

Require Export Coq.Strings.String.

Require Import Coq.Logic.FunctionalExtensionality.

Require Import Coq.Lists.List.

Import ListNotations.

Require Import Coq.Bool.Bool.

Require Export Coq.Strings.String.

Require Import Coq.Logic.FunctionalExtensionality.

Require Import Coq.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

Definition beq_string x y :=

if string_dec x y then true else false.

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

Theorem beq_string_refl : ∀ s, true = beq_string s s.

Proof. intros s. unfold beq_string. destruct (string_dec s s) as [|Hs].

- reflexivity.

- destruct Hs. reflexivity.

Qed.

- reflexivity.

- destruct Hs. reflexivity.

Qed.

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

Theorem beq_string_true_iff : ∀ x y : string,

beq_string x y = true ↔ x = y.

beq_string x y = true ↔ x = y.

Proof.

intros x y.

unfold beq_string.

destruct (string_dec x y) as [|Hs].

- subst. split. reflexivity. reflexivity.

- split.

+ intros contra. inversion contra.

+ intros H. inversion H. subst. destruct Hs. reflexivity.

Qed.

intros x y.

unfold beq_string.

destruct (string_dec x y) as [|Hs].

- subst. split. reflexivity. reflexivity.

- split.

+ intros contra. inversion contra.

+ intros H. inversion H. subst. destruct Hs. reflexivity.

Qed.

Similarly:

Theorem beq_string_false_iff : ∀ x y : string,

beq_string x y = false

↔ x ≠ y.

beq_string x y = false

↔ x ≠ y.

Proof.

intros x y. rewrite <- beq_string_true_iff.

rewrite not_true_iff_false. reflexivity. Qed.

intros x y. rewrite <- beq_string_true_iff.

rewrite not_true_iff_false. reflexivity. Qed.

This useful variant follows just by rewriting:

Theorem false_beq_string : ∀ x y : string,

x ≠ y → beq_string x y = false.

x ≠ y → beq_string x y = false.

Proof.

intros x y. rewrite beq_string_false_iff.

intros H. apply H. Qed.

intros x y. rewrite beq_string_false_iff.

intros H. apply H. Qed.

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

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

(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 beq_string x x' then v else m x'.

(x : string) (v : A) :=

fun x' ⇒ if beq_string x x' then v else m x'.

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

*function*m and yields a new function fun x' ⇒ ... that behaves like the desired map.
Definition examplemap :=

t_update (t_update (t_empty false) "foo" true)

"bar" true.

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 "{ --> d }" := (t_empty d) (at level 0).

We then introduce a convenient notation for extending an existing
map with some bindings.
(The definition of the notation is a bit ugly, but because the
notation mechanism of Coq is not very well suited for recursive
notations, it's the best we can do.)

Notation "m '&' { a --> x }" :=

(t_update m a x) (at level 20).

Notation "m '&' { a --> x ; b --> y }" :=

(t_update (m & { a --> x }) b y) (at level 20).

Notation "m '&' { a --> x ; b --> y ; c --> z }" :=

(t_update (m & { a --> x ; b --> y }) c z) (at level 20).

Notation "m '&' { a --> x ; b --> y ; c --> z ; d --> t }" :=

(t_update (m & { a --> x ; b --> y ; c --> z }) d t) (at level 20).

Notation "m '&' { a --> x ; b --> y ; c --> z ; d --> t ; e --> u }" :=

(t_update (m & { a --> x ; b --> y ; c --> z ; d --> t }) e u) (at level 20).

Notation "m '&' { a --> x ; b --> y ; c --> z ; d --> t ; e --> u ; f --> v }" :=

(t_update (m & { a --> x ; b --> y ; c --> z ; d --> t ; e --> u }) f v) (at level 20).

(t_update m a x) (at level 20).

Notation "m '&' { a --> x ; b --> y }" :=

(t_update (m & { a --> x }) b y) (at level 20).

Notation "m '&' { a --> x ; b --> y ; c --> z }" :=

(t_update (m & { a --> x ; b --> y }) c z) (at level 20).

Notation "m '&' { a --> x ; b --> y ; c --> z ; d --> t }" :=

(t_update (m & { a --> x ; b --> y ; c --> z }) d t) (at level 20).

Notation "m '&' { a --> x ; b --> y ; c --> z ; d --> t ; e --> u }" :=

(t_update (m & { a --> x ; b --> y ; c --> z ; d --> t }) e u) (at level 20).

Notation "m '&' { a --> x ; b --> y ; c --> z ; d --> t ; e --> u ; f --> v }" :=

(t_update (m & { a --> x ; b --> y ; c --> z ; d --> t ; e --> u }) f v) (at level 20).

The examplemap above can now be defined as follows:

Definition examplemap' :=

{ --> false } & { "foo" --> true ; "bar" --> true }.

{ --> false } & { "foo" --> true ; "bar" --> true }.

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

#### Exercise: 1 star, optional (t_apply_empty)

First, the empty map returns its default element for all keys:
Lemma t_apply_empty: ∀ (A:Type) (x: string) (v: A), { --> v } x = v.

Proof.

(* FILL IN HERE *) Admitted.

☐
Proof.

(* FILL IN HERE *) Admitted.

#### 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:
Lemma t_update_eq : ∀ A (m: total_map A) x v,

(m & {x --> v}) x = v.

Proof.

(* FILL IN HERE *) Admitted.

☐
(m & {x --> v}) x = v.

Proof.

(* FILL IN HERE *) Admitted.

#### Exercise: 2 stars, optional (t_update_neq)

On the other hand, if we update a map m at a key x_{1}and then look up a

*different*key x

_{2}in the resulting map, we get the same result that m would have given:

Theorem t_update_neq : ∀ (X:Type) v x

(m : total_map X),

x

(m & {x

Proof.

(* FILL IN HERE *) Admitted.

☐
_{1}x_{2}(m : total_map X),

x

_{1}≠ x_{2}→(m & {x

_{1}--> v}) x_{2}= m x_{2}.Proof.

(* FILL IN HERE *) Admitted.

#### Exercise: 2 stars, optional (t_update_shadow)

If we update a map m at a key x with a value v_{1}and then update again with the same key x and another value v

_{2}, 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 : ∀ A (m: total_map A) v

m & {x --> v

Proof.

(* FILL IN HERE *) Admitted.

☐
_{1}v_{2}x,m & {x --> v

_{1}; x --> v_{2}} = m & {x --> v_{2}}.Proof.

(* FILL IN HERE *) Admitted.

*reflection lemma*relating the equality proposition on ids with the boolean function beq_id.

#### Exercise: 2 stars, optional (beq_stringP)

Use the proof of beq_natP in chapter IndProp as a template to prove the following:
Lemma beq_stringP : ∀ x y, reflect (x = y) (beq_string x y).

Proof.

(* FILL IN HERE *) Admitted.

☐
Proof.

(* FILL IN HERE *) Admitted.

_{1}and x

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

_{1}x

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

_{1}x

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

_{1}and x

_{2}.

#### Exercise: 2 stars (t_update_same)

With the example in chapter IndProp as a template, use beq_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 : ∀ X x (m : total_map X),

m & { x --> m x } = m.

Proof.

(* FILL IN HERE *) Admitted.

☐
m & { x --> m x } = m.

Proof.

(* FILL IN HERE *) Admitted.

#### Exercise: 3 stars, recommended (t_update_permute)

Use beq_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 : ∀ (X:Type) v

(m : total_map X),

x

m & { x

= m & { x

Proof.

(* FILL IN HERE *) Admitted.

☐
_{1}v_{2}x_{1}x_{2}(m : total_map X),

x

_{2}≠ x_{1}→m & { x

_{2}--> v_{2}; x_{1}--> v_{1}}= m & { x

_{1}--> v_{1}; x_{2}--> v_{2}}.Proof.

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

m & { x --> (Some v) }.

Definition empty {A:Type} : partial_map A :=

t_empty None.

Definition update {A:Type} (m : partial_map A)

(x : string) (v : A) :=

m & { x --> (Some v) }.

We introduce a similar notation for partial maps, using double
curly-brackets.

Notation "m '&' {{ a --> x }}" :=

(update m a x) (at level 20).

Notation "m '&' {{ a --> x ; b --> y }}" :=

(update (m & {{ a --> x }}) b y) (at level 20).

Notation "m '&' {{ a --> x ; b --> y ; c --> z }}" :=

(update (m & {{ a --> x ; b --> y }}) c z) (at level 20).

Notation "m '&' {{ a --> x ; b --> y ; c --> z ; d --> t }}" :=

(update (m & {{ a --> x ; b --> y ; c --> z }}) d t) (at level 20).

Notation "m '&' {{ a --> x ; b --> y ; c --> z ; d --> t ; e --> u }}" :=

(update (m & {{ a --> x ; b --> y ; c --> z ; d --> t }}) e u) (at level 20).

Notation "m '&' {{ a --> x ; b --> y ; c --> z ; d --> t ; e --> u ; f --> v }}" :=

(update (m & {{ a --> x ; b --> y ; c --> z ; d --> t ; e --> u }}) f v) (at level 20).

(update m a x) (at level 20).

Notation "m '&' {{ a --> x ; b --> y }}" :=

(update (m & {{ a --> x }}) b y) (at level 20).

Notation "m '&' {{ a --> x ; b --> y ; c --> z }}" :=

(update (m & {{ a --> x ; b --> y }}) c z) (at level 20).

Notation "m '&' {{ a --> x ; b --> y ; c --> z ; d --> t }}" :=

(update (m & {{ a --> x ; b --> y ; c --> z }}) d t) (at level 20).

Notation "m '&' {{ a --> x ; b --> y ; c --> z ; d --> t ; e --> u }}" :=

(update (m & {{ a --> x ; b --> y ; c --> z ; d --> t }}) e u) (at level 20).

Notation "m '&' {{ a --> x ; b --> y ; c --> z ; d --> t ; e --> u ; f --> v }}" :=

(update (m & {{ a --> x ; b --> y ; c --> z ; d --> t ; e --> u }}) f v) (at level 20).

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

Lemma apply_empty : ∀ (A: Type) (x: string), @empty A x = None.

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

(m & {{ x --> v }}) x = Some v.

Theorem update_neq : ∀ (X:Type) v x

(m : partial_map X),

x

(m & {{ x

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

m & {{ x --> v

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

m x = Some v →

m & {{x --> v}} = m.

Theorem update_permute : ∀ (X:Type) v

(m : partial_map X),

x

m & {{x

= m & {{x

Proof.

intros. unfold empty. rewrite t_apply_empty.

reflexivity.

Qed.

intros. unfold empty. rewrite t_apply_empty.

reflexivity.

Qed.

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

(m & {{ x --> v }}) x = Some v.

Proof.

intros. unfold update. rewrite t_update_eq.

reflexivity.

Qed.

intros. unfold update. rewrite t_update_eq.

reflexivity.

Qed.

Theorem update_neq : ∀ (X:Type) v x

_{1}x_{2}(m : partial_map X),

x

_{2}≠ x_{1}→(m & {{ x

_{2}--> v }}) x_{1}= m x_{1}.
Proof.

intros X v x

unfold update. rewrite t_update_neq. reflexivity.

apply H. Qed.

intros X v x

_{1}x_{2}m H.unfold update. rewrite t_update_neq. reflexivity.

apply H. Qed.

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

_{1}v_{2}x,m & {{ x --> v

_{1}; x --> v_{2}}} = m & {{x --> v_{2}}}.
Proof.

intros A m v

reflexivity.

Qed.

intros A m v

_{1}v_{2}x_{1}. unfold update. rewrite t_update_shadow.reflexivity.

Qed.

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

m x = Some v →

m & {{x --> v}} = m.

Proof.

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

apply t_update_same.

Qed.

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

apply t_update_same.

Qed.

Theorem update_permute : ∀ (X:Type) v

_{1}v_{2}x_{1}x_{2}(m : partial_map X),

x

_{2}≠ x_{1}→m & {{x

_{2}--> v_{2}; x_{1}--> v_{1}}}= m & {{x

_{1}--> v_{1}; x_{2}--> v_{2}}}.
Proof.

intros X v

apply t_update_permute.

Qed.

intros X v

_{1}v_{2}x_{1}x_{2}m. unfold update.apply t_update_permute.

Qed.