Require Import List.
Import ListNotations.
Require Import StructTact.StructTactics.
Require Import StructTact.ListTactics.
Require Import StructTact.ListUtil.

Set Implicit Arguments.

Section dedup.
  Variable A : Type.
  Hypothesis A_eq_dec : forall x y : A, {x = y} + {x <> y}.

  Fixpoint dedup (xs : list A) : list A :=
    match xs with
    | [] => []
    | x :: xs => let tail := dedup xs in
                 if in_dec A_eq_dec x xs then
                   tail
                 else
                   x :: tail
    end.

  Lemma dedup_eliminates_duplicates : forall a l l',
      dedup (a :: l ++ a :: l') = dedup (l ++ a :: l').
  Proof using.
(* Goal: forall (x y : A) (_ : @In A x xs) (_ : @In A y ys), not (@eq A x y) *)
    intros. simpl in *.
(* Goal: @eq (list A) (if @in_dec A A_eq_dec a (@app A l (@cons A a l')) then dedup (@app A l (@cons A a l')) else @cons A a (dedup (@app A l (@cons A a l')))) (dedup (@app A l (@cons A a l'))) *)
    break_match.
    + auto.
    + exfalso. intuition.
  Qed.

  Lemma dedup_In : forall (x : A) xs,
      In x xs ->
      In x (dedup xs).
  Proof using.
(* Goal: @eq (list A) (@cons A x (dedup (@cons A a xs))) (dedup (@cons A x (@cons A a xs))) *)
    induction xs; intros; simpl in *.
(* Goal: @eq (list A) (@cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) (if match A_eq_dec a x with | left e => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_introl (@eq A a x) (@In A x xs) e) | right n => match @in_dec A A_eq_dec x xs with | left i => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_intror (@eq A a x) (@In A x xs) i) | right n0 => @right (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (fun H0 : or (@eq A a x) (@In A x xs) => match H0 with | or_introl Hc1 => n Hc1 | or_intror Hc2 => n0 Hc2 end) end end then if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs) else @cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) *)
    - intuition.
(* Goal: @eq (list A) (@cons A x (dedup (@nil A))) (dedup (@cons A x (@nil A))) *)
    - break_if; intuition; subst; simpl; auto.
  Qed.

  Lemma filter_dedup (pred : A -> bool) :
    forall xs (p : A) ys,
      pred p = false ->
      filter pred (dedup (xs ++ ys)) = filter pred (dedup (xs ++ p :: ys)).
  Proof using.
(* Goal: forall (x y : A) (_ : @In A x xs) (_ : @In A y ys), not (@eq A x y) *)
    intros.
    induction xs; simpl; repeat (break_match; simpl);
      auto using f_equal2; try discriminate.
      + exfalso. apply n. apply in_app_iff. apply in_app_or in i. intuition.
      + exfalso. apply n. apply in_app_or in i. intuition.
(* Goal: @eq (list A) (@cons A x (dedup (@cons A a xs))) (dedup (@cons A x (@cons A a xs))) *)
        * simpl in *. intuition. congruence.
  Qed.

  Lemma dedup_app : forall (xs ys : list A),
      (forall x y, In x xs -> In y ys -> x <> y) ->
      dedup (xs ++ ys) = dedup xs ++ dedup ys.
  Proof using.
(* Goal: forall (x y : A) (_ : @In A x xs) (_ : @In A y ys), not (@eq A x y) *)
    intros. induction xs; simpl; auto.
(* Goal: @eq (list A) (if @in_dec A A_eq_dec a (@app A l (@cons A a l')) then dedup (@app A l (@cons A a l')) else @cons A a (dedup (@app A l (@cons A a l')))) (dedup (@app A l (@cons A a l'))) *)
    repeat break_match.
    - apply IHxs.
(* Goal: forall (x y : A) (_ : @In A x xs) (_ : @In A y ys), not (@eq A x y) *)
      intros. apply H; intuition.
(* Goal: @eq (list A) (@cons A a (@remove A A_eq_dec x (dedup xs))) (dedup (@remove A A_eq_dec x xs)) *)
    - exfalso. specialize (H a a).
(* Goal: @eq (list A) (@cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) (if match A_eq_dec a x with | left e => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_introl (@eq A a x) (@In A x xs) e) | right n => match @in_dec A A_eq_dec x xs with | left i => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_intror (@eq A a x) (@In A x xs) i) | right n0 => @right (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (fun H0 : or (@eq A a x) (@In A x xs) => match H0 with | or_introl Hc1 => n Hc1 | or_intror Hc2 => n0 Hc2 end) end end then if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs) else @cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) *)
      apply H; intuition.
(* Goal: @eq (list A) (@cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) (if match A_eq_dec a x with | left e => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_introl (@eq A a x) (@In A x xs) e) | right n => match @in_dec A A_eq_dec x xs with | left i => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_intror (@eq A a x) (@In A x xs) i) | right n0 => @right (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (fun H0 : or (@eq A a x) (@In A x xs) => match H0 with | or_introl Hc1 => n Hc1 | or_intror Hc2 => n0 Hc2 end) end end then if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs) else @cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) *)
      do_in_app. intuition.
(* Goal: @eq (list A) (@cons A a (@remove A A_eq_dec x (dedup xs))) (dedup (@remove A A_eq_dec x xs)) *)
    - exfalso. apply n. intuition.
    - simpl. f_equal.
(* Goal: @eq (list A) (dedup (@app A xs ys)) (@app A (dedup xs) (dedup ys)) *)
      apply IHxs.
(* Goal: forall (x y : A) (_ : @In A x xs) (_ : @In A y ys), not (@eq A x y) *)
      intros. apply H; intuition.
  Qed.

  Lemma in_dedup_was_in :
    forall xs (x : A),
      In x (dedup xs) ->
      In x xs.
  Proof using.
(* Goal: @eq (list A) (@cons A x (dedup (@cons A a xs))) (dedup (@cons A x (@cons A a xs))) *)
    induction xs; intros; simpl in *.
(* Goal: @eq (list A) (@cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) (if match A_eq_dec a x with | left e => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_introl (@eq A a x) (@In A x xs) e) | right n => match @in_dec A A_eq_dec x xs with | left i => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_intror (@eq A a x) (@In A x xs) i) | right n0 => @right (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (fun H0 : or (@eq A a x) (@In A x xs) => match H0 with | or_introl Hc1 => n Hc1 | or_intror Hc2 => n0 Hc2 end) end end then if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs) else @cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) *)
    - intuition.
(* Goal: @eq (list A) (@cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) (if match A_eq_dec a x with | left e => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_introl (@eq A a x) (@In A x xs) e) | right n => match @in_dec A A_eq_dec x xs with | left i => @left (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (@or_intror (@eq A a x) (@In A x xs) i) | right n0 => @right (or (@eq A a x) (@In A x xs)) (not (or (@eq A a x) (@In A x xs))) (fun H0 : or (@eq A a x) (@In A x xs) => match H0 with | or_introl Hc1 => n Hc1 | or_intror Hc2 => n0 Hc2 end) end end then if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs) else @cons A x (if @in_dec A A_eq_dec a xs then dedup xs else @cons A a (dedup xs))) *)
    - break_if; simpl in *; intuition.
  Qed.

  Lemma NoDup_dedup :
    forall (xs : list A),
      NoDup (dedup xs).
  Proof using.
(* Goal: @eq (list A) (dedup (@cons A a xs)) (@cons A a xs) *)
    induction xs; simpl.
    - constructor.
(* Goal: @eq (list A) (@cons A x (dedup (@nil A))) (dedup (@cons A x (@nil A))) *)
    - break_if; auto.
(* Goal: @eq (list A) (@cons A x (dedup (@nil A))) (dedup (@cons A x (@nil A))) *)
      constructor; auto.
(* Goal: not (@In A a (dedup xs)) *)
      intro.
(* Goal: False *)
      apply n.
(* Goal: @eq (list A) (@cons A x (dedup (@nil A))) (dedup (@cons A x (@nil A))) *)
      eapply in_dedup_was_in; eauto.
  Qed.

  Lemma remove_dedup_comm : forall (x : A) xs,
      remove A_eq_dec x (dedup xs) =
      dedup (remove A_eq_dec x xs).
  Proof using.
(* Goal: forall (x y : A) (_ : @In A x xs) (_ : @In A y ys), not (@eq A x y) *)
    induction xs; intros.
(* Goal: @eq (list A) (@cons A x (dedup (@nil A))) (dedup (@cons A x (@nil A))) *)
    - auto.
    - simpl. repeat (break_match; simpl); auto using f_equal.
      + exfalso. apply n0. apply remove_preserve; auto.
      + exfalso. apply n. eapply in_remove; eauto.
  Qed.

  Lemma dedup_partition :
    forall xs (p : A) ys xs' ys',
      dedup (xs ++ p :: ys) = xs' ++ p :: ys' ->
      remove A_eq_dec p (dedup (xs ++ ys)) = xs' ++ ys'.
  Proof using.
(* Goal: forall (xs : list A) (p : A) (ys xs' ys' : list A) (_ : @eq (list A) (dedup (@app A xs (@cons A p ys))) (@app A xs' (@cons A p ys'))), @eq (list A) (@remove A A_eq_dec p (dedup (@app A xs ys))) (@app A xs' ys') *)
    intros xs p ys xs' ys' H.
(* Goal: @eq (list A) (@remove A A_eq_dec p (dedup (@app A xs ys))) (@app A xs' ys') *)
    f_apply H (remove A_eq_dec p).
(* Goal: @In A a (@app A xs ys) *)
    rewrite remove_dedup_comm, remove_partition in *.
(* Goal: @eq (list A) (dedup (@remove A A_eq_dec p (@app A xs ys))) (@app A xs' ys') *)
    find_rewrite.
(* Goal: @eq (list A) (@remove A A_eq_dec p (@app A xs' (@cons A p ys'))) (@app A xs' ys') *)
    rewrite remove_partition.

(* Goal: @eq (list A) (@remove A A_eq_dec p (@app A xs' ys')) (@app A xs' ys') *)
    apply remove_not_in.
(* Goal: not (@In A p (@app A xs' ys')) *)
    apply NoDup_remove_2.
    rewrite <- H.
(* Goal: @NoDup A (dedup (@app A xs (@cons A p ys))) *)
    apply NoDup_dedup.
  Qed.

  Lemma dedup_NoDup_id : forall (xs : list A),
      NoDup xs -> dedup xs = xs.
  Proof using.
(* Goal: forall (x y : A) (_ : @In A x xs) (_ : @In A y ys), not (@eq A x y) *)
    induction xs; intros.
(* Goal: @eq (list A) (@cons A x (dedup (@nil A))) (dedup (@cons A x (@nil A))) *)
    - auto.
    - simpl. invc_NoDup. concludes.
(* Goal: @In A a (@app A xs ys) *)
      break_if; congruence.
  Qed.

  Lemma dedup_not_in_cons :
    forall x xs,
      (~ In x xs) ->
      x :: dedup xs = dedup (x :: xs).
  Proof using.
(* Goal: forall (x y : A) (_ : @In A x xs) (_ : @In A y ys), not (@eq A x y) *)
    induction xs; intros.
(* Goal: @eq (list A) (@cons A x (dedup (@nil A))) (dedup (@cons A x (@nil A))) *)
    - auto.
(* Goal: @eq (list A) (@cons A x (dedup (@cons A a xs))) (dedup (@cons A x (@cons A a xs))) *)
    - simpl in *. intuition. repeat break_match; intuition.
  Qed.
End dedup.
