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

Set Implicit Arguments.

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

  Fixpoint remove_all (to_delete l : list A) : list A :=
    match to_delete with
    | [] => l
    | d :: ds => remove_all ds (remove A_eq_dec d l)
    end.

  Lemma in_remove_all_was_in :
    forall ds l x,
      In x (remove_all ds l) ->
      In x l.
  Proof using.
(* Goal: forall (ds l : list A) (x : A) (_ : @In A x (remove_all ds l)) (_ : @In A x ds), False *)
    induction ds; intros; simpl in *; intuition.
(* Goal: @In A x l *)
    eauto using in_remove.
  Qed.

  Lemma in_remove_all_preserve :
    forall ds l x,
      ~ In x ds ->
      In x l ->
      In x (remove_all ds l).
  Proof using.
(* Goal: forall (ds l : list A) (x : A) (_ : not (@In A x ds)) (_ : @In A x l), @In A x (remove_all ds l) *)
    induction ds; intros; simpl in *; intuition auto using remove_preserve.
  Qed.

  Lemma in_remove_all_not_in :
    forall ds l x,
      In x (remove_all ds l) ->
      In x ds ->
      False.
  Proof using.
(* Goal: forall (ds l : list A) (x : A) (_ : @In A x (remove_all ds l)) (_ : @In A x ds), False *)
    induction ds; intros; simpl in *; intuition.
    - subst. find_apply_lem_hyp in_remove_all_was_in.
(* Goal: False *)
      eapply remove_In; eauto.
    - eauto.
  Qed.

  Lemma remove_all_nil :
    forall ys,
      remove_all ys [] = [].
  Proof using.
(* Goal: forall xs ys zs : list A, @eq (list A) (remove_all xs (remove_all ys zs)) (remove_all ys (remove_all xs zs)) *)
    intros. induction ys; simpl in *; intuition.
  Qed.

  Lemma remove_all_cons :
    forall ys a l,
      (remove_all ys (a :: l) = remove_all ys l /\
       In a ys) \/
      (remove_all ys (a :: l) = a :: (remove_all ys l) /\
       ~In a ys).
  Proof using.
(* Goal: forall (ys : list A) (a : A) (l : list A), or (and (@eq (list A) (remove_all ys (@cons A a l)) (remove_all ys l)) (@In A a ys)) (and (@eq (list A) (remove_all ys (@cons A a l)) (@cons A a (remove_all ys l))) (not (@In A a ys))) *)
    induction ys; intros; simpl in *; intuition.
(* Goal: or (and (@eq (list A) (remove_all ys (if A_eq_dec a a0 then @remove A A_eq_dec a l else @cons A a0 (@remove A A_eq_dec a l))) (remove_all ys (@remove A A_eq_dec a l))) (or (@eq A a a0) (@In A a0 ys))) (and (@eq (list A) (remove_all ys (if A_eq_dec a a0 then @remove A A_eq_dec a l else @cons A a0 (@remove A A_eq_dec a l))) (@cons A a0 (remove_all ys (@remove A A_eq_dec a l)))) (forall _ : or (@eq A a a0) (@In A a0 ys), False)) *)
    break_if; subst; simpl in *; intuition.
(* Goal: or (and (@eq (list A) (remove_all ys (@cons A a0 (@remove A A_eq_dec a l))) (remove_all ys (@remove A A_eq_dec a l))) (or (@eq A a a0) (@In A a0 ys))) (and (@eq (list A) (remove_all ys (@cons A a0 (@remove A A_eq_dec a l))) (@cons A a0 (remove_all ys (@remove A A_eq_dec a l)))) (forall _ : or (@eq A a a0) (@In A a0 ys), False)) *)
    specialize (IHys a0 (remove A_eq_dec a l)). intuition.
  Qed.

  Lemma before_remove_all :
    forall x y l ys,
      before x y (remove_all ys l) ->
      ~ In y ys ->
      before x y l.
  Proof using.
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
    induction l; intros; simpl in *; intuition.
    - rewrite remove_all_nil in *. simpl in *. intuition.
    - pose proof remove_all_cons ys a l. intuition.
(* Goal: False *)
      + repeat find_rewrite. right. intuition eauto.
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
        subst; intuition.
(* Goal: False *)
      + repeat find_rewrite. simpl in *. intuition eauto.
  Qed.

  Lemma before_remove_all_if :
    forall x y l xs,
      before x y l ->
      ~ In x xs ->
      before x y (remove_all xs l).
  Proof using.
    induction l; intros; simpl in *; intuition;
      pose proof remove_all_cons xs a l; subst; intuition;
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
        repeat find_rewrite; simpl in *; intuition.
  Qed.

  Lemma NoDup_remove_all :
    forall l l',
    NoDup l' ->
    NoDup (remove_all l l').
  Proof using.
(* Goal: forall xs ys zs : list A, @eq (list A) (remove_all xs (remove_all ys zs)) (remove_all ys (remove_all xs zs)) *)
    intros.
(* Goal: @NoDup A (remove_all l l') *)
    induction l'.
    - rewrite remove_all_nil; auto.
    - invc_NoDup.
(* Goal: @NoDup A (remove_all l (@cons A a l')) *)
      concludes.
(* Goal: @eq (list A) (remove_all l (@cons A a (@remove A A_eq_dec a0 l'))) (@app A l0 l1) *)
      pose proof remove_all_cons l a l'.
(* Goal: @NoDup A (remove_all l (@cons A a l')) *)
      break_or_hyp; break_and; find_rewrite; auto.
(* Goal: @NoDup A (@cons A a (remove_all l l')) *)
      constructor; auto.
(* Goal: not (@In A a (remove_all l l')) *)
      intro.
(* Goal: False *)
      find_apply_lem_hyp in_remove_all_was_in; auto.
  Qed.

  Lemma remove_all_NoDup_split :
    forall l l' l0 l1 a,
     NoDup l' ->
     remove_all l l' = l0 ++ a :: l1 ->
     remove_all l (remove A_eq_dec a l') = l0 ++ l1.
  Proof using.
(* Goal: or (@eq A a x) (and (forall _ : @eq A a y, False) (@before A x y l)) *)
    induction l'; intros; simpl in *.
    - find_rewrite_lem remove_all_nil.
      destruct l0; simpl in *; match goal with H: [] = _ |- _ => contradict H end; auto using nil_cons.
    - invc_NoDup.
(* Goal: False *)
      break_if; subst.
      * rewrite remove_not_in; auto.
(* Goal: @eq (list A) (remove_all l (@cons A a (@remove A A_eq_dec a0 l'))) (@app A l0 l1) *)
        pose proof remove_all_cons l a l'.
(* Goal: @eq (list A) (remove_all l l') (@app A l0 l1) *)
        break_or_hyp; break_and.
        + find_rewrite.          
          match goal with H0: NoDup _, H1: _ = remove_all _ _ |- _ => specialize (IHl' _ _ _ H0 (eq_sym H1)) end.
(* Goal: @eq (list A) (remove_all l l') (@app A l0 l1) *)
          rewrite remove_not_in in IHl'; auto.
        + destruct l0; simpl in *; find_rewrite; find_injection; auto.
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
          assert (In a (remove_all l l')).
            match goal with H: _ = remove_all _ _ |- _ => rewrite <- H end.
(* Goal: @In A a (@app A l0 (@cons A a l1)) *)
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
            apply in_or_app.
(* Goal: or (@In A a l0) (@In A a (@cons A a l1)) *)
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
            right; left; auto.
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
          find_apply_lem_hyp in_remove_all_was_in.
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
          intuition.
(* Goal: @eq (list A) (remove_all l (@cons A a (@remove A A_eq_dec a0 l'))) (@app A l0 l1) *)
      * pose proof remove_all_cons l a l'.
(* Goal: @eq (list A) (remove_all l l') (@app A l0 l1) *)
        break_or_hyp; break_and; find_rewrite.
        + pose proof remove_all_cons l a (remove A_eq_dec a0 l').
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
          break_or_hyp; break_and; intuition.
(* Goal: @eq (list A) (remove_all l (@cons A a (@remove A A_eq_dec a0 l'))) (@app A l0 l1) *)
          aggressive_rewrite_goal; auto.
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
        + destruct l0; simpl in *; find_injection; intuition.
          match goal with H0: NoDup _, H1: _ = remove_all _ _ |- _ => specialize (IHl' _ _ _ H0 (eq_sym H1)) end.
          rewrite <- IHl'.
(* Goal: @eq (list A) (remove_all l (@cons A a (@remove A A_eq_dec a0 l'))) (@cons A a (remove_all l (@remove A A_eq_dec a0 l'))) *)
          pose proof remove_all_cons l a (remove A_eq_dec a0 l').
(* Goal: @eq (list A) (remove_all l l') (@cons A a (@app A l0 l1)) *)
          break_or_hyp; break_and; intuition.
  Qed.

  Lemma remove_all_app_l :
    forall xs ys zs,
      remove_all (xs ++ ys) zs = remove_all xs (remove_all ys zs).
  Proof using.
(* Goal: forall xs ys zs : list A, @eq (list A) (remove_all xs (remove_all ys zs)) (remove_all ys (remove_all xs zs)) *)
    induction zs; intros.
    - now repeat rewrite remove_all_nil.
    - pose proof (remove_all_cons (xs ++ ys) a zs).
(* Goal: @eq (list A) (remove_all xs (remove_all ys (@cons A a zs))) (remove_all ys (remove_all xs (@cons A a zs))) *)
      pose proof (remove_all_cons ys a zs).
(* Goal: @eq (list A) (remove_all xs (remove_all ys (@cons A a zs))) (remove_all ys (remove_all xs (@cons A a zs))) *)
      pose proof (remove_all_cons xs a (remove_all ys zs)).
      repeat (break_or_hyp; break_and); repeat find_rewrite;
      try find_eapply_lem_hyp in_app_or;
      try assert (In a (xs ++ ys)) by (eapply in_or_app; eauto);
(* Goal: @eq (list A) (remove_all xs (@app A (@remove A A_eq_dec a ys) (@remove A A_eq_dec a zs))) (@app A (remove_all xs (@remove A A_eq_dec a ys)) (remove_all xs (@remove A A_eq_dec a zs))) *)
      tauto.
  Qed.

  Lemma remove_all_app_r :
    forall xs ys zs,
      remove_all xs (ys ++ zs) = remove_all xs ys ++ remove_all xs zs.
  Proof using.
(* Goal: forall xs ys zs : list A, @eq (list A) (remove_all xs (@app A ys zs)) (@app A (remove_all xs ys) (remove_all xs zs)) *)
    induction xs.
    - auto.
    - intros.
(* Goal: @eq (list A) (remove_all (@cons A a xs) (@app A ys zs)) (@app A (remove_all (@cons A a xs) ys) (remove_all (@cons A a xs) zs)) *)
      simpl.
(* Goal: @eq (list A) (remove_all xs (@remove A A_eq_dec a (@app A ys zs))) (@app A (remove_all xs (@remove A A_eq_dec a ys)) (remove_all xs (@remove A A_eq_dec a zs))) *)
      rewrite remove_app_comm.
(* Goal: @eq (list A) (remove_all xs (@app A (@remove A A_eq_dec a ys) (@remove A A_eq_dec a zs))) (@app A (remove_all xs (@remove A A_eq_dec a ys)) (remove_all xs (@remove A A_eq_dec a zs))) *)
      auto.
  Qed.

  Lemma remove_all_del_comm :
    forall xs ys zs,
      remove_all xs (remove_all ys zs) = remove_all ys (remove_all xs zs).
  Proof using.
(* Goal: forall xs ys zs : list A, @eq (list A) (remove_all xs (remove_all ys zs)) (remove_all ys (remove_all xs zs)) *)
    intros.
(* Goal: forall xs ys zs : list A, @eq (list A) (remove_all xs (remove_all ys zs)) (remove_all ys (remove_all xs zs)) *)
    induction zs; intros.
    - now repeat rewrite remove_all_nil.
    - pose proof (remove_all_cons xs a zs).
(* Goal: @eq (list A) (remove_all xs (remove_all ys (@cons A a zs))) (remove_all ys (remove_all xs (@cons A a zs))) *)
      pose proof (remove_all_cons ys a zs).
(* Goal: @eq (list A) (remove_all xs (remove_all ys (@cons A a zs))) (remove_all ys (remove_all xs (@cons A a zs))) *)
      pose proof (remove_all_cons ys a (remove_all xs zs)).
(* Goal: @eq (list A) (remove_all xs (remove_all ys (@cons A a zs))) (remove_all ys (remove_all xs (@cons A a zs))) *)
      pose proof (remove_all_cons xs a (remove_all ys zs)).
      repeat (break_or_hyp; break_and);
        repeat find_rewrite;
        congruence.
  Qed.

End remove_all.
Arguments in_remove_all_was_in : clear implicits.
