(** * ADT: Abstract Data Types *)
(** An _Abstract Data Type_ comprises:
- A _type_ with a hidden representation.
- Interface functions that operate on that type.
- Axioms about the interaction of those functions. *)
Require Import Omega.
(** Let's consider the concept of lookup tables, indexed by keys that are
numbers, mapping those keys to values of arbitrary (parametric) type.
We can express this in Coq as follows: *)
Module Type TABLE.
Parameter V: Type.
Parameter default: V.
Parameter table: Type.
Definition key := nat.
Parameter empty: table.
Parameter get: key -> table -> V.
Parameter set: key -> V -> table -> table.
Axiom gempty: forall k, (* get-empty *)
get k empty = default.
Axiom gss: forall k v t, (* get-set-same *)
get k (set k v t) = v.
Axiom gso: forall j k v t, (* get-set-other *)
j <> k -> get j (set k v t) = get j t.
End TABLE.
(** This means: in any [Module] that satisfies this [Module Type],
there's a type [table] of lookup-tables, a type [V] of values,
and operators [empty], [get], [set] that satisfy the axioms
[gempty], [gss], and [gso].
It's easy to make an implementation of [TABLE], using [Maps].
Just for example, let's choose [V] to be [string]. *)
From VFA Require Import Maps.
Require Import String.
Open Scope string_scope.
(** First, let's specialize the definition of [TABLE] to have values
that are strings. Why? Let's return to that question after we
define the module. *)
Module Type TABLE_STRING := TABLE with Definition V := string.
(** To define a [Module] that implements a [Module Type], you need to
provide a [Definition] or [Theorem] for each [Parameter] or [Axiom]. *)
Module MapsTable : TABLE_STRING.
Definition V := string.
Definition default: V := "".
Definition table := total_map V.
Definition key := nat.
Definition empty : table := t_empty default.
Definition get (k: key) (m: table) : V := m k.
Definition set (k: key) (v: V) (m: table) : table :=
t_update m k v.
Theorem gempty: forall k, get k empty = default.
Proof. intros. reflexivity. Qed.
Theorem gss: forall k v t, get k (set k v t) = v.
Proof. intros. unfold get, set. apply t_update_eq. Qed.
Theorem gso: forall j k v t, j<>k -> get j (set k v t) = get j t.
Proof. intros. unfold get, set. apply t_update_neq.
congruence.
Qed.
End MapsTable.
(** The specialization of [TABLE] to [TABLE_STRING] exposes the
definition of [V] as [string] to the world outside the module.
Without it, all that would be known is what [TABLE] exposes, which
is that [V] is some [Type].
You could instead write [Module MapsTable <: TABLE.]. That would
cause Coq to check that [MapsTable] does conform to the [TABLE]
type, but would leave all the definitions of [MapsTable] exposed
to the outside world. That is, there would be no encapsulation.
Now we can see that [V] is known to be [string], but [table] is
_abstract_: all that is known is that it is some [Type]. *)
Print MapsTable.V.
(* ====>
MapsTable.V = string
: Type *)
Print MapsTable.table.
(* ====>
*** [ MapsTable.table : Type ] *)
(** As an example, let's put 1 and 3 into a map, then lookup 1. *)
Definition ex_t :=
MapsTable.set 3 "three"
(MapsTable.set 1 "one"
MapsTable.empty).
Example test_maps_table : MapsTable.get 1 ex_t = "one".
Proof. Fail reflexivity. Abort.
(** Why does the proof fail? Because like [table], [get] and [set] and
[empty] are also abstract. Outside the module, nothing is known
about their implementation except what is revealed in [TABLE].
Fortunately, [TABLE] reveals some useful theorems. *)
Example test_maps_table : MapsTable.get 1 ex_t = "one".
Proof.
unfold ex_t.
rewrite MapsTable.gso.
rewrite MapsTable.gss.
reflexivity.
omega.
Qed.
(** The problem with [MapsTable] is that the [Maps] implementation is
very inefficient: linear time per [get] operation. If you do a
sequence of [N] [get] and [set] operations, it can take time
quadratic in [N]. For a more efficient implementation, let's use
our search trees. *)
From VFA Require Import SearchTree.
Module TreeTable : TABLE.
Definition V := string.
Definition default : V := "".
Definition table := tree V.
Definition key := nat.
Definition empty : table := empty_tree V.
Definition get (k: key) (m: table) : V := lookup V default k m.
Definition set (k: key) (v: V) (m: table) : table :=
insert V k v m.
Theorem gempty: forall k, get k empty = default.
Proof. intros. reflexivity. Qed.
Theorem gss: forall k v t, get k (set k v t) = v.
Proof. intros. unfold get, set.
destruct (unrealistically_strong_can_relate V default t)
as [m H].
assert (H0 := insert_relate V default k v t m H).
assert (H1 := lookup_relate V default k _ _ H0).
rewrite H1. apply t_update_eq.
Qed.
(** **** Exercise: 3 stars, standard (TreeTable_gso)
Prove this using techniques similar to the proof of [gss] just above. *)
Theorem gso: forall j k v t, j<>k -> get j (set k v t) = get j t.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
End TreeTable.
(** But suppose we don't have an unrealistically strong can-relate theorem?
Remember the type of the "ordinary" can_relate: *)
Check can_relate.
(* : forall (V : Type) (default : V) (t : tree V),
SearchTree V t ->
exists m : total_map V, Abs V default t m *)
(** This requires that [t] have the [SearchTree] property, or in
general, any value of type [table] should be well-formed, that is,
should satisfy the representation invariant. We must ensure that
the client of an ADT cannot "forge" values, that is, cannot coerce
the representation type into the abstract type; especially
ill-formed values of the representation type. This
"unforgeability" is enforced in some real programming languages:
ML (Standard ML or OCaml) with its module system; Java, whose
Classes have "private variables" that the client cannot see. *)
(* ################################################################# *)
(** * A Brief Excursion into Dependent Types *)
(** Let's briefly look at a different way of enforcing the
representation invariant: every value of the representation type
will carry along with it a proof that the value satisfies the
representation invariant.
To do this, we'll use _sigma types_, aka _dependent sums_, which
are defined in the Coq standard library. Suppose [P] is a
predicate on type [A], that is, [P : A -> Prop]. Then [sig A P] is the
type of elements of [A] that satisfy [P]. You could think of this
as a subset: [sig A P] is the subset of values of [A] that satisfy
[P]. Based on that intuition, there is a notation [{x : A | P}]
that means [sig A P]. *)
Check sig.
(* ====>
sig : forall A : Type, (A -> Prop) -> Type *)
(* As an example, here is a type for even natural numbers. [Nat.Even :
nat -> Prop] is defined in the standard library. The [A] argument to
[sig] is implicit, so we don't write it below. *)
Definition even_nat := sig Nat.Even.
Print even_nat.
(* ====>
even_nat = {x : nat | Nat.Even x}
: Set
*)
(** A value of type [sig A P] is a like a "package" of two things: a value
[x : A], and a proof of [P x], that is, that [x] satisfies [P].
Such values are created with the constructor [exist]. *)
Print sig.
(* ====>
Inductive sig (A : Type) (P : A -> Prop) : Type :=
exist : forall x : A, P x -> {x : A | P x}
*)
Theorem zero_even : Nat.Even 0.
Proof.
unfold Nat.Even. exists 0. omega.
Qed.
Definition even_zero : even_nat :=
exist Nat.Even 0 zero_even.
(** Sigma types and existential quantification no doubt seem quite
similar. They are! We can see that by looking at their definitions
side by side, and removing some of the notational sugar: *)
(*
Inductive sig (A : Type) (P : A -> Prop) : Type :=
exist : forall x : A, P x -> sig A (fun y => P y)
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
ex_intro : forall x : A, P x -> ex A (fun y => P y)
*)
(** The essential difference is that [sig] creates a [Type] whereas
[ex] creates a [Prop]. That is, the former is computational in
content, whereas the latter is logical. Therefore we can write
functions to recover the witness from a [sig], even though we
cannot do the same from an [ex]. The standard library defines
those functions to _project_ the first or second component
of a [sig]: *)
Check proj1_sig.
(* ====>
forall {A : Type} {P : A -> Prop},
{x | P x} -> A
*)
Check proj2_sig.
(* ====>
forall (A : Type) {P : A -> Prop} (e : {x | P x}),
P (proj1_sig e)
*)
Definition the_witness : nat := proj1_sig even_zero.
Compute the_witness. (* = 0 : nat *)
Definition the_proof : Nat.Even 0 := proj2_sig even_zero.
Compute the_proof. (* = zero_even : Nat.Even 0 *)
(* ================================================================= *)
(** ** Search Trees using Sigma Types *)
(** Let's apply this idea to search trees. The type [A] will be [tree
V]. The predicate [P x] will be [SearchTree x]. *)
Module TreeTable2 : TABLE.
Definition V := string.
Definition default : V := "".
Definition table := {x | SearchTree V x}.
Definition key := nat.
Definition empty : table :=
exist (SearchTree V) (empty_tree V) (empty_tree_SearchTree V).
Definition get (k: key) (m: table) : V :=
(lookup V default k (proj1_sig m)).
Definition set (k: key) (v: V) (m: table) : table :=
exist (SearchTree V) (insert V k v (proj1_sig m))
(insert_SearchTree _ _ _ _ (proj2_sig m)).
Theorem gempty: forall k, get k empty = default.
Proof. intros. reflexivity. Qed.
Theorem gss: forall k v t, get k (set k v t) = v.
Proof. intros. unfold get, set.
unfold table in t.
(** Now: [t] is a package with two components: The first component is
a tree, and the second component is a proof that the first
component has the SearchTree property. We can destruct [t] to see
that more clearly. *)
destruct t as [a Ha].
(* Watch what this [simpl] does: *)
simpl.
(* Now we can use [can_relate] instead of
[unrealistically_strong_can_relate]: *)
destruct (can_relate V default a Ha) as [m H].
pose proof (insert_relate V default k v a m H).
pose proof (lookup_relate V default k _ _ H0).
rewrite H1. apply t_update_eq.
Qed.
(** **** Exercise: 3 stars, standard (TreeTable_gso)
Prove this using techniques similar to the proof of [gss] just above;
don't use [unrealistically_strong_can_relate]. *)
Theorem gso: forall j k v t, j<>k -> get j (set k v t) = get j t.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
End TreeTable2.
(** (End of the brief excursion into dependent types.) *)
(* ################################################################# *)
(** * Summary of Abstract Data Type Proofs *)
Section ADT_SUMMARY.
Variable V: Type.
Variable default: V.
(** Step 1. Define a _representation invariant_. (In the case of
search trees, the representation invariant is the [SearchTree]
predicate.) Prove that each operation on the data type _preserves_
the representation invariant. For example: *)
Check (empty_tree_SearchTree V).
(* SearchTree V (empty_tree V) *)
Check (insert_SearchTree V).
(* forall (k : key) (v : V) (t : tree V),
SearchTree V t -> SearchTree V (insert V k v t) *)
(** Notice two things: Any operator (such as [insert]) that takes a
[tree] _parameter_ can _assume_ that the parameter satisfies the
representation invariant. That is, the [insert_SearchTree] theorem
takes a premise, [SearchTree V t].
Any operator that produces a [tree] _result_ must prove that the
result satisfies the representation invariant. Thus, the
conclusions, [SearchTree V (empty_tree V)] and [SearchTree V
(empty_tree V)] of the two theorems above.
Finally, any operator that produces a result of "base type", has
no obligation to prove that the result satisfies the
representation invariant; that wouldn't make any sense anyway,
because the types wouldn't match. That is, there's no
"lookup_SearchTree" theorem, because [lookup] doesn't return a
result that's a [tree].
Step 2. Define an _abstraction relation_. (In the case of search
trees, it's the [Abs] relation. This relates the data structure to
some mathematical value that is (presumably) simpler to reason
about. *)
Check (Abs V default). (* tree V -> total_map V -> Prop *)
(** For each operator, prove that: assuming each [tree] argument
satisfies the representation invariant _and_ the abstraction
relation, prove that the results also satisfy the appropriate
abstraction relation. *)
Check (empty_tree_relate V default). (*
Abs V default (empty_tree V) (t_empty default) *)
Check (lookup_relate' V default). (* forall k t m,
SearchTree V t ->
Abs V default t m ->
lookup V default k t = m (Id k) *)
Check (insert_relate' V default). (* : forall k v t m,
SearchTree V t ->
Abs V default t m ->
Abs V default (insert V k v t) (t_update m (Id k) v) *)
(** Step 3. Using the representation invariant and the abstraction
relation, prove that all the axioms of your ADT are valid. For
example... *)
Check TreeTable2.gso. (*
: forall (j k : TreeTable2.key) (v : TreeTable2.V)
(t : TreeTable2.table),
j <> k ->
TreeTable2.get j (TreeTable2.set k v t) = TreeTable2.get j t *)
End ADT_SUMMARY.
(* ################################################################# *)
(** * Exercise in Data Abstraction *)
(** The rest of this chapter is optional. *)
Require Import List.
Import ListNotations.
(** Here's the Fibonacci function. *)
Fixpoint fibonacci (n: nat) :=
match n with
| 0 => 1
| S i => match i with 0 => 1 | S j => fibonacci i + fibonacci j end
end.
Eval compute in map fibonacci [0;1;2;3;4;5;6].
(** Here's a silly little program that computes the Fibonacci function. *)
Fixpoint repeat {A} (f: A->A) (x: A) n :=
match n with O => x | S n' => f (repeat f x n') end.
Definition step (al: list nat) : list nat :=
List.cons (nth 0 al 0 + nth 1 al 0) al.
Eval compute in map (repeat step [1;0;0]) [0;1;2;3;4;5].
Definition fib n := nth 0 (repeat step [1;0;0] n) 0.
Eval compute in map fib [0;1;2;3;4;5;6].
(** Here's a strange "List" module. *)
Module Type LISTISH.
Parameter list: Type.
Parameter create : nat -> nat -> nat -> list.
Parameter cons: nat -> list -> list.
Parameter nth: nat -> list -> nat.
End LISTISH.
Module L <: LISTISH.
Definition list := (nat*nat*nat)%type.
Definition create (a b c: nat) : list := (a,b,c).
Definition cons (i: nat) (il : list) := match il with (a,b,c) => (i,a,b) end.
Definition nth (n: nat) (al: list) :=
match al with (a,b,c) =>
match n with 0 => a | 1 => b | 2 => c | _ => 0 end
end.
End L.
Definition sixlist := L.cons 0 (L.cons 1 (L.cons 2 (L.create 3 4 5))).
Eval compute in map (fun i => L.nth i sixlist) [0;1;2;3;4;5;6;7].
(** Module [L] implements _approximations_ of lists: it can remember
the first three elements, and forget the rest. Now watch: *)
Definition stepish (al: L.list) : L.list :=
L.cons (L.nth 0 al + L.nth 1 al) al.
Eval compute in map (repeat stepish (L.create 1 0 0)) [0;1;2;3;4;5].
Definition fibish n := L.nth 0 (repeat stepish (L.create 1 0 0) n).
Eval compute in map fibish [0;1;2;3;4;5;6].
(** This little theorem may be useful in the next exercise. *)
Lemma nth_firstn:
forall A d i j (al: list A), i nth i (firstn j al) d = nth i al d.
Proof.
induction i; destruct j,al; simpl; intros; auto; try omega.
apply IHi. omega.
Qed.
(** **** Exercise: 4 stars, standard, optional (listish_abstraction)
In this exercise we will not need a _representation invariant_.
Define an abstraction relation: *)
Inductive L_Abs: L.list -> List.list nat -> Prop :=
(* FILL IN HERE *)
.
Definition O_Abs al al' := L_Abs al al'.
(* State these theorems using O_Abs, not L_Abs.
You'll see why below, at "Opaque". *)
Lemma create_relate : True. (* change this line appropriately *)
(* FILL IN HERE *) Admitted.
Lemma cons_relate : True. (* change this line appropriately *)
(* FILL IN HERE *) Admitted.
Lemma nth_relate : True. (* change this line appropriately *)
(* FILL IN HERE *) Admitted.
(** Now, we will make these operators opaque. Therefore, in the rest of
the proofs in this exercise, you will not unfold their definitions. Instead,
you will just use the theorems [create_relate], [cons_relate], [nth_relate]. *)
Opaque L.list.
Opaque L.create.
Opaque L.cons.
Opaque L.nth.
Opaque O_Abs.
Lemma step_relate:
forall al al',
O_Abs al al' ->
O_Abs (stepish al) (step al').
Proof.
(* FILL IN HERE *) Admitted.
Lemma repeat_step_relate:
forall n al al',
O_Abs al al' ->
O_Abs (repeat stepish al n) (repeat step al' n).
Proof.
(* FILL IN HERE *) Admitted.
Lemma fibish_correct: forall n, fibish n = fib n.
Proof. (* No induction needed in this proof! *)
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 2 stars, standard, optional (fib_time_complexity)
Suppose you run these three programs call-by-value, that is,
as if they were ML programs.
[fibonacci N]
[fib N]
[fibish N]
What is the asymptotic time complexity (big-Oh run time) of each,
as a function of N? Assume that the [plus] function runs in constant time.
You can use terms like "linear," "N log N," "quadratic," "cubic," "exponential."
Explain your answers briefly.
fibonacci: (* fill in here *)
fib: (* fill in here *)
fibish: (* fill in here *)
[] *)