Maps
Table of Contents
Homepage | Previous: IndPrinciples.v | Code | Next: Rel.v
1. Summary
We define total maps and partial maps as functions. Total maps return a default value; partial maps are total maps with the partiality simulated by option types.
1.1. Terms
Total maps, partial maps, String.eqb
2. Notes
2.1. Identifiers
We use the string type as the key type for maps. To compare strings, we use String.eqb. Interesting properties of string equality include: String.eqb_refl, String.eqb_eq, String.eqb_neq, String.eqb_spec. The first says that string equality is reflexive. The other two establish a correspondence between string equality and equality: if two strings are equal under eqb, then they are equal under eq (=) (and similarly with neq). eqb_spec is a bit mysterious.
2.2. Total Maps
Total maps are defined here as functions. The advantage is that this is more “extensional”; two maps are equal if they give the same output value for every input key, rather than two maps-as-lists being equal when their list structures are equal.
Total maps are maps that return a default value when we lookup a key.
Here is the map definition:
Definition total_map (A : Type) := string -> A Definition t_empty {A : Type} (v : A) : total_map A := (fun _ => v). 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'.
Total maps here are defined as functions from string (key) to some value of type A.
Empty total maps simply return the default value v. Updating a total map extends a map
by wrapping the function. See t_update.
Querying a map is the same as function application.
The exercises are about some basic results.
2.3. Functional extensionality
Recall from Logic.v, one notion of functional equivalence (functional extensionality.)
#+BEGINSRC coq Axiom functionalextensionality : forall {X Y: Type} {f g : X -> Y}, (forall (x:X), f x = g x) -> f = g. #+ENDSRC coq
2.4. Partial maps
A partial map on type A is simply a total map on option A.
That is, elements either Some _ (if they are in the map) else None (the default element).
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).
A notion of map inclusion was then introduced - a map m is included in map m' if all entries in map m are in map m'. Then, it was proven that map update preserves map inclusion.
Apparently this property is useful for reasoning with variable binding in the STLC chapter (Programming Language Foundations book), as maps are used to keep track of variable scope.
3. Exercises
Most were pretty simple. We had to unfold t_update and t_empty; and apply the String.eqb properties. For showing that two maps were equal, we used functional_extensionality.
String.eqb_spec was used to analyse the equality of two strings and case on whether they were equal (in the sense of = and not String.eqb) or not equal.
3.1. t_apply_empty
1 star, standard, optional
3.2. t_update_eq
2 stars, standard, optional
3.3. t_update_neq
2 stars, standard, optional
3.4. t_update_shadow
2 stars, standard, optional
3.5. t_update_same
2 stars, standard
3.6. t_update_permute
3 stars, standard, especially useful
4. Scores
All exercises done. 12/12
5. Questions
N/A
6. Metacognition
Pretty simple chapter.
7. Further Knowledge
N/A