MapsTotal and Partial Maps

This brief chapter defines two kinds of maps: total maps, which include a default element to be returned when a key being looked up does not exist, and partial maps, which return an option to indicate success or failure. We'll use maps in upcoming chapters to verify other data structures.
From Coq Require Import Bool.Bool.
From Coq Require Import Logic.FunctionalExtensionality.
From VFA Require Import Perm.

Total Maps

The Lists chapter in Volume 1 previously implemented maps with lists of key-value pairs. Here, we instead use functions to implement maps. Functions enable an extensional treatment of maps: two maps will be equal if they take the keys to the same values. We won't have to worry about issues that arise with lists, such as duplicate keys, or order of pairs in the list, etc. Proofs that use maps will therefore be simpler.
Intuitively, a total map over a type A is just a function that can be used to look up keys, yielding As. For simplicity, the keys in our maps will be natural numbers.
Definition total_map (A : Type) : Type := nat A.
The function t_empty yields an empty total map, given a default element; this map always returns the default element when applied to any id.
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 : nat) (v : A) : total_map A :=
  fun x'if x =? x' then v else m x'.
This definition is a nice example of higher-order programming. The t_update function 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 ids to bools, where Id 3 is mapped to true and every other key is mapped to false, like this:
Definition examplemap :=
  t_update (t_update (t_empty false) 1 false) 3 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!
Example update_example1 : examplemap 0 = false.
Proof. reflexivity. Qed.

Example update_example2 : examplemap 1 = false.
Proof. reflexivity. Qed.

Example update_example3 : examplemap 2 = false.
Proof. reflexivity. Qed.

Example update_example4 : examplemap 3 = true.
Proof. reflexivity. Qed.

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, standard (t_apply_empty)

The empty map returns its default element for all keys:
Lemma t_apply_empty: A x v, @t_empty A v x = v.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (t_update_eq)

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,
  (t_update m x v) x = v.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (t_update_neq)

If we update a map m at a key x1 and then look up a different key x2 in the resulting map, we get the same result that m would have given:
Theorem t_update_neq : (X:Type) v x1 x2
                         (m : total_map X),
  x1 x2
  (t_update m x1 v) x2 = m x2.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (t_update_shadow)

If we update a map m at a key x with a value v1 and then update again with the same key x and another value v2, 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) v1 v2 x,
    t_update (t_update m x v1) x v2
  = t_update m x v2.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (t_update_same)

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),
  t_update m x (m x) = m.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (t_update_permute)

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) v1 v2 x1 x2
                             (m : total_map X),
  x2 x1
    (t_update (t_update m x2 v2) x1 v1)
  = (t_update (t_update m x1 v1) x2 v2).
Proof.
  (* FILL IN HERE *) Admitted.

Partial 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 : nat) (v : A) : partial_map A :=
  t_update m x (Some v).
We can easily lift all of the basic lemmas about total maps to partial maps.
Lemma apply_empty : A x, @empty A x = None.
Proof.
  intros. unfold empty. rewrite t_apply_empty.
  reflexivity.
Qed.

Lemma update_eq : A (m: partial_map A) x v,
  (update m x v) x = Some v.
Proof.
  intros. unfold update. rewrite t_update_eq.
  reflexivity.
Qed.

Theorem update_neq : (X:Type) v x1 x2
                       (m : partial_map X),
  x2 x1
  (update m x2 v) x1 = m x1.
Proof.
  intros X v x1 x2 m H.
  unfold update. rewrite t_update_neq; auto.
Qed.

Lemma update_shadow : A (m: partial_map A) v1 v2 x,
  update (update m x v1) x v2 = update m x v2.
Proof.
  intros A m v1 v2 x1. unfold update. rewrite t_update_shadow.
  reflexivity.
Qed.

Theorem update_same : X v x (m : partial_map X),
  m x = Some v
  update m x v = m.
Proof.
  intros X v x m H. unfold update. rewrite <- H.
  apply t_update_same.
Qed.

Theorem update_permute : (X:Type) v1 v2 x1 x2
                                (m : partial_map X),
  x2 x1
    (update (update m x2 v2) x1 v1)
  = (update (update m x1 v1) x2 v2).
Proof.
  intros X v1 v2 x1 x2 m. unfold update.
  apply t_update_permute.
Qed.

(* 2023-10-01 07:22 *)