from #haskell: Sensored: i think you can define nub with a fold

nub.v

Require Import Arith.
Require Import List.
Require Import Recdef.

Definition EqDec (A : Type) := forall (x y : A), {x = y} + {x <> y}.

Fixpoint delete {A : Type} (eq : EqDec A) (x : A) (ls : list A) : list A :=
  match ls with
  | nil => nil
  | cons h t => if eq x h
                   then delete eq x t
                   else cons h (delete eq x t)
  end.


Fixpoint deleteFirst {A : Type} (eq : EqDec A) (x : A) (ls : list A) : list A :=
  match ls with
  | nil => nil
  | cons h t => if eq x h
                   then t
                   else cons h (deleteFirst eq x t)
  end.

Lemma delete_length : forall {A : Type} (eq : EqDec A) (x : A) (ls : list A),
  length (delete eq x ls) <= length ls.
Proof.
  intros.
  induction ls; auto.
  simpl.
  destruct (eq x a).
  apply le_S. apply IHls.
  simpl. apply le_n_S. apply IHls. Qed.

Fixpoint nubBy {A : Type} (eq : EqDec A) (ls : list A) :=
  match ls with
  | nil => nil
  | cons h t => cons h (delete eq h (nubBy eq t))
  end.

Function nubByOrig {A : Type} (eq : EqDec A) (ls : list A) {measure length ls} :=
  match ls with
  | nil => nil
  | cons h t => cons h (@nubByOrig A eq (delete eq h t))
  end.
Proof.
  intros. simpl. apply le_n_S. apply delete_length. Defined.

Fixpoint nubBySpec {A : Type} (eq : EqDec A) (ls : list A) :=
  match ls with
  | nil => nil
  | cons h t => cons h (deleteFirst eq h (nubBySpec eq t))
  end.

Lemma delete_idemp : forall {A : Type} (eq : EqDec A) (x : A) (ls : list A),
  delete eq x (delete eq x ls) = delete eq x ls.
Proof.
  intros.
  induction ls; auto.
  simpl.
  remember (eq x a) as eqxa.
  destruct eqxa.
  subst. apply IHls.
  simpl. rewrite <- Heqeqxa. f_equal. apply IHls. Qed.

Lemma delete_comm : forall {A : Type} (eq : EqDec A) (x y : A) (ls : list A),
  delete eq x (delete eq y ls) = delete eq y (delete eq x ls).
Proof.
  intros.
  generalize dependent x.
  generalize dependent y.
  intros.
  induction ls. auto.
  remember (eq x a) as eqxa.
  remember (eq y a) as eqya.
  destruct eqxa, eqya; simpl;
  try rewrite <- Heqeqya; try rewrite <- Heqeqxa; simpl;
  try rewrite <- Heqeqya; try rewrite <- Heqeqxa; simpl.
  apply IHls.
  apply IHls.
  apply IHls.
  f_equal; apply IHls. Qed.

Lemma deleteFirst_length : forall {A : Type} (eq : EqDec A) (x : A) (ls : list A),
  length (delete eq x ls) <= length ls.
Proof.
  intros.
  induction ls; auto.
  simpl.
  destruct (eq x a).
  apply le_S. apply IHls.
  simpl. apply le_n_S. apply IHls. Qed. 

Lemma deleteFirst_delete_idemp : forall {A : Type} (eq : EqDec A) (x : A) (ls : list A),
  deleteFirst eq x (delete eq x ls) = delete eq x ls.
Proof.
  intros.
  induction ls.
  auto.
  simpl.
  remember (eq x a) as eqxa.
  destruct eqxa.
  apply IHls.
  simpl.
  rewrite <- Heqeqxa.
  f_equal. apply IHls. Qed.

Lemma deleteFirst_delete_comm : forall {A : Type} (eq : EqDec A) (x y : A) (ls : list A),
  deleteFirst eq x (delete eq y ls) = delete eq y (deleteFirst eq x ls).
Proof.
  intros.
  generalize dependent x.
  generalize dependent y.
  induction ls; intros; auto.
  simpl.
  remember (eq x a) as eqxa.
  remember (eq y a) as eqya.
  destruct eqxa, eqya; simpl;
  try rewrite <- Heqeqya; try rewrite <- Heqeqxa; simpl;
  try rewrite <- Heqeqya; try rewrite <- Heqeqxa; simpl.
  subst.
  rewrite IHls.
  rewrite <- IHls. apply deleteFirst_delete_idemp.
  auto.
  apply IHls.
  f_equal. apply IHls. Qed.

Lemma deleteFirst_comm : forall {A : Type} (eq : EqDec A) (x y : A) (ls : list A),
  deleteFirst eq x (deleteFirst eq y ls) = deleteFirst eq y (deleteFirst eq x ls).
Proof.
  intros.
  generalize dependent x.
  generalize dependent y.
  induction ls; intros; auto.
  remember (eq x a) as eqxa.
  remember (eq y a) as eqya.
  destruct eqxa, eqya; simpl;
  try rewrite <- Heqeqya; try rewrite <- Heqeqxa; simpl;
  try rewrite <- Heqeqya; try rewrite <- Heqeqxa; simpl.
  subst. auto.
  auto.
  auto.
  f_equal. apply IHls. Qed.

Lemma delete_nubBy_comm :  forall {A : Type} (eq : EqDec A) (x : A) (ls : list A),
  delete eq x (nubBy eq ls) = nubBy eq (delete eq x ls).
Proof.
  intros.
  induction ls; auto.
  simpl.
  case (eq x a).
  intros; subst.
  rewrite delete_idemp. apply IHls.
  intros. simpl.
  f_equal.
  rewrite <- IHls.
  apply delete_comm. Qed.

Lemma list_length_ind_size :
  forall (A : Type) (P : list A -> Prop)
    (Pnil : P nil)
    (Pnext : forall (a : A) (l : list A), (forall k : list A, length k <= length l -> P k) -> P (a :: l))
    (n : nat) (l : list A) ,
    length l <= n -> P l.
Proof.
  intros until n.
  induction n; intros.
  destruct l. apply Pnil.
  inversion H.
  destruct l. apply Pnil.
  apply Pnext. intros. apply IHn. simpl in H.
  apply le_trans with (m := length l).
  apply H0. apply le_S_n. apply H. Qed.

Lemma nubDelete : forall {A : Type} (eq : EqDec A) (x : A) (ls : list A),
  delete eq x (nubBy eq ls) = deleteFirst eq x (nubBy eq ls).
Proof.
  intros.
  generalize dependent x.
  induction ls; intros; auto.
  simpl. destruct (eq x a).
  (* x = a *)
  subst. rewrite delete_idemp. auto.
  (* x <> a *)
  f_equal.
  rewrite delete_comm. rewrite IHls.
  rewrite deleteFirst_delete_comm. auto. Qed.

Lemma list_length_ind :
  forall (A : Type) (P : list A -> Prop)
    (Pnil : P nil)
    (Pnext : forall (a : A) (l : list A), (forall k : list A, length k <= length l -> P k) -> P (a :: l))
    (l : list A),
  P l.
Proof.
  intros.
  apply list_length_ind_size with (n := length l); auto. Qed.

Theorem nubEquivalent1 : forall {A : Type} (eq : EqDec A) (ls : list A),
  nubBy eq ls = nubByOrig A eq ls.
Proof.
  intros.
  induction ls using list_length_ind.
  reflexivity.
  simpl.
  rewrite nubByOrig_equation.
  f_equal.
  rewrite <- H.
  apply delete_nubBy_comm. apply delete_length. Qed.

Theorem nubEquivalent2 : forall {A : Type} (eq : EqDec A) (ls : list A),
  nubBy eq ls = nubBySpec eq ls.
Proof.
  intros.
  induction ls.
  reflexivity.
  simpl.
  f_equal.
  rewrite <- IHls.
  apply nubDelete. Qed.

Theorem nubEquivalent3 : forall {A : Type} (eq : EqDec A) (ls : list A),
  nubByOrig A eq ls = nubBySpec eq ls.
Proof.
  intros.
  rewrite <- nubEquivalent1.
  rewrite <- nubEquivalent2.
  auto. Qed.