Require Import Bool List Arith.
Set Implicit Arguments.

Section ListDefs.

Variables A B C D : Type.
Variable myeq : forall a b:A,{a=b}+{a<>b}.

Implicit Types (a : A) (b : B).

Fixpoint map_pair (f : A -> B) (g : C -> D) l :=
  match l with
    | nil => nil
    | x :: l => (f (fst x), g (snd x)) :: map_pair f g l
  end.

Fixpoint list_mem (x:A) (l:list A) : bool :=
  match l with
    | nil => false
    | cons h t => if myeq h x then true else list_mem x t
  end.

Fixpoint list_assoc (x:A) (l:list (A*B)) : option B :=
  match l with
    | nil => None
    | cons (a,b) t => if myeq a x then Some b else list_assoc x t
  end.

Fixpoint list_minus (l1:list A) (l2:list A) : list A :=
  match l1 with
    | nil => nil
    | cons h t => if list_mem h l2 then list_minus t l2 else cons h (list_minus t l2)
  end.

Fixpoint list_minus2 (l1:list (A*B)) (l2:list A) : list (A*B) :=
  match l1 with
    | nil => nil
    | cons h t => if list_mem (fst h) l2 then list_minus2 t l2 else cons h (list_minus2 t l2)
  end.

Fixpoint list_disj (l l': list A) : Prop :=
  match l' with
    | nil => True
    | cons h t => if list_mem h l then False else list_disj l t
  end.

Fixpoint list_remdup (l : list A) : list A :=
  match l with
    | nil => nil
    | h :: t => h :: list_minus (list_remdup t) (cons h nil)
  end.

Fixpoint list_remdup2 (l : list (A * B)) : list (A * B) :=
  match l with
    | nil => nil
    | (x,e) :: l => (x, e) :: list_minus2 (list_remdup2 l) (cons x nil)
  end.

Lemma map_fst_map_pair :
  forall f g l, map (@fst _ _) (map_pair f g l) = map f (map (@fst _ _) l).
Proof. induction l; intros; simpl; try rewrite IHl; auto. Qed.

Lemma map_snd_map_pair :
  forall f g l, map (@snd _ _) (map_pair f g l) = map g (map (@snd _ _) l).
Proof. induction l; intros; simpl; try rewrite IHl; auto. Qed.

Lemma in_map_fst :
  forall x (l: list (A * B)),
    In x (map (@fst _ _) l) <-> exists b, In (x, b) l.
Proof.
  induction l as [|[a b]]; simpl; intros; intuition; try contradiction;
    subst; eauto; firstorder.
  inversion H1; auto.
Qed.

Lemma in_list_minusI :
  forall x l l', In x l -> list_mem x l' = false -> In x (list_minus l l').
Proof.
  induction l as [|a l IH]; simpl; try tauto.
  intros l' [-> | IN] H; [rewrite H|destruct (list_mem a l')]; simpl; auto.
Qed.

Lemma in_list_minus :
  forall x l l',
    In x (list_minus l l') <-> (In x l /\ list_mem x l' = false).
Proof.
  intros; induction l as [|a l]; simpl; [|destruct (list_mem a l') as [] _eqn];
  simpl in *; intuition (subst; simpl in *; try congruence).
Qed.

Lemma in_list_minus2I :
  forall x l l', In x l -> list_mem (fst x) l' = false -> In x (list_minus2 l l').
Proof.
  induction l as [|a l IH]; simpl; try tauto.
  intros l' [-> | IN] H; [rewrite H|destruct (list_mem (fst a) l')]; simpl; auto.
Qed.

Lemma in_list_minus2 :
  forall x l l',
    In x (list_minus2 l l') <-> (In x l /\ list_mem (fst x) l' = false).
Proof.
  intros; induction l as [|[a b] l]; simpl; [|destruct (list_mem a l') as [] _eqn];
  simpl in *; intuition (subst; simpl in *; try congruence).
Qed.

Lemma list_mem_app :
  forall a l1 l2, list_mem a (app l1 l2) = (list_mem a l1 || list_mem a l2).
Proof.
  induction l1 as [|a1 l1 IH]; intros; simpl; trivial; rewrite IH.
  destruct myeq; trivial.
Qed.

Lemma list_mem_minus :
  forall a l1 l2, list_mem a (list_minus l1 l2) = (list_mem a l1 && negb (list_mem a l2)).
Proof.
  induction l1 as [|a1 l1 IH]; intros; simpl; trivial.
  destruct (list_mem a1 l2) as [] _eqn: X; simpl; rewrite IH;
  destruct (myeq a1 a); subst; rewrite ?X; simpl; trivial using andb_false_r.
Qed.

Lemma list_mem_remdup :
  forall x l, list_mem x (list_remdup l) = list_mem x l.
Proof.
  induction l as [|y l IH]; simpl in *; trivial.
  destruct (myeq y x); simpl; trivial; rewrite <- IH.
  generalize (list_remdup l); clear l IH.
  induction l as [|a l IH]; simpl in *; trivial.
  destruct (myeq y); simpl; subst; destruct (myeq a); simpl; subst; tauto.
Qed.

Lemma list_mem_spec :
  forall x l, if list_mem x l then In x l else ~ In x l.
Proof.
  induction l as [|a l IH]; simpl; [|destruct (myeq a x)]; auto.
  destruct (list_mem); tauto.
Qed.

Lemma list_mem_eq:
  forall x l1 l2,
    (In x l1 <-> In x l2) ->
    list_mem x l1 = list_mem x l2.
Proof.
  intros; generalize (list_mem_spec x l1), (list_mem_spec x l2).
  do 2 destruct (list_mem); tauto.
Qed.

Lemma list_mem_map_fst :
  forall x l,
    list_mem x (map (@fst _ _) l) =
    (match list_assoc x l with Some _ => true | None => false end).
Proof.
  induction l as [|[a b] l IH]; simpl; [|destruct (myeq a x)]; trivial.
Qed.

Lemma list_assoc_app :
  forall x l1 l2,
    list_assoc x (l1 ++ l2)
    = (match list_assoc x l1 with Some y => Some y | None => list_assoc x l2 end).
Proof.
  induction l1 as [|[a b] l1 IH]; intros; simpl; trivial; rewrite IH.
  destruct myeq; trivial.
Qed.

Lemma list_assoc_minus2 :
  forall a l1 l2, list_assoc a (list_minus2 l1 l2) = (if list_mem a l2 then None else list_assoc a l1).
Proof.
  induction l1 as [|[a1 b1] l1 IH]; intros; simpl; [destruct list_mem; reflexivity|].
  destruct (list_mem a1 l2) as [] _eqn: X; simpl; rewrite IH;
  destruct (myeq a1 a); subst; rewrite ?X; simpl; trivial using andb_false_r.
Qed.

Lemma list_assoc_remdup2 :
  forall x l, list_assoc x (list_remdup2 l) = list_assoc x l.
Proof.
  induction l as [|[y e] l IH]; simpl in *; trivial.
  destruct (myeq y x); simpl; trivial; rewrite <- IH.
  generalize (list_remdup2 l); clear l IH.
  induction l as [|[a b] l IH]; simpl in *; trivial.
  destruct (myeq y); simpl; subst; destruct (myeq a); simpl; subst; tauto.
Qed.

Lemma list_assoc_spec :
  forall x l,
    match list_assoc x l with
      | None => ~ In x (map (@fst _ _) l)
      | Some y => In (x, y) l
    end.
Proof.
  induction l as [|[a b] l IH]; simpl; try tauto.
  destruct (myeq a x); subst; try tauto.
  destruct (list_assoc x l); tauto.
Qed.

Lemma list_assoc_noneD :
  forall x l (H: list_assoc x l = None), ~ In x (map (@fst A B) l).
Proof. intros; generalize (list_assoc_spec x l); rewrite H; trivial. Qed.

Lemma list_assoc_someD :
  forall x l y, list_assoc x l = Some y -> In (x, y) l.
Proof. intros; generalize (list_assoc_spec x l); rewrite H; trivial. Qed.

Lemma list_minus_app :
  forall l1 l2 l, list_minus (l1 ++ l2) l = list_minus l1 l ++ list_minus l2 l.
Proof.
  induction l1 as [|a l1]; intros; simpl; [|destruct (list_mem a l)]; simpl; f_equal; trivial.
Qed.

Lemma list_minus_app_r :
  forall l l1 l2, list_minus l (l1 ++ l2) = list_minus (list_minus l l1) l2.
Proof.
  induction l as [|a l IH]; intros; simpl; try rewrite list_mem_app, IH; trivial.
  do 2 (destruct (list_mem); simpl; trivial).
Qed.

Lemma list_minus_comm :
  forall l l1 l2, list_minus (list_minus l l1) l2 = list_minus (list_minus l l2) l1.
Proof.
  induction l as [|a l IH]; intros; simpl; trivial.
  destruct (list_mem a l1) as [] _eqn: X; simpl;
  destruct (list_mem a l2) as [] _eqn: Y; simpl; rewrite ?X, ?Y, IH; trivial.
Qed.

Lemma list_minus_map_fst :
  forall l l',
    list_minus (map (@fst _ _) l) l' = map (@fst A B) (list_minus2 l l').
Proof.
  induction l; simpl; intros; auto.
  destruct (list_mem); simpl; rewrite IHl; auto.
Qed.

Lemma list_minus_red :
  forall l1 l2 l,
  list_minus (list_minus l1 l) (list_minus l2 l) = list_minus (list_minus l1 l) l2.
Proof.
  induction l1 as [|a l1 IH]; simpl; intros; auto.
  destruct (list_mem a l) as [] _eqn: X; simpl; auto.
  rewrite list_mem_minus, X, IH; destruct (list_mem a l2); trivial.
Qed.

Lemma list_minus_swap :
  forall l x y l', list_minus l (x :: y :: l') = list_minus l (y :: x :: l').
Proof.
  intros; induction l as [|a l IH]; simpl in *; trivial.
  rewrite IH; destruct (myeq x); destruct (myeq y); trivial.
Qed.

Lemma list_minus2_app :
  forall l1 l2 l, list_minus2 (l1 ++ l2) l = list_minus2 l1 l ++ list_minus2 l2 l.
Proof.
  induction l1 as [|[a b] l1]; intros; simpl; [|destruct (list_mem a l)]; simpl; f_equal; trivial.
Qed.

Lemma list_minus2_app_r :
  forall l l1 l2, list_minus2 l (l1 ++ l2) = list_minus2 (list_minus2 l l1) l2.
Proof.
  induction l as [|[a b] l IH]; intros; simpl; try rewrite list_mem_app, IH; trivial.
  do 2 (destruct (list_mem); simpl; trivial).
Qed.

Lemma list_minus2_comm :
  forall l l1 l2, list_minus2 (list_minus2 l l1) l2 = list_minus2 (list_minus2 l l2) l1.
Proof.
  induction l as [|[a b] l IH]; intros; simpl; trivial.
  destruct (list_mem a l1) as [] _eqn: X; simpl;
  destruct (list_mem a l2) as [] _eqn: Y; simpl; rewrite ?X, ?Y, IH; trivial.
Qed.

Lemma list_minus2_remdup2 :
  forall l l', list_minus2 (list_remdup2 l) l' = list_remdup2 (list_minus2 l l').
Proof.
  induction l as [|[y e] l IH]; intros; simpl in *; trivial.
  rewrite list_minus2_comm, IH.
  case_eq (list_mem y l'); simpl; [f_equal|]; intros; simpl in *; trivial.
  rewrite <- IH; generalize (list_remdup2 l); clear l IH.
  induction l as [|[a b] l IH]; intros; simpl in *; trivial.
  case_eq (list_mem a l'); intros; simpl in *; trivial.
  rewrite IH; destruct (myeq y); subst; trivial; congruence.
Qed.

Lemma list_map_fst_minus2 :
  forall l l',
    map (@fst A B) (list_minus2 l l') = list_minus (map (@fst _ _) l) l'.
Proof. symmetry; apply list_minus_map_fst. Qed.

Lemma list_minus2_eq:
  forall l l1 l2,
    (forall x , In x l1 <-> In x l2) ->
    list_minus2 l l1 = list_minus2 l l2.
Proof.
  intros; induction l; simpl; try rewrite IHl, (list_mem_eq _ _ _ (H _)); auto.
Qed.

Lemma list_disj_cons_l :
  forall a l l', list_disj (a :: l) l' <-> (list_disj l l' /\ list_mem a l' = false).
Proof.
  induction l' as [|a' l' IH]; simpl; try tauto.
  destruct (myeq a a'); subst; try tauto; destruct (myeq a'); subst;
  do 2 destruct (list_mem); intuition.
Qed.

Lemma list_disj_comm :
  forall l' l, list_disj l l' -> list_disj l' l.
Proof.
  induction l' as [|a l' IH]; simpl; auto.
    solve [clear; induction l; simpl; auto].
  intros; apply list_disj_cons_l; destruct (list_mem a l); intuition auto.
Qed.

Lemma list_disj_app_rI :
  forall l l1 l2, list_disj l l1 -> list_disj l l2 -> list_disj l (l1 ++ l2).
Proof. induction l1; simpl; intros; [|destruct (list_mem)]; auto. Qed.

Lemma list_disj_app_rD :
  forall l l1 l2, list_disj l (l1 ++ l2) -> list_disj l l1 /\ list_disj l l2.
Proof. induction l1; simpl; intros; [|destruct (list_mem)]; auto; tauto. Qed.
Implicit Arguments list_disj_app_rD [l l1 l2].

Lemma list_disj_app_r :
  forall l l1 l2, list_disj l (l1 ++ l2) <-> list_disj l l1 /\ list_disj l l2.
Proof. induction l1; simpl; intros; [|destruct (list_mem)]; auto; tauto. Qed.

Lemma list_disj_app_l :
  forall l1 l2 l, list_disj (l1 ++ l2) l <-> list_disj l1 l /\ list_disj l2 l.
Proof.
  split.
    intros H; apply list_disj_comm, list_disj_app_r in H; destruct H; auto using list_disj_comm.
  intros [H1 H2]; apply list_disj_comm, list_disj_app_r; auto using list_disj_comm.
Qed.

Lemma list_disj_minus_l :
  forall l l1 l2, list_disj l (list_minus l1 l2) -> list_disj (list_minus l l2) l1.
Proof.
  intros; apply list_disj_comm.
  revert l1 H; induction l as [|a l]; simpl in *; intros; auto.
  apply list_disj_cons_l in H.
  rewrite list_mem_minus in *.
  destruct (list_mem a l2); simpl;
  destruct (list_mem a l1); simpl; intuition auto; discriminate.
Qed.

Lemma list_disj_minus_r :
  forall l l1 l2, list_disj (list_minus l1 l2) l -> list_disj l1 (list_minus l l2).
Proof.
  auto using list_disj_comm, list_disj_minus_l.
Qed.

Lemma list_disj_mon_l :
  forall l1 l2 l,
    list_disj l1 l ->
    (forall x, In x l2 -> In x l1) ->
    list_disj l2 l.
Proof.
  intros; induction l as [|a l IH]; simpl in *; auto.
  specialize (H0 a).
  pose proof (list_mem_spec a l1).
  pose proof (list_mem_spec a l2).
  do 2 destruct list_mem; auto; contradiction.
Qed.

Lemma list_disj_mon_r :
  forall l1 l2 l,
    list_disj l l1 ->
    (forall x, In x l2 -> In x l1) ->
    list_disj l l2.
Proof. eauto using list_disj_mon_l, list_disj_comm. Qed.

Lemma list_disj_spec :
  forall l1 l2, list_disj l1 l2 <-> (forall x, In x l1 -> ~ In x l2).
Proof.
  intros; revert l1; induction l2; simpl; intuition; subst.
    pose proof (list_mem_spec x l1); destruct list_mem; firstorder.
   pose proof (list_mem_spec a l1); destruct list_mem; firstorder.
  pose proof (list_mem_spec a l1); destruct list_mem; firstorder.
Qed.

Lemma list_assoc_flip:
  forall l' l (DISJ: list_disj (map (@fst _ _) l) (map (@fst _ _) l')) x,
  list_assoc x (l' ++ l) = list_assoc x (l ++ l').
Proof.
  intros; rewrite !list_assoc_app.
  pose proof (proj1 (list_disj_spec _ _) DISJ x).
  pose proof (list_assoc_spec x l).
  pose proof (list_assoc_spec x l').
  do 2 destruct list_assoc; auto.
  destruct H; apply in_map_fst; eauto.
Qed.

Lemma list_disj_map_fst_minus2 :
  forall l l' l'',
    list_disj (list_minus (map (@fst A B) l) l') l'' ->
    list_disj (map (@fst A B) (list_minus2 l l')) l''.
Proof. intros; rewrite list_map_fst_minus2; trivial. Qed.

Lemma list_disj_minus2_mon:
  forall l l' l'',
    list_disj (map (@fst A B) l) (map (@fst A B) l') ->
    list_disj
      (map (@fst A B) (list_minus2 l l''))
      (map (@fst A B) (list_minus2 l' l'')).
Proof.
  intros; eapply list_disj_mon_l; [eapply (list_disj_mon_r _ _ _ H)|];
  intros x X; apply in_map_fst in X; destruct X as [y X];
  apply in_map_fst; exists y; eapply in_list_minus2 in X; tauto.
Qed.

End ListDefs.

Create HintDb subst_lemmas.

Hint Resolve list_disj_minus_l : subst_lemmas.
Hint Resolve list_disj_minus2_mon : subst_lemmas.
Hint Resolve list_disj_map_fst_minus2 : subst_lemmas.
Hint Rewrite list_assoc_remdup2 list_minus2_remdup2 : subst_rw_lemmas.

Ltac subst_tac :=
  solve [simpl; intros; repeat match goal with
   | _ => solve [trivial | contradiction | discriminate]
   | H : list_disj _ _ (app _ _) |- _ => apply list_disj_app_r in H; destruct H
   | _ => progress f_equal
   | H : context[list_mem _ _ (map (@fst _ _) _)] |- _ => rewrite list_mem_map_fst in H
   | |- context[match ?x with Some _ => _ | None => _ end] => destruct x
   | |- context[if ?x then _ else _] => destruct x
  end; auto with subst_lemmas].

Ltac subst_tac' :=
  try solve [simpl; intros;
  repeat (match goal with
          | _ => solve [congruence | eauto with subst_lemmas]
          | _ => progress autorewrite with subst_rw_lemmas
          | |- context[if ?x then _ else _] =>
            destruct x; simpl in *
          | _ => progress f_equal
          end)].