(*|
========================
Week 2: Data Abstraction
========================

Author
  `Adam Chlipala <http://adam.chlipala.net/frap/>`__, with modifications by CS-428 staff.
License
  No redistribution allowed (usage by permission in CS-428).

.. contents::

.. coq:: none
|*)

From Coq Require Import Lists.List.
Import ListNotations.

(*|
Perhaps the essence of effective programming is division of large tasks into
smaller ones, and *data abstraction* is a key technique to that end.
We provide a clear separation between *interfaces* and *implementations*.
The author of a library can take responsibility for making it implement an
interface faithfully, *encapsulating* private state and other implementation
details in a way that client code can't observe.  Then that client code can
mix and match implementations of some well-specified functionality.

As part of our quick tour through effective Coq programming, we will dwell on
patterns for data abstraction, including how to state it formally, from the
perspectives of both libraries and client code.

Algebraic specifications
========================
|*)

Module Algebraic.

(*|
Specying a queue in axiomatic style
-----------------------------------

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.

Here's an example of an algebraic interface or *specification* ("spec" for
short).  It's for purely functional queues, which follow first-in-first-out
disciplines.
|*)

  Module Type QUEUE.
    Parameter t : Set -> Set.

(*|
An implementation must include some data type `t`.
Actually, it's more of a *type family*, e.g. like `list` and some other
polymorphic container types we looked at last time.
|*)

    Parameter empty : forall A, t A.

(*|
For any type `A` of data, we can build a queue for that element type.
|*)

    Parameter enqueue : forall {A}, t A -> A -> t A.

(*|
Enqueue a new element, in the functional style, where we build a new
queue instead of modifying the original.
|*)

    Parameter dequeue : forall {A}, t A -> option (t A * A).

(*|
Given a queue, either return `None` if it is empty or `Some (q', v)` for
the result of dequeuing one element, where `q'` is the new queue (now
one element shorter) and `v` is the element we dequeue.

Which algebraic properties characterize correct queues?

First, `dequeue` returns `None` exactly on empty queues.
|*)

    Axiom dequeue_empty : forall A,
        dequeue (empty A) = None.
    Axiom empty_dequeue : forall A (q : t A),
        dequeue q = None -> q = empty A.

(*|
Second, `dequeue` forms a kind of inverse for `enqueue`.
|*)

    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).

(*|
These properties turn out to be enough to prove interesting properties
about client code that uses queues.  Before we get there, we should
define some concrete queue implementations.  (If we don't give an
implementation, we often realize that the spec is *unrealizable*!)
|*)

  End QUEUE.

(*|
Verifying a simple queue
------------------------

First, there is a fairly straightforward implementation with lists.
|*)

  Module ListQueue : QUEUE.
    Definition t : Set -> Set := list.

(*|
Note that we use identifier `list` alone as a first-class type family,
without specifying a parameter explicitly.

We follow the convention of enqueuing onto the fronts of lists and
dequeuing from the backs, so the first two operations are just the first
two constructors of `list`.
|*)

    Definition empty A : t A := nil.
    Definition enqueue {A} (q : t A) (x : A) : t A := x :: q.

(*|
`dequeue` is a little more work: we use recursion to step down to the
last element of a list.
|*)

    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.

(*|
Applying our experience so far with Coq proofs, the algebraic laws are
unremarkable to establish.
|*)

    Theorem dequeue_empty : forall A, dequeue (empty A) = None.
    Proof.
      simpl.
      congruence.
    Qed.

    Theorem empty_dequeue : forall A (q : t A),
        dequeue q = None -> q = empty A.
    Proof.
      unfold empty.
      destruct q.
      - reflexivity.
      - simpl in *.
        destruct (dequeue q) as [ [? ?] | ];
          discriminate.
    Qed.

    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.
      simpl; intros.
      destruct (dequeue q) as [ [? ?] | ];
        reflexivity.
    Qed.
  End ListQueue.

(*|
There are software-engineering benefits to interface-implementation
separation even when one only bothers to build a single implementation.
However, often there are naive and clever optimized versions of a single
interface.  Queues are no exception.  Before we get to a truly clever
version, we'll demonstrate with a less obviously better version:
enqueuing at the back and dequeuing from the front.
|*)

  Module ReversedListQueue : QUEUE.
    Definition t : Set -> Set := list.

(*|
Still the same internal queue type, but note that Coq's type system
prevents client code from knowing that fact!  `t` appears *opaque*
or *abstract* from the outside, as we'll see shortly.

The first two operations are similar, but now we enqueue at the
list end.
|*)

    Definition empty A : t A := [].
    Definition enqueue {A} (q : t A) (x : A) : t A := q ++ [x].

(*|
`dequeue` is now constant-time, with no recursion and just a single
pattern match.
|*)

    Definition dequeue {A} (q : t A) : option (t A * A) :=
      match q with
      | [] => None
      | x :: q' => Some (q', x)
      end.

(*|
The proofs of the laws are still boring.
|*)

    Theorem dequeue_empty : forall A, dequeue (empty A) = None.
    Proof.
      reflexivity.
    Qed.

    Theorem empty_dequeue : forall {A} (q : t A),
        dequeue q = None -> q = empty A.
    Proof.
      unfold empty; destruct q.
      all: simpl.
      all: congruence.
    Qed.

    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.
      unfold dequeue, enqueue; destruct q.
      all: simpl.
      all: reflexivity.
    Qed.
  End ReversedListQueue.

(*|
Let's take a look at some client code that is agnostic to queue
implementation details.  We have been using Coq's *module system*, inspired
by those of the ML programming languages, to encode interfaces and
implementations.  Coq also adopts from ML the idea of *functors*, or
functions from modules to modules.

Proving client code against the Queue interface
-----------------------------------------------
|*)

  Module DelayedSum (Q : QUEUE).

(*|
The code in this scope may refer to some unknown implementation `Q` of
the `QUEUE` interface.

We will only use a simple example here: enqueue the first `n` natural
numbers and then successively dequeue them, computing the sum as we
go.

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.

(*|
A crucial lemma: what results from dequeuing out of a `makeQueue`
call?  The answer depends on whether the initial queue `q` has anything
to dequeue.
|*)

    Lemma dequeue_makeQueue : forall n q,
        Q.dequeue (makeQueue n q)
        = match Q.dequeue q with
          | Some (q', v) =>
              (* The queue we started with had content.
                 We dequeue from it. *)
            Some (makeQueue n q', v)
          | None =>
              (* No content in initial queue.
                 We get `n-1` (unless `n = 0`). *)
            match n with
            | 0 => None
            | S n' => Some (makeQueue n' q, n')
            end
          end.
    Proof.
      induction n; simpl; intros.
      - destruct (Q.dequeue q) as [ [? ?] | ];
          reflexivity.
      - rewrite IHn. (* .unfold *)

(*|
A crucial step!  The first use of a law from the interface:
|*)

        rewrite Q.dequeue_enqueue. (* .unfold *)
        destruct (Q.dequeue q) as [ [? ?] | ] eqn:Hdeq.
        + reflexivity.
        + (* .unfold *)

(*|
Another law!
|*)

          rewrite Q.empty_dequeue with (q := q)
            by assumption. (* .unfold *)
          reflexivity.
    Qed.

(*|
Now we can tackle the final property directly by induction.
|*)

    Theorem computeSum_ok : forall n,
        computeSum n (makeQueue n (Q.empty nat)) = sumUpto n.
    Proof.
      induction n; simpl.
      - reflexivity.
      - (* .unfold *)
        rewrite dequeue_makeQueue. (* .unfold *)
        rewrite Q.dequeue_enqueue. (* .unfold *)
        rewrite Q.dequeue_empty. (* .unfold *)
        rewrite IHn. (* .unfold *)
        congruence.
    Qed.
  End DelayedSum.
End Algebraic.

(*|
Algebraic specifications with equivalences
==========================================

There is a famous implementation of queues with two stacks, achieving
amortized constant time for all operations, in contrast to the worst-case
quadratic time of both queue implementations we just saw.  However, to
justify this fancy implementation, we will need to choose a more permissive
interface, based on the idea of parameterizing over an arbitrary *equivalence
relation* between queues, which need not be simple congruence.
|*)

Module AlgebraicWithEquivalenceRelation.
  Module Type QUEUE.

(*|
We still have a type family of queues, plus the same three operations.
|*)

    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).

(*|
What's new?  This equivalence relation.  The type `Prop` stands for
logical truth values, so a function returning it can be seen as a
relation in the usual mathematical sense.  This is a *binary* relation,
in particular, since it takes two arguments.
|*)

    Parameter equiv : forall {A}, t A -> t A -> Prop.

(*|
Let's declare convenient syntax for the relation.
|*)

    Infix "~=" := equiv (at level 70).

(*|
It really is an equivalence relation, as formalized by the usual three
laws.
|*)

    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.

(*|
It must be the case that enqueuing elements preserves the relation.
|*)

    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`: either both
`dequeue`\s failed to return anything, or both returned the same data
value along with new queues that are themselves related.
|*)

    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.

(*|
.. exercise:: `dequeue_equiv` is a relation

   Functors (modules that take other modules as argument) are a
   convenient way to package lemmas that follow from the axioms
   of a module type:
|*)
  Module QueueProps (Q: QUEUE).
    Import Q.

(*|
   Prove the following properties:
|*)

    Lemma dequeue_equiv_refl : forall A (a : option (t A * A)), a ~~= a.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      destruct a as [ [? ?] | ]; simpl.
      + split; [apply equiv_refl | reflexivity ].
      + tauto.
    Qed.

(*|
   .. coq::
|*)

    Lemma dequeue_equiv_sym : forall A (a b : option (t A * A)),
        a ~~= b -> b ~~= a.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      destruct a as [ [? ?] | ], b as [ [? ?] | ]; simpl; intros;
        repeat match goal with
          | [ H: _ /\ _ |- _ ] => destruct H; subst
          | [  |- _ /\ _ ] => split
          | _ => tauto
          end.
      apply equiv_sym; assumption.
    Qed.

(*|
   .. coq::
|*)

    Lemma dequeue_equiv_trans : forall A (a b c : option (t A * A)),
        a ~~= b -> b ~~= c -> a ~~= c.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      destruct a as [ [? ?] | ], b as [ [? ?] | ], c as [ [? ?] | ];
        simpl; intros;
        repeat match goal with
          | [ H: _ /\ _ |- _ ] => destruct H; subst
          | [  |- _ /\ _ ] => split
          | _ => tauto
          end.
      apply (equiv_trans t0 t1 t2); assumption.
    Qed.

(*|
   .. coq::
|*)

  End QueueProps.

(*|
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.
      congruence.
    Qed.

    Theorem equiv_sym : forall A (a b : t A),
        a ~= b -> b ~= a.
    Proof.
      congruence.
    Qed.

    Theorem equiv_trans : forall A (a b c : t A),
        a ~= b -> b ~= c -> a ~= c.
    Proof.
      congruence.
    Qed.

    Theorem equiv_enqueue : forall A (a b : t A) (x : A),
        a ~= b
        -> enqueue a x ~= enqueue b x.
    Proof.
      unfold equiv; congruence.
    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; simpl.
      intros * Heq. rewrite Heq.
      destruct (dequeue b) as [ [? ?] | ].
      - split; reflexivity.
      - tauto.
    Qed.

    Theorem dequeue_empty : forall {A}, dequeue (empty A) = None.
    Proof.
      reflexivity.
    Qed.

    Theorem empty_dequeue : forall {A} (q : t A),
        dequeue q = None -> q ~= empty A.
    Proof.
      destruct q; simpl.
      - reflexivity.
      - destruct (dequeue q) as [ [? ?] | ];
          congruence.
    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.
      induction q; simpl; intros.
      - split; reflexivity.
      - destruct (dequeue q) as [ (? & ?) | ].
        all: split; reflexivity.
    Qed.
  End ListQueue.

(*|
However, now we can implement the classic two-stacks optimized queue!
|*)

  Module TwoStacksQueue : QUEUE.

(*|
Every queue is a pair of stacks: one for enqueuing and one for
dequeuing.  The first stack, `EnqueueHere`, has more recently
enqueued elements closer to the front, making enqueuing constant-time.
The second stack, `DequeueHere`, has least recently enqueued elements
closer to the front, making dequeuing constant-time.
|*)

    Record stackpair {A : Set} := {
      EnqueueHere : list A;
      DequeueHere : list A
    }.
    Arguments stackpair: clear implicits.

(*|
What's the catch?  Sometimes we need to reverse `EnqueueHere` and
transfer it to `DequeueHere`, or otherwise there would never be anything
to dequeue!  Luckily, the work we do in transfering is bounded
asymptotically by the total number of enqueue/dequeue operations, so
we get *amortized* constant time.

By the way, the `Record` feature we used above is similar to e.g. structs
in C.
|*)

    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)
      | [] => (* Ran out of dequeuable elements. Reverse enqueued
                 elements and transfer to the other stack. *)
        match rev q.(EnqueueHere) with
        | [] => None
        | x :: eq => Some ({| EnqueueHere := [];
                              DequeueHere := eq |}, x)
        end
      end.

(*|
This function explains which simple queue representation we have in mind,
for each fancy two-stack representation.
|*)

    Definition elements {A} (q : t A) : list A :=
      q.(EnqueueHere) ++ rev q.(DequeueHere).

(*|
That function is useful to define our equivalence relation.
|*)

    Definition equiv {A} (a b : t A) :=
      elements a = elements b.
    Infix "~=" := equiv (at level 70).

    Theorem equiv_refl : forall A (a : t A),
        a ~= a.
    Proof.
      congruence.
    Qed.

    Theorem equiv_sym : forall A (a b : t A),
        a ~= b -> b ~= a.
    Proof.
      congruence.
    Qed.

    Theorem equiv_trans : forall A (a b c : t A),
        a ~= b -> b ~= c -> a ~= c.
    Proof.
      congruence.
    Qed.

(*|
Now it is mostly routine to prove the laws, though a few tricks may
be worth reading through.
|*)

    Theorem equiv_enqueue : forall A (a b : t A) (x : A),
        a ~= b
        -> enqueue a x ~= enqueue b x.
    Proof.
      unfold equiv, elements; simpl.
      congruence.
    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).

(*|
The following proof offers an interesting example of automation.
Mindlessly destructing the discriminands of the `match`\es that
appear in the goal works, but ends up destructing too much: we end
up with having to reason about the result of destructing `l` and
`rev l` simultaneously.

Instead, the proof below starts by using properties of `rev` to align
the hypotheses with the terms in the goal:
|*)

    Theorem equiv_dequeue : forall {A} (a b : t A),
        a ~= b
        -> dequeue a ~~= dequeue b.
    Proof.
      unfold dequeue_equiv, equiv, elements, dequeue;
        intros. (* .unfold *)

(*|
Notice that at this point the goal mentions `DequeueHere a`,
whereas the hypothesis mentions `rev (DequeueHere a)`,
and vice-versa for `EnqueueHere`.
|*)

      apply (f_equal (@rev _)) in H;
        rewrite !rev_app_distr, !rev_involutive in H. (* .unfold *)

(*|
Aligning the two using properties of `rev` makes the proof much simpler:
|*)

      repeat
        match goal with
        | _ => progress (subst; simpl in * )
        | [  |- _ /\ _ ] => split
        | [  |- context[match ?x with _ => _ end] ] =>
            destruct x eqn:?
        | [ h: context[match ?x with _ => _ end] |- _ ] =>
            destruct x eqn:?
        | [ H: Some _ = Some _ |- _ ] => injection H as H; subst
        | [ H: _ :: _ = _ :: _ |- _ ] => injection H as ? H; subst
        | _ => rewrite rev_app_distr
        | _ => rewrite rev_involutive
        | _ => discriminate || congruence || tauto
        end.

(*|
After running a very simple automated solver, we are left with
just one goal that requires us to undo the `rev` trick that we
previously applied:
|*)

      { (* .unfold *)
        apply (f_equal (@rev _)) in H;
          rewrite !rev_app_distr, !rev_involutive in H. (* .unfold *)
        assumption. }
    Qed.

    Theorem dequeue_empty : forall {A}, dequeue (empty A) = None.
    Proof.
      reflexivity.
    Qed.

(*|
A similar technique is applicable here:
|*)

    Lemma rev_inj : forall A (l1 l2: list A),
        rev l1 = rev l2 -> l1 = l2.
    Proof.
      intros.
      rewrite <- (rev_involutive l1), <- (rev_involutive l2).
      congruence.
    Qed.

    Theorem empty_dequeue : forall A (q : t A),
        dequeue q = None -> q ~= empty A.
    Proof.
      destruct q as [EH DH]; unfold dequeue, empty, equiv, elements;
        simpl; intros.
      apply rev_inj; rewrite !rev_app_distr, !rev_involutive.
      destruct DH, (rev EH); simpl in *.
      all: congruence.
    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.
      destruct q as [EH DH];
        unfold dequeue, enqueue, empty, dequeue_equiv, equiv, elements;
        simpl; intros.
      destruct DH, (rev EH); simpl; split.
      all: rewrite ?rev_app_distr; simpl.
      all: reflexivity.
    Qed.
  End TwoStacksQueue.

(*|
The exercise of the generic delayed sum may be repeated with equivalence
relations.
|*)

  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.
      induction n; intros.
      - 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.
      induction n; simpl; intros.
      - destruct (Q.dequeue q) as [ [? ?] | ]; simpl.
        + split; [ apply Q.equiv_refl | reflexivity ].
        + tauto.
      - specialize (IHn (Q.enqueue q n)).
        pose proof (Q.dequeue_enqueue q n) as Hde.
        destruct (Q.dequeue (Q.enqueue q n)) as [[??]|],
            (Q.dequeue (makeQueue n (Q.enqueue q n))) as [[??]|],
              (Q.dequeue q) as [[??]|] eqn:Hdq;
          simpl in *; try (exfalso; assumption).
        all: destruct IHn as [IHeqv IHeq], Hde as [Heqv Heq];
          split; [ | congruence ].
        + apply Q.equiv_trans with (b := makeQueue n t).
          * assumption.
          * apply makeQueue_congruence; assumption.
        + apply Q.empty_dequeue in Hdq.
          apply Q.equiv_trans with (b := makeQueue n t).
          * assumption.
          * apply makeQueue_congruence.
            apply Q.equiv_trans with (b := Q.empty nat).
            -- assumption.
            -- apply Q.equiv_sym.
               assumption.
    Qed.

    Theorem computeSum_congruence : forall n a b,
        a ~= b
        -> computeSum n a = computeSum n b.
    Proof.
      induction n; simpl; intros * Heqv.
      - reflexivity.
      - pose proof (Q.equiv_dequeue a b Heqv) as Heqd.
        unfold Q.dequeue_equiv in Heqd.
        destruct (Q.dequeue a) as [[??]|], (Q.dequeue b) as [[??]|].
        + destruct Heqd as [Heqv' Heq].
          rewrite (IHn _ _ Heqv'), Heq.
          reflexivity.
        + exfalso; assumption.
        + exfalso; assumption.
        + reflexivity.
    Qed.

    Theorem computeSum_ok : forall n,
        computeSum n (makeQueue n (Q.empty nat)) = sumUpto n.
    Proof.
      induction n; simpl; intros.
      - reflexivity.
      - pose proof (dequeue_makeQueue n (Q.enqueue (Q.empty nat) n))
          as HdmQ.
        pose proof (Q.dequeue_enqueue (Q.empty nat) n) as Hdev.
        unfold Q.dequeue_equiv in *.
        destruct (Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)))
          as [[??]|] eqn:Hdm,
              (Q.dequeue (Q.enqueue (Q.empty nat) n))
            as [[??]|] eqn:Hde;
          simpl in *.
        all: rewrite Q.dequeue_empty in Hdev.
        all: try (exfalso; assumption).
        { destruct HdmQ as [Heqv Heq], Hdev as [Hdeqv Hdeq]; subst.
          rewrite <- IHn.
          f_equal.
          apply computeSum_congruence.
          apply Q.equiv_trans with (b := makeQueue n t0).
          - assumption.
          - apply makeQueue_congruence.
            assumption. }
    Qed.
  End DelayedSum.
End AlgebraicWithEquivalenceRelation.

(*|
Specifications with representation functions
============================================

It's worth presenting one final style of data-abstraction formalism: we
introduce *representation functions* in the interface, to map the internal
representation to some standard one that is easy to reason about.  We don't
expect "real code" to call the representation function.  Instead, it's just a
proof device to let us write convincing laws.  Here's the previous example
redone in this manner, without comment.
|*)

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.

    Axiom empty_rep : forall {A},
        rep (empty A) = [].

    Axiom enqueue_rep : forall {A} (q : t A) x,
        rep (enqueue q x) = x :: rep q.

    Axiom dequeue_empty : forall {A} (q : t A),
        rep q = []
        -> dequeue q = None.

    Axiom dequeue_nonempty : forall {A} (q : t A) xs x,
        rep q = xs ++ [x]
        -> exists q', dequeue q = Some (q', x) /\ rep q' = xs.
  End QUEUE.

(*|
We leave the proofs of using this new style as exercises:

.. exercise:: Revisiting the list-based queue

   Reimplement `ListQueue` using this new specification style.
|*)

  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) := q.

    Theorem empty_rep : forall {A},
        rep (empty A) = [].

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      reflexivity.
    Qed.

(*|
   .. coq::
|*)

    Theorem enqueue_rep : forall {A} (q : t A) x,
        rep (enqueue q x) = x :: rep q.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      reflexivity.
    Qed.

(*|
   .. coq::
|*)

    Theorem dequeue_empty : forall {A} (q : t A),
        rep q = []
        -> dequeue q = None.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      unfold rep; simpl; intros * ->.
      reflexivity.
    Qed.

(*|
   .. coq::
|*)

    Theorem dequeue_nonempty : forall {A} (q : t A) xs x,
        rep q = xs ++ [x]
        -> exists q', dequeue q = Some (q', x) /\ rep q' = xs.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      unfold rep; induction q; simpl; intros.
      - destruct xs; simpl in *; congruence.
      - destruct xs; simpl in *.
        all: injection H as H; subst; simpl in *.
        + exists []; split; reflexivity.
        + specialize (IHq _ _ eq_refl).
          destruct IHq as [q' [-> ->]].
          eexists; split; reflexivity.
    Qed.

(*|
   .. coq::
|*)

  End ListQueue.

(*|
.. exercise:: Revisiting the two-stack queue

   Reimplement `TwoStacksQueue` using this new specification style.
|*)

  Module TwoStacksQueue : QUEUE.
    Record stackpair {A : Set} := {
      EnqueueHere : list A;
      DequeueHere : list A
    }.
    Arguments stackpair: clear implicits.

    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 :=
      q.(EnqueueHere) ++ rev q.(DequeueHere).

    Theorem empty_rep : forall {A},
        rep (empty A) = [].

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      reflexivity.
    Qed.

(*|
   .. coq::
|*)

    Theorem enqueue_rep : forall {A} (q : t A) x,
        rep (enqueue q x) = x :: rep q.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      reflexivity.
    Qed.

(*|
   .. coq::
|*)

    Theorem dequeue_empty : forall {A} (q : t A),
        rep q = []
        -> dequeue q = None.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      unfold rep, dequeue; intros.
      destruct (EnqueueHere q), (DequeueHere q); simpl in *.
      - reflexivity.
      - destruct (rev _); simpl in *; congruence.
      - congruence.
      - congruence.
    Qed.

(*|
   .. coq::
|*)

    Theorem dequeue_nonempty : forall {A} (q : t A) xs x,
        rep q = xs ++ [x]
        -> exists q', dequeue q = Some (q', x) /\ rep q' = xs.

(*|
   .. solution::

      .. coq::
|*)

    Ltac rev_both H :=
      apply (f_equal (@rev _)) in H;
      rewrite ?rev_app_distr, ?rev_involutive in H; simpl in H.

    Proof.
      unfold rep, dequeue; intros * H; rev_both H.
      destruct (DequeueHere q), (rev (EnqueueHere q)) eqn:HE;
        simpl in *.
      all: try congruence.
      all: injection H as Hhd Htl; subst.
      all: rewrite ?app_nil_r in *; subst.
      all: eexists; split; [reflexivity|simpl].
      - apply rev_involutive.
      - rev_both HE; rewrite HE, rev_involutive.
        reflexivity.
      - rev_both HE; rewrite HE.
        rev_both Htl; rewrite Htl.
        reflexivity.
    Qed.

(*|
   .. coq::
|*)

  End TwoStacksQueue.

(*|
.. exercise:: Revisiting the delayed sum client

   Reimplement `DelayedSum` using this new specification style.
|*)

  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.

(*|
   .. coq::
|*)

    Lemma makeQueue_rep : forall n q,
        Q.rep (makeQueue n q) = upto n ++ Q.rep q.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      induction n; simpl; intros.
      - reflexivity.
      - rewrite IHn.
        rewrite Q.enqueue_rep.
        rewrite <- app_assoc.
        reflexivity.
    Qed.

(*|
   .. coq::
|*)

    Lemma computeSum_makeQueue' : forall n q,
        Q.rep q = upto n
        -> computeSum n q = sumUpto n.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      induction n; simpl; intros.
      - reflexivity.
      - pose proof (Q.dequeue_nonempty _ _ _ H) as [q' [Hdq Hrep]].
        rewrite Hdq.
        rewrite IHn by assumption.
        reflexivity.
    Qed.

(*|
   .. coq::
|*)

    Theorem computeSum_ok : forall n,
        computeSum n (makeQueue n (Q.empty nat)) = sumUpto n.

(*|
   .. solution::

      .. coq::
|*)

    Proof.
      intros.
      apply computeSum_makeQueue'.
      rewrite makeQueue_rep.
      rewrite Q.empty_rep.
      apply app_nil_r.
    Qed.
  End DelayedSum.
End RepFunction.