diff --git a/DataAbstraction_template.v b/DataAbstraction_template.v
new file mode 100644
index 0000000..1d4b901
--- /dev/null
+++ b/DataAbstraction_template.v
@@ -0,0 +1,1561 @@
+Require Import Frap.
+
+Set Implicit Arguments.
+
+
+(** * Specification styles for data abstraction *)
+
+(* One of the classic formalisms for data abstraction is the *algebraic* style,
+ * where requirements on implementations are written out as quantified
+ * equalities.  Any implementation must satisfy these equalities, but we grant
+ * implementations freedom in internal details. *)
+Module Algebraic.
+  (* Here's an example of an algebraic interface or *specification* ("spec" for
+   * short).  It's for purely function queues, which follow first-in-first-out
+   * disciplines. *)
+  Module Type QUEUE.
+    Parameter t : Set -> Set.
+
+    Parameter empty : forall A, t A.
+    Parameter enqueue : forall A, t A -> A -> t A.
+    Parameter dequeue : forall A, t A -> option (t A * A).
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    Axiom dequeue_empty : forall A,
+        dequeue (empty A) = None.
+    Axiom empty_dequeue : forall A (q : t A),
+        dequeue q = None -> q = empty A.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    Axiom dequeue_enqueue : forall A (q : t A) x,
+        dequeue (enqueue q x) = Some (match dequeue q with
+                                      | None => (empty A, x)
+                                      | Some (q', y) => (enqueue q' x, y)
+                                      end).
+  End QUEUE.
+
+  (* First, there is a fairly straightforward implementation with lists. *)
+  Module ListQueue : QUEUE.
+    Definition t : Set -> Set := list.
+
+    Definition empty A : t A. Admitted.
+    Definition enqueue A (q : t A) (x : A) : t A. Admitted.
+    Fixpoint dequeue A (q : t A) : option (t A * A). Admitted.
+
+    Theorem dequeue_empty : forall A, dequeue (empty A) = None.
+    Proof.
+    Admitted.
+
+    Theorem empty_dequeue : forall A (q : t A),
+        dequeue q = None -> q = empty A.
+    Proof.
+    Admitted.
+
+    Theorem dequeue_enqueue : forall A (q : t A) x,
+        dequeue (enqueue q x) = Some (match dequeue q with
+                                      | None => (empty A, x)
+                                      | Some (q', y) => (enqueue q' x, y)
+                                      end).
+    Proof.
+    Admitted.
+  End ListQueue.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+  Module ReversedListQueue : QUEUE.
+    Definition t : Set -> Set := list.
+
+    Definition empty A : t A. Admitted.
+    Definition enqueue A (q : t A) (x : A) : t A. Admitted.
+    Fixpoint dequeue A (q : t A) : option (t A * A). Admitted.
+
+    Theorem dequeue_empty : forall A, dequeue (empty A) = None.
+    Proof.
+    Admitted.
+
+    Theorem empty_dequeue : forall A (q : t A),
+        dequeue q = None -> q = empty A.
+    Proof.
+    Admitted.
+
+    Theorem dequeue_enqueue : forall A (q : t A) x,
+        dequeue (enqueue q x) = Some (match dequeue q with
+                                      | None => (empty A, x)
+                                      | Some (q', y) => (enqueue q' x, y)
+                                      end).
+    Proof.
+    Admitted.
+  End ReversedListQueue.
+
+
+
+
+
+  Module DelayedSum (Q : QUEUE).
+    (* First, the function to enqueue the first [n] natural numbers. *)
+    Fixpoint makeQueue (n : nat) (q : Q.t nat) : Q.t nat :=
+      match n with
+      | 0 => q
+      | S n' => makeQueue n' (Q.enqueue q n')
+      end.
+
+    (* Next, the function to dequeue repeatedly, keeping a sum. *)
+    Fixpoint computeSum (n : nat) (q : Q.t nat) : nat :=
+      match n with
+      | 0 => 0
+      | S n' => match Q.dequeue q with
+                | None => 0
+                | Some (q', v) => v + computeSum n' q'
+                end
+      end.
+
+    (* This function gives the expected answer, in a simpler form, of
+     * [computeSum] after [makeQueue]. *)
+    Fixpoint sumUpto (n : nat) : nat :=
+      match n with
+      | 0 => 0
+      | S n' => n' + sumUpto n'
+      end.
+
+    Theorem computeSum_ok : forall n,
+        computeSum n (makeQueue n (Q.empty nat)) = sumUpto n.
+    Proof.
+    Admitted.
+  End DelayedSum.
+End Algebraic.
+
+
+
+
+
+
+
+
+
+
+
+
+
+Module AlgebraicWithEquivalenceRelation.
+  Module Type QUEUE.
+    Parameter t : Set -> Set.
+
+    Parameter empty : forall A, t A.
+    Parameter enqueue : forall A, t A -> A -> t A.
+    Parameter dequeue : forall A, t A -> option (t A * A).
+
+    (* v-- New part! *)
+    Parameter equiv : forall A, t A -> t A -> Prop.
+    Infix "~=" := equiv (at level 70).
+
+    (* It really is an equivalence relation. *)
+    Axiom equiv_refl : forall A (a : t A), a ~= a.
+    Axiom equiv_sym : forall A (a b : t A), a ~= b -> b ~= a.
+    Axiom equiv_trans : forall A (a b c : t A), a ~= b -> b ~= c -> a ~= c.
+
+    Axiom equiv_enqueue : forall A (a b : t A) (x : A),
+        a ~= b
+        -> enqueue a x ~= enqueue b x.
+
+    (* We define a derived relation for results of [dequeue]. *)
+    Definition dequeue_equiv A (a b : option (t A * A)) :=
+      match a, b with
+      | None, None => True
+      | Some (qa, xa), Some (qb, xb) => qa ~= qb /\ xa = xb
+      | _, _ => False
+      end.
+
+    Infix "~~=" := dequeue_equiv (at level 70).
+
+    Axiom equiv_dequeue : forall A (a b : t A),
+        a ~= b
+        -> dequeue a ~~= dequeue b.
+
+    (* We retain the three axioms from the prior interface, using our fancy
+     * relation instead of equality on queues. *)
+
+    Axiom dequeue_empty : forall A,
+        dequeue (empty A) = None.
+    Axiom empty_dequeue : forall A (q : t A),
+        dequeue q = None -> q ~= empty A.
+
+    Axiom dequeue_enqueue : forall A (q : t A) x,
+        dequeue (enqueue q x)
+        ~~= match dequeue q with
+            | None => Some (empty A, x)
+            | Some (q', y) => Some (enqueue q' x, y)
+            end.
+  End QUEUE.
+
+  (* It's easy to redo [ListQueue], specifying normal equality for the
+   * equivalence relation. *)
+  Module ListQueue : QUEUE.
+    Definition t : Set -> Set := list.
+
+    Definition empty A : t A := nil.
+    Definition enqueue A (q : t A) (x : A) : t A := x :: q.
+    Fixpoint dequeue A (q : t A) : option (t A * A) :=
+      match q with
+      | [] => None
+      | x :: q' =>
+        match dequeue q' with
+        | None => Some ([], x)
+        | Some (q'', y) => Some (x :: q'', y)
+        end
+      end.
+
+    Definition equiv A (a b : t A) := a = b.
+    Infix "~=" := equiv (at level 70).
+
+    Theorem equiv_refl : forall A (a : t A), a ~= a.
+    Proof.
+      equality.
+    Qed.
+
+    Theorem equiv_sym : forall A (a b : t A), a ~= b -> b ~= a.
+    Proof.
+      equality.
+    Qed.
+
+    Theorem equiv_trans : forall A (a b c : t A), a ~= b -> b ~= c -> a ~= c.
+    Proof.
+      equality.
+    Qed.
+
+    Theorem equiv_enqueue : forall A (a b : t A) (x : A),
+        a ~= b
+        -> enqueue a x ~= enqueue b x.
+    Proof.
+      unfold equiv; equality.
+    Qed.
+
+    Definition dequeue_equiv A (a b : option (t A * A)) :=
+      match a, b with
+      | None, None => True
+      | Some (qa, xa), Some (qb, xb) => qa ~= qb /\ xa = xb
+      | _, _ => False
+      end.
+
+    Infix "~~=" := dequeue_equiv (at level 70).
+
+    Theorem equiv_dequeue : forall A (a b : t A),
+        a ~= b
+        -> dequeue a ~~= dequeue b.
+    Proof.
+      unfold equiv, dequeue_equiv; simplify.
+      rewrite H.
+      cases (dequeue b).
+
+      cases p.
+      equality.
+
+      propositional.
+    Qed.
+
+    Theorem dequeue_empty : forall A, dequeue (empty A) = None.
+    Proof.
+      simplify.
+      equality.
+    Qed.
+
+    Theorem empty_dequeue : forall A (q : t A),
+        dequeue q = None -> q ~= empty A.
+    Proof.
+      simplify.
+      cases q.
+
+      simplify.
+      unfold equiv.
+      equality.
+
+      simplify.
+      cases (dequeue q).
+      cases p.
+      equality.
+      equality.
+    Qed.
+
+    Theorem dequeue_enqueue : forall A (q : t A) x,
+        dequeue (enqueue q x)
+        ~~= match dequeue q with
+            | None => Some (empty A, x)
+            | Some (q', y) => Some (enqueue q' x, y)
+            end.
+    Proof.
+      unfold dequeue_equiv, equiv.
+      induct q; simplify.
+
+      equality.
+
+      cases (dequeue q).
+
+      cases p.
+      equality.
+      equality.
+    Qed.
+  End ListQueue.
+
+  (* However, now we can implement the classic two-stacks optimized queue! *)
+  Module TwoStacksQueue : QUEUE.
+    Record stackpair (A : Set) := {
+      EnqueueHere : list A;
+      DequeueHere : list A
+    }.
+
+    Definition t := stackpair.
+
+    Definition empty A : t A := {|
+      EnqueueHere := [];
+      DequeueHere := []
+    |}.
+    Definition enqueue A (q : t A) (x : A) : t A := {|
+      EnqueueHere := x :: q.(EnqueueHere);
+      DequeueHere := q.(DequeueHere)
+    |}.
+    Definition dequeue A (q : t A) : option (t A * A) :=
+      match q.(DequeueHere) with
+      | x :: dq => Some ({| EnqueueHere := q.(EnqueueHere);
+                            DequeueHere := dq |}, x)
+      | [] =>
+        match rev q.(EnqueueHere) with
+        | [] => None
+        | x :: eq => Some ({| EnqueueHere := [];
+                              DequeueHere := eq |}, x)
+        end
+      end.
+
+    Definition equiv A (a b : t A) : Prop. Admitted.
+    Infix "~=" := equiv (at level 70).
+
+    Theorem equiv_refl : forall A (a : t A), a ~= a.
+    Proof.
+    Admitted.
+
+    Theorem equiv_sym : forall A (a b : t A), a ~= b -> b ~= a.
+    Proof.
+    Admitted.
+
+    Theorem equiv_trans : forall A (a b c : t A), a ~= b -> b ~= c -> a ~= c.
+    Proof.
+    Admitted.
+
+    Theorem equiv_enqueue : forall A (a b : t A) (x : A),
+        a ~= b
+        -> enqueue a x ~= enqueue b x.
+    Proof.
+    Admitted.
+
+    Definition dequeue_equiv A (a b : option (t A * A)) :=
+      match a, b with
+      | None, None => True
+      | Some (qa, xa), Some (qb, xb) => qa ~= qb /\ xa = xb
+      | _, _ => False
+      end.
+
+    Infix "~~=" := dequeue_equiv (at level 70).
+
+    Theorem equiv_dequeue : forall A (a b : t A),
+        a ~= b
+        -> dequeue a ~~= dequeue b.
+    Proof.
+    Admitted.
+      (*unfold equiv, dequeue_equiv, elements, dequeue; simplify.
+      cases (DequeueHere a); simplify.
+      cases (rev (EnqueueHere a)); simplify.
+      cases (DequeueHere b); simplify.
+      cases (rev (EnqueueHere b)); simplify.
+      propositional.
+      SearchRewrite (_ ++ []).
+      rewrite app_nil_r in H.
+      rewrite app_nil_r in H.
+      equality.
+      cases (EnqueueHere a); simplify.
+      cases (EnqueueHere b); simplify.
+      cases (rev l); simplify.
+      equality.
+      equality.
+      equality.
+      cases (rev l0); simplify.
+      equality.
+      equality.
+      cases (DequeueHere b); simplify.
+      cases (rev (EnqueueHere b)); simplify.
+      rewrite app_nil_r in H.
+      rewrite app_nil_r in H.
+      equality.
+      rewrite app_nil_r in H.
+      rewrite app_nil_r in H.
+      equality.
+      rewrite app_nil_r in H.
+      rewrite H in Heq0.
+      SearchRewrite (rev (_ ++ _)).
+      rewrite rev_app_distr in Heq0.
+      rewrite rev_app_distr in Heq0.
+      simplify.
+      invert Heq0.
+      unfold equiv, elements.
+      simplify.
+      rewrite rev_app_distr.
+      SearchRewrite (rev (rev _)).
+      rewrite rev_involutive.
+      rewrite rev_involutive.
+      equality.
+      cases (DequeueHere b); simplify.
+      cases (rev (EnqueueHere b)); simplify.
+      rewrite app_nil_r in H.
+      rewrite <- H in Heq1.
+      cases (EnqueueHere a); simplify.
+      cases (rev l); simplify.
+      equality.
+      rewrite rev_app_distr in Heq1.
+      simplify.
+      equality.
+      rewrite rev_app_distr in Heq1.
+      rewrite rev_app_distr in Heq1.
+      simplify.
+      equality.
+      unfold equiv, elements.
+      simplify.
+      rewrite app_nil_r in H.
+      rewrite <- H in Heq1.
+      rewrite rev_app_distr in Heq1.      rewrite rev_app_distr in Heq1.
+      simplify.
+      invert Heq1.
+      rewrite rev_involutive.
+      rewrite rev_app_distr.
+      rewrite rev_involutive.
+      equality.
+      unfold equiv, elements.
+      simplify.
+      SearchAbout app cons nil.
+      apply app_inj_tail.
+      rewrite <- app_assoc.
+      rewrite <- app_assoc.
+      assumption.
+    Qed.*)
+
+    Theorem dequeue_empty : forall A, dequeue (empty A) = None.
+    Proof.
+      simplify.
+      equality.
+    Qed.
+
+    Theorem empty_dequeue : forall A (q : t A),
+        dequeue q = None -> q ~= empty A.
+    Proof.
+    Admitted.
+      (*simplify.
+      cases q.
+      unfold dequeue in *.
+      simplify.
+      cases DequeueHere0.
+      cases (rev EnqueueHere0).
+      cases EnqueueHere0.
+      equality.
+      simplify.
+      cases (rev EnqueueHere0); simplify.
+      equality.
+      equality.
+      equality.
+      equality.
+    Qed.*)
+
+    Theorem dequeue_enqueue : forall A (q : t A) x,
+        dequeue (enqueue q x)
+        ~~= match dequeue q with
+            | None => Some (empty A, x)
+            | Some (q', y) => Some (enqueue q' x, y)
+            end.
+    Proof.
+    Admitted.
+      (*unfold dequeue_equiv, equiv; simplify.
+      cases q; simplify.
+      unfold dequeue, enqueue; simplify.
+      cases DequeueHere0; simplify.
+
+      cases (rev EnqueueHere0); simplify.
+
+      equality.
+
+      unfold elements; simplify.
+      SearchRewrite (rev (_ ++ _)).
+      rewrite rev_app_distr.
+      simplify.
+      equality.
+
+      equality.
+    Qed.*)
+  End TwoStacksQueue.
+
+  Module DelayedSum (Q : QUEUE).
+    Fixpoint makeQueue (n : nat) (q : Q.t nat) : Q.t nat :=
+      match n with
+      | 0 => q
+      | S n' => makeQueue n' (Q.enqueue q n')
+      end.
+
+    Fixpoint computeSum (n : nat) (q : Q.t nat) : nat :=
+      match n with
+      | 0 => 0
+      | S n' => match Q.dequeue q with
+                | None => 0
+                | Some (q', v) => v + computeSum n' q'
+                end
+      end.
+
+    Fixpoint sumUpto (n : nat) : nat :=
+      match n with
+      | 0 => 0
+      | S n' => n' + sumUpto n'
+      end.
+
+    Infix "~=" := Q.equiv (at level 70).
+    Infix "~~=" := Q.dequeue_equiv (at level 70).
+
+    Lemma makeQueue_congruence : forall n a b,
+        a ~= b
+        -> makeQueue n a ~= makeQueue n b.
+    Proof.
+      induct n; simplify.
+
+      assumption.
+
+      apply IHn.
+      apply Q.equiv_enqueue.
+      assumption.
+    Qed.
+
+    Lemma dequeue_makeQueue : forall n q,
+        Q.dequeue (makeQueue n q)
+        ~~= match Q.dequeue q with
+            | Some (q', v) => Some (makeQueue n q', v)
+            | None =>
+              match n with
+              | 0 => None
+              | S n' => Some (makeQueue n' q, n')
+              end
+            end.
+    Proof.
+      induct n.
+
+      simplify.
+      cases (Q.dequeue q).
+      cases p.
+      unfold Q.dequeue_equiv.
+      propositional.
+      apply Q.equiv_refl.
+      unfold Q.dequeue_equiv.
+      propositional.
+
+      simplify.
+      unfold Q.dequeue_equiv in *.
+      specialize (IHn (Q.enqueue q n)).
+      cases (Q.dequeue (makeQueue n (Q.enqueue q n))).
+
+      cases p.
+      pose proof (Q.dequeue_enqueue q n).
+      unfold Q.dequeue_equiv in *.
+      cases (Q.dequeue (Q.enqueue q n)).
+
+      cases p.
+      cases (Q.dequeue q).
+
+      cases p.
+      propositional.
+      apply Q.equiv_trans with (b := makeQueue n t0).
+      assumption.
+      apply makeQueue_congruence.
+      assumption.
+      equality.
+
+      propositional.
+      apply Q.equiv_trans with (b := makeQueue n t0).
+      assumption.
+      apply makeQueue_congruence.
+      apply Q.equiv_trans with (b := Q.empty nat).
+      assumption.
+      apply Q.equiv_sym.
+      apply Q.empty_dequeue.
+      assumption.
+      equality.
+
+      cases (Q.dequeue q).
+
+      cases p.
+      propositional.
+
+      propositional.
+
+      pose proof (Q.dequeue_enqueue q n).
+      unfold Q.dequeue_equiv in H.
+      cases (Q.dequeue (Q.enqueue q n)).
+
+      cases p.
+      propositional.
+
+      cases (Q.dequeue q).
+
+      cases p.
+      propositional.
+
+      propositional.
+    Qed.
+
+    Theorem computeSum_congruence : forall n a b,
+        a ~= b
+        -> computeSum n a = computeSum n b.
+    Proof.
+      induct n.
+
+      simplify.
+      equality.
+
+      simplify.
+      pose proof (Q.equiv_dequeue H).
+      unfold Q.dequeue_equiv in H0.
+      cases (Q.dequeue a).
+
+      cases p.
+      cases (Q.dequeue b).
+      cases p.
+      rewrite IHn with (b := t0).
+      equality.
+      equality.
+      propositional.
+
+      cases (Q.dequeue b).
+      propositional.
+      equality.
+    Qed.
+
+    Theorem computeSum_ok : forall n,
+        computeSum n (makeQueue n (Q.empty nat)) = sumUpto n.
+    Proof.
+      induct n.
+
+      simplify.
+      equality.
+
+      simplify.
+      pose proof (dequeue_makeQueue n (Q.enqueue (Q.empty nat) n)).
+      unfold Q.dequeue_equiv in H.
+      cases (Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n))).
+
+      cases p.
+      pose proof (Q.dequeue_enqueue (Q.empty nat) n).
+      unfold Q.dequeue_equiv in H0.
+      cases (Q.dequeue (Q.enqueue (Q.empty nat) n)).
+
+      cases p.
+      rewrite Q.dequeue_empty in H0.
+      propositional.
+      f_equal.
+      equality.
+      rewrite <- IHn.
+      
+      apply computeSum_congruence.
+      apply Q.equiv_trans with (b := makeQueue n t0).
+      assumption.
+      apply makeQueue_congruence.
+      assumption.
+
+      rewrite Q.dequeue_empty in H0.
+      propositional.
+
+      pose proof (Q.dequeue_enqueue (Q.empty nat) n).
+      unfold Q.dequeue_equiv in H0.
+      cases (Q.dequeue (Q.enqueue (Q.empty nat) n)).
+
+      cases p.
+      propositional.
+
+      rewrite Q.dequeue_empty in H0.
+      propositional.
+    Qed.
+  End DelayedSum.
+End AlgebraicWithEquivalenceRelation.
+
+Module RepFunction.
+  Module Type QUEUE.
+    Parameter t : Set -> Set.
+
+    Parameter empty : forall A, t A.
+    Parameter enqueue : forall A, t A -> A -> t A.
+    Parameter dequeue : forall A, t A -> option (t A * A).
+
+    Parameter rep : forall A, t A -> list A.
+
+    (* Fill in laws here. *)
+  End QUEUE.
+
+  Module ListQueue : QUEUE.
+    Definition t : Set -> Set := list.
+
+    Definition empty A : t A := nil.
+    Definition enqueue A (q : t A) (x : A) : t A := x :: q.
+    Fixpoint dequeue A (q : t A) : option (t A * A) :=
+      match q with
+      | [] => None
+      | x :: q' =>
+        match dequeue q' with
+        | None => Some ([], x)
+        | Some (q'', y) => Some (x :: q'', y)
+        end
+      end.
+
+    Definition rep A (q : t A) : list A. Admitted.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    (*Theorem empty_rep : forall A,
+        rep (empty A) = [].
+    Proof.
+      equality.
+    Qed.
+
+    Theorem enqueue_rep : forall A (q : t A) x,
+        rep (enqueue q x) = x :: rep q.
+    Proof.
+      equality.
+    Qed.
+
+    Theorem dequeue_empty : forall A (q : t A),
+        rep q = []
+        -> dequeue q = None.
+    Proof.
+      unfold rep; simplify.
+      rewrite H.
+      equality.
+    Qed.
+
+    Theorem dequeue_nonempty : forall A (q : t A) xs x,
+        rep q = xs ++ [x]
+        -> exists q', dequeue q = Some (q', x) /\ rep q' = xs.
+    Proof.
+      unfold rep; induct q.
+
+      simplify.
+      cases xs; simplify.
+      equality.
+      equality.
+
+      simplify.
+      cases xs; simplify.
+      invert H; simplify.
+      exists [].
+      equality.
+
+      invert H.
+      assert (exists q' : t A, dequeue (xs ++ [x]) = Some (q', x) /\ q' = xs).
+      apply IHq.
+      equality.
+      first_order.
+      rewrite H.
+      exists (a0 :: x0).
+      equality.
+    Qed.*)
+  End ListQueue.
+
+  Module TwoStacksQueue : QUEUE.
+    Record stackpair (A : Set) := {
+      EnqueueHere : list A;
+      DequeueHere : list A
+    }.
+
+    Definition t := stackpair.
+
+    Definition empty A : t A := {|
+      EnqueueHere := [];
+      DequeueHere := []
+    |}.
+    Definition enqueue A (q : t A) (x : A) : t A := {|
+      EnqueueHere := x :: q.(EnqueueHere);
+      DequeueHere := q.(DequeueHere)
+    |}.
+    Definition dequeue A (q : t A) : option (t A * A) :=
+      match q.(DequeueHere) with
+      | x :: dq => Some ({| EnqueueHere := q.(EnqueueHere);
+                            DequeueHere := dq |}, x)
+      | [] =>
+        match rev q.(EnqueueHere) with
+        | [] => None
+        | x :: eq => Some ({| EnqueueHere := [];
+                              DequeueHere := eq |}, x)
+        end
+      end.
+
+    Definition rep A (q : t A) : list A. Admitted.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+    (*Theorem empty_rep : forall A,
+        rep (empty A) = [].
+    Proof.
+      equality.
+    Qed.
+
+    Theorem enqueue_rep : forall A (q : t A) x,
+        rep (enqueue q x) = x :: rep q.
+    Proof.
+      equality.
+    Qed.
+
+    Theorem dequeue_empty : forall A (q : t A),
+        rep q = []
+        -> dequeue q = None.
+    Proof.
+      unfold rep, dequeue; simplify.
+      cases (DequeueHere q); simplify.
+      rewrite app_nil_r in H.
+      rewrite H.
+      simplify.
+      equality.
+      cases (EnqueueHere q); simplify.
+      cases (rev l); simplify.
+      equality.
+      equality.
+      equality.
+    Qed.
+
+    Theorem dequeue_nonempty : forall A (q : t A) xs x,
+        rep q = xs ++ [x]
+        -> exists q', dequeue q = Some (q', x) /\ rep q' = xs.
+    Proof.
+      unfold rep, dequeue; simplify.
+
+      cases (DequeueHere q); simplify.
+
+      rewrite app_nil_r in H.
+      rewrite H.
+      rewrite rev_app_distr; simplify.
+      exists {| EnqueueHere := []; DequeueHere := rev xs |}.
+      simplify.
+      rewrite rev_involutive.
+      equality.
+
+      exists {| EnqueueHere := EnqueueHere q; DequeueHere := l |}.
+      simplify.
+      rewrite app_assoc in H.
+      apply app_inj_tail in H.
+      propositional.
+      rewrite H1.
+      equality.
+    Qed.*)
+  End TwoStacksQueue.
+
+  Module DelayedSum (Q : QUEUE).
+    Fixpoint makeQueue (n : nat) (q : Q.t nat) : Q.t nat :=
+      match n with
+      | 0 => q
+      | S n' => makeQueue n' (Q.enqueue q n')
+      end.
+
+    Fixpoint computeSum (n : nat) (q : Q.t nat) : nat :=
+      match n with
+      | 0 => 0
+      | S n' => match Q.dequeue q with
+                | None => 0
+                | Some (q', v) => v + computeSum n' q'
+                end
+      end.
+
+    Fixpoint sumUpto (n : nat) : nat :=
+      match n with
+      | 0 => 0
+      | S n' => n' + sumUpto n'
+      end.
+
+    Fixpoint upto (n : nat) : list nat :=
+      match n with
+      | 0 => []
+      | S n' => upto n' ++ [n']
+      end.
+
+    Theorem computeSum_ok : forall n,
+        computeSum n (makeQueue n (Q.empty nat)) = sumUpto n.
+    Proof.
+    Admitted.
+  End DelayedSum.
+End RepFunction.
+
+
+(** * Data abstraction with fixed parameter types *)
+
+Module Type FINITE_SET.
+  Parameter key : Set. (* What type of data may be added to these sets? *)
+  Parameter t : Set.   (* What is the type of sets themselves? *)
+
+  Parameter empty : t.
+  Parameter add : t -> key -> t.
+  Parameter member : t -> key -> bool.
+
+  Axiom member_empty : forall k, member empty k = false.
+
+  Axiom member_add_eq : forall k s,
+      member (add s k) k = true.
+  Axiom member_add_noteq : forall k1 k2 s,
+      k1 <> k2
+      -> member (add s k1) k2 = member s k2.
+
+  Axiom decidable_equality : forall a b : key, a = b \/ a <> b.
+  (* ^-- This one may be surprising. *)
+End FINITE_SET.
+
+Module Type SET_WITH_EQUALITY.
+  Parameter t : Set.
+  Parameter equal : t -> t -> bool.
+
+  Axiom equal_ok : forall a b, if equal a b then a = b else a <> b.
+End SET_WITH_EQUALITY.
+
+Module ListSet(SE : SET_WITH_EQUALITY) <: FINITE_SET with Definition key := SE.t.
+  Definition key := SE.t.
+  Definition t := list SE.t.
+
+  Definition empty : t := [].
+  Definition add (s : t) (k : key) : t := k :: s.
+  Fixpoint member (s : t) (k : key) : bool :=
+    match s with
+    | [] => false
+    | k' :: s' => SE.equal k' k || member s' k
+    end.
+
+  Theorem member_empty : forall k, member empty k = false.
+  Proof.
+    simplify.
+    equality.
+  Qed.
+
+  Theorem member_add_eq : forall k s,
+      member (add s k) k = true.
+  Proof.
+    simplify.
+    pose proof (SE.equal_ok k k).
+    cases (SE.equal k k); simplify.
+    equality.
+    equality.
+  Qed.
+
+  Theorem member_add_noteq : forall k1 k2 s,
+      k1 <> k2
+      -> member (add s k1) k2 = member s k2.
+  Proof.
+    simplify.
+    pose proof (SE.equal_ok k1 k2).
+    cases (SE.equal k1 k2); simplify.
+    equality.
+    equality.
+  Qed.
+
+  Theorem decidable_equality : forall a b : key, a = b \/ a <> b.
+  Proof.
+    simplify.
+    pose proof (SE.equal_ok a b).
+    cases (SE.equal a b); propositional.
+  Qed.
+End ListSet.
+
+(* Here's an example decidable-equality type for natural numbers. *)
+Module NatWithEquality <: SET_WITH_EQUALITY with Definition t := nat.
+  Definition t := nat.
+
+  Fixpoint equal (a b : nat) : bool :=
+    match a, b with
+    | 0, 0 => true
+    | S a', S b' => equal a' b'
+    | _, _ => false
+    end.
+
+  Theorem equal_ok : forall a b, if equal a b then a = b else a <> b.
+  Proof.
+    induct a; simplify.
+
+    cases b.
+    equality.
+    equality.
+
+    cases b.
+    equality.
+    specialize (IHa b).
+    cases (equal a b).
+    equality.
+    equality.
+  Qed.
+End NatWithEquality.
+
+(* And here's how to instantiate the generic set for the naturals. *)
+Module NatSet := ListSet(NatWithEquality).
+
+(* Now, some generic client code, for testing duplicate-freeness of lists. *)
+Module FindDuplicates (FS : FINITE_SET).
+  Fixpoint noDuplicates' (ls : list FS.key) (s : FS.t) : bool :=
+    match ls with
+    | [] => true
+    | x :: ls' => negb (FS.member s x) && noDuplicates' ls' (FS.add s x)
+    end.
+
+  Definition noDuplicates (ls : list FS.key) := noDuplicates' ls FS.empty.
+
+  (* A characterization of having a duplicate: the list can be partitioned into
+   * pieces revealing the same element [a] at two boundaries. *)
+  Definition hasDuplicate (ls : list FS.key) :=
+    exists ls1 a ls2 ls3, ls = ls1 ++ a :: ls2 ++ a :: ls3.
+
+  (* A characterization of containing an element [a]: the list can be
+   * partitioned into two pieces, with [a] at the boundary. *)
+  Definition contains (a : FS.key) (ls : list FS.key) :=
+    exists ls1 ls2, ls = ls1 ++ a :: ls2.
+
+  Lemma noDuplicates'_ok : forall ls s, if noDuplicates' ls s
+                                        then ~(hasDuplicate ls
+                                               \/ exists a, FS.member s a = true
+                                                            /\ contains a ls)
+                                        else (hasDuplicate ls
+                                              \/ exists a, FS.member s a = true
+                                                           /\ contains a ls).
+  Proof.
+    induct ls; simplify.
+
+    unfold hasDuplicate, contains.
+    propositional.
+    first_order.
+    cases x; simplify.
+    equality.
+    equality.
+
+    first_order.
+    cases x0; simplify.
+    equality.
+    equality.
+    cases (FS.member s a); simplify.
+    right.
+    exists a.
+    propositional.
+    unfold contains.
+    exists [].
+    exists ls.
+    simplify.
+    equality.
+
+    specialize (IHls (FS.add s a)).
+    cases (noDuplicates' ls (FS.add s a)).
+    propositional.
+
+    apply H1.
+    exists a.
+    propositional.
+    apply FS.member_add_eq.
+    unfold hasDuplicate, contains in *.
+    first_order.
+    cases x; simplify.
+    invert H0.
+    exists x1.
+    exists x2.
+    equality.
+
+    invert H0.
+    exfalso.
+    apply H with (x3 := x).
+    exists x0.
+    exists x1.
+    exists x2.
+    equality.
+
+    first_order.
+    apply H1 with x.
+    propositional.
+    pose proof (FS.decidable_equality a x).
+    propositional.
+    rewrite H4.
+    apply FS.member_add_eq.
+    rewrite FS.member_add_noteq.
+    assumption.
+    assumption.
+    cases x0; simplify.
+    equality.
+    invert H2.
+    exists x0.
+    exists x1.
+    equality.
+
+    first_order.
+    left.
+    exists (a :: x).
+    exists x0.
+    exists x1.
+    exists x2.
+    simplify.
+    equality.
+    cases (FS.member s x).
+
+    right.
+    exists x.
+    propositional.
+    exists (a :: x0).
+    exists x1.
+    simplify.
+    equality.
+
+    left.
+    pose proof (FS.decidable_equality a x).
+    propositional.
+
+    exists nil.
+    exists a.
+    exists x0.
+    exists x1.
+    simplify.
+    equality.
+    rewrite FS.member_add_noteq in H.
+    equality.
+    assumption.
+  Qed.
+
+  Theorem noDuplicates_ok : forall ls, if noDuplicates ls
+                                       then ~hasDuplicate ls 
+                                       else hasDuplicate ls.
+  Proof.
+    simplify.
+    pose proof (noDuplicates'_ok ls FS.empty).
+    unfold noDuplicates.
+    cases (noDuplicates' ls FS.empty); first_order.
+    rewrite FS.member_empty in H.
+    equality.
+  Qed.
+End FindDuplicates.
+
+Module NatDuplicateFinder := FindDuplicates(NatSet).
+
+Compute NatDuplicateFinder.noDuplicates [].
+Compute NatDuplicateFinder.noDuplicates [1].
+Compute NatDuplicateFinder.noDuplicates [1; 2].
+Compute NatDuplicateFinder.noDuplicates [1; 2; 3].
+Compute NatDuplicateFinder.noDuplicates [1; 2; 1; 3].
+
+
+(** * Custom implementations of abstract data types *)
+
+Fixpoint fromRange' (from to : nat) : NatSet.t :=
+  match to with
+  | 0 => NatSet.add NatSet.empty 0
+  | S to' => if NatWithEquality.equal to from
+             then NatSet.add NatSet.empty to
+             else NatSet.add (fromRange' from to') (S to')
+  end.
+
+Definition fromRange (from to : nat) : NatSet.t :=
+  if Compare_dec.leb from to
+  then fromRange' from to
+  else NatSet.empty.
+
+Module NatRangeSet (*<: FINITE_SET with Definition key := nat*).
+  Definition key := nat.
+
+  (*Definition t := ....
+
+  Definition empty : t := ....
+  Definition add (s : t) (k : key) : t := ....
+  Definition member (s : t) (k : key) : bool := ....*)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+  (*Theorem member_empty : forall k, member empty k = false.
+  Proof.
+    simplify.
+    equality.
+  Qed.
+
+  Lemma member_fromRange' : forall k from to,
+      from <= to
+      -> NatSet.member (fromRange' from to) k = Compare_dec.leb from k && Compare_dec.leb k to.
+  Proof.
+    induct to; simplify.
+
+    cases k; simplify.
+    rewrite Compare_dec.leb_correct by assumption.
+    equality.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+
+    cases from; simplify.
+    cases k; simplify.
+    apply IHto.
+    linear_arithmetic.
+    pose proof (NatWithEquality.equal_ok to k).
+    cases (NatWithEquality.equal to k); simplify.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+    rewrite IHto by linear_arithmetic.
+    cases to.
+    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
+    equality.
+    cases (Compare_dec.leb k to).
+    apply Compare_dec.leb_complete in Heq0.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+    apply Compare_dec.leb_complete_conv in Heq0.
+    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
+    equality.
+    
+    pose proof (NatWithEquality.equal_ok to from).
+    cases (NatWithEquality.equal to from); simplify.
+
+    cases k; simplify.
+    equality.
+    pose proof (NatWithEquality.equal_ok to k).
+    cases (NatWithEquality.equal to k); simplify.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+    cases (Compare_dec.leb from k); simplify.
+    apply Compare_dec.leb_complete in Heq1.
+    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
+    equality.
+    equality.
+
+    cases k; simplify.
+    apply IHto.
+    linear_arithmetic.
+    rewrite IHto by linear_arithmetic.
+    pose proof (NatWithEquality.equal_ok to k).
+    cases (NatWithEquality.equal to k); simplify.    
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+
+    cases to.
+    rewrite (Compare_dec.leb_correct_conv 0 k) by linear_arithmetic.
+    equality.
+    cases (Compare_dec.leb k to).
+    apply Compare_dec.leb_complete in Heq1.
+    rewrite (Compare_dec.leb_correct k (S to)) by linear_arithmetic.
+    equality.
+    apply Compare_dec.leb_complete_conv in Heq1.
+    rewrite (Compare_dec.leb_correct_conv (S to) k) by linear_arithmetic.
+    equality.
+  Qed.
+
+  Theorem member_add_eq : forall k s,
+      member (add s k) k = true.
+  Proof.
+    unfold member, add; simplify.
+    cases s.
+
+    SearchAbout Compare_dec.leb.
+    rewrite Compare_dec.leb_correct.
+    equality.
+    linear_arithmetic.
+
+    cases (Compare_dec.leb from k); simplify.
+    cases (Compare_dec.leb k to); simplify.
+    rewrite Heq.
+    rewrite Heq0.
+    apply Compare_dec.leb_complete in Heq.
+    apply Compare_dec.leb_complete in Heq0.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+
+    pose proof (NatWithEquality.equal_ok k (from - 1)).
+    cases (NatWithEquality.equal k (from - 1)).
+    apply leb_complete in Heq.
+    apply leb_complete_conv in Heq0.
+    linear_arithmetic.
+    simplify.
+    pose proof (NatWithEquality.equal_ok k (to + 1)).
+    cases (NatWithEquality.equal k (to + 1)); simplify.
+    cases (Compare_dec.leb from to).
+    rewrite Heq.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+    apply NatSet.member_add_eq.
+    pose proof (NatWithEquality.equal_ok k k).
+    cases (NatWithEquality.equal k k); simplify.
+    equality.
+    equality.
+
+    pose proof (NatWithEquality.equal_ok k (from - 1)).
+    cases (NatWithEquality.equal k (from - 1)); simplify.
+    cases (Compare_dec.leb from to).
+    apply Compare_dec.leb_complete in Heq1.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+    pose proof (NatWithEquality.equal_ok k (to + 1)).
+    cases (NatWithEquality.equal k (to + 1)); simplify.
+    pose proof (NatWithEquality.equal_ok k k).
+    cases (NatWithEquality.equal k k); simplify.
+    equality.
+    equality.
+    pose proof (NatWithEquality.equal_ok k k).
+    cases (NatWithEquality.equal k k); simplify.
+    equality.
+    equality.
+    pose proof (NatWithEquality.equal_ok k (to + 1)).
+    cases (NatWithEquality.equal k (to + 1)); simplify.
+    cases (Compare_dec.leb from to).
+    apply Compare_dec.leb_complete in Heq2.
+    apply Compare_dec.leb_complete_conv in Heq.
+    linear_arithmetic.
+    apply NatSet.member_add_eq.
+    pose proof (NatWithEquality.equal_ok k k).
+    cases (NatWithEquality.equal k k); simplify.
+    equality.
+    equality.    
+
+    apply NatSet.member_add_eq.
+  Qed.
+
+  Theorem member_add_noteq : forall k1 k2 s,
+      k1 <> k2
+      -> member (add s k1) k2 = member s k2.
+  Proof.
+    simplify.
+    unfold member, add.
+    cases s.
+
+    cases (Compare_dec.leb k1 k2); simplify.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    apply Compare_dec.leb_complete in Heq.
+    rewrite Compare_dec.leb_correct_conv.
+    equality.
+    unfold key in *. (* Tricky step!  Coq needs to see that we are really working with numbers. *)
+    linear_arithmetic.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+
+    cases (Compare_dec.leb from k1); simplify.
+    cases (Compare_dec.leb k1 to); simplify.
+    equality.
+
+    pose proof (NatWithEquality.equal_ok k1 (from - 1)).
+    cases (NatWithEquality.equal k1 (from - 1)); simplify.
+    apply leb_complete in Heq.
+    apply leb_complete_conv in Heq0.
+    linear_arithmetic.
+    pose proof (NatWithEquality.equal_ok k1 (to + 1)).
+    cases (NatWithEquality.equal k1 (to + 1)); simplify.
+    cases (Compare_dec.leb from to).
+    rewrite H1.
+    cases (Compare_dec.leb from k2); simplify.
+    cases (Compare_dec.leb k2 to).
+    apply Compare_dec.leb_complete in Heq5.
+    apply Compare_dec.leb_complete in Heq3.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+    apply Compare_dec.leb_complete in Heq3.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    apply Compare_dec.leb_complete_conv in Heq5.
+    unfold key in *.
+    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
+    equality.
+    rewrite andb_false_r.
+    equality.
+    simplify.
+    pose proof (NatWithEquality.equal_ok k1 k2).
+    cases (NatWithEquality.equal k1 k2); simplify.
+    equality.
+    unfold fromRange.
+    rewrite Heq3.
+    apply NatSet.member_empty.
+    pose proof (NatWithEquality.equal_ok k1 k2).
+    cases (NatWithEquality.equal k1 k2); simplify.
+    equality.
+    unfold fromRange.
+    cases (Compare_dec.leb from to); simplify.
+    apply member_fromRange'.
+    apply Compare_dec.leb_complete.
+    assumption.
+    equality.
+
+    pose proof (NatWithEquality.equal_ok k1 (from - 1)).
+    cases (NatWithEquality.equal k1 (from - 1)); simplify.
+    cases (Compare_dec.leb from to).
+    apply Compare_dec.leb_complete in Heq1.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    f_equal.
+    f_equal.
+    cases (Compare_dec.leb k1 k2).
+    apply Compare_dec.leb_complete in Heq2.
+    apply Compare_dec.leb_complete_conv in Heq.
+    unfold key in *.
+    rewrite Compare_dec.leb_correct by linear_arithmetic.
+    equality.
+    apply Compare_dec.leb_complete_conv in Heq2.
+    apply Compare_dec.leb_complete_conv in Heq.
+    unfold key in *.
+    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
+    equality.
+    pose proof (NatWithEquality.equal_ok k1 (to + 1)).
+    cases (NatWithEquality.equal k1 (to + 1)); simplify.
+    pose proof (NatWithEquality.equal_ok k1 k2).
+    cases (NatWithEquality.equal k1 k2); simplify.
+    unfold key in *; linear_arithmetic.
+    unfold fromRange.
+    rewrite Heq1.
+    apply NatSet.member_empty. 
+    pose proof (NatWithEquality.equal_ok k1 k2).
+    cases (NatWithEquality.equal k1 k2); simplify.
+    equality.
+    unfold fromRange.
+    rewrite Heq1.
+    apply NatSet.member_empty. 
+    pose proof (NatWithEquality.equal_ok k1 (to + 1)).
+    cases (NatWithEquality.equal k1 (to + 1)); simplify.
+    cases (Compare_dec.leb from to).
+    rewrite Heq; simplify.
+    apply Compare_dec.leb_complete in Heq2.
+    apply Compare_dec.leb_complete_conv in Heq.
+    linear_arithmetic.
+    rewrite NatSet.member_add_noteq by assumption; simplify.
+    unfold fromRange.
+    rewrite Heq2.
+    apply NatSet.member_empty. 
+    pose proof (NatWithEquality.equal_ok k1 k2).
+    cases (NatWithEquality.equal k1 k2); simplify.
+    equality.
+    unfold fromRange.
+    cases (Compare_dec.leb from to); simplify.
+    apply member_fromRange'.
+    apply Compare_dec.leb_complete; assumption.
+    equality.
+    apply NatSet.member_add_noteq.
+    assumption.
+  Qed.
+
+  Theorem decidable_equality : forall a b : key, a = b \/ a <> b.
+  Proof.
+    simplify.
+    pose proof (NatWithEquality.equal_ok a b).
+    cases (NatWithEquality.equal a b); propositional.
+  Qed.*)
+End NatRangeSet.
+
+(* Time for a head-to-head performance contest between our naive and clever
+ * sets! *)
+
+(*Module FasterNatDuplicateFinder := FindDuplicates(NatRangeSet).
+
+Fixpoint upto (n : nat) : list nat :=
+  match n with
+  | 0 => []
+  | S n' => n' :: upto n'
+  end.
+
+Compute upto 10.
+
+Compute NatDuplicateFinder.noDuplicates (upto 1000).
+Compute FasterNatDuplicateFinder.noDuplicates (upto 1000).*)
diff --git a/_CoqProject b/_CoqProject
index c098c77..10db5b8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -13,6 +13,7 @@ BasicSyntax.v
 Polymorphism.v
 Polymorphism_template.v
 DataAbstraction.v
+DataAbstraction_template.v
 Interpreters_template.v
 Interpreters.v
 TransitionSystems_template.v