ADTAbstract Data Types

An abstract data type (ADT) comprises:
  • A type with a hidden representation.
  • Operations on that type.
  • Specifications of the operations.
Coq's module system enables programming of --and proofs about-- ADTs.

The Table ADT

An interface for the association table ADT:

Module Type Table.
A table is a binding from keys to values. It is total, meaning it binds all keys.
  Parameter table : Type.
Keys are natural numbers.
  Definition key := nat.
Values are an arbitrary type V.
  Parameter V : Type.
The default value to which keys are bound.
  Parameter default : V.
empty is the table that binds all keys to the default value.
  Parameter empty : table.
get k t is the value v to which k is bound in t.
  Parameter get : key → table → V.
set k v t is the table that binds k to v and otherwise has the same bindings as t.
  Parameter set : key → V → table → table.
The following three axioms are an equational specification for the table ADT.

  Axiom get_empty_default : ∀ (k : key),
      get k empty = default.
  Axiom get_set_same : ∀ (k : key) (v : V) (t : table),
      get k (set k v t) = v.
  Axiom get_set_other : ∀ (k k' : key) (v : V) (t : table),
      k ≠ k' → get k' (set k v t) = get k' t.
End Table.

Implementing Table with Functions

An interface for values:

Module Type ValType.
  Parameter V : Type.
  Parameter default : V.
End ValType.
A functor that implements Table:

Module FunTable (VT : ValType) <: (Table with Definition V := VT.V with Definition default := VT.default).
  Definition V := VT.V.
  Definition default := VT.default.
  Definition key := nat.
A table is a function from keys to values.
  Definition table := key → V.
  Definition empty : table :=
    fun _ ⇒ default.
  Definition get (k : key) (t : table) : V :=
    t k.
  Definition set (k : key) (v : V) (t : table) : table :=
    fun k' ⇒ if k =? k' then v else t k'.
The implementation must prove the theorems that the interface specified as axioms.

  Theorem get_empty_default: ∀ (k : key),
      get k empty = default.
  Proof. intros. unfold get, empty. reflexivity. Qed.
  Theorem get_set_same: ∀ (k : key) (v : V) (t : table),
      get k (set k v t) = v.
  Proof. intros. unfold get, set. bdall. Qed.
  Theorem get_set_other: ∀ (k k' : key) (v : V) (t : table),
      k ≠ k' → get k' (set k v t) = get k' t.
  Proof. intros. unfold get, set. bdall. Qed.
End FunTable.

As an example, let's instantiate FunTable with strings as values.

Module StringVal.
  Definition V := string.
  Definition default := ""%string.
End StringVal.
Module FunTableExamples.
  Module StringFunTable := FunTable StringVal.
  Import StringFunTable.
  Open Scope string_scope.
  Example ex1 : get 0 empty = "".
  Proof. reflexivity. Qed.
  Example ex2 : get 0 (set 0 "A" empty) = "A".
  Proof. reflexivity. Qed.
  Example ex3 : get 1 (set 0 "A" empty) = "".
  Proof. reflexivity. Qed.
End FunTableExamples.

Encapsulation

Modules can encapsulate when defined with : instead of <::

Module FunTableEncapsulated (VT : ValType) : (Table with Definition V := VT.V with Definition default := VT.default) :=
  FunTable VT.
Module FunTableEncapsulatedExamples.
  Module StringFunTableEncapsulated := FunTableEncapsulated StringVal.
  Import StringFunTableEncapsulated.
  Open Scope string_scope.
  Example ex1 : get 0 empty = "".
  Proof.
    simpl. Fail reflexivity.
get and empty implementations aren't visible.
    apply get_empty_default.
  Qed.
  Example ex2 : get 0 (set 0 "A" empty) = "A".
  Proof. apply get_set_same. Qed.
  Example ex3 : get 1 (set 0 "A" empty) = "".
  Proof. rewrite get_set_other. apply get_empty_default. auto. Qed.
End FunTableEncapsulatedExamples.

Implementing Table with Lists

You will implement Table with association lists as an exercise.

Implementing Table with BSTs

Tables implemented with functions and association lists are, of course, inefficient. For a more efficient implementation, we can use BSTs.

Module TreeTable (VT : ValType) <: (Table with Definition V := VT.V with Definition default := VT.default).
  Definition V := VT.V.
  Definition default := VT.default.
  Definition key := nat.
  Definition table := tree V.
  Definition empty : table :=
    @empty_tree V.
  Definition get (k : key) (t: table) : V :=
    lookup default k t.
  Definition set (k : key) (v : V) (t : table) : table :=
    insert k v t.
The three basic equations we proved about tree in SearchTree make short work of the theorems we need to prove for Table.

  Theorem get_empty_default: ∀ (k : key),
      get k empty = default.
  Proof.
    apply lookup_empty.
  Qed.
  Theorem get_set_same: ∀ (k : key) (v : V) (t : table),
      get k (set k v t) = v.
  Proof.
    intros. unfold get, set. apply lookup_insert_eq.
  Qed.
  Theorem get_set_other: ∀ (k k' : key) (v : V) (t : table),
      k ≠ k' → get k' (set k v t) = get k' t.
  Proof.
    intros. unfold get, set. apply lookup_insert_neq. assumption.
  Qed.
End TreeTable.

Tables with an elements Operation

Now let's consider a richer interface ETable for Tables that support bound and elements operation.

A First Attempt at ETable


Module Type ETable_first_attempt.
Include all the declarations from Table.
  Include Table.
  Parameter bound : key → table → bool.
  Parameter elements : table → list (key × V).
  Axiom elements_complete : ∀ (k : key) (v : V) (t : table),
      bound k t = true →
      get k t = v →
      In (k, v) (elements t).
  Axiom elements_correct : ∀ (k : key) (v : V) (t : table),
      In (k, v) (elements t) →
      bound k t = true ∧ get k t = v.
End ETable_first_attempt.

We proved in SearchTree that the BST elements operation is correct and complete. So we ought to be able to implement ETable with BSTs. Let's try.

Module TreeETable_first_attempt (VT : ValType) : (ETable_first_attempt with Definition V := VT.V with Definition default := VT.default).
Include all the definitions from TreeTable, instantiated on VT.
  Include TreeTable VT.
  Definition bound (k : key) (t : table) : bool :=
    SearchTree.bound k t.
  Definition elements (t : table) : list (key × V) :=
    SearchTree.elements t.
  Theorem elements_complete : ∀ (k : key) (v : V) (t : table),
      bound k t = true →
      get k t = v →
      In (k, v) (elements t).
  Proof.
    intros k v t Hbound Hlookup. unfold get in Hlookup.
pose proof t as H is equivalent to assert (H : ...the type of t...). { apply t. } but saves some keystrokes.
    pose proof (SearchTree.elements_complete) as Hcomplete.
    unfold elements_complete_spec in Hcomplete.
    apply Hcomplete with default.
    -
Stuck! We don't know that t satisfies the BST invariant.
  Admitted.
  Theorem elements_correct : ∀ (k : key) (v : V) (t : table),
      In (k, v) (elements t) →
      bound k t = true ∧ get k t = v.
  Proof.
    intros k v t Hin.
    pose proof (SearchTree.elements_correct) as Hcorrect.
    unfold elements_correct_spec in Hcorrect.
    apply Hcorrect.
    -
Again stuck because of the BST invariant.
  Admitted.
End TreeETable_first_attempt.

A Second Attempt at ETable


Module Type ETable_second_attempt.
  Include Table.
We declare a function rep_ok in the interface. It exposes only that there is a representation invariant, not what that invariant is.

  Parameter rep_ok : table → Prop.
  Parameter bound : key → table → bool.
  Parameter elements : table → list (key × V).

We use rep_ok as a precondition for values of type table.

  Axiom elements_complete : ∀ (k : key) (v : V) (t : table),
      rep_ok t →
      bound k t = true →
      get k t = v →
      In (k, v) (elements t).
  Axiom elements_correct : ∀ (k : key) (v : V) (t : table),
      rep_ok t →
      In (k, v) (elements t) →
      bound k t = true ∧ get k t = v.
End ETable_second_attempt.

Now we can instantiate rep_ok with BST, and encapsulate that behind an interface.

Module TreeETable_second_attempt (VT : ValType) : (ETable_second_attempt with Definition V := VT.V with Definition default := VT.default).
  Include TreeTable VT.
  Definition rep_ok (t : table) : Prop :=
    BST t.
  Definition bound (k : key) (t : table) : bool :=
    SearchTree.bound k t.
  Definition elements (t : table) : list (key × V) :=
    SearchTree.elements t.
  Theorem elements_complete : ∀ (k : key) (v : V) (t : table),
      rep_ok t →
      bound k t = true →
      get k t = v →
      In (k, v) (elements t).
  Proof.
    intros k v t Hbound Hlookup.
    pose proof SearchTree.elements_complete as Hcomplete.
    unfold elements_complete_spec in Hcomplete.
    apply Hcomplete; (* proof succeeds *) assumption.
  Qed.
  Theorem elements_correct : ∀ (k : key) (v : V) (t : table),
      rep_ok t →
      In (k, v) (elements t) →
      bound k t = true ∧ get k t = v.
  Proof.
    intros k v t Hin.
    pose proof SearchTree.elements_correct as Hcorrect.
    unfold elements_correct_spec in Hcorrect.
    apply Hcorrect; (* proof succeeds *) assumption.
  Qed.
End TreeETable_second_attempt.

But when we try to use that functor, we encounter a problem.

Module StringTreeETable_second_attempt_Examples.
  Module StringTreeETable := TreeETable_second_attempt StringVal.
  Import StringTreeETable.
  Open Scope string_scope.
  Example ex1 :
    In (0, "A") (elements (set 0 "A" (set 1 "B" empty))).
  Proof.
    apply elements_complete.
Stuck! We don't know that empty and set produce trees that satisfy the representation invariant.
  Admitted.
End StringTreeETable_second_attempt_Examples.

A Final Attempt at ETable

We need to expose the fact that the ADT operations produce values that satisfy the representation invariant, i.e., it is a postcondition. That leads us to our third and final attempt, in which we also expose the specification of bound:

Module Type ETable.
  Include Table.
  Parameter rep_ok : table → Prop.
  Parameter bound : key → table → bool.
  Parameter elements : table → list (key × V).
empty and set produce valid representations.

  Axiom empty_ok : rep_ok empty.
  Axiom set_ok : ∀ (k : key) (v : V) (t : table),
      rep_ok t → rep_ok (set k v t).
The specification of bound:

  Axiom bound_empty : ∀ (k : key),
      bound k empty = false.
  Axiom bound_set_same : ∀ (k : key) (v : V) (t : table),
      bound k (set k v t) = true.
  Axiom bound_set_other : ∀ (k k' : key) (v : V) (t : table),
      k ≠ k' → bound k' (set k v t) = bound k' t.
The specification of elements:

  Axiom elements_complete : ∀ (k : key) (v : V) (t : table),
      rep_ok t →
      bound k t = true →
      get k t = v →
      In (k, v) (elements t).
  Axiom elements_correct : ∀ (k : key) (v : V) (t : table),
      rep_ok t →
      In (k, v) (elements t) →
      bound k t = true ∧ get k t = v.
End ETable.

Module TreeETable (VT : ValType) : (ETable with Definition V := VT.V with Definition default := VT.default).
  Include TreeTable VT.
  Definition rep_ok (t : table) : Prop :=
    BST t.
  Definition bound (k : key) (t : table) : bool :=
    SearchTree.bound k t.
  Definition elements (t : table) : list (key × V) :=
    SearchTree.elements t.
  Theorem empty_ok : rep_ok empty.
  Proof.
    apply empty_tree_BST.
  Qed.
  Theorem set_ok : ∀ (k : key) (v : V) (t : table),
      rep_ok t → rep_ok (set k v t).
  Proof.
    apply insert_BST.
  Qed.
  Theorem bound_empty : ∀ (k : key),
      bound k empty = false.
  Proof.
    reflexivity.
  Qed.
  Theorem bound_set_same : ∀ (k : key) (v : V) (t : table),
      bound k (set k v t) = true.
  Proof.
    intros k v t. unfold bound, set. induction t; bdall.
  Qed.
  Theorem bound_set_other : ∀ (k k' : key) (v : V) (t : table),
      k ≠ k' → bound k' (set k v t) = bound k' t.
  Proof.
    intros k k' v t Hneq. unfold bound, set. induction t; bdall.
  Qed.
  Theorem elements_complete : ∀ (k : key) (v : V) (t : table),
      rep_ok t →
      bound k t = true →
      get k t = v →
      In (k, v) (elements t).
  Proof.
    intros k v t Hbound Hlookup.
    pose proof SearchTree.elements_complete as Hcomplete.
    unfold elements_complete_spec in Hcomplete.
    apply Hcomplete; assumption.
  Qed.
  Theorem elements_correct : ∀ (k : key) (v : V) (t : table),
      rep_ok t →
      In (k, v) (elements t) →
      bound k t = true ∧ get k t = v.
  Proof.
    intros k v t. simpl. intros Hin.
    pose proof SearchTree.elements_correct as Hcorrect.
    unfold elements_correct_spec in Hcorrect.
    apply Hcorrect; assumption.
  Qed.
End TreeETable.

Now we can use the table.

Module StringTreeETableExamples.
  Module StringTreeETable := TreeETable StringVal.
  Import StringTreeETable.
  Open Scope string_scope.
  Example ex1 :
    In (0, "A") (elements (set 0 "A" (set 1 "B" empty))).
  Proof.
    apply elements_complete;
      auto using empty_ok, set_ok, bound_set_same, get_set_same.
  Qed.
End StringTreeETableExamples.

Note what we've happily achieved: we can reason about the behavior of an ADT entirely from its specification, rather than depending on the implementation code. This is what specification comments in interfaces attempt to achieve in most real world code. We see here the work that is required to make it fully verifiable.

Model-based Specification

The interfaces above have been based on equational specification of tables. Let's consider model-based specifications. Recall from SearchTree that in this style of specification, we
  • introduce an abstraction function (or relation) that associates a concrete value of the ADT implementation with an abstract value in an already well-understood type; and
  • show that the concrete and abstract operations are related in a sensible way.

We begin by defining a new map operation, bound, and redefining existing operations to make them more clear in the table specification we are about to write.

Definition map_update {V : Type}
           (k : key) (v : V) (m : partial_map V) : partial_map V :=
  update m k v.
Definition map_find {V : Type} := @find V.
Definition empty_map {V : Type} := @Maps.empty V.

Now we can define an interface for tables that includes an abstraction function Abs, and specifications written in terms of it.

Module Type ETableAbs.
  Parameter table : Type.
  Definition key := nat.
  Parameter V : Type.
  Parameter default : V.
  Parameter empty : table.
  Parameter get : key → table → V.
  Parameter set : key → V → table → table.
  Parameter bound : key → table → bool.
  Parameter elements : table → list (key × V).
Note that we reveal the abstract type, but not how Abs converts concrete values to abstract values. That conversion itself is kept abstract.

  Parameter Abs : table → partial_map V.
  Parameter rep_ok : table → Prop.
  Axiom empty_ok :
      rep_ok empty.
  Axiom set_ok : ∀ (k : key) (v : V) (t : table),
      rep_ok t → rep_ok (set k v t).
  Axiom empty_relate :
      Abs empty = empty_map.
  Axiom bound_relate : ∀ (t : table) (k : key),
      rep_ok t →
      map_bound k (Abs t) = bound k t.
  Axiom lookup_relate : ∀ (t : table) (k : key),
      rep_ok t →
      map_find default k (Abs t) = get k t.
  Axiom insert_relate : ∀ (t : table) (k : key) (v : V),
      rep_ok t →
      map_update k v (Abs t) = Abs (set k v t).
  Axiom elements_relate : ∀ (t : table),
      rep_ok t →
      Abs t = map_of_list (elements t).
End ETableAbs.

Summary of ADT Verification

With equational specifications:
  • Define a representation invariant to characterize which values of the representation type are legal. Prove that each operation on the representation type preserves the representation invariant.
  • Using the representation invariant, verify the equational specification.
With model-based specifications:
  • Define and verify preservation of the the representation invariant.
  • Define an abstraction function that relates the representation type to another type that is easier to reason about.
  • Prove that operations of the abstract and concrete types commute with the abstraction function.

Representation Invariants and Subset Types

Representation invariants should be part of the type, not an extra clause in specifications.
Subset types make it possible:
      {x : A | P}
That's the type of all values x of type A that satisfy property P.

Example: The Even Naturals

The type of all even naturals:

Definition even_nat := {x : nat | Nat.Even x}.
Fail Definition two : even_nat := 2.
Lemma Even2 : Nat.Even 2.
Proof. ∃ 1. reflexivity. Qed.
Now we can provide that proof to convince Coq two is an even_nat. We can do that with function exist, which is suggestive of "there exists an x : A such that P x."

Check exist : ∀ {A : Type} (P : A → Prop) (x : A), P x → {x : A | P x}.
Definition two : even_nat := exist Nat.Even 2 Even2.
Definition two' : even_nat.
Proof.
  apply exist with (x := 2).
  ∃ 1. reflexivity.
Defined.

A value of type even_nat is like a "package" containing the nat and the proof that the nat is even. We have to use functions to extract those components from the package.

Fail Example plus_two : 1 + two = 3.
Check proj1_sig : ∀ {A : Type} {P : A → Prop} (e : {x : A | P x}), A.
Example plus_two : 1 + proj1_sig two = 3.
Proof. reflexivity. Qed.
Check proj2_sig : ∀ {A : Type} {P : A → Prop} (e : {x : A | P x}), P (proj1_sig e).
Example Even2' : Nat.Even 2 := proj2_sig two.

Defining Subset Types


Module SigSandbox.
Subset types are just a syntactic notation for sig:

  Inductive sig {A : Type} (P : A → Prop) : Type :=
  | exist (x : A) : P x → sig P.
  Notation "{ x : A | P }" := (sig A (fun x ⇒ P)).
The name sig is short for the Greek capital letter sigma, because subset types are similar to something known in type theory as sigma types, aka dependent sums.
Subset types and existential quantification are quite similar. Recall how the latter is defined:

  Inductive ex {A : Type} (P : A → Prop) : Prop :=
  | ex_intro (x : A) : P x → ex P.

  Definition proj1_sig {A : Type} {P : A → Prop} (e : sig P) : A :=
    match e with
    | exist _ x _ ⇒ x
    end.
  Definition proj2_sig {A : Type} {P : A → Prop} (e : sig P) : P (proj1_sig e) :=
    match e with
    | exist _ _ p ⇒ p
    end.
  Fail Definition proj1_ex {A : Type} {P : A → Prop} (e : ex P) : A :=
    match e with
    | ex_intro _ x _ ⇒ x
    end.
End SigSandbox.

Using Subset Types to Enforce the BST Invariant


Module Type ETableSubset.
  Include Table.
Note: no rep_ok anywhere.

  Parameter bound : key → table → bool.
  Parameter elements : table → list (key × V).
  Axiom bound_empty : ∀ (k : key),
      bound k empty = false.
  Axiom bound_set_same : ∀ (k : key) (v : V) (t : table),
      bound k (set k v t) = true.
  Axiom bound_set_other : ∀ (k k' : key) (v : V) (t : table),
      k ≠ k' → bound k' (set k v t) = bound k' t.
  Axiom elements_complete : ∀ (k : key) (v : V) (t : table),
      bound k t = true →
      get k t = v →
      In (k, v) (elements t).
  Axiom elements_correct : ∀ (k : key) (v : V) (t : table),
      In (k, v) (elements t) →
      bound k t = true ∧ get k t = v.
End ETableSubset.

Module TreeETableSubset (VT : ValType) : (ETableSubset with Definition V := VT.V with Definition default := VT.default).
  Definition V := VT.V.
  Definition default := VT.default.
  Definition key := nat.
table now is required to enforce BST.
  Definition table := { t : tree V | BST t }.
Now instead of proving separate theorems that operations return valid representations, the proofs are "baked in" to the operations.
  Definition empty : table.
  Proof.
    apply (exist _ empty_tree).
    apply empty_tree_BST.
  Defined.
Now we insert a projection to get to the tree.
  Definition get (k : key) (t : table) : V :=
    lookup default k (proj1_sig t).
  Definition set (k : key) (v : V) (t : table) : table.
  Proof.
    destruct t as [t Ht].
    apply (exist _ (insert k v t)).
    apply insert_BST. assumption.
  Defined.
  Definition bound (k : key) (t : table) : bool :=
    SearchTree.bound k (proj1_sig t).
  Definition elements (t : table) : list (key × V) :=
    elements (proj1_sig t).
  Theorem get_empty_default: ∀ (k : key),
      get k empty = default.
  Proof.
    apply lookup_empty.
  Qed.
Now the rest of the proofs require minor modifications to destruct the table to get the tree and the representation invariant, and use the latter where needed.

  Theorem get_set_same: ∀ (k : key) (v : V) (t : table),
      get k (set k v t) = v.
  Proof.
    intros. unfold get, set.
    destruct t as [t Hbst]. simpl.
    apply lookup_insert_eq.
  Qed.
  Theorem get_set_other: ∀ (k k' : key) (v : V) (t : table),
      k ≠ k' → get k' (set k v t) = get k' t.
  Proof.
    intros. unfold get, set.
    destruct t as [t Hbst]. simpl.
    apply lookup_insert_neq. assumption.
  Qed.
  Theorem bound_empty : ∀ (k : key),
      bound k empty = false.
  Proof.
    reflexivity.
  Qed.
  Theorem bound_set_same : ∀ (k : key) (v : V) (t : table),
      bound k (set k v t) = true.
  Proof.
    intros k v t. unfold bound, set.
    destruct t as [t Hbst]. simpl in ×.
    induction t; inv Hbst; bdall.
  Qed.
  Theorem bound_set_other : ∀ (k k' : key) (v : V) (t : table),
      k ≠ k' → bound k' (set k v t) = bound k' t.
  Proof.
    intros k k' v t Hneq. unfold bound, set.
    destruct t as [t Hbst]. simpl in ×.
    induction t; inv Hbst; bdall.
  Qed.
  Theorem elements_complete : ∀ (k : key) (v : V) (t : table),
      bound k t = true →
      get k t = v →
      In (k, v) (elements t).
  Proof.
    intros k v t Hbound Hlookup.
    pose proof SearchTree.elements_complete as Hcomplete.
    unfold elements_complete_spec in Hcomplete.
    apply Hcomplete with default; try assumption.
    destruct t as [t Hbst]. assumption.
  Qed.
  Theorem elements_correct : ∀ (k : key) (v : V) (t : table),
      In (k, v) (elements t) →
      bound k t = true ∧ get k t = v.
  Proof.
    intros k v t. simpl. intros Hin.
    pose proof SearchTree.elements_correct as Hcorrect.
    unfold elements_correct_spec in Hcorrect.
    apply Hcorrect; try assumption.
    destruct t as [t Hbst]. assumption.
  Qed.
End TreeETableSubset.