Require Import Frap.

Set Implicit Arguments.


(** * Specification styles for data abstraction *)

(* One of the classic formalisms for data abstraction is the *algebraic* style,
 * where requirements on implementations are written out as quantified
 * equalities.  Any implementation must satisfy these equalities, but we grant
 * implementations freedom in internal details. *)
Module Algebraic.
  (* Here's an example of an algebraic interface or *specification* ("spec" for
   * short).  It's for purely functional queues, which follow first-in-first-out
   * disciplines. *)
  Module Type QUEUE.
    Parameter t : Set -> Set.

    Parameter empty : forall A, t A.
    Parameter enqueue : forall A, t A -> A -> t A.
    Parameter dequeue : forall A, t A -> option (t A * A).

















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


















    Axiom dequeue_enqueue : forall A (q : t A) x,
        dequeue (enqueue q x) = Some (match dequeue q with
                                      | None => (empty A, x)
                                      | Some (q', y) => (enqueue q' x, y)
                                      end).
  End QUEUE.

  (* First, there is a fairly straightforward implementation with lists. *)
  Module ListQueue : QUEUE.
    Definition t : Set -> Set := list.

    Definition empty A : t A. Admitted.
    Definition enqueue A (q : t A) (x : A) : t A. Admitted.
    Fixpoint dequeue A (q : t A) : option (t A * A). Admitted.

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

    Theorem empty_dequeue : forall A (q : t A),
        dequeue q = None -> q = empty A.
    Proof.
    Admitted.

    Theorem dequeue_enqueue : forall A (q : t A) x,
        dequeue (enqueue q x) = Some (match dequeue q with
                                      | None => (empty A, x)
                                      | Some (q', y) => (enqueue q' x, y)
                                      end).
    Proof.
    Admitted.
  End ListQueue.

















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

    Definition empty A : t A. Admitted.
    Definition enqueue A (q : t A) (x : A) : t A. Admitted.
    Fixpoint dequeue A (q : t A) : option (t A * A). Admitted.

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

    Theorem empty_dequeue : forall A (q : t A),
        dequeue q = None -> q = empty A.
    Proof.
    Admitted.

    Theorem dequeue_enqueue : forall A (q : t A) x,
        dequeue (enqueue q x) = Some (match dequeue q with
                                      | None => (empty A, x)
                                      | Some (q', y) => (enqueue q' x, y)
                                      end).
    Proof.
    Admitted.
  End ReversedListQueue.





  Module DelayedSum (Q : QUEUE).
    (* First, the function to enqueue the first [n] natural numbers. *)
    Fixpoint makeQueue (n : nat) (q : Q.t nat) : Q.t nat :=
      match n with
      | 0 => q
      | S n' => makeQueue n' (Q.enqueue q n')
      end.

    (* Next, the function to dequeue repeatedly, keeping a sum. *)
    Fixpoint computeSum (n : nat) (q : Q.t nat) : nat :=
      match n with
      | 0 => 0
      | S n' => match Q.dequeue q with
                | None => 0
                | Some (q', v) => v + computeSum n' q'
                end
      end.

    (* This function gives the expected answer, in a simpler form, of
     * [computeSum] after [makeQueue]. *)
    Fixpoint sumUpto (n : nat) : nat :=
      match n with
      | 0 => 0
      | S n' => n' + sumUpto n'
      end.

    Theorem computeSum_ok : forall n,
        computeSum n (makeQueue n (Q.empty nat)) = sumUpto n.
    Proof.
    Admitted.
  End DelayedSum.
End Algebraic.













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

    Parameter empty : forall A, t A.
    Parameter enqueue : forall A, t A -> A -> t A.
    Parameter dequeue : forall A, t A -> option (t A * A).

    (* v-- New part! *)
    Parameter equiv : forall A, t A -> t A -> Prop.
    Infix "~=" := equiv (at level 70).

    (* It really is an equivalence relation. *)
    Axiom equiv_refl : forall A (a : t A), a ~= a.
    Axiom equiv_sym : forall A (a b : t A), a ~= b -> b ~= a.
    Axiom equiv_trans : forall A (a b c : t A), a ~= b -> b ~= c -> a ~= c.

    Axiom equiv_enqueue : forall A (a b : t A) (x : A),
        a ~= b
        -> enqueue a x ~= enqueue b x.

    (* We define a derived relation for results of [dequeue]. *)
    Definition dequeue_equiv A (a b : option (t A * A)) :=
      match a, b with
      | None, None => True
      | Some (qa, xa), Some (qb, xb) => qa ~= qb /\ xa = xb
      | _, _ => False
      end.

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

    Axiom equiv_dequeue : forall A (a b : t A),
        a ~= b
        -> dequeue a ~~= dequeue b.

    (* We retain the three axioms from the prior interface, using our fancy
     * relation instead of equality on queues. *)

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

    Axiom dequeue_enqueue : forall A (q : t A) x,
        dequeue (enqueue q x)
        ~~= match dequeue q with
            | None => Some (empty A, x)
            | Some (q', y) => Some (enqueue q' x, y)
            end.
  End QUEUE.

  (* It's easy to redo [ListQueue], specifying normal equality for the
   * equivalence relation. *)
  Module ListQueue : QUEUE.
    Definition t : Set -> Set := list.

    Definition empty A : t A := nil.
    Definition enqueue A (q : t A) (x : A) : t A := x :: q.
    Fixpoint dequeue A (q : t A) : option (t A * A) :=
      match q with
      | [] => None
      | x :: q' =>
        match dequeue q' with
        | None => Some ([], x)
        | Some (q'', y) => Some (x :: q'', y)
        end
      end.

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

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

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

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

    Theorem equiv_enqueue : forall A (a b : t A) (x : A),
        a ~= b
        -> enqueue a x ~= enqueue b x.
    Proof.
      unfold equiv; equality.
    Qed.

    Definition dequeue_equiv A (a b : option (t A * A)) :=
      match a, b with
      | None, None => True
      | Some (qa, xa), Some (qb, xb) => qa ~= qb /\ xa = xb
      | _, _ => False
      end.

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

    Theorem equiv_dequeue : forall A (a b : t A),
        a ~= b
        -> dequeue a ~~= dequeue b.
    Proof.
      unfold equiv, dequeue_equiv; simplify.
      rewrite H.
      cases (dequeue b).

      cases p.
      equality.

      propositional.
    Qed.

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

    Theorem empty_dequeue : forall A (q : t A),
        dequeue q = None -> q ~= empty A.
    Proof.
      simplify.
      cases q.

      simplify.
      unfold equiv.
      equality.

      simplify.
      cases (dequeue q).
      cases p.
      equality.
      equality.
    Qed.

    Theorem dequeue_enqueue : forall A (q : t A) x,
        dequeue (enqueue q x)
        ~~= match dequeue q with
            | None => Some (empty A, x)
            | Some (q', y) => Some (enqueue q' x, y)
            end.
    Proof.
      unfold dequeue_equiv, equiv.
      induct q; simplify.

      equality.

      cases (dequeue q).

      cases p.
      equality.
      equality.
    Qed.
  End ListQueue.

  (* However, now we can implement the classic two-stacks optimized queue! *)
  Module TwoStacksQueue : QUEUE.
    Record stackpair (A : Set) := {
      EnqueueHere : list A;
      DequeueHere : list A
    }.

    Definition t := stackpair.

    Definition empty A : t A := {|
      EnqueueHere := [];
      DequeueHere := []
    |}.
    Definition enqueue A (q : t A) (x : A) : t A := {|
      EnqueueHere := x :: q.(EnqueueHere);
      DequeueHere := q.(DequeueHere)
    |}.
    Definition dequeue A (q : t A) : option (t A * A) :=
      match q.(DequeueHere) with
      | x :: dq => Some ({| EnqueueHere := q.(EnqueueHere);
                            DequeueHere := dq |}, x)
      | [] =>
        match rev q.(EnqueueHere) with
        | [] => None
        | x :: eq => Some ({| EnqueueHere := [];
                              DequeueHere := eq |}, x)
        end
      end.

    Definition equiv A (a b : t A) : Prop. Admitted.
    Infix "~=" := equiv (at level 70).

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

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

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

    Theorem equiv_enqueue : forall A (a b : t A) (x : A),
        a ~= b
        -> enqueue a x ~= enqueue b x.
    Proof.
    Admitted.

    Definition dequeue_equiv A (a b : option (t A * A)) :=
      match a, b with
      | None, None => True
      | Some (qa, xa), Some (qb, xb) => qa ~= qb /\ xa = xb
      | _, _ => False
      end.

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

    Theorem equiv_dequeue : forall A (a b : t A),
        a ~= b
        -> dequeue a ~~= dequeue b.
    Proof.
    Admitted.
      (*unfold equiv, dequeue_equiv, elements, dequeue; simplify.
      cases (DequeueHere a); simplify.
      cases (rev (EnqueueHere a)); simplify.
      cases (DequeueHere b); simplify.
      cases (rev (EnqueueHere b)); simplify.
      propositional.
      SearchRewrite (_ ++ []).
      rewrite app_nil_r in H.
      rewrite app_nil_r in H.
      equality.
      cases (EnqueueHere a); simplify.
      cases (EnqueueHere b); simplify.
      cases (rev l); simplify.
      equality.
      equality.
      equality.
      cases (rev l0); simplify.
      equality.
      equality.
      cases (DequeueHere b); simplify.
      cases (rev (EnqueueHere b)); simplify.
      rewrite app_nil_r in H.
      rewrite app_nil_r in H.
      equality.
      rewrite app_nil_r in H.
      rewrite app_nil_r in H.
      equality.
      rewrite app_nil_r in H.
      rewrite H in Heq0.
      SearchRewrite (rev (_ ++ _)).
      rewrite rev_app_distr in Heq0.
      rewrite rev_app_distr in Heq0.
      simplify.
      invert Heq0.
      unfold equiv, elements.
      simplify.
      rewrite rev_app_distr.
      SearchRewrite (rev (rev _)).
      rewrite rev_involutive.
      rewrite rev_involutive.
      equality.
      cases (DequeueHere b); simplify.
      cases (rev (EnqueueHere b)); simplify.
      rewrite app_nil_r in H.
      rewrite <- H in Heq1.
      cases (EnqueueHere a); simplify.
      cases (rev l); simplify.
      equality.
      rewrite rev_app_distr in Heq1.
      simplify.
      equality.
      rewrite rev_app_distr in Heq1.
      rewrite rev_app_distr in Heq1.
      simplify.
      equality.
      unfold equiv, elements.
      simplify.
      rewrite app_nil_r in H.
      rewrite <- H in Heq1.
      rewrite rev_app_distr in Heq1.
      rewrite rev_app_distr in Heq1.
      simplify.
      invert Heq1.
      rewrite rev_involutive.
      rewrite rev_app_distr.
      rewrite rev_involutive.
      equality.
      unfold equiv, elements.
      simplify.
      SearchAbout app cons nil.
      apply app_inj_tail.
      rewrite <- app_assoc.
      rewrite <- app_assoc.
      assumption.
    Qed.*)

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

    Theorem empty_dequeue : forall A (q : t A),
        dequeue q = None -> q ~= empty A.
    Proof.
    Admitted.
      (*simplify.
      cases q.
      unfold dequeue in *.
      simplify.
      cases DequeueHere0.
      cases (rev EnqueueHere0).
      cases EnqueueHere0.
      equality.
      simplify.
      cases (rev EnqueueHere0); simplify.
      equality.
      equality.
      equality.
      equality.
    Qed.*)

    Theorem dequeue_enqueue : forall A (q : t A) x,
        dequeue (enqueue q x)
        ~~= match dequeue q with
            | None => Some (empty A, x)
            | Some (q', y) => Some (enqueue q' x, y)
            end.
    Proof.
    Admitted.
      (*unfold dequeue_equiv, equiv; simplify.
      cases q; simplify.
      unfold dequeue, enqueue; simplify.
      cases DequeueHere0; simplify.

      cases (rev EnqueueHere0); simplify.

      equality.

      unfold elements; simplify.
      SearchRewrite (rev (_ ++ _)).
      rewrite rev_app_distr.
      simplify.
      equality.

      equality.
    Qed.*)
  End TwoStacksQueue.

  Module DelayedSum (Q : QUEUE).
    Fixpoint makeQueue (n : nat) (q : Q.t nat) : Q.t nat :=
      match n with
      | 0 => q
      | S n' => makeQueue n' (Q.enqueue q n')
      end.

    Fixpoint computeSum (n : nat) (q : Q.t nat) : nat :=
      match n with
      | 0 => 0
      | S n' => match Q.dequeue q with
                | None => 0
                | Some (q', v) => v + computeSum n' q'
                end
      end.

    Fixpoint sumUpto (n : nat) : nat :=
      match n with
      | 0 => 0
      | S n' => n' + sumUpto n'
      end.

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

    Lemma makeQueue_congruence : forall n a b,
        a ~= b
        -> makeQueue n a ~= makeQueue n b.
    Proof.
      induct n; simplify.

      assumption.

      apply IHn.
      apply Q.equiv_enqueue.
      assumption.
    Qed.

    Lemma dequeue_makeQueue : forall n q,
        Q.dequeue (makeQueue n q)
        ~~= match Q.dequeue q with
            | Some (q', v) => Some (makeQueue n q', v)
            | None =>
              match n with
              | 0 => None
              | S n' => Some (makeQueue n' q, n')
              end
            end.
    Proof.
      induct n.

      simplify.
      cases (Q.dequeue q).
      cases p.
      unfold Q.dequeue_equiv.
      propositional.
      apply Q.equiv_refl.
      unfold Q.dequeue_equiv.
      propositional.

      simplify.
      unfold Q.dequeue_equiv in *.
      specialize (IHn (Q.enqueue q n)).
      cases (Q.dequeue (makeQueue n (Q.enqueue q n))).

      cases p.
      pose proof (Q.dequeue_enqueue q n).
      unfold Q.dequeue_equiv in *.
      cases (Q.dequeue (Q.enqueue q n)).

      cases p.
      cases (Q.dequeue q).

      cases p.
      propositional.
      apply Q.equiv_trans with (b := makeQueue n t0).
      assumption.
      apply makeQueue_congruence.
      assumption.
      equality.

      propositional.
      apply Q.equiv_trans with (b := makeQueue n t0).
      assumption.
      apply makeQueue_congruence.
      apply Q.equiv_trans with (b := Q.empty nat).
      assumption.
      apply Q.equiv_sym.
      apply Q.empty_dequeue.
      assumption.
      equality.

      cases (Q.dequeue q).

      cases p.
      propositional.

      propositional.

      pose proof (Q.dequeue_enqueue q n).
      unfold Q.dequeue_equiv in H.
      cases (Q.dequeue (Q.enqueue q n)).

      cases p.
      propositional.

      cases (Q.dequeue q).

      cases p.
      propositional.

      propositional.
    Qed.

    Theorem computeSum_congruence : forall n a b,
        a ~= b
        -> computeSum n a = computeSum n b.
    Proof.
      induct n.

      simplify.
      equality.

      simplify.
      pose proof (Q.equiv_dequeue H).
      unfold Q.dequeue_equiv in H0.
      cases (Q.dequeue a).

      cases p.
      cases (Q.dequeue b).
      cases p.
      rewrite IHn with (b := t0).
      equality.
      equality.
      propositional.

      cases (Q.dequeue b).
      propositional.
      equality.
    Qed.

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

      simplify.
      equality.

      simplify.
      pose proof (dequeue_makeQueue n (Q.enqueue (Q.empty nat) n)).
      unfold Q.dequeue_equiv in H.
      cases (Q.dequeue (makeQueue n (Q.enqueue (Q.empty nat) n))).

      cases p.
      pose proof (Q.dequeue_enqueue (Q.empty nat) n).
      unfold Q.dequeue_equiv in H0.
      cases (Q.dequeue (Q.enqueue (Q.empty nat) n)).

      cases p.
      rewrite Q.dequeue_empty in H0.
      propositional.
      f_equal.
      equality.
      rewrite <- IHn.
      
      apply computeSum_congruence.
      apply Q.equiv_trans with (b := makeQueue n t0).
      assumption.
      apply makeQueue_congruence.
      assumption.

      rewrite Q.dequeue_empty in H0.
      propositional.

      pose proof (Q.dequeue_enqueue (Q.empty nat) n).
      unfold Q.dequeue_equiv in H0.
      cases (Q.dequeue (Q.enqueue (Q.empty nat) n)).

      cases p.
      propositional.

      rewrite Q.dequeue_empty in H0.
      propositional.
    Qed.
  End DelayedSum.
End AlgebraicWithEquivalenceRelation.

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

    Parameter empty : forall A, t A.
    Parameter enqueue : forall A, t A -> A -> t A.
    Parameter dequeue : forall A, t A -> option (t A * A).

    Parameter rep : forall A, t A -> list A.

    (* Fill in laws here. *)
  End QUEUE.

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

    Definition empty A : t A := nil.
    Definition enqueue A (q : t A) (x : A) : t A := x :: q.
    Fixpoint dequeue A (q : t A) : option (t A * A) :=
      match q with
      | [] => None
      | x :: q' =>
        match dequeue q' with
        | None => Some ([], x)
        | Some (q'', y) => Some (x :: q'', y)
        end
      end.

    Definition rep A (q : t A) : list A. Admitted.


























    (*Theorem empty_rep : forall A,
        rep (empty A) = [].
    Proof.
      equality.
    Qed.

    Theorem enqueue_rep : forall A (q : t A) x,
        rep (enqueue q x) = x :: rep q.
    Proof.
      equality.
    Qed.

    Theorem dequeue_empty : forall A (q : t A),
        rep q = []
        -> dequeue q = None.
    Proof.
      unfold rep; simplify.
      rewrite H.
      equality.
    Qed.

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

      simplify.
      cases xs; simplify.
      equality.
      equality.

      simplify.
      cases xs; simplify.
      invert H; simplify.
      exists [].
      equality.

      invert H.
      assert (exists q' : t A, dequeue (xs ++ [x]) = Some (q', x) /\ q' = xs).
      apply IHq.
      equality.
      first_order.
      rewrite H.
      exists (a0 :: x0).
      equality.
    Qed.*)
  End ListQueue.

  Module TwoStacksQueue : QUEUE.
    Record stackpair (A : Set) := {
      EnqueueHere : list A;
      DequeueHere : list A
    }.

    Definition t := stackpair.

    Definition empty A : t A := {|
      EnqueueHere := [];
      DequeueHere := []
    |}.
    Definition enqueue A (q : t A) (x : A) : t A := {|
      EnqueueHere := x :: q.(EnqueueHere);
      DequeueHere := q.(DequeueHere)
    |}.
    Definition dequeue A (q : t A) : option (t A * A) :=
      match q.(DequeueHere) with
      | x :: dq => Some ({| EnqueueHere := q.(EnqueueHere);
                            DequeueHere := dq |}, x)
      | [] =>
        match rev q.(EnqueueHere) with
        | [] => None
        | x :: eq => Some ({| EnqueueHere := [];
                              DequeueHere := eq |}, x)
        end
      end.

    Definition rep A (q : t A) : list A. Admitted.























    (*Theorem empty_rep : forall A,
        rep (empty A) = [].
    Proof.
      equality.
    Qed.

    Theorem enqueue_rep : forall A (q : t A) x,
        rep (enqueue q x) = x :: rep q.
    Proof.
      equality.
    Qed.

    Theorem dequeue_empty : forall A (q : t A),
        rep q = []
        -> dequeue q = None.
    Proof.
      unfold rep, dequeue; simplify.
      cases (DequeueHere q); simplify.
      rewrite app_nil_r in H.
      rewrite H.
      simplify.
      equality.
      cases (EnqueueHere q); simplify.
      cases (rev l); simplify.
      equality.
      equality.
      equality.
    Qed.

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

      cases (DequeueHere q); simplify.

      rewrite app_nil_r in H.
      rewrite H.
      rewrite rev_app_distr; simplify.
      exists {| EnqueueHere := []; DequeueHere := rev xs |}.
      simplify.
      rewrite rev_involutive.
      equality.

      exists {| EnqueueHere := EnqueueHere q; DequeueHere := l |}.
      simplify.
      rewrite app_assoc in H.
      apply app_inj_tail in H.
      propositional.
      rewrite H1.
      equality.
    Qed.*)
  End TwoStacksQueue.

  Module DelayedSum (Q : QUEUE).
    Fixpoint makeQueue (n : nat) (q : Q.t nat) : Q.t nat :=
      match n with
      | 0 => q
      | S n' => makeQueue n' (Q.enqueue q n')
      end.

    Fixpoint computeSum (n : nat) (q : Q.t nat) : nat :=
      match n with
      | 0 => 0
      | S n' => match Q.dequeue q with
                | None => 0
                | Some (q', v) => v + computeSum n' q'
                end
      end.

    Fixpoint sumUpto (n : nat) : nat :=
      match n with
      | 0 => 0
      | S n' => n' + sumUpto n'
      end.

    Fixpoint upto (n : nat) : list nat :=
      match n with
      | 0 => []
      | S n' => upto n' ++ [n']
      end.

    Theorem computeSum_ok : forall n,
        computeSum n (makeQueue n (Q.empty nat)) = sumUpto n.
    Proof.
    Admitted.
  End DelayedSum.
End RepFunction.


(** * Data abstraction with fixed parameter types *)

Module Type FINITE_SET.
  Parameter key : Set. (* What type of data may be added to these sets? *)
  Parameter t : Set.   (* What is the type of sets themselves? *)

  Parameter empty : t.
  Parameter add : t -> key -> t.
  Parameter member : t -> key -> bool.

  Axiom member_empty : forall k, member empty k = false.

  Axiom member_add_eq : forall k s,
      member (add s k) k = true.
  Axiom member_add_noteq : forall k1 k2 s,
      k1 <> k2
      -> member (add s k1) k2 = member s k2.

  Axiom decidable_equality : forall a b : key, a = b \/ a <> b.
  (* ^-- This one may be surprising. *)
End FINITE_SET.

Module Type SET_WITH_EQUALITY.
  Parameter t : Set.
  Parameter equal : t -> t -> bool.

  Axiom equal_ok : forall a b, if equal a b then a = b else a <> b.
End SET_WITH_EQUALITY.

Module ListSet(SE : SET_WITH_EQUALITY) <: FINITE_SET with Definition key := SE.t.
  Definition key := SE.t.
  Definition t := list SE.t.

  Definition empty : t := [].
  Definition add (s : t) (k : key) : t := k :: s.
  Fixpoint member (s : t) (k : key) : bool :=
    match s with
    | [] => false
    | k' :: s' => SE.equal k' k || member s' k
    end.

  Theorem member_empty : forall k, member empty k = false.
  Proof.
    simplify.
    equality.
  Qed.

  Theorem member_add_eq : forall k s,
      member (add s k) k = true.
  Proof.
    simplify.
    pose proof (SE.equal_ok k k).
    cases (SE.equal k k); simplify.
    equality.
    equality.
  Qed.

  Theorem member_add_noteq : forall k1 k2 s,
      k1 <> k2
      -> member (add s k1) k2 = member s k2.
  Proof.
    simplify.
    pose proof (SE.equal_ok k1 k2).
    cases (SE.equal k1 k2); simplify.
    equality.
    equality.
  Qed.

  Theorem decidable_equality : forall a b : key, a = b \/ a <> b.
  Proof.
    simplify.
    pose proof (SE.equal_ok a b).
    cases (SE.equal a b); propositional.
  Qed.
End ListSet.

(* Here's an example decidable-equality type for natural numbers. *)
Module NatWithEquality <: SET_WITH_EQUALITY with Definition t := nat.
  Definition t := nat.

  Fixpoint equal (a b : nat) : bool :=
    match a, b with
    | 0, 0 => true
    | S a', S b' => equal a' b'
    | _, _ => false
    end.

  Theorem equal_ok : forall a b, if equal a b then a = b else a <> b.
  Proof.
    induct a; simplify.

    cases b.
    equality.
    equality.

    cases b.
    equality.
    specialize (IHa b).
    cases (equal a b).
    equality.
    equality.
  Qed.
End NatWithEquality.

(* And here's how to instantiate the generic set for the naturals. *)
Module NatSet := ListSet(NatWithEquality).

(* Now, some generic client code, for testing duplicate-freeness of lists. *)
Module FindDuplicates (FS : FINITE_SET).
  Fixpoint noDuplicates' (ls : list FS.key) (s : FS.t) : bool :=
    match ls with
    | [] => true
    | x :: ls' => negb (FS.member s x) && noDuplicates' ls' (FS.add s x)
    end.

  Definition noDuplicates (ls : list FS.key) := noDuplicates' ls FS.empty.

  (* A characterization of having a duplicate: the list can be partitioned into
   * pieces revealing the same element [a] at two boundaries. *)
  Definition hasDuplicate (ls : list FS.key) :=
    exists ls1 a ls2 ls3, ls = ls1 ++ a :: ls2 ++ a :: ls3.

  (* A characterization of containing an element [a]: the list can be
   * partitioned into two pieces, with [a] at the boundary. *)
  Definition contains (a : FS.key) (ls : list FS.key) :=
    exists ls1 ls2, ls = ls1 ++ a :: ls2.

  Lemma noDuplicates'_ok : forall ls s, if noDuplicates' ls s
                                        then ~(hasDuplicate ls
                                               \/ exists a, FS.member s a = true
                                                            /\ contains a ls)
                                        else (hasDuplicate ls
                                              \/ exists a, FS.member s a = true
                                                           /\ contains a ls).
  Proof.
    induct ls; simplify.

    unfold hasDuplicate, contains.
    propositional.
    first_order.
    cases x; simplify.
    equality.
    equality.

    first_order.
    cases x0; simplify.
    equality.
    equality.
    cases (FS.member s a); simplify.
    right.
    exists a.
    propositional.
    unfold contains.
    exists [].
    exists ls.
    simplify.
    equality.

    specialize (IHls (FS.add s a)).
    cases (noDuplicates' ls (FS.add s a)).
    propositional.

    apply H1.
    exists a.
    propositional.
    apply FS.member_add_eq.
    unfold hasDuplicate, contains in *.
    first_order.
    cases x; simplify.
    invert H0.
    exists x1.
    exists x2.
    equality.

    invert H0.
    exfalso.
    apply H with (x := x).
    exists x0.
    exists x1.
    exists x2.
    equality.

    first_order.
    apply H1 with x.
    propositional.
    pose proof (FS.decidable_equality a x).
    propositional.
    rewrite H4.
    apply FS.member_add_eq.
    rewrite FS.member_add_noteq.
    assumption.
    assumption.
    cases x0; simplify.
    equality.
    invert H2.
    exists x0.
    exists x1.
    equality.

    first_order.
    left.
    exists (a :: x).
    exists x0.
    exists x1.
    exists x2.
    simplify.
    equality.
    cases (FS.member s x).

    right.
    exists x.
    propositional.
    exists (a :: x0).
    exists x1.
    simplify.
    equality.

    left.
    pose proof (FS.decidable_equality a x).
    propositional.

    exists nil.
    exists a.
    exists x0.
    exists x1.
    simplify.
    equality.
    rewrite FS.member_add_noteq in H.
    equality.
    assumption.
  Qed.

  Theorem noDuplicates_ok : forall ls, if noDuplicates ls
                                       then ~hasDuplicate ls 
                                       else hasDuplicate ls.
  Proof.
    simplify.
    pose proof (noDuplicates'_ok ls FS.empty).
    unfold noDuplicates.
    cases (noDuplicates' ls FS.empty); first_order.
    rewrite FS.member_empty in H.
    equality.
  Qed.
End FindDuplicates.

Module NatDuplicateFinder := FindDuplicates(NatSet).

Compute NatDuplicateFinder.noDuplicates [].
Compute NatDuplicateFinder.noDuplicates [1].
Compute NatDuplicateFinder.noDuplicates [1; 2].
Compute NatDuplicateFinder.noDuplicates [1; 2; 3].
Compute NatDuplicateFinder.noDuplicates [1; 2; 1; 3].


(** * Custom implementations of abstract data types *)

Fixpoint fromRange' (from to : nat) : NatSet.t :=
  match to with
  | 0 => NatSet.add NatSet.empty 0
  | S to' => if NatWithEquality.equal to from
             then NatSet.add NatSet.empty to
             else NatSet.add (fromRange' from to') (S to')
  end.

Definition fromRange (from to : nat) : NatSet.t :=
  if Compare_dec.leb from to
  then fromRange' from to
  else NatSet.empty.

Module NatRangeSet (*<: FINITE_SET with Definition key := nat*).
  Definition key := nat.

  (*Definition t := ....

  Definition empty : t := ....
  Definition add (s : t) (k : key) : t := ....
  Definition member (s : t) (k : key) : bool := ....*)




























  (*Theorem member_empty : forall k, member empty k = false.
  Proof.
    simplify.
    equality.
  Qed.

  Lemma member_fromRange' : forall k from to,
      from <= to
      -> NatSet.member (fromRange' from to) k = Compare_dec.leb from k && Compare_dec.leb k to.
  Proof.
    induct to; simplify.

    cases k; simplify.
    rewrite Compare_dec.leb_correct by assumption.
    equality.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.

    cases from; simplify.
    cases k; simplify.
    apply IHto.
    linear_arithmetic.
    pose proof (NatWithEquality.equal_ok to k).
    cases (NatWithEquality.equal to k); simplify.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.
    rewrite IHto by linear_arithmetic.
    cases to.
    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
    equality.
    cases (Compare_dec.leb k to).
    apply Compare_dec.leb_complete in Heq0.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.
    apply Compare_dec.leb_complete_conv in Heq0.
    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
    equality.
    
    pose proof (NatWithEquality.equal_ok to from).
    cases (NatWithEquality.equal to from); simplify.

    cases k; simplify.
    equality.
    pose proof (NatWithEquality.equal_ok to k).
    cases (NatWithEquality.equal to k); simplify.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.
    cases (Compare_dec.leb from k); simplify.
    apply Compare_dec.leb_complete in Heq1.
    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
    equality.
    equality.

    cases k; simplify.
    apply IHto.
    linear_arithmetic.
    rewrite IHto by linear_arithmetic.
    pose proof (NatWithEquality.equal_ok to k).
    cases (NatWithEquality.equal to k); simplify.    
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.

    cases to.
    rewrite (Compare_dec.leb_correct_conv 0 k) by linear_arithmetic.
    equality.
    cases (Compare_dec.leb k to).
    apply Compare_dec.leb_complete in Heq1.
    rewrite (Compare_dec.leb_correct k (S to)) by linear_arithmetic.
    equality.
    apply Compare_dec.leb_complete_conv in Heq1.
    rewrite (Compare_dec.leb_correct_conv (S to) k) by linear_arithmetic.
    equality.
  Qed.

  Theorem member_add_eq : forall k s,
      member (add s k) k = true.
  Proof.
    unfold member, add; simplify.
    cases s.

    SearchAbout Compare_dec.leb.
    rewrite Compare_dec.leb_correct.
    equality.
    linear_arithmetic.

    cases (Compare_dec.leb from k); simplify.
    cases (Compare_dec.leb k to); simplify.
    rewrite Heq.
    rewrite Heq0.
    apply Compare_dec.leb_complete in Heq.
    apply Compare_dec.leb_complete in Heq0.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.

    pose proof (NatWithEquality.equal_ok k (from - 1)).
    cases (NatWithEquality.equal k (from - 1)).
    apply leb_complete in Heq.
    apply leb_complete_conv in Heq0.
    linear_arithmetic.
    simplify.
    pose proof (NatWithEquality.equal_ok k (to + 1)).
    cases (NatWithEquality.equal k (to + 1)); simplify.
    cases (Compare_dec.leb from to).
    rewrite Heq.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.
    apply NatSet.member_add_eq.
    pose proof (NatWithEquality.equal_ok k k).
    cases (NatWithEquality.equal k k); simplify.
    equality.
    equality.

    pose proof (NatWithEquality.equal_ok k (from - 1)).
    cases (NatWithEquality.equal k (from - 1)); simplify.
    cases (Compare_dec.leb from to).
    apply Compare_dec.leb_complete in Heq1.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.
    pose proof (NatWithEquality.equal_ok k (to + 1)).
    cases (NatWithEquality.equal k (to + 1)); simplify.
    pose proof (NatWithEquality.equal_ok k k).
    cases (NatWithEquality.equal k k); simplify.
    equality.
    equality.
    pose proof (NatWithEquality.equal_ok k k).
    cases (NatWithEquality.equal k k); simplify.
    equality.
    equality.
    pose proof (NatWithEquality.equal_ok k (to + 1)).
    cases (NatWithEquality.equal k (to + 1)); simplify.
    cases (Compare_dec.leb from to).
    apply Compare_dec.leb_complete in Heq2.
    apply Compare_dec.leb_complete_conv in Heq.
    linear_arithmetic.
    apply NatSet.member_add_eq.
    pose proof (NatWithEquality.equal_ok k k).
    cases (NatWithEquality.equal k k); simplify.
    equality.
    equality.    

    apply NatSet.member_add_eq.
  Qed.

  Theorem member_add_noteq : forall k1 k2 s,
      k1 <> k2
      -> member (add s k1) k2 = member s k2.
  Proof.
    simplify.
    unfold member, add.
    cases s.

    cases (Compare_dec.leb k1 k2); simplify.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    apply Compare_dec.leb_complete in Heq.
    rewrite Compare_dec.leb_correct_conv.
    equality.
    unfold key in *. (* Tricky step!  Coq needs to see that we are really working with numbers. *)
    linear_arithmetic.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.

    cases (Compare_dec.leb from k1); simplify.
    cases (Compare_dec.leb k1 to); simplify.
    equality.

    pose proof (NatWithEquality.equal_ok k1 (from - 1)).
    cases (NatWithEquality.equal k1 (from - 1)); simplify.
    apply leb_complete in Heq.
    apply leb_complete_conv in Heq0.
    linear_arithmetic.
    pose proof (NatWithEquality.equal_ok k1 (to + 1)).
    cases (NatWithEquality.equal k1 (to + 1)); simplify.
    cases (Compare_dec.leb from to).
    rewrite H1.
    cases (Compare_dec.leb from k2); simplify.
    cases (Compare_dec.leb k2 to).
    apply Compare_dec.leb_complete in Heq5.
    apply Compare_dec.leb_complete in Heq3.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.
    apply Compare_dec.leb_complete in Heq3.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    apply Compare_dec.leb_complete_conv in Heq5.
    unfold key in *.
    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
    equality.
    rewrite andb_false_r.
    equality.
    simplify.
    pose proof (NatWithEquality.equal_ok k1 k2).
    cases (NatWithEquality.equal k1 k2); simplify.
    equality.
    unfold fromRange.
    rewrite Heq3.
    apply NatSet.member_empty.
    pose proof (NatWithEquality.equal_ok k1 k2).
    cases (NatWithEquality.equal k1 k2); simplify.
    equality.
    unfold fromRange.
    cases (Compare_dec.leb from to); simplify.
    apply member_fromRange'.
    apply Compare_dec.leb_complete.
    assumption.
    equality.

    pose proof (NatWithEquality.equal_ok k1 (from - 1)).
    cases (NatWithEquality.equal k1 (from - 1)); simplify.
    cases (Compare_dec.leb from to).
    apply Compare_dec.leb_complete in Heq1.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    f_equal.
    f_equal.
    cases (Compare_dec.leb k1 k2).
    apply Compare_dec.leb_complete in Heq2.
    apply Compare_dec.leb_complete_conv in Heq.
    unfold key in *.
    rewrite Compare_dec.leb_correct by linear_arithmetic.
    equality.
    apply Compare_dec.leb_complete_conv in Heq2.
    apply Compare_dec.leb_complete_conv in Heq.
    unfold key in *.
    rewrite Compare_dec.leb_correct_conv by linear_arithmetic.
    equality.
    pose proof (NatWithEquality.equal_ok k1 (to + 1)).
    cases (NatWithEquality.equal k1 (to + 1)); simplify.
    pose proof (NatWithEquality.equal_ok k1 k2).
    cases (NatWithEquality.equal k1 k2); simplify.
    unfold key in *; linear_arithmetic.
    unfold fromRange.
    rewrite Heq1.
    apply NatSet.member_empty. 
    pose proof (NatWithEquality.equal_ok k1 k2).
    cases (NatWithEquality.equal k1 k2); simplify.
    equality.
    unfold fromRange.
    rewrite Heq1.
    apply NatSet.member_empty. 
    pose proof (NatWithEquality.equal_ok k1 (to + 1)).
    cases (NatWithEquality.equal k1 (to + 1)); simplify.
    cases (Compare_dec.leb from to).
    rewrite Heq; simplify.
    apply Compare_dec.leb_complete in Heq2.
    apply Compare_dec.leb_complete_conv in Heq.
    linear_arithmetic.
    rewrite NatSet.member_add_noteq by assumption; simplify.
    unfold fromRange.
    rewrite Heq2.
    apply NatSet.member_empty. 
    pose proof (NatWithEquality.equal_ok k1 k2).
    cases (NatWithEquality.equal k1 k2); simplify.
    equality.
    unfold fromRange.
    cases (Compare_dec.leb from to); simplify.
    apply member_fromRange'.
    apply Compare_dec.leb_complete; assumption.
    equality.
    apply NatSet.member_add_noteq.
    assumption.
  Qed.

  Theorem decidable_equality : forall a b : key, a = b \/ a <> b.
  Proof.
    simplify.
    pose proof (NatWithEquality.equal_ok a b).
    cases (NatWithEquality.equal a b); propositional.
  Qed.*)
End NatRangeSet.

(* Time for a head-to-head performance contest between our naive and clever
 * sets! *)

(*Module FasterNatDuplicateFinder := FindDuplicates(NatRangeSet).

Fixpoint upto (n : nat) : list nat :=
  match n with
  | 0 => []
  | S n' => n' :: upto n'
  end.

Compute upto 10.

Time Compute NatDuplicateFinder.noDuplicates (upto 1000).
Time Compute FasterNatDuplicateFinder.noDuplicates (upto 1000).*)