Homework Assignment 7 Interactive Computer Theorem Proving CS2949, Fall 2006 UC Berkeley 
Require
Import
List.
Set Implicit
Arguments.
This assignment involves producing two stronglyspecified implementations of
the same abstract data type. We'll use Coq's module system to express this
idea. I don't think you need to be an expert on MLstyle module systems to do
this assignment, since I've filled in all of the modulerelated parts in the
template, but the curious can consult
the
OCaml manual's tutorial.
Feel free to copy some of the infrastructure for programming with specifications from the Lecture 8 code; you might want to add some of your own code in that spirit, too. Template source file 
Signatures 
First, we define what it means to implement the dictionary ADT. 
Module Type
DICTIONARY.
We have some Set that forms the keys of dictionaries.

Parameter
domain : Set.
We have the type of dictionaries, indexed by the type of data being stored. 
Parameter
dict : Set > Set.
Look up the data associated with a given key. 
Parameter
lookup : forall (range : Set), dict range > domain > option range.
The empty dictionary 
Parameter
empty : forall (range : Set),
{D : dict range  forall (d : domain), lookup D d = None}.
Adding a mapping 
Parameter
add : forall (range : Set) (D : dict range) (d : domain) (r : range),
{D' : dict range  lookup D' d = Some r
/\ forall (d' : domain), d <> d' > lookup D' d' = lookup D d'}.
End
DICTIONARY.
This signature defines what we will require from clients who want to build dictionaries for particular key types. 
Module Type
DICTIONARY_PARAM.
Parameter
domain : Set.
Parameter
domain_eq_dec : forall (x y : domain), {x = y} + {x <> y}.
...so all that we require is that equality on the key type is decidable. 
End
DICTIONARY_PARAM.
Naive dictionaries using functions 
We'll implement the dictionary ADT using the most obvious (and quite inefficient!) representation: dictionaries will be the lookup functions themselves. 
Module
FuncDictionary (Param : DICTIONARY_PARAM) : DICTIONARY
with Definition
domain := Param.domain.
Import
Param.
Section
dict.
Variable
range : Set.
Defined as promised, dictionaries are lookup functions. 
Definition
dict := domain > option range.
That makes lookup very convenient to write. :)

Definition
lookup : dict > domain > option range := fun D => D.
Fill in a definition for empty .

Definition
empty : {D : dict  forall (d : domain), lookup D d = None}.
Admitted.
Fill in a definition for add .

Definition
add : forall (D : dict) (d : domain) (r : range),
{D' : dict  lookup D' d = Some r
/\ forall (d' : domain), d <> d' > lookup D' d' = lookup D d'}.
Admitted.
End
dict.
Definition
domain := domain.
End
FuncDictionary.
Of course, it's always fun to see the OCaml version of your implementation. 
Extraction FuncDictionary.
Dictionaries using unsorted lists 
Now we'll implement dictionaries using the more efficient representation of unsorted association lists with no duplicates. 
Module
ListDictionary (Param : DICTIONARY_PARAM) : DICTIONARY
with Definition
domain := Param.domain.
Import
Param.
Section
dict.
Variable
range : Set.
We start by defining an auxiliary dependent, listlike type.
The list parameter to dict' expresses the keys that have "already been
used" and so may not appear again.

Inductive
dict' : list domain > Set :=
 Nil : forall ls,
dict' ls
 Cons : forall ls d,
~In d ls
> range
> dict' (d :: ls)
> dict' ls.
A dictionary is just a dict' where no keys have already been used.

Definition
dict := dict' nil.
The obvious lookup function 
Fixpoint
lookup' (ls : list domain) (D : dict' ls) (d : domain) {struct D}
: option range :=
match D with
 Nil _ => None
 Cons _ d' _ r D' =>
if domain_eq_dec d d'
then Some r
else lookup' D' d
end.
Definition
lookup := lookup' (ls:= nil).
Fill in a definition for empty .

Definition
empty : {D : dict  forall (d : domain), lookup D d = None}.
Admitted.
Fill in a definition for add . You'll probably want some auxiliary
definitions for this one.

Definition
add : forall (D : dict) (d : domain) (r : range),
{D' : dict  lookup D' d = Some r
/\ forall (d' : domain), d <> d' > lookup D' d' = lookup D d'}.
Admitted.
End
dict.
Definition
domain := domain.
End
ListDictionary.
Extraction ListDictionary.