# MapsTotal and Partial Maps

*Maps*(or

*dictionaries*) are ubiquitous data structures both in ordinary programming and in the theory of programming languages; we're going to need them in many places in the coming chapters.

*total*maps, which include a "default" element to be returned when a key being looked up doesn't exist, and

*partial*maps, which instead 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

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.

Set Default Goal Selector "!".

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.

Set Default Goal Selector "!".

Documentation for the standard library can be found at
https://coq.inria.fr/library/.
The Search command is a good way to look for theorems involving
objects of specific types. See Lists for a reminder of how
to use it.
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 of the + notation, but only one for
naturals.)

Print Init.Nat.add.

We'll see some more uses of Locate in the Imp chapter.

# Identifiers

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

We will often use a few basic properties of string equality...

Check String.eqb_eq :

∀ n m : string, (n =? m)%string = true ↔ n = m.

Check String.eqb_neq :

∀ n m : string, (n =? m)%string = false ↔ n ≠ m.

Check String.eqb_spec :

∀ x y : string, reflect (x = y) (String.eqb x y).

∀ n m : string, (n =? m)%string = true ↔ n = m.

Check String.eqb_neq :

∀ n m : string, (n =? m)%string = false ↔ n ≠ m.

Check String.eqb_spec :

∀ x y : string, reflect (x = y) (String.eqb 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: two maps that respond to queries in the same way will be represented as exactly the same function, rather than just as "equivalent" list 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 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.

More interesting is the map-updating function, which (as always)
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. The novelty here is that we achieve this effect by wrapping
a new function around the old one.

Definition t_update {A : Type} (m : total_map A)

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

fun x' ⇒ if String.eqb x x' then v else m x'.

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

fun x' ⇒ if String.eqb 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.
Next, let's introduce some notations to facilitate working with
maps.
First, we use the following notation to represent an empty total
map with a default value.

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

(at level 100, right associativity).

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

(at level 100, right associativity).

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

We next introduce a convenient notation for extending an existing
map with a new binding.

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

The examplemap above can now be defined as follows:

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

When we use maps in later chapters, we'll need several fundamental
facts about how they behave.
Even if you don't bother to work the following exercises,
make sure you thoroughly understand the statements of the
lemmas!
(Some of the proofs require the functional extensionality axiom,
which was 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 : ∀ (A : Type) (x : string) (v : A),

(_ !-> v) x = v.

Proof.

(* FILL IN HERE *) Admitted.

☐

(_ !-> v) x = v.

Proof.

(* 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 : ∀ (A : Type) (m : total_map A) x v,

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

Proof.

(* FILL IN HERE *) Admitted.

☐

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

Proof.

(* 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 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 : ∀ (A : Type) (m : total_map A) x

x

(x

Proof.

(* FILL IN HERE *) Admitted.

☐

_{1}x_{2}v,x

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

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

(* 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 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 : Type) (m : total_map A) x v

(x !-> v

Proof.

(* FILL IN HERE *) Admitted.

☐

_{1}v_{2},(x !-> v

_{2}; x !-> v_{1}; m) = (x !-> v_{2}; m).Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 2 stars, standard (t_update_same)

Given strings x_{1}and x

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

_{1}x

_{2}) to simultaneously perform case analysis on the result of String.eqb x

_{1}x

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

_{1}and x

_{2}. With the example in chapter IndProp as a template, use String.eqb_spec 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 : ∀ (A : Type) (m : total_map A) x,

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

Proof.

(* FILL IN HERE *) Admitted.

☐

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

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 3 stars, standard, especially useful (t_update_permute)

Similarly, use String.eqb_spec 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 : ∀ (A : Type) (m : total_map A)

v

x

(x

=

(x

Proof.

(* FILL IN HERE *) Admitted.

☐

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.

☐

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

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:

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

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

(at level 100).

Definition examplepmap :=

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

(at level 100).

Definition examplepmap :=

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

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 : Type) (m : partial_map A) x v,

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

@empty A x = None.

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

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

The update_eq lemma is used very often in proofs. Adding it to
Coq's global "hint database" allows proof-automation tactics such
as auto to find it.

#[global] Hint Resolve update_eq : core.

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

x

(x

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

(x ⊢> v

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

x

(x

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}.
Proof.

intros A m x

unfold update. rewrite t_update_neq.

- reflexivity.

- apply H.

Qed.

intros A m x

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

- reflexivity.

- apply H.

Qed.

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).
One last thing: For partial maps, it's convenient to introduce a
notion of map inclusion, stating that all the entries in one map
are also present in another:

We can then show that map update preserves map inclusion -- that is:

Lemma includedin_update : ∀ (A : Type) (m m' : partial_map A)

(x : string) (vx : A),

includedin m m' →

includedin (x ⊢> vx ; m) (x ⊢> vx ; m').

(x : string) (vx : A),

includedin m m' →

includedin (x ⊢> vx ; m) (x ⊢> vx ; m').

Proof.

unfold includedin.

intros A m m' x vx H.

intros y vy.

destruct (eqb_spec x y) as [Hxy | Hxy].

- rewrite Hxy.

rewrite update_eq. rewrite update_eq. intro H

- rewrite update_neq.

+ rewrite update_neq.

× apply H.

× apply Hxy.

+ apply Hxy.

Qed.

unfold includedin.

intros A m m' x vx H.

intros y vy.

destruct (eqb_spec x y) as [Hxy | Hxy].

- rewrite Hxy.

rewrite update_eq. rewrite update_eq. intro H

_{1}. apply H_{1}.- rewrite update_neq.

+ rewrite update_neq.

× apply H.

× apply Hxy.

+ apply Hxy.

Qed.

This property is quite useful for reasoning about languages with
variable binding -- e.g., the Simply Typed Lambda Calculus, which
we will see in

*Programming Language Foundations*, where maps are used to keep track of which program variables are defined in a given scope.
(* 2024-08-25 14:45 *)