「SF-LC」8 Maps

useful as env

Map == Dictionary

building data structure.
use of reflection to streamline proofs.

Two flavors of maps:

total maps, return default when lookup fails
partial maps, return option to indicate success/failure, using None as the default.

The Coq Standard Lib

From now on, importing from std lib. (but should not notice much difference)

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.

TODO: what’s the differences above? Answered in Coq Intensive:

Require give access but need to use qualified name
Import no need to use qualified name
Export module importing me no need to use qualified name as well

String in Coq is list of Char and Char is record of 8 Bool…

Identifiers

we need a type for the keys that we use to index into our maps.

In Lists.v (Partial Maps):

Inductive id : Type := 
  | Id (n : nat).

From now on we will use the string from Coq’s std lib:

Definition eqb_string (x y : string) : bool :=
  if string_dec x y then true else false.

Check string_dec: (* ===> *)
     : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}

The equality check fn for string from stdlib is string_des, which returns a sumbool type, i.e. {x=y} + {x≠y}.

which can be thought of as an “evidence-carrying boolean”. Formally, an element of sumbool is either or

a proof that two things are equal

a proof that they are unequal, together with a tag indicating which.

Some properties:

(* reflexive relation *)
Theorem eqb_string_refl : ∀s : string, true = eqb_string s s.

(* functional extensionality *)
Theorem eqb_string_true_iff : ∀x y : string, eqb_string x y = true ↔ x = y.
Theorem eqb_string_false_iff : ∀x y : string, eqb_string x y = false ↔ x ≠ y.

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. 外延性

(where two maps that respond to queries in the same way will be represented as literally the same thing rather than just “equivalent” data structures. This, in turn, simplifies proofs that use maps.)

Definition total_map (A : Type) := string -> A.

(* empty take a default value *)
Definition t_empty {A : Type} (v : A) : total_map A :=
  (fun _ => v).

(* update take a key value pair *)
Definition t_update {A : Type} (m : total_map A)
                    (x : string) (v : A) (* : total_map A *) :=
  fun x' => if eqb_string x x' then v else m x'.

Where is the data stored? Closure!

My Reviews on API style of ML

Definition examplemap :=
  t_update (t_update (t_empty false) "foo" true)
           "bar" true.

since t_update is defined as so called “t-first” style. Reason/BuckleScript and OCaml stdlib uses this style as well:

let examplemap = 
  t_empty(false)
  |. t_update("foo", true)         /* fast pipe */
  |. t_update("bar", true) 

val add : key -> 'a -> 'a t -> 'a t
let examplemap = 
  Map.empty 
  |> Map.add "foo" true
  |> Map.add "bar" true

Or, In Jane Street “named-argument” style e.g. Real World OCaml

let examplemap = 
  Map.empty
  |> Map.add ~key:"foo" ~data:true
  |> Map.add ~key:"bar" ~data:true

Lightweight Meta-Programming in Coq - Notation

In Coq, we can leverage some meta programming:

Notation "'_' '!->' v" := (t_empty v)
  (at level 100, right associativity).

Notation "x '!->' v ';' m" := (t_update m x v)
  (at level 100, v at next level, right associativity).

Definition examplemap' :=
  ( "bar" !-> true;
    "foo" !-> true;
    _     !-> false
  ).

Noticed that the “Map building” is in a reversed order…

Note that we don’t need to define a find operation because it is just function application!

Example update_example2 : examplemap' "foo" = true.
Example update_example4 : examplemap' "bar" = true.
Example update_example1 : examplemap' "baz" = false. (* default *)

Partial Maps

we define 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).
  
Notation "x '⊢>' v ';' m" := (update m x v)
  (at level 100, v at next level, right associativity).

(** hide the empty case. Since it's always [None] **)
Notation "x '⊢>' v" := (update empty x v)
  (at level 100).
  
(** so nice **)
Example examplepmap :=
  ("Church" ⊢> true ; 
   "Turing" ⊢> false).

we use the “standard” map operator ↦ for partial map since maps in CS are usually partial.

Maps are functions

In many branches of mathematics, the term map is used to mean a function. partial map = partial function, total map = total function.

In category theory, “map” is often used as a synonym for morphism or arrow.

In formal logic, “map” is sometimes used for a functional symbol.

Logical Foundations - Total and Partial Maps