MapsTotal and Partial Maps
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.
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 for that notation, but only one for
naturals.
Identifiers
(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 {x = y} + {x ≠ y} is either a proof that x and y 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.)
Now we need a few basic properties of string equality...
Theorem eqb_string_refl : ∀ s : string, true = eqb_string s s.
Proof.
intros s. unfold eqb_string.
destruct (string_dec s s) as [Hs_eq | Hs_not_eq].
- reflexivity.
- destruct Hs_not_eq. reflexivity.
Qed.
intros s. unfold eqb_string.
destruct (string_dec s s) as [Hs_eq | Hs_not_eq].
- reflexivity.
- destruct Hs_not_eq. reflexivity.
Qed.
Two strings are equal according to eqb_string iff they
are equal according to =. So = is reflected in eqb_string,
in the sense of "reflection" as discussed in IndProp.
Theorem eqb_string_true_iff : ∀ x y : string,
eqb_string x y = true ↔ x = y.
Proof.
intros x y.
unfold eqb_string.
destruct (string_dec x y) as [Hs_eq | Hs_not_eq].
- rewrite Hs_eq. split. reflexivity. reflexivity.
- split.
+ intros contra. discriminate contra.
+ intros H. exfalso. apply Hs_not_eq. apply H.
Qed.
intros x y.
unfold eqb_string.
destruct (string_dec x y) as [Hs_eq | Hs_not_eq].
- rewrite Hs_eq. split. reflexivity. reflexivity.
- split.
+ intros contra. discriminate contra.
+ intros H. exfalso. apply Hs_not_eq. apply H.
Qed.
Similarly:
This corollary follows just by rewriting:
Total Maps
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 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 eqb_string x x' then v else m x'.
This definition is a nice example of higher-order programming:
t_update 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 strings to bools, where
"foo" and "bar" are mapped to true and every other key is
mapped to false, like this:
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 "'_' '!->' v" := (t_empty v)
(at level 100, right associativity).
Example example_empty := (_ !-> false).
(at level 100, right associativity).
Example example_empty := (_ !-> false).
We then introduce a convenient notation for extending an existing
map with some bindings.
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 because it is just
function application!
Example update_example1 : examplemap' "baz" = false.
Example update_example2 : examplemap' "foo" = true.
Example update_example3 : examplemap' "quux" = false.
Example update_example4 : examplemap' "bar" = true.
Proof. reflexivity. Qed.
Example update_example2 : examplemap' "foo" = true.
Proof. reflexivity. Qed.
Example update_example3 : examplemap' "quux" = false.
Proof. reflexivity. Qed.
Example update_example4 : examplemap' "bar" = 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, 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.
☐
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.
☐
Exercise: 2 stars, standard, optional (t_update_neq)
On the other hand, 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 : ∀ (A : Type) (m : total_map A) x1 x2 v,
x1 ≠ x2 →
(x1 !-> v ; m) x2 = m x2.
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 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 : Type) (m : total_map A) x v1 v2,
(x !-> v2 ; x !-> v1 ; m) = (x !-> v2 ; m).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard, optional (eqb_stringP)
Use the proof of eqbP in chapter IndProp as a template to prove the following:Lemma eqb_stringP : ∀ x y : string,
reflect (x = y) (eqb_string x y).
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (t_update_same)
With the example in chapter IndProp as a template, use eqb_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 : ∀ (A : Type) (m : total_map A) x,
(x !-> m x ; m) = m.
Proof.
(* FILL IN HERE *) Admitted.
☐
Exercise: 3 stars, standard, especially useful (t_update_permute)
Use eqb_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 : ∀ (A : Type) (m : total_map A)
v1 v2 x1 x2,
x2 ≠ x1 →
(x1 !-> v1 ; x2 !-> v2 ; m)
=
(x2 !-> v2 ; x1 !-> v1 ; m).
Proof.
(* FILL IN HERE *) Admitted.
☐
Partial maps
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).
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).
Example examplepmap :=
("Church" ⊢> true ; "Turing" ⊢> false).
(at level 100).
Example 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.
Theorem update_neq : ∀ (A : Type) (m : partial_map A) x1 x2 v,
x2 ≠ x1 →
(x2 ⊢> v ; m) x1 = m x1.
Lemma update_shadow : ∀ (A : Type) (m : partial_map A) x v1 v2,
(x ⊢> v2 ; x ⊢> v1 ; m) = (x ⊢> v2 ; 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)
x1 x2 v1 v2,
x2 ≠ x1 →
(x1 ⊢> v1 ; x2 ⊢> v2 ; m) = (x2 ⊢> v2 ; x1 ⊢> v1 ; m).
Finally, for partial maps we introduce a notion of map inclusion,
stating that one map includes another:
We then show that map update preserves map inclusion, that is:
Lemma inclusion_update : ∀ (A : Type) (m m' : partial_map A)
(x : string) (vx : A),
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.
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 very useful for reasoning about languages with
variable binding, such as the Simply Typed Lambda Calculus that we
will see in Programming Language Foundations, where maps are
used to keep track of which program variables are defined at a
given point.
(* 2021-03-18 17:23 *)