|
Homework Assignment 7 Interactive Computer Theorem Proving CS294-9, Fall 2006 UC Berkeley |
Require Import List.
Set Implicit Arguments.
|
This assignment involves producing two strongly-specified 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 ML-style module systems to do
this assignment, since I've filled in all of the module-related 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, list-like 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.