Maps

Definition total maps and partial maps.

A nice case study using ideas we've seen in previous chapters, including building data structures out of high-order functions and the use of reflection to streamline proofs.

Total Maps

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

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 [string]s, yielding [A]s. *)

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

Partial Maps

Give a series of defs and lemmas proved by the former ones in total maps

Finally give the def o inclusion

(** Finally, for partial maps we introduce a notion of map inclusion,
    stating that one map includes another:  *)

Definition inclusion {A : Type} (m m' : partial_map A) :=
  forall x v, m x = Some v -> m' x = Some v.

(** We show that map update preserves map inclusion, that is: *)

Lemma inclusion_update : forall (A : Type) (m m': partial_map A)
                              x vx,
  inclusion m m' ->
  inclusion (x |-> vx ; m) (x |-> vx ; m').
Proof.
  unfold inclusion.
  intros A m m' x vx H.
  intros y vy.
  destruct (eqb_stringP x y) as [Hxy | Hxy].
  - rewrite Hxy.
    rewrite update_eq. rewrite update_eq. intro H1. apply H1.
  - rewrite update_neq. rewrite update_neq.
    + apply H.
    + apply Hxy.
    + apply Hxy.
Qed.

This property is useful for reasoning about the lambda-calculus, where maps are used to keey track of which program variables are defined at a given point.