Week 2: Data Abstraction

Author: Adam Chlipala, with modifications by CS-428 staff.
License: No redistribution allowed (usage by permission in CS-428).

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.forall A : Set, dequeue (empty A) = None
    Proof.forall A : Set, dequeue (empty A) = None
      simpl.forall A : Set, None = None
      congruence.
    Qed.

    Theorem empty_dequeue : forall A (q : t A),
        dequeue q = None -> q = empty A.forall (A : Set) (q : t A),
dequeue q = None -> q = empty A
    Proof.forall (A : Set) (q : t A),
dequeue q = None -> q = empty A
      unfold empty.forall (A : Set) (q : t A), dequeue q = None -> q = []
      destruct q.A: Set
dequeue [] = None -> [] = []
A: Set
a: A
q: list A
dequeue (a :: q) = None -> a :: q = []
      -A: Set
dequeue [] = None -> [] = [] reflexivity.
      -A: Set
a: A
q: list A
dequeue (a :: q) = None -> a :: q = [] simpl in *.A: Set
a: A
q: list A
match dequeue q with
| Some (q'', y) => Some (a :: q'', y)
| None => Some ([], a)
end = None -> a :: q = []
        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).forall (A : Set) (q : t A) (x : A),
dequeue (enqueue q x) =
Some
  match dequeue q with
  | Some (q', y) => (enqueue q' x, y)
  | None => (empty A, x)
  end
    Proof.forall (A : Set) (q : t A) (x : A),
dequeue (enqueue q x) =
Some
  match dequeue q with
  | Some (q', y) => (enqueue q' x, y)
  | None => (empty A, x)
  end
      simpl; intros.A: Set
q: t A
x: A
match dequeue q with
| Some (q'', y) => Some (x :: q'', y)
| None => Some ([], x)
end =
Some
  match dequeue q with
  | Some (q', y) => (enqueue q' x, y)
  | None => (empty A, x)
  end
      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.forall A : Set, dequeue (empty A) = None
    Proof.forall A : Set, dequeue (empty A) = None
      reflexivity.
    Qed.

    Theorem empty_dequeue : forall {A} (q : t A),
        dequeue q = None -> q = empty A.forall (A : Set) (q : t A),
dequeue q = None -> q = empty A
    Proof.forall (A : Set) (q : t A),
dequeue q = None -> q = empty A
      unfold empty; destruct q.A: Set
dequeue [] = None -> [] = []
A: Set
a: A
q: list A
dequeue (a :: q) = None -> a :: q = []
      all: simpl.A: Set
None = None -> [] = []
A: Set
a: A
q: list A
Some (q, a) = None -> a :: q = []
      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).forall (A : Set) (q : t A) (x : A),
dequeue (enqueue q x) =
Some
  match dequeue q with
  | Some (q', y) => (enqueue q' x, y)
  | None => (empty A, x)
  end
    Proof.forall (A : Set) (q : t A) (x : A),
dequeue (enqueue q x) =
Some
  match dequeue q with
  | Some (q', y) => (enqueue q' x, y)
  | None => (empty A, x)
  end
      unfold dequeue, enqueue; destruct q.A: Set
forall x : A,
match [] ++ [x] with
| [] => None
| x0 :: q' => Some (q', x0)
end = Some (empty A, x)
A: Set
a: A
q: list A
forall x : A,
match (a :: q) ++ [x] with
| [] => None
| x0 :: q' => Some (q', x0)
end = Some (q ++ [x], a)
      all: simpl.A: Set
forall x : A, Some ([], x) = Some (empty A, x)
A: Set
a: A
q: list A
forall x : A, Some (q ++ [x], a) = Some (q ++ [x], a)
      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.forall (n : nat) (q : Q.t nat),
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.forall (n : nat) (q : Q.t nat),
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
      induction n; simpl; intros.q: Q.t nat
Q.dequeue q =
match Q.dequeue q with
| Some (q', v) => Some (q', v)
| None => None
end
n: nat
IHn: forall q : Q.t nat,
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
q: Q.t nat
Q.dequeue (makeQueue n (Q.enqueue q n)) =
match Q.dequeue q with
| Some (q', v) =>
    Some (makeQueue n (Q.enqueue q' n), v)
| None => Some (makeQueue n q, n)
end
      -q: Q.t nat
Q.dequeue q =
match Q.dequeue q with
| Some (q', v) => Some (q', v)
| None => None
end destruct (Q.dequeue q) as [ [? ?] | ];
          reflexivity.
      -n: nat
IHn: forall q : Q.t nat,
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
q: Q.t nat
Q.dequeue (makeQueue n (Q.enqueue q n)) =
match Q.dequeue q with
| Some (q', v) =>
    Some (makeQueue n (Q.enqueue q' n), v)
| None => Some (makeQueue n q, n)
end rewrite IHn.n: nat
IHn: forall q : Q.t nat,
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
q: Q.t nat
match Q.dequeue (Q.enqueue q n) with
| Some (q', v) => Some (makeQueue n q', v)
| None =>
    match n with
    | 0 => None
    | S n' => Some (makeQueue n' (Q.enqueue q n), n')
    end
end =
match Q.dequeue q with
| Some (q', v) =>
    Some (makeQueue n (Q.enqueue q' n), v)
| None => Some (makeQueue n q, n)
end

A crucial step! The first use of a law from the interface:

        rewrite Q.dequeue_enqueue.n: nat
IHn: forall q : Q.t nat,
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
q: Q.t nat
(let (q', v) :=
   match Q.dequeue q with
   | Some (q', y) => (Q.enqueue q' n, y)
   | None => (Q.empty nat, n)
   end in
 Some (makeQueue n q', v)) =
match Q.dequeue q with
| Some (q', v) =>
    Some (makeQueue n (Q.enqueue q' n), v)
| None => Some (makeQueue n q, n)
end
        destruct (Q.dequeue q) as [ [? ?] | ] eqn:Hdeq.n: nat
IHn: forall q : Q.t nat,
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
q, t: Q.t nat
n0: nat
Hdeq: Q.dequeue q = Some (t, n0)
Some (makeQueue n (Q.enqueue t n), n0) =
Some (makeQueue n (Q.enqueue t n), n0)
n: nat
IHn: forall q : Q.t nat,
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
q: Q.t nat
Hdeq: Q.dequeue q = None
Some (makeQueue n (Q.empty nat), n) =
Some (makeQueue n q, n)
        +n: nat
IHn: forall q : Q.t nat,
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
q, t: Q.t nat
n0: nat
Hdeq: Q.dequeue q = Some (t, n0)
Some (makeQueue n (Q.enqueue t n), n0) =
Some (makeQueue n (Q.enqueue t n), n0) reflexivity.
        +n: nat
IHn: forall q : Q.t nat,
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
q: Q.t nat
Hdeq: Q.dequeue q = None
Some (makeQueue n (Q.empty nat), n) =
Some (makeQueue n q, n)

Another law!

          rewrite Q.empty_dequeue with (q := q)
            by assumption.n: nat
IHn: forall q : Q.t nat,
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
q: Q.t nat
Hdeq: Q.dequeue q = None
Some (makeQueue n (Q.empty nat), n) =
Some (makeQueue n (Q.empty nat), n)
          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.forall n : nat,
computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
    Proof.forall n : nat,
computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
      induction n; simpl.0 = 0
n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
match
  Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n))
with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
      -0 = 0 reflexivity.
      -n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
match
  Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n))
with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
        rewrite dequeue_makeQueue.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
match
  match Q.dequeue (Q.enqueue (Q.empty nat) n) with
  | Some (q', v) => Some (makeQueue n q', v)
  | None =>
      match n with
      | 0 => None
      | S n' =>
          Some
            (makeQueue n' (Q.enqueue (Q.empty nat) n),
             n')
      end
  end
with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
        rewrite Q.dequeue_enqueue.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
match
  (let (q', v) :=
     match Q.dequeue (Q.empty nat) with
     | Some (q', y) => (Q.enqueue q' n, y)
     | None => (Q.empty nat, n)
     end in
   Some (makeQueue n q', v))
with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
        rewrite Q.dequeue_empty.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
n + computeSum n (makeQueue n (Q.empty nat)) =
n + sumUpto n
        rewrite IHn.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
n + sumUpto n = n + sumUpto n
        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 dequeues 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.forall (A : Set) (a : option (t A * A)), a ~~= a

Solution

    Proof.forall (A : Set) (a : option (t A * A)), a ~~= a
      destruct a as [ [? ?] | ]; simpl.A: Set
t0: t A
a: A
t0 ~= t0 /\ a = a
A: Set
True
      +A: Set
t0: t A
a: A
t0 ~= t0 /\ a = a split; [apply equiv_refl | reflexivity ].
      +A: Set
True tauto.
    Qed.

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

Solution

    Proof.forall (A : Set) (a b : option (t A * A)),
a ~~= b -> b ~~= a
      destruct a as [ [? ?] | ], b as [ [? ?] | ]; simpl; intros;
        repeat match goal with
          | [ H: _ /\ _ |- _ ] => destruct H; subst
          | [  |- _ /\ _ ] => split
          | _ => tauto
          end.A: Set
t0, t1: t A
a0: A
H: t0 ~= t1
t1 ~= t0
      apply equiv_sym; assumption.
    Qed.

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

Solution

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

  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.forall (A : Set) (a : t A), a ~= a
    Proof.forall (A : Set) (a : t A), a ~= a
      congruence.
    Qed.

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

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

    Theorem equiv_enqueue : forall A (a b : t A) (x : A),
        a ~= b
        -> enqueue a x ~= enqueue b x.forall (A : Set) (a b : t A) (x : A),
a ~= b -> enqueue a x ~= enqueue b x
    Proof.forall (A : Set) (a b : t A) (x : A),
a ~= b -> enqueue a x ~= enqueue b x
      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.forall (A : Set) (a b : t A),
a ~= b -> dequeue a ~~= dequeue b
    Proof.forall (A : Set) (a b : t A),
a ~= b -> dequeue a ~~= dequeue b
      unfold equiv, dequeue_equiv; simpl.forall (A : Set) (a b : t A),
a = b ->
match dequeue a with
| Some (qa, xa) =>
    match dequeue b with
    | Some (qb, xb) => qa ~= qb /\ xa = xb
    | None => False
    end
| None =>
    match dequeue b with
    | Some _ => False
    | None => True
    end
end
      intros * Heq.A: Set
a, b: t A
Heq: a = b
match dequeue a with
| Some (qa, xa) =>
    match dequeue b with
    | Some (qb, xb) => qa ~= qb /\ xa = xb
    | None => False
    end
| None =>
    match dequeue b with
    | Some _ => False
    | None => True
    end
end rewrite Heq.A: Set
a, b: t A
Heq: a = b
match dequeue b with
| Some (qa, xa) =>
    match dequeue b with
    | Some (qb, xb) => qa ~= qb /\ xa = xb
    | None => False
    end
| None =>
    match dequeue b with
    | Some _ => False
    | None => True
    end
end
      destruct (dequeue b) as [ [? ?] | ].A: Set
a, b: t A
Heq: a = b
t0: t A
a0: A
t0 ~= t0 /\ a0 = a0
A: Set
a, b: t A
Heq: a = b
True
      -A: Set
a, b: t A
Heq: a = b
t0: t A
a0: A
t0 ~= t0 /\ a0 = a0 split; reflexivity.
      -A: Set
a, b: t A
Heq: a = b
True tauto.
    Qed.

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

    Theorem empty_dequeue : forall {A} (q : t A),
        dequeue q = None -> q ~= empty A.forall (A : Set) (q : t A),
dequeue q = None -> q ~= empty A
    Proof.forall (A : Set) (q : t A),
dequeue q = None -> q ~= empty A
      destruct q; simpl.A: Set
None = None -> [] ~= empty A
A: Set
a: A
q: list A
match dequeue q with
| Some (q'', y) => Some (a :: q'', y)
| None => Some ([], a)
end = None -> a :: q ~= empty A
      -A: Set
None = None -> [] ~= empty A reflexivity.
      -A: Set
a: A
q: list A
match dequeue q with
| Some (q'', y) => Some (a :: q'', y)
| None => Some ([], a)
end = None -> a :: q ~= empty A 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.forall (A : Set) (q : t A) (x : A),
dequeue (enqueue q x) ~~=
match dequeue q with
| Some (q', y) => Some (enqueue q' x, y)
| None => Some (empty A, x)
end
    Proof.forall (A : Set) (q : t A) (x : A),
dequeue (enqueue q x) ~~=
match dequeue q with
| Some (q', y) => Some (enqueue q' x, y)
| None => Some (empty A, x)
end
      unfold dequeue_equiv, equiv.forall (A : Set) (q : t A) (x : A),
match dequeue (enqueue q x) with
| Some (qa, xa) =>
    match
      match dequeue q with
      | Some (q', y) => Some (enqueue q' x, y)
      | None => Some (empty A, x)
      end
    with
    | Some (qb, xb) => qa = qb /\ xa = xb
    | None => False
    end
| None =>
    match
      match dequeue q with
      | Some (q', y) => Some (enqueue q' x, y)
      | None => Some (empty A, x)
      end
    with
    | Some _ => False
    | None => True
    end
end
      induction q; simpl; intros.A: Set
x: A
[] = empty A /\ x = x
A: Set
a: A
q: list A
IHq: forall x : A,
match dequeue (enqueue q x) with
| Some (qa, xa) =>
match
match dequeue q with
| Some (q', y) => Some (enqueue q' x, y)
| None => Some (empty A, x)
end
with
| Some (qb, xb) => qa = qb /\ xa = xb
| None => False
end
| None =>
match
match dequeue q with
| Some (q', y) => Some (enqueue q' x, y)
| None => Some (empty A, x)
end
with
| Some _ => False
| None => True
end
end
x: A
match
  match
    match dequeue q with
    | Some (q'', y) => Some (a :: q'', y)
    | None => Some ([], a)
    end
  with
  | Some (q'', y) => Some (x :: q'', y)
  | None => Some ([], x)
  end
with
| Some (qa, xa) =>
    match
      match
        match dequeue q with
        | Some (q'', y) => Some (a :: q'', y)
        | None => Some ([], a)
        end
      with
      | Some (q', y) => Some (enqueue q' x, y)
      | None => Some (empty A, x)
      end
    with
    | Some (qb, xb) => qa = qb /\ xa = xb
    | None => False
    end
| None =>
    match
      match
        match dequeue q with
        | Some (q'', y) => Some (a :: q'', y)
        | None => Some ([], a)
        end
      with
      | Some (q', y) => Some (enqueue q' x, y)
      | None => Some (empty A, x)
      end
    with
    | Some _ => False
    | None => True
    end
end
      -A: Set
x: A
[] = empty A /\ x = x split; reflexivity.
      -A: Set
a: A
q: list A
IHq: forall x : A,
match dequeue (enqueue q x) with
| Some (qa, xa) =>
match
match dequeue q with
| Some (q', y) => Some (enqueue q' x, y)
| None => Some (empty A, x)
end
with
| Some (qb, xb) => qa = qb /\ xa = xb
| None => False
end
| None =>
match
match dequeue q with
| Some (q', y) => Some (enqueue q' x, y)
| None => Some (empty A, x)
end
with
| Some _ => False
| None => True
end
end
x: A
match
  match
    match dequeue q with
    | Some (q'', y) => Some (a :: q'', y)
    | None => Some ([], a)
    end
  with
  | Some (q'', y) => Some (x :: q'', y)
  | None => Some ([], x)
  end
with
| Some (qa, xa) =>
    match
      match
        match dequeue q with
        | Some (q'', y) => Some (a :: q'', y)
        | None => Some ([], a)
        end
      with
      | Some (q', y) => Some (enqueue q' x, y)
      | None => Some (empty A, x)
      end
    with
    | Some (qb, xb) => qa = qb /\ xa = xb
    | None => False
    end
| None =>
    match
      match
        match dequeue q with
        | Some (q'', y) => Some (a :: q'', y)
        | None => Some ([], a)
        end
      with
      | Some (q', y) => Some (enqueue q' x, y)
      | None => Some (empty A, x)
      end
    with
    | Some _ => False
    | None => True
    end
end destruct (dequeue q) as [ (? & ?) | ].A: Set
a: A
q: list A
t0: t A
a0: A
IHq: forall x : A,
match dequeue (enqueue q x) with
| Some (qa, xa) => qa = enqueue t0 x /\ xa = a0
| None => False
end
x: A
x :: a :: t0 = enqueue (a :: t0) x /\ a0 = a0
A: Set
a: A
q: list A
IHq: forall x : A,
match dequeue (enqueue q x) with
| Some (qa, xa) => qa = empty A /\ xa = x
| None => False
end
x: A
[x] = enqueue [] x /\ a = a
        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.forall (A : Set) (a : t A), a ~= a
    Proof.forall (A : Set) (a : t A), a ~= a
      congruence.
    Qed.

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

    Theorem equiv_trans : forall A (a b c : t A),
        a ~= b -> b ~= c -> a ~= c.forall (A : Set) (a b c : t A),
a ~= b -> b ~= c -> a ~= c
    Proof.forall (A : Set) (a b c : t A),
a ~= b -> b ~= c -> a ~= c
      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.forall (A : Set) (a b : t A) (x : A),
a ~= b -> enqueue a x ~= enqueue b x
    Proof.forall (A : Set) (a b : t A) (x : A),
a ~= b -> enqueue a x ~= enqueue b x
      unfold equiv, elements; simpl.forall (A : Set) (a b : t A) (x : A),
EnqueueHere a ++ rev (DequeueHere a) =
EnqueueHere b ++ rev (DequeueHere b) ->
x :: EnqueueHere a ++ rev (DequeueHere a) =
x :: EnqueueHere b ++ rev (DequeueHere b)
      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 matches 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.forall (A : Set) (a b : t A),
a ~= b -> dequeue a ~~= dequeue b
    Proof.forall (A : Set) (a b : t A),
a ~= b -> dequeue a ~~= dequeue b
      unfold dequeue_equiv, equiv, elements, dequeue;
        intros.A: Set
a, b: t A
H: EnqueueHere a ++ rev (DequeueHere a) =
EnqueueHere b ++ rev (DequeueHere b)
match
  match DequeueHere a with
  | [] =>
      match rev (EnqueueHere a) with
      | [] => None
      | x :: eq =>
          Some
            ({|
               EnqueueHere := []; DequeueHere := eq
             |}, x)
      end
  | x :: dq =>
      Some
        ({|
           EnqueueHere := EnqueueHere a;
           DequeueHere := dq
         |}, x)
  end
with
| Some (qa, xa) =>
    match
      match DequeueHere b with
      | [] =>
          match rev (EnqueueHere b) with
          | [] => None
          | x :: eq =>
              Some
                ({|
                   EnqueueHere := [];
                   DequeueHere := eq
                 |}, x)
          end
      | x :: dq =>
          Some
            ({|
               EnqueueHere := EnqueueHere b;
               DequeueHere := dq
             |}, x)
      end
    with
    | Some (qb, xb) =>
        EnqueueHere qa ++ rev (DequeueHere qa) =
        EnqueueHere qb ++ rev (DequeueHere qb) /\
        xa = xb
    | None => False
    end
| None =>
    match
      match DequeueHere b with
      | [] =>
          match rev (EnqueueHere b) with
          | [] => None
          | x :: eq =>
              Some
                ({|
                   EnqueueHere := [];
                   DequeueHere := eq
                 |}, x)
          end
      | x :: dq =>
          Some
            ({|
               EnqueueHere := EnqueueHere b;
               DequeueHere := dq
             |}, x)
      end
    with
    | Some _ => False
    | None => True
    end
end

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.A: Set
a, b: t A
H: DequeueHere a ++ rev (EnqueueHere a) =
DequeueHere b ++ rev (EnqueueHere b)
match
  match DequeueHere a with
  | [] =>
      match rev (EnqueueHere a) with
      | [] => None
      | x :: eq =>
          Some
            ({|
               EnqueueHere := []; DequeueHere := eq
             |}, x)
      end
  | x :: dq =>
      Some
        ({|
           EnqueueHere := EnqueueHere a;
           DequeueHere := dq
         |}, x)
  end
with
| Some (qa, xa) =>
    match
      match DequeueHere b with
      | [] =>
          match rev (EnqueueHere b) with
          | [] => None
          | x :: eq =>
              Some
                ({|
                   EnqueueHere := [];
                   DequeueHere := eq
                 |}, x)
          end
      | x :: dq =>
          Some
            ({|
               EnqueueHere := EnqueueHere b;
               DequeueHere := dq
             |}, x)
      end
    with
    | Some (qb, xb) =>
        EnqueueHere qa ++ rev (DequeueHere qa) =
        EnqueueHere qb ++ rev (DequeueHere qb) /\
        xa = xb
    | None => False
    end
| None =>
    match
      match DequeueHere b with
      | [] =>
          match rev (EnqueueHere b) with
          | [] => None
          | x :: eq =>
              Some
                ({|
                   EnqueueHere := [];
                   DequeueHere := eq
                 |}, x)
          end
      | x :: dq =>
          Some
            ({|
               EnqueueHere := EnqueueHere b;
               DequeueHere := dq
             |}, x)
      end
    with
    | Some _ => False
    | None => True
    end
end

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.A: Set
a, b: t A
l: list A
a1: A
Heql: DequeueHere b = a1 :: l
l0: list A
H: l0 ++ rev (EnqueueHere a) =
l ++ rev (EnqueueHere b)
Heql0: DequeueHere a = a1 :: l0
EnqueueHere a ++ rev l0 = EnqueueHere b ++ rev l

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:

      {A: Set
a, b: t A
l: list A
a1: A
Heql: DequeueHere b = a1 :: l
l0: list A
H: l0 ++ rev (EnqueueHere a) =
l ++ rev (EnqueueHere b)
Heql0: DequeueHere a = a1 :: l0
EnqueueHere a ++ rev l0 = EnqueueHere b ++ rev l
        apply (f_equal (@rev _)) in H;
          rewrite !rev_app_distr, !rev_involutive in H.A: Set
a, b: t A
l: list A
a1: A
Heql: DequeueHere b = a1 :: l
l0: list A
H: EnqueueHere a ++ rev l0 = EnqueueHere b ++ rev l
Heql0: DequeueHere a = a1 :: l0
EnqueueHere a ++ rev l0 = EnqueueHere b ++ rev l
        assumption. }
    Qed.

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

A similar technique is applicable here:

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

    Theorem empty_dequeue : forall A (q : t A),
        dequeue q = None -> q ~= empty A.forall (A : Set) (q : t A),
dequeue q = None -> q ~= empty A
    Proof.forall (A : Set) (q : t A),
dequeue q = None -> q ~= empty A
      destruct q as [EH DH]; unfold dequeue, empty, equiv, elements;
        simpl; intros.A: Set
EH, DH: list A
H: match DH with
| [] =>
    match rev EH with
    | [] => None
    | x :: eq =>
        Some
          ({|
             EnqueueHere := []; DequeueHere := eq
           |}, x)
    end
| x :: dq =>
    Some
      ({| EnqueueHere := EH; DequeueHere := dq |},
       x)
end = None
EH ++ rev DH = []
      apply rev_inj; rewrite !rev_app_distr, !rev_involutive.A: Set
EH, DH: list A
H: match DH with
| [] =>
    match rev EH with
    | [] => None
    | x :: eq =>
        Some
          ({|
             EnqueueHere := []; DequeueHere := eq
           |}, x)
    end
| x :: dq =>
    Some
      ({| EnqueueHere := EH; DequeueHere := dq |},
       x)
end = None
DH ++ rev EH = rev []
      destruct DH, (rev EH); simpl in *.A: Set
EH: list A
H: None = None
[] = []
A: Set
EH: list A
a: A
l: list A
H: Some
  ({| EnqueueHere := []; DequeueHere := l |}, a) =
None
a :: l = []
A: Set
EH: list A
a: A
DH: list A
H: Some
  ({| EnqueueHere := EH; DequeueHere := DH |}, a) =
None
a :: DH ++ [] = []
A: Set
EH: list A
a: A
DH: list A
H: Some
  ({| EnqueueHere := EH; DequeueHere := DH |}, a) =
None
a0: A
l: list A
a :: DH ++ a0 :: l = []
      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.forall (A : Set) (q : t A) (x : A),
dequeue (enqueue q x) ~~=
match dequeue q with
| Some (q', y) => Some (enqueue q' x, y)
| None => Some (empty A, x)
end
    Proof.forall (A : Set) (q : t A) (x : A),
dequeue (enqueue q x) ~~=
match dequeue q with
| Some (q', y) => Some (enqueue q' x, y)
| None => Some (empty A, x)
end
      destruct q as [EH DH];
        unfold dequeue, enqueue, empty, dequeue_equiv, equiv, elements;
        simpl; intros.A: Set
EH, DH: list A
x: A
match
  match DH with
  | [] =>
      match rev EH ++ [x] with
      | [] => None
      | x :: eq =>
          Some
            ({|
               EnqueueHere := []; DequeueHere := eq
             |}, x)
      end
  | x0 :: dq =>
      Some
        ({|
           EnqueueHere := x :: EH; DequeueHere := dq
         |}, x0)
  end
with
| Some (qa, xa) =>
    match
      match
        match DH with
        | [] =>
            match rev EH with
            | [] => None
            | x :: eq =>
                Some
                  ({|
                     EnqueueHere := [];
                     DequeueHere := eq
                   |}, x)
            end
        | x :: dq =>
            Some
              ({|
                 EnqueueHere := EH; DequeueHere := dq
               |}, x)
        end
      with
      | Some (q', y) =>
          Some
            ({|
               EnqueueHere := x :: EnqueueHere q';
               DequeueHere := DequeueHere q'
             |}, y)
      | None =>
          Some
            ({|
               EnqueueHere := []; DequeueHere := []
             |}, x)
      end
    with
    | Some (qb, xb) =>
        EnqueueHere qa ++ rev (DequeueHere qa) =
        EnqueueHere qb ++ rev (DequeueHere qb) /\
        xa = xb
    | None => False
    end
| None =>
    match
      match
        match DH with
        | [] =>
            match rev EH with
            | [] => None
            | x :: eq =>
                Some
                  ({|
                     EnqueueHere := [];
                     DequeueHere := eq
                   |}, x)
            end
        | x :: dq =>
            Some
              ({|
                 EnqueueHere := EH; DequeueHere := dq
               |}, x)
        end
      with
      | Some (q', y) =>
          Some
            ({|
               EnqueueHere := x :: EnqueueHere q';
               DequeueHere := DequeueHere q'
             |}, y)
      | None =>
          Some
            ({|
               EnqueueHere := []; DequeueHere := []
             |}, x)
      end
    with
    | Some _ => False
    | None => True
    end
end
      destruct DH, (rev EH); simpl; split.A: Set
EH: list A
x: A
[] = []
A: Set
EH: list A
x: A
x = x
A: Set
EH: list A
x, a: A
l: list A
rev (l ++ [x]) = x :: rev l
A: Set
EH: list A
x, a: A
l: list A
a = a
A: Set
EH: list A
a: A
DH: list A
x: A
x :: EH ++ rev DH = x :: EH ++ rev DH
A: Set
EH: list A
a: A
DH: list A
x: A
a = a
A: Set
EH: list A
a: A
DH: list A
x, a0: A
l: list A
x :: EH ++ rev DH = x :: EH ++ rev DH
A: Set
EH: list A
a: A
DH: list A
x, a0: A
l: list A
a = a
      all: rewrite ?rev_app_distr; simpl.A: Set
EH: list A
x: A
[] = []
A: Set
EH: list A
x: A
x = x
A: Set
EH: list A
x, a: A
l: list A
x :: rev l = x :: rev l
A: Set
EH: list A
x, a: A
l: list A
a = a
A: Set
EH: list A
a: A
DH: list A
x: A
x :: EH ++ rev DH = x :: EH ++ rev DH
A: Set
EH: list A
a: A
DH: list A
x: A
a = a
A: Set
EH: list A
a: A
DH: list A
x, a0: A
l: list A
x :: EH ++ rev DH = x :: EH ++ rev DH
A: Set
EH: list A
a: A
DH: list A
x, a0: A
l: list A
a = a
      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.forall (n : nat) (a b : Q.t nat),
a ~= b -> makeQueue n a ~= makeQueue n b
    Proof.forall (n : nat) (a b : Q.t nat),
a ~= b -> makeQueue n a ~= makeQueue n b
      induction n; intros.a, b: Q.t nat
H: a ~= b
makeQueue 0 a ~= makeQueue 0 b
n: nat
IHn: forall a b : Q.t nat, a ~= b -> makeQueue n a ~= makeQueue n b
a, b: Q.t nat
H: a ~= b
makeQueue (S n) a ~= makeQueue (S n) b
      -a, b: Q.t nat
H: a ~= b
makeQueue 0 a ~= makeQueue 0 b assumption.
      -n: nat
IHn: forall a b : Q.t nat, a ~= b -> makeQueue n a ~= makeQueue n b
a, b: Q.t nat
H: a ~= b
makeQueue (S n) a ~= makeQueue (S n) b apply IHn.n: nat
IHn: forall a b : Q.t nat, a ~= b -> makeQueue n a ~= makeQueue n b
a, b: Q.t nat
H: a ~= b
Q.enqueue a n ~= Q.enqueue b n
        apply Q.equiv_enqueue.n: nat
IHn: forall a b : Q.t nat, a ~= b -> makeQueue n a ~= makeQueue n b
a, b: Q.t nat
H: a ~= b
a ~= b
        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.forall (n : nat) (q : Q.t nat),
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.forall (n : nat) (q : Q.t nat),
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
      induction n; simpl; intros.q: Q.t nat
Q.dequeue q ~~=
match Q.dequeue q with
| Some (q', v) => Some (q', v)
| None => None
end
n: nat
IHn: forall q : Q.t nat,
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
q: Q.t nat
Q.dequeue (makeQueue n (Q.enqueue q n)) ~~=
match Q.dequeue q with
| Some (q', v) =>
    Some (makeQueue n (Q.enqueue q' n), v)
| None => Some (makeQueue n q, n)
end
      -q: Q.t nat
Q.dequeue q ~~=
match Q.dequeue q with
| Some (q', v) => Some (q', v)
| None => None
end destruct (Q.dequeue q) as [ [? ?] | ]; simpl.q, t: Q.t nat
n: nat
t ~= t /\ n = n
q: Q.t nat
True
        +q, t: Q.t nat
n: nat
t ~= t /\ n = n split; [ apply Q.equiv_refl | reflexivity ].
        +q: Q.t nat
True tauto.
      -n: nat
IHn: forall q : Q.t nat,
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
q: Q.t nat
Q.dequeue (makeQueue n (Q.enqueue q n)) ~~=
match Q.dequeue q with
| Some (q', v) =>
    Some (makeQueue n (Q.enqueue q' n), v)
| None => Some (makeQueue n q, n)
end specialize (IHn (Q.enqueue q n)).n: nat
q: Q.t nat
IHn: Q.dequeue (makeQueue n (Q.enqueue q n)) ~~=
match Q.dequeue (Q.enqueue q n) with
| Some (q', v) => Some (makeQueue n q', v)
| None =>
match n with
| 0 => None
| S n' => Some (makeQueue n' (Q.enqueue q n), n')
end
end
Q.dequeue (makeQueue n (Q.enqueue q n)) ~~=
match Q.dequeue q with
| Some (q', v) =>
    Some (makeQueue n (Q.enqueue q' n), v)
| None => Some (makeQueue n q, n)
end
        pose proof (Q.dequeue_enqueue q n) as Hde.n: nat
q: Q.t nat
IHn: Q.dequeue (makeQueue n (Q.enqueue q n)) ~~=
match Q.dequeue (Q.enqueue q n) with
| Some (q', v) => Some (makeQueue n q', v)
| None =>
match n with
| 0 => None
| S n' => Some (makeQueue n' (Q.enqueue q n), n')
end
end
Hde: Q.dequeue (Q.enqueue q n) ~~=
match Q.dequeue q with
| Some (q', y) => Some (Q.enqueue q' n, y)
| None => Some (Q.empty nat, n)
end
Q.dequeue (makeQueue n (Q.enqueue q n)) ~~=
match Q.dequeue q with
| Some (q', v) =>
    Some (makeQueue n (Q.enqueue q' n), v)
| None => Some (makeQueue n q, n)
end
        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).n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHn: t0 ~= makeQueue n t /\ n1 = n0
t1: Q.t nat
n2: nat
Hdq: Q.dequeue q = Some (t1, n2)
Hde: t ~= Q.enqueue t1 n /\ n0 = n2
t0 ~= makeQueue n (Q.enqueue t1 n) /\ n1 = n2
n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHn: t0 ~= makeQueue n t /\ n1 = n0
Hdq: Q.dequeue q = None
Hde: t ~= Q.empty nat /\ n0 = n
t0 ~= makeQueue n q /\ n1 = n
        all: destruct IHn as [IHeqv IHeq], Hde as [Heqv Heq];
          split; [ | congruence ].n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
t1: Q.t nat
n2: nat
Hdq: Q.dequeue q = Some (t1, n2)
Heqv: t ~= Q.enqueue t1 n
Heq: n0 = n2
t0 ~= makeQueue n (Q.enqueue t1 n)
n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: Q.dequeue q = None
Heqv: t ~= Q.empty nat
Heq: n0 = n
t0 ~= makeQueue n q
        +n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
t1: Q.t nat
n2: nat
Hdq: Q.dequeue q = Some (t1, n2)
Heqv: t ~= Q.enqueue t1 n
Heq: n0 = n2
t0 ~= makeQueue n (Q.enqueue t1 n) apply Q.equiv_trans with (b := makeQueue n t).n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
t1: Q.t nat
n2: nat
Hdq: Q.dequeue q = Some (t1, n2)
Heqv: t ~= Q.enqueue t1 n
Heq: n0 = n2
t0 ~= makeQueue n t
n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
t1: Q.t nat
n2: nat
Hdq: Q.dequeue q = Some (t1, n2)
Heqv: t ~= Q.enqueue t1 n
Heq: n0 = n2
makeQueue n t ~= makeQueue n (Q.enqueue t1 n)
          *n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
t1: Q.t nat
n2: nat
Hdq: Q.dequeue q = Some (t1, n2)
Heqv: t ~= Q.enqueue t1 n
Heq: n0 = n2
t0 ~= makeQueue n t assumption.
          *n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
t1: Q.t nat
n2: nat
Hdq: Q.dequeue q = Some (t1, n2)
Heqv: t ~= Q.enqueue t1 n
Heq: n0 = n2
makeQueue n t ~= makeQueue n (Q.enqueue t1 n) apply makeQueue_congruence; assumption.
        +n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: Q.dequeue q = None
Heqv: t ~= Q.empty nat
Heq: n0 = n
t0 ~= makeQueue n q apply Q.empty_dequeue in Hdq.n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
t0 ~= makeQueue n q
          apply Q.equiv_trans with (b := makeQueue n t).n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
t0 ~= makeQueue n t
n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
makeQueue n t ~= makeQueue n q
          *n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
t0 ~= makeQueue n t assumption.
          *n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
makeQueue n t ~= makeQueue n q apply makeQueue_congruence.n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
t ~= q
            apply Q.equiv_trans with (b := Q.empty nat).n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
t ~= Q.empty nat
n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
Q.empty nat ~= q
            --n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
t ~= Q.empty nat assumption.
            --n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
Q.empty nat ~= q apply Q.equiv_sym.n: nat
q, t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
IHeqv: t0 ~= makeQueue n t
IHeq: n1 = n0
Hdq: q ~= Q.empty nat
Heqv: t ~= Q.empty nat
Heq: n0 = n
q ~= Q.empty nat
               assumption.
    Qed.

    Theorem computeSum_congruence : forall n a b,
        a ~= b
        -> computeSum n a = computeSum n b.forall (n : nat) (a b : Q.t nat),
a ~= b -> computeSum n a = computeSum n b
    Proof.forall (n : nat) (a b : Q.t nat),
a ~= b -> computeSum n a = computeSum n b
      induction n; simpl; intros * Heqv.a, b: Q.t nat
Heqv: a ~= b
0 = 0
n: nat
IHn: forall a b : Q.t nat,
a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
match Q.dequeue a with
| Some (q', v) => v + computeSum n q'
| None => 0
end =
match Q.dequeue b with
| Some (q', v) => v + computeSum n q'
| None => 0
end
      -a, b: Q.t nat
Heqv: a ~= b
0 = 0 reflexivity.
      -n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
match Q.dequeue a with
| Some (q', v) => v + computeSum n q'
| None => 0
end =
match Q.dequeue b with
| Some (q', v) => v + computeSum n q'
| None => 0
end pose proof (Q.equiv_dequeue a b Heqv) as Heqd.n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
Heqd: Q.dequeue a ~~= Q.dequeue b
match Q.dequeue a with
| Some (q', v) => v + computeSum n q'
| None => 0
end =
match Q.dequeue b with
| Some (q', v) => v + computeSum n q'
| None => 0
end
        unfold Q.dequeue_equiv in Heqd.n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
Heqd: match Q.dequeue a with
| Some (qa, xa) =>
    match Q.dequeue b with
    | Some (qb, xb) => qa ~= qb /\ xa = xb
    | None => False
    end
| None =>
    match Q.dequeue b with
    | Some _ => False
    | None => True
    end
end
match Q.dequeue a with
| Some (q', v) => v + computeSum n q'
| None => 0
end =
match Q.dequeue b with
| Some (q', v) => v + computeSum n q'
| None => 0
end
        destruct (Q.dequeue a) as [[??]|], (Q.dequeue b) as [[??]|].n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
Heqd: t ~= t0 /\ n0 = n1
n0 + computeSum n t = n1 + computeSum n t0
n: nat
IHn: forall a b : Q.t nat,
a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
t: Q.t nat
n0: nat
Heqd: False
n0 + computeSum n t = 0
n: nat
IHn: forall a b : Q.t nat,
a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
t: Q.t nat
n0: nat
Heqd: False
0 = n0 + computeSum n t
n: nat
IHn: forall a b : Q.t nat,
a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
Heqd: True
0 = 0
        +n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
Heqd: t ~= t0 /\ n0 = n1
n0 + computeSum n t = n1 + computeSum n t0 destruct Heqd as [Heqv' Heq].n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
Heqv': t ~= t0
Heq: n0 = n1
n0 + computeSum n t = n1 + computeSum n t0
          rewrite (IHn _ _ Heqv'), Heq.n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
t: Q.t nat
n0: nat
t0: Q.t nat
n1: nat
Heqv': t ~= t0
Heq: n0 = n1
n1 + computeSum n t0 = n1 + computeSum n t0
          reflexivity.
        +n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
t: Q.t nat
n0: nat
Heqd: False
n0 + computeSum n t = 0 exfalso; assumption.
        +n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
t: Q.t nat
n0: nat
Heqd: False
0 = n0 + computeSum n t exfalso; assumption.
        +n: nat
IHn: forall a b : Q.t nat, a ~= b -> computeSum n a = computeSum n b
a, b: Q.t nat
Heqv: a ~= b
Heqd: True
0 = 0 reflexivity.
    Qed.

    Theorem computeSum_ok : forall n,
        computeSum n (makeQueue n (Q.empty nat)) = sumUpto n.forall n : nat,
computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
    Proof.forall n : nat,
computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
      induction n; simpl; intros.0 = 0
n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
match
  Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n))
with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
      -0 = 0 reflexivity.
      -n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
match
  Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n))
with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n pose proof (dequeue_makeQueue n (Q.enqueue (Q.empty nat) n))
          as HdmQ.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
HdmQ: Q.dequeue
  (makeQueue n (Q.enqueue (Q.empty nat) n)) ~~=
match
  Q.dequeue (Q.enqueue (Q.empty nat) n)
with
| Some (q', v) => Some (makeQueue n q', v)
| None =>
    match n with
    | 0 => None
    | S n' =>
        Some
          (makeQueue n'
             (Q.enqueue (Q.empty nat) n), n')
    end
end
match
  Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n))
with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
        pose proof (Q.dequeue_enqueue (Q.empty nat) n) as Hdev.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
HdmQ: Q.dequeue
  (makeQueue n (Q.enqueue (Q.empty nat) n)) ~~=
match
  Q.dequeue (Q.enqueue (Q.empty nat) n)
with
| Some (q', v) => Some (makeQueue n q', v)
| None =>
    match n with
    | 0 => None
    | S n' =>
        Some
          (makeQueue n'
             (Q.enqueue (Q.empty nat) n), n')
    end
end
Hdev: Q.dequeue (Q.enqueue (Q.empty nat) n) ~~=
match Q.dequeue (Q.empty nat) with
| Some (q', y) => Some (Q.enqueue q' n, y)
| None => Some (Q.empty nat, n)
end
match
  Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n))
with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
        unfold Q.dequeue_equiv in *.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
HdmQ: match
  Q.dequeue
    (makeQueue n (Q.enqueue (Q.empty nat) n))
with
| Some (qa, xa) =>
    match
      match
        Q.dequeue (Q.enqueue (Q.empty nat) n)
      with
      | Some (q', v) =>
          Some (makeQueue n q', v)
      | None =>
          match n with
          | 0 => None
          | S n' =>
              Some
                (makeQueue n'
                   (Q.enqueue (Q.empty nat) n),
                 n')
          end
      end
    with
    | Some (qb, xb) => qa ~= qb /\ xa = xb
    | None => False
    end
| None =>
    match
      match
        Q.dequeue (Q.enqueue (Q.empty nat) n)
      with
      | Some (q', v) =>
          Some (makeQueue n q', v)
      | None =>
          match n with
          | 0 => None
          | S n' =>
              Some
                (makeQueue n'
                   (Q.enqueue (Q.empty nat) n),
                 n')
          end
      end
    with
    | Some _ => False
    | None => True
    end
end
Hdev: match
  Q.dequeue (Q.enqueue (Q.empty nat) n)
with
| Some (qa, xa) =>
    match
      match Q.dequeue (Q.empty nat) with
      | Some (q', y) =>
          Some (Q.enqueue q' n, y)
      | None => Some (Q.empty nat, n)
      end
    with
    | Some (qb, xb) => qa ~= qb /\ xa = xb
    | None => False
    end
| None =>
    match
      match Q.dequeue (Q.empty nat) with
      | Some (q', y) =>
          Some (Q.enqueue q' n, y)
      | None => Some (Q.empty nat, n)
      end
    with
    | Some _ => False
    | None => True
    end
end
match
  Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n))
with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
        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 *.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
n0: nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n0)
t0: Q.t nat
n1: nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n1)
HdmQ: t ~= makeQueue n t0 /\ n0 = n1
Hdev: match
  match Q.dequeue (Q.empty nat) with
  | Some (q', y) => Some (Q.enqueue q' n, y)
  | None => Some (Q.empty nat, n)
  end
with
| Some (qb, xb) => t0 ~= qb /\ n1 = xb
| None => False
end
n0 + computeSum n t = n + sumUpto n
n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) =
sumUpto n
t: Q.t nat
n0: nat
Hdm: Q.dequeue
  (makeQueue n (Q.enqueue (Q.empty nat) n)) =
Some (t, n0)
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = None
HdmQ: match
  match n with
  | 0 => None
  | S n' =>
      Some
        (makeQueue n'
           (Q.enqueue (Q.empty nat) n), n')
  end
with
| Some (qb, xb) => t ~= qb /\ n0 = xb
| None => False
end
Hdev: match
  match Q.dequeue (Q.empty nat) with
  | Some (q', y) => Some (Q.enqueue q' n, y)
  | None => Some (Q.empty nat, n)
  end
with
| Some _ => False
| None => True
end
n0 + computeSum n t = n + sumUpto n
n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) =
sumUpto n
Hdm: Q.dequeue
  (makeQueue n (Q.enqueue (Q.empty nat) n)) =
None
t: Q.t nat
n0: nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) =
Some (t, n0)
HdmQ: False
Hdev: match
  match Q.dequeue (Q.empty nat) with
  | Some (q', y) => Some (Q.enqueue q' n, y)
  | None => Some (Q.empty nat, n)
  end
with
| Some (qb, xb) => t ~= qb /\ n0 = xb
| None => False
end
0 = n + sumUpto n
n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) =
sumUpto n
Hdm: Q.dequeue
  (makeQueue n (Q.enqueue (Q.empty nat) n)) =
None
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = None
HdmQ: match
  match n with
  | 0 => None
  | S n' =>
      Some
        (makeQueue n'
           (Q.enqueue (Q.empty nat) n), n')
  end
with
| Some _ => False
| None => True
end
Hdev: match
  match Q.dequeue (Q.empty nat) with
  | Some (q', y) => Some (Q.enqueue q' n, y)
  | None => Some (Q.empty nat, n)
  end
with
| Some _ => False
| None => True
end
0 = n + sumUpto n
        all: rewrite Q.dequeue_empty in Hdev.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
n0: nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n0)
t0: Q.t nat
n1: nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n1)
HdmQ: t ~= makeQueue n t0 /\ n0 = n1
Hdev: t0 ~= Q.empty nat /\ n1 = n
n0 + computeSum n t = n + sumUpto n
n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) =
sumUpto n
t: Q.t nat
n0: nat
Hdm: Q.dequeue
  (makeQueue n (Q.enqueue (Q.empty nat) n)) =
Some (t, n0)
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = None
HdmQ: match
  match n with
  | 0 => None
  | S n' =>
      Some
        (makeQueue n'
           (Q.enqueue (Q.empty nat) n), n')
  end
with
| Some (qb, xb) => t ~= qb /\ n0 = xb
| None => False
end
Hdev: False
n0 + computeSum n t = n + sumUpto n
n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) =
sumUpto n
Hdm: Q.dequeue
  (makeQueue n (Q.enqueue (Q.empty nat) n)) =
None
t: Q.t nat
n0: nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) =
Some (t, n0)
HdmQ: False
Hdev: t ~= Q.empty nat /\ n0 = n
0 = n + sumUpto n
n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) =
sumUpto n
Hdm: Q.dequeue
  (makeQueue n (Q.enqueue (Q.empty nat) n)) =
None
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = None
HdmQ: match
  match n with
  | 0 => None
  | S n' =>
      Some
        (makeQueue n'
           (Q.enqueue (Q.empty nat) n), n')
  end
with
| Some _ => False
| None => True
end
Hdev: False
0 = n + sumUpto n
        all: try (exfalso; assumption).n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
n0: nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n0)
t0: Q.t nat
n1: nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n1)
HdmQ: t ~= makeQueue n t0 /\ n0 = n1
Hdev: t0 ~= Q.empty nat /\ n1 = n
n0 + computeSum n t = n + sumUpto n
        {n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
n0: nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n0)
t0: Q.t nat
n1: nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n1)
HdmQ: t ~= makeQueue n t0 /\ n0 = n1
Hdev: t0 ~= Q.empty nat /\ n1 = n
n0 + computeSum n t = n + sumUpto n destruct HdmQ as [Heqv Heq], Hdev as [Hdeqv Hdeq]; subst.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n)
t0: Q.t nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n)
Heqv: t ~= makeQueue n t0
Hdeqv: t0 ~= Q.empty nat
n + computeSum n t = n + sumUpto n
          rewrite <- IHn.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n)
t0: Q.t nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n)
Heqv: t ~= makeQueue n t0
Hdeqv: t0 ~= Q.empty nat
n + computeSum n t =
n + computeSum n (makeQueue n (Q.empty nat))
          f_equal.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n)
t0: Q.t nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n)
Heqv: t ~= makeQueue n t0
Hdeqv: t0 ~= Q.empty nat
computeSum n t =
computeSum n (makeQueue n (Q.empty nat))
          apply computeSum_congruence.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n)
t0: Q.t nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n)
Heqv: t ~= makeQueue n t0
Hdeqv: t0 ~= Q.empty nat
t ~= makeQueue n (Q.empty nat)
          apply Q.equiv_trans with (b := makeQueue n t0).n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n)
t0: Q.t nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n)
Heqv: t ~= makeQueue n t0
Hdeqv: t0 ~= Q.empty nat
t ~= makeQueue n t0
n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) =
sumUpto n
t: Q.t nat
Hdm: Q.dequeue
  (makeQueue n (Q.enqueue (Q.empty nat) n)) =
Some (t, n)
t0: Q.t nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) =
Some (t0, n)
Heqv: t ~= makeQueue n t0
Hdeqv: t0 ~= Q.empty nat
makeQueue n t0 ~= makeQueue n (Q.empty nat)
          -n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n)
t0: Q.t nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n)
Heqv: t ~= makeQueue n t0
Hdeqv: t0 ~= Q.empty nat
t ~= makeQueue n t0 assumption.
          -n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n)
t0: Q.t nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n)
Heqv: t ~= makeQueue n t0
Hdeqv: t0 ~= Q.empty nat
makeQueue n t0 ~= makeQueue n (Q.empty nat) apply makeQueue_congruence.n: nat
IHn: computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
t: Q.t nat
Hdm: Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n)) = Some (t, n)
t0: Q.t nat
Hde: Q.dequeue (Q.enqueue (Q.empty nat) n) = Some (t0, n)
Heqv: t ~= makeQueue n t0
Hdeqv: t0 ~= Q.empty nat
t0 ~= Q.empty nat
            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) = [].forall A : Set, rep (empty A) = []

Solution

    Proof.forall A : Set, rep (empty A) = []
      reflexivity.
    Qed.

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

Solution

    Proof.forall (A : Set) (q : t A) (x : A),
rep (enqueue q x) = x :: rep q
      reflexivity.
    Qed.

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

Solution

    Proof.forall (A : Set) (q : t A),
rep q = [] -> dequeue q = None
      unfold rep; simpl; intros * ->.A: Set
dequeue [] = None
      reflexivity.
    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.forall (A : Set) (q : t A) (xs : list A) (x : A),
rep q = xs ++ [x] ->
exists q' : t A,
  dequeue q = Some (q', x) /\ rep q' = xs

Solution

    Proof.forall (A : Set) (q : t A) (xs : list A) (x : A),
rep q = xs ++ [x] ->
exists q' : t A,
  dequeue q = Some (q', x) /\ rep q' = xs
      unfold rep; induction q; simpl; intros.A: Set
xs: list A
x: A
H: [] = xs ++ [x]
exists q' : t A, None = Some (q', x) /\ q' = xs
A: Set
a: A
q: list A
IHq: forall (xs : list A) (x : A),
q = xs ++ [x] -> exists q' : t A, dequeue q = Some (q', x) /\ q' = xs
xs: list A
x: A
H: a :: q = xs ++ [x]
exists q' : t A,
  match dequeue q with
  | Some (q'', y) => Some (a :: q'', y)
  | None => Some ([], a)
  end = Some (q', x) /\ q' = xs
      -A: Set
xs: list A
x: A
H: [] = xs ++ [x]
exists q' : t A, None = Some (q', x) /\ q' = xs destruct xs; simpl in *; congruence.
      -A: Set
a: A
q: list A
IHq: forall (xs : list A) (x : A),
q = xs ++ [x] -> exists q' : t A, dequeue q = Some (q', x) /\ q' = xs
xs: list A
x: A
H: a :: q = xs ++ [x]
exists q' : t A,
  match dequeue q with
  | Some (q'', y) => Some (a :: q'', y)
  | None => Some ([], a)
  end = Some (q', x) /\ q' = xs destruct xs; simpl in *.A: Set
a: A
q: list A
IHq: forall (xs : list A) (x : A),
q = xs ++ [x] -> exists q' : t A, dequeue q = Some (q', x) /\ q' = xs
x: A
H: a :: q = [x]
exists q' : t A,
  match dequeue q with
  | Some (q'', y) => Some (a :: q'', y)
  | None => Some ([], a)
  end = Some (q', x) /\ q' = []
A: Set
a: A
q: list A
IHq: forall (xs : list A) (x : A),
q = xs ++ [x] -> exists q' : t A, dequeue q = Some (q', x) /\ q' = xs
a0: A
xs: list A
x: A
H: a :: q = a0 :: xs ++ [x]
exists q' : t A,
  match dequeue q with
  | Some (q'', y) => Some (a :: q'', y)
  | None => Some ([], a)
  end = Some (q', x) /\ q' = a0 :: xs
        all: injection H as H; subst; simpl in *.A: Set
IHq: forall (xs : list A) (x : A),
[] = xs ++ [x] -> exists q' : t A, None = Some (q', x) /\ q' = xs
x: A
exists q' : t A,
  Some ([], x) = Some (q', x) /\ q' = []
A: Set
xs: list A
x: A
IHq: forall (xs0 : list A) (x0 : A),
xs ++ [x] = xs0 ++ [x0] ->
exists q' : t A, dequeue (xs ++ [x]) = Some (q', x0) /\ q' = xs0
a0: A
exists q' : t A,
  match dequeue (xs ++ [x]) with
  | Some (q'', y) => Some (a0 :: q'', y)
  | None => Some ([], a0)
  end = Some (q', x) /\ q' = a0 :: xs
        +A: Set
IHq: forall (xs : list A) (x : A),
[] = xs ++ [x] -> exists q' : t A, None = Some (q', x) /\ q' = xs
x: A
exists q' : t A,
  Some ([], x) = Some (q', x) /\ q' = [] exists []; split; reflexivity.
        +A: Set
xs: list A
x: A
IHq: forall (xs0 : list A) (x0 : A),
xs ++ [x] = xs0 ++ [x0] ->
exists q' : t A, dequeue (xs ++ [x]) = Some (q', x0) /\ q' = xs0
a0: A
exists q' : t A,
  match dequeue (xs ++ [x]) with
  | Some (q'', y) => Some (a0 :: q'', y)
  | None => Some ([], a0)
  end = Some (q', x) /\ q' = a0 :: xs specialize (IHq _ _ eq_refl).A: Set
xs: list A
x: A
IHq: exists q' : t A, dequeue (xs ++ [x]) = Some (q', x) /\ q' = xs
a0: A
exists q' : t A,
  match dequeue (xs ++ [x]) with
  | Some (q'', y) => Some (a0 :: q'', y)
  | None => Some ([], a0)
  end = Some (q', x) /\ q' = a0 :: xs
          destruct IHq as [q' [-> ->]].A: Set
xs: list A
x, a0: A
exists q' : t A,
  Some (a0 :: xs, x) = Some (q', x) /\ q' = a0 :: xs
          eexists; split; reflexivity.
    Qed.

  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) = [].forall A : Set, rep (empty A) = []

Solution

    Proof.forall A : Set, rep (empty A) = []
      reflexivity.
    Qed.

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

Solution

    Proof.forall (A : Set) (q : t A) (x : A),
rep (enqueue q x) = x :: rep q
      reflexivity.
    Qed.

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

Solution

    Proof.forall (A : Set) (q : t A),
rep q = [] -> dequeue q = None
      unfold rep, dequeue; intros.A: Set
q: t A
H: EnqueueHere q ++ rev (DequeueHere q) = []
match DequeueHere q with
| [] =>
    match rev (EnqueueHere q) with
    | [] => None
    | x :: eq =>
        Some
          ({| EnqueueHere := []; DequeueHere := eq |},
           x)
    end
| x :: dq =>
    Some
      ({|
         EnqueueHere := EnqueueHere q;
         DequeueHere := dq
       |}, x)
end = None
      destruct (EnqueueHere q), (DequeueHere q); simpl in *.A: Set
q: t A
H: [] = []
None = None
A: Set
q: t A
a: A
l: list A
H: rev l ++ [a] = []
Some ({| EnqueueHere := []; DequeueHere := l |}, a) =
None
A: Set
q: t A
a: A
l: list A
H: a :: l ++ [] = []
match rev l ++ [a] with
| [] => None
| x :: eq =>
    Some
      ({| EnqueueHere := []; DequeueHere := eq |}, x)
end = None
A: Set
q: t A
a: A
l: list A
a0: A
l0: list A
H: a :: l ++ rev l0 ++ [a0] = []
Some
  ({| EnqueueHere := a :: l; DequeueHere := l0 |}, a0) =
None
      -A: Set
q: t A
H: [] = []
None = None reflexivity.
      -A: Set
q: t A
a: A
l: list A
H: rev l ++ [a] = []
Some ({| EnqueueHere := []; DequeueHere := l |}, a) =
None destruct (rev _); simpl in *; congruence.
      -A: Set
q: t A
a: A
l: list A
H: a :: l ++ [] = []
match rev l ++ [a] with
| [] => None
| x :: eq =>
    Some
      ({| EnqueueHere := []; DequeueHere := eq |}, x)
end = None congruence.
      -A: Set
q: t A
a: A
l: list A
a0: A
l0: list A
H: a :: l ++ rev l0 ++ [a0] = []
Some
  ({| EnqueueHere := a :: l; DequeueHere := l0 |}, a0) =
None congruence.
    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.forall (A : Set) (q : t A) (xs : list A) (x : A),
rep q = xs ++ [x] ->
exists q' : t A,
  dequeue q = Some (q', x) /\ rep q' = xs

Solution

    Ltac rev_both H :=
      apply (f_equal (@rev _)) in H;
      rewrite ?rev_app_distr, ?rev_involutive in H; simpl in H.forall (A : Set) (q : t A) (xs : list A) (x : A),
rep q = xs ++ [x] ->
exists q' : t A,
  dequeue q = Some (q', x) /\ rep q' = xs

    Proof.forall (A : Set) (q : t A) (xs : list A) (x : A),
rep q = xs ++ [x] ->
exists q' : t A,
  dequeue q = Some (q', x) /\ rep q' = xs
      unfold rep, dequeue; intros * H; rev_both H.A: Set
q: t A
xs: list A
x: A
H: DequeueHere q ++ rev (EnqueueHere q) = x :: rev xs
exists q' : t A,
  match DequeueHere q with
  | [] =>
      match rev (EnqueueHere q) with
      | [] => None
      | x :: eq =>
          Some
            ({|
               EnqueueHere := []; DequeueHere := eq
             |}, x)
      end
  | x :: dq =>
      Some
        ({|
           EnqueueHere := EnqueueHere q;
           DequeueHere := dq
         |}, x)
  end = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
      destruct (DequeueHere q), (rev (EnqueueHere q)) eqn:HE;
        simpl in *.A: Set
q: t A
xs: list A
x: A
HE: rev (EnqueueHere q) = []
H: [] = x :: rev xs
exists q' : t A,
  None = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
A: Set
q: t A
xs: list A
x, a: A
l: list A
HE: rev (EnqueueHere q) = a :: l
H: a :: l = x :: rev xs
exists q' : t A,
  Some ({| EnqueueHere := []; DequeueHere := l |}, a) =
  Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
A: Set
q: t A
xs: list A
x, a: A
l: list A
HE: rev (EnqueueHere q) = []
H: a :: l ++ [] = x :: rev xs
exists q' : t A,
  Some
    ({|
       EnqueueHere := EnqueueHere q; DequeueHere := l
     |}, a) = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
A: Set
q: t A
xs: list A
x, a: A
l: list A
a0: A
l0: list A
HE: rev (EnqueueHere q) = a0 :: l0
H: a :: l ++ a0 :: l0 = x :: rev xs
exists q' : t A,
  Some
    ({|
       EnqueueHere := EnqueueHere q; DequeueHere := l
     |}, a) = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
      all: try congruence.A: Set
q: t A
xs: list A
x, a: A
l: list A
HE: rev (EnqueueHere q) = a :: l
H: a :: l = x :: rev xs
exists q' : t A,
  Some ({| EnqueueHere := []; DequeueHere := l |}, a) =
  Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
A: Set
q: t A
xs: list A
x, a: A
l: list A
HE: rev (EnqueueHere q) = []
H: a :: l ++ [] = x :: rev xs
exists q' : t A,
  Some
    ({|
       EnqueueHere := EnqueueHere q; DequeueHere := l
     |}, a) = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
A: Set
q: t A
xs: list A
x, a: A
l: list A
a0: A
l0: list A
HE: rev (EnqueueHere q) = a0 :: l0
H: a :: l ++ a0 :: l0 = x :: rev xs
exists q' : t A,
  Some
    ({|
       EnqueueHere := EnqueueHere q; DequeueHere := l
     |}, a) = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
      all: injection H as Hhd Htl; subst.A: Set
q: t A
xs: list A
x: A
HE: rev (EnqueueHere q) = x :: rev xs
exists q' : t A,
  Some
    ({| EnqueueHere := []; DequeueHere := rev xs |}, x) =
  Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
A: Set
q: t A
xs: list A
x: A
l: list A
HE: rev (EnqueueHere q) = []
Htl: l ++ [] = rev xs
exists q' : t A,
  Some
    ({|
       EnqueueHere := EnqueueHere q; DequeueHere := l
     |}, x) = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
A: Set
q: t A
xs: list A
x: A
l: list A
a0: A
l0: list A
HE: rev (EnqueueHere q) = a0 :: l0
Htl: l ++ a0 :: l0 = rev xs
exists q' : t A,
  Some
    ({|
       EnqueueHere := EnqueueHere q; DequeueHere := l
     |}, x) = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
      all: rewrite ?app_nil_r in *; subst.A: Set
q: t A
xs: list A
x: A
HE: rev (EnqueueHere q) = x :: rev xs
exists q' : t A,
  Some
    ({| EnqueueHere := []; DequeueHere := rev xs |}, x) =
  Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
A: Set
q: t A
xs: list A
x: A
HE: rev (EnqueueHere q) = []
exists q' : t A,
  Some
    ({|
       EnqueueHere := EnqueueHere q;
       DequeueHere := rev xs
     |}, x) = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
A: Set
q: t A
xs: list A
x: A
l: list A
a0: A
l0: list A
HE: rev (EnqueueHere q) = a0 :: l0
Htl: l ++ a0 :: l0 = rev xs
exists q' : t A,
  Some
    ({|
       EnqueueHere := EnqueueHere q; DequeueHere := l
     |}, x) = Some (q', x) /\
  EnqueueHere q' ++ rev (DequeueHere q') = xs
      all: eexists; split; [reflexivity|simpl].A: Set
q: t A
xs: list A
x: A
HE: rev (EnqueueHere q) = x :: rev xs
rev (rev xs) = xs
A: Set
q: t A
xs: list A
x: A
HE: rev (EnqueueHere q) = []
EnqueueHere q ++ rev (rev xs) = xs
A: Set
q: t A
xs: list A
x: A
l: list A
a0: A
l0: list A
HE: rev (EnqueueHere q) = a0 :: l0
Htl: l ++ a0 :: l0 = rev xs
EnqueueHere q ++ rev l = xs
      -A: Set
q: t A
xs: list A
x: A
HE: rev (EnqueueHere q) = x :: rev xs
rev (rev xs) = xs apply rev_involutive.
      -A: Set
q: t A
xs: list A
x: A
HE: rev (EnqueueHere q) = []
EnqueueHere q ++ rev (rev xs) = xs rev_both HE; rewrite HE, rev_involutive.A: Set
q: t A
xs: list A
x: A
HE: EnqueueHere q = []
[] ++ xs = xs
        reflexivity.
      -A: Set
q: t A
xs: list A
x: A
l: list A
a0: A
l0: list A
HE: rev (EnqueueHere q) = a0 :: l0
Htl: l ++ a0 :: l0 = rev xs
EnqueueHere q ++ rev l = xs rev_both HE; rewrite HE.A: Set
q: t A
xs: list A
x: A
l: list A
a0: A
l0: list A
HE: EnqueueHere q = rev l0 ++ [a0]
Htl: l ++ a0 :: l0 = rev xs
(rev l0 ++ [a0]) ++ rev l = xs
        rev_both Htl; rewrite Htl.A: Set
q: t A
xs: list A
x: A
l: list A
a0: A
l0: list A
HE: EnqueueHere q = rev l0 ++ [a0]
Htl: (rev l0 ++ [a0]) ++ rev l = xs
xs = xs
        reflexivity.
    Qed.

  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.

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

Solution

    Proof.forall (n : nat) (q : Q.t nat),
Q.rep (makeQueue n q) = upto n ++ Q.rep q
      induction n; simpl; intros.q: Q.t nat
Q.rep q = Q.rep q
n: nat
IHn: forall q : Q.t nat, Q.rep (makeQueue n q) = upto n ++ Q.rep q
q: Q.t nat
Q.rep (makeQueue n (Q.enqueue q n)) =
(upto n ++ [n]) ++ Q.rep q
      -q: Q.t nat
Q.rep q = Q.rep q reflexivity.
      -n: nat
IHn: forall q : Q.t nat, Q.rep (makeQueue n q) = upto n ++ Q.rep q
q: Q.t nat
Q.rep (makeQueue n (Q.enqueue q n)) =
(upto n ++ [n]) ++ Q.rep q rewrite IHn.n: nat
IHn: forall q : Q.t nat, Q.rep (makeQueue n q) = upto n ++ Q.rep q
q: Q.t nat
upto n ++ Q.rep (Q.enqueue q n) =
(upto n ++ [n]) ++ Q.rep q
        rewrite Q.enqueue_rep.n: nat
IHn: forall q : Q.t nat, Q.rep (makeQueue n q) = upto n ++ Q.rep q
q: Q.t nat
upto n ++ n :: Q.rep q = (upto n ++ [n]) ++ Q.rep q
        rewrite <- app_assoc.n: nat
IHn: forall q : Q.t nat, Q.rep (makeQueue n q) = upto n ++ Q.rep q
q: Q.t nat
upto n ++ n :: Q.rep q = upto n ++ [n] ++ Q.rep q
        reflexivity.
    Qed.

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

Solution

    Proof.forall (n : nat) (q : Q.t nat),
Q.rep q = upto n -> computeSum n q = sumUpto n
      induction n; simpl; intros.q: Q.t nat
H: Q.rep q = []
0 = 0
n: nat
IHn: forall q : Q.t nat, Q.rep q = upto n -> computeSum n q = sumUpto n
q: Q.t nat
H: Q.rep q = upto n ++ [n]
match Q.dequeue q with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
      -q: Q.t nat
H: Q.rep q = []
0 = 0 reflexivity.
      -n: nat
IHn: forall q : Q.t nat, Q.rep q = upto n -> computeSum n q = sumUpto n
q: Q.t nat
H: Q.rep q = upto n ++ [n]
match Q.dequeue q with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n pose proof (Q.dequeue_nonempty _ _ _ H) as [q' [Hdq Hrep]].n: nat
IHn: forall q : Q.t nat, Q.rep q = upto n -> computeSum n q = sumUpto n
q: Q.t nat
H: Q.rep q = upto n ++ [n]
q': Q.t nat
Hdq: Q.dequeue q = Some (q', n)
Hrep: Q.rep q' = upto n
match Q.dequeue q with
| Some (q', v) => v + computeSum n q'
| None => 0
end = n + sumUpto n
        rewrite Hdq.n: nat
IHn: forall q : Q.t nat,
Q.rep q = upto n -> computeSum n q = sumUpto n
q: Q.t nat
H: Q.rep q = upto n ++ [n]
q': Q.t nat
Hdq: Q.dequeue q = Some (q', n)
Hrep: Q.rep q' = upto n
n + computeSum n q' = n + sumUpto n
        rewrite IHn by assumption.n: nat
IHn: forall q : Q.t nat,
Q.rep q = upto n -> computeSum n q = sumUpto n
q: Q.t nat
H: Q.rep q = upto n ++ [n]
q': Q.t nat
Hdq: Q.dequeue q = Some (q', n)
Hrep: Q.rep q' = upto n
n + sumUpto n = n + sumUpto n
        reflexivity.
    Qed.

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

Solution

    Proof.forall n : nat,
computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
      intros.n: nat
computeSum n (makeQueue n (Q.empty nat)) = sumUpto n
      apply computeSum_makeQueue'.n: nat
Q.rep (makeQueue n (Q.empty nat)) = upto n
      rewrite makeQueue_rep.n: nat
upto n ++ Q.rep (Q.empty nat) = upto n
      rewrite Q.empty_rep.n: nat
upto n ++ [] = upto n
      apply app_nil_r.
    Qed.
  End DelayedSum.
End RepFunction.