Library LibListExt

Set Implicit Arguments.
Generalizable Variables A B.

Require Import LibReflect LibTactics LibList LibListSorted LibNat LibFset LibFsetExt LibVar.

Fixing implicit arguments

Implicit Arguments nil [[A]].
Implicit Arguments cons [[A]].


Section Defs.

Variables A B : Type.
Implicit Types E : fset A.
Implicit Types l t : list A.
Implicit Types x : A.

Parameter to_list : fset Alist A.

Fixpoint removeOne x l :=
  match l with
   | nilnil
   | y :: If (x = y)
                    then
                    else y :: (removeOne x )
  end.

Fixpoint removeN l t :=
  match l with
   | nilt
   | y :: removeOne y (removeN t)
  end.

Fixpoint noDup l :=
  match l with
   | nilTrue
   | y :: ~(Mem y ) (noDup )
  end.

Fixpoint remDup l :=
  match l with
   | nilnil
   | y :: If (Mem y )
                    then remDup
                    else y :: (remDup )
  end.

Fixpoint count x l :=
  match l with
   | nil ⇒ 0
   | y :: (If (x = y)
                     then 1
                     else 0) + count x
  end.

End Defs.

Implicit Arguments removeOne [[A]].
Implicit Arguments removeN [[A]].
Implicit Arguments noDup [[A]].
Implicit Arguments remDup [[A]].
Implicit Arguments count [[A]].


Section Count.
Variables A: Type.
Implicit Types E : fset A.
Implicit Types l : list A.
Implicit Types x : A.

Lemma count_nil : x, count x nil = 0.
Proof. auto. Qed.

Lemma count_cons_pos : x l, count x (x :: l) = 1 + count x l.
Proof. introv; simpl; cases_if×. Qed.

Lemma count_cons_cancel : x l1 l2, count x (x :: l1) = count x (x :: l2) → count x l1 = count x l2.
Proof. introv; repeat rewrite count_cons_pos; nat_math. Qed.

Lemma count_Mem : x l,
  count x l > 0 Mem x l.
Proof.
  induction l.
    simpl; split; intro H.
      nat_math.
      rewrites× Mem_nil_eq in H.
      simpl; cases_if.
      splits; try nat_math.
      intros _; constructor.
      rewrite plus_0_l; rewrite IHl.
      rewrite Mem_cons_eq; splits×.
Qed.

Lemma count_app_plus : x l1 l2, count x (l1 ++ l2) = count x l1 + count x l2.
Proof.
  inductions l1; introv.
    rewrite app_nil_l; simpls¬.
    specialize (IHl1 l2); rewrite app_cons; simpls~; cases_if*; nat_math.
Qed.

End Count.


Fixpoint Mem_dec (a : var) (l : list var) : bool :=
  match l with
    | nilfalse
    | (x :: l) ⇒ ifb (a = x) then true else (Mem_dec a l)
  end.

Instance Mem_var_decidable : (a : var) (l : list var), Decidable (Mem a l).
Proof.
  intros.
  applys¬ decidable_make (Mem_dec a l).
  induction l; simpls¬.
    symmetry; rewrite Mem_nil_eq; applys¬ isTrue_false.
    cases_if~; subst; rewrites isTrue_def; cases_if×.
      false; apply H; constructor.
      inverts H; try solve [false].
      rewrites IHl; applys¬ isTrue_true.
      rewrites IHl; rewrite Mem_cons_eq in H; rew_logic in H.
      applys× isTrue_false.
Qed.


Section RemDup.
Variables A: Type.
Implicit Types E : fset A.
Implicit Types l : list A.
Implicit Types x : A.

Lemma remdup_inv: l, remDup l = nill = nil.
Proof.
  introv H. induction l; simpls¬. cases_if.
  apply IHl in H. subst. false. rewrite¬ Mem_nil_eq in H0.
Qed.

Lemma mem_remdup: l x, Mem x (remDup l) → Mem x l.
Proof.
  induction l; simpls¬. cases_if~; simpls; introv Hm.
    constructor. applys¬ IHl.
    rewrite Mem_cons_eq in ×. destruct Hm.
      left¬.
      right¬.
Qed.

Lemma mem_remdup_iff: l x,
  Mem x (remDup l) Mem x l.
Proof.
  introv; split; intro Hm; [applys¬ mem_remdup | ].
  induction l; simpls~; cases_if*; rewrite Mem_cons_eq in Hm; inverts× Hm; constructor¬.
Qed.

Lemma nodup_remdup: l,
  noDup (remDup l).
Proof.
  introv. induction l; simpls¬.
    cases_if¬. simpls. split¬.
      introv . apply H. apply¬ mem_remdup.
Qed.

Lemma remdup_eq_fl: l,
  from_list l = from_list (remDup l).
Proof.
  induction l; simpls~; cases_if; rewrite_all from_list_cons.
    rewrite <- IHl. rewrite¬ union_already_in.
    rewrite¬ from_list_spec. rewrite¬ IHl.
Qed.

Lemma fset_nodup : E,
   L, E = from_list L noDup L.
Proof.
  introv.
  lets (L & HL): fset_finite A E.
   (remDup L). split.
    rewrite¬ <- remdup_eq_fl.
    apply nodup_remdup.
Qed.

End RemDup.


Section ListBasic.
Variables A: Type.
Implicit Types l t r s : list A.
Implicit Types n : nat.

Lemma length0 : l, length l = 0 → l = nil.
Proof.
  introv.
  induction l.
    reflexivity.
    simpl. introv H. exfalso. discriminate.
Qed.

Lemma lengthn : l n,
  length l = S n y ys, l = y::ys .
Proof.
  introv.
  induction l.
    simpls. introv H. exfalso. rewrite length_nil in H. nat_math.
    introv H. ¬ a l.
Qed.

Lemma mem_len_pos : l x, Mem x llength l > 0.
Proof.
  introv Hm. induction l.
    false. rewrite¬ Mem_nil_eq in Hm.
    rew_list. nat_math.
Qed.

Lemma mem_app_inv1: l t u x, l = t ++ uMem x tMem x l.
Proof.
  introv H Hm. rewrite H. rewrite Mem_app_or_eq. left¬.
Qed.

Lemma mem_app_inv2: l t u x, l = t ++ uMem x uMem x l.
Proof.
  introv H Hm. rewrite H. rewrite Mem_app_or_eq. right¬.
Qed.

Lemma length_app_inv: l t r s,
  length l = length rlength t = length sl ++ t= r ++ s
    l = r t = s.
Proof.
  induction l; introv Hl1 Hl2 Hb.
    symmetry in Hl1. apply length0 in Hl1. rewrite Hl1 in Hb. split¬.
    remember Hl1. clear Heqe. rewrite length_cons in e.
    symmetry in e. apply lengthn in e. destruct e as ( y & ys & Hr).
    subst. rew_app in Hb. inverts Hb.
    assert (length l = length ys); auto.
    specializes IHl (>> t ys s H Hl2 H1). destruct IHl.
    subst¬.
Qed.

Lemma Forall_Mem : l (P : AProp),
  ( x, Mem x lP x) Forall P l.
Proof.
  split; induction l; try constructor¬.
    assert (Mem a (a :: l)) by constructor; auto.
    apply IHl; intros x Hm.
    specialize (H x); assert (Mem x (a :: l)) by constructor~; auto.
    introv _ Hm; rewrites× Mem_nil_eq in Hm.
    introv Hf Hm; inverts Hf.
    inverts¬ Hm.
Qed.

End ListBasic.


Section RemoveOne.
Variables A: Type.
Implicit Types E : fset A.
Implicit Types l : list A.
Implicit Types x : A.

Lemma mem_rem1_l: l x y, Mem x (removeOne y l) → Mem x l.
Proof.
  induction l; introv Hm; simpls¬.
    cases_if.
      constructor¬.
      rewrite Mem_cons_eq in ×. destruct× Hm.
Qed.

Lemma mem_rem1_r: l x y, x yMem x lMem x (removeOne y l).
Proof.
  induction l; introv Hne Hm; simpls¬.
    cases_if; rewrite Mem_cons_eq in *; destruct× Hm.
Qed.

Lemma rem1_notin_list: l x,
  ¬Mem x lremoveOne x l = l.
Proof.
  introv H. induction l; simpls¬.
    cases_if.
      false H. constructor.
      rewrite¬ IHl. introv . apply H. constructor¬.
Qed.

Lemma from_list_rem1: l x, noDup l
  from_list l \- \{x} = from_list (removeOne x l).
Proof.
  introv Hnd. induction l; simpls.
    rewrite_all from_list_nil. apply remove_from_empty.
    cases_if; rewrite_all from_list_cons.
      rewrite union_remove. rewrite remove_same. rewrite union_empty_l. rewrite× IHl.
        rewrite× rem1_notin_list.
      rewrite union_remove. rewrite remove_while_notin.
        rewrite× IHl.
        rewrite¬ notin_singleton.
Qed.

Lemma length_rem1 : l x,
  Mem x llength (removeOne x l) = length l - 1.
Proof.
  induction l; introv Hm.
    simpls¬.
    rewrite length_cons. simpls. cases_if¬.
      nat_math.
      rewrite length_cons. rewrite Mem_cons_eq in Hm. destruct× Hm. rewrite¬ IHl.
        apply mem_len_pos in H0. nat_math.
Qed.

Lemma rem1_comm: l x y,
  removeOne x (removeOne y l) = removeOne y (removeOne x l).
Proof.
  induction l; introv ; simpls¬.
    cases_if; cases_if~; simpls~; cases_if~; cases_if¬.
      rewrite¬ IHl.
Qed.

Lemma rem1_mem_comm: l x y, Mem x l
Mem y (removeOne x l) → Mem x (removeOne y l).
Proof.
  induction l; introv Hl1 Hl2; simpls¬.
    cases_if; cases_if~; rewrite Mem_cons_eq in ×.
      destruct× Hl1.
      left¬.
      right. applys× IHl.
Qed.

Lemma rem1_remN_comm: l t x, removeOne x (removeN l t) = removeN l (removeOne x t).
Proof.
  induction l; introv; simpls¬.
  rewrite (IHl (removeOne x t) a). rewrite rem1_comm.
  do 2 rewrite IHl; auto.
Qed.

Lemma count_removeOne_pos : l x,
  Mem x lcount x (removeOne x l) = count x l - 1.
Proof.
  induction l; introv Hm.
    rewrite× Mem_nil_eq in Hm.
  inverts Hm.
  simpl; cases_if*; nat_math.
  elim (classic (x = a)); introv Hneq; subst.
    simpl; cases_if*; nat_math.
    simpl; cases_if*; simpl; cases_if×.
Qed.

Lemma count_removeOne_neg : l x y,
  x ycount x (removeOne y l) = count x l.
Proof.
  induction l; introv Hneq.
    simpls¬.
  simpl; cases_if*; simpl; cases_if×.
Qed.

Lemma count_length : l1 l2,
  ( x, count x l1 = count x l2) → length l1 = length l2.
Proof.
  inductions l1; introv; introv Hyp.
    simpls; rew_length.
    elim (classic (length l2 = 0)); intro Hneq; jauto.
    assert (Hge : length l2 > 0) by nat_math; clear Hneq.
    assert ( n : nat, n > 0 → m, n = S m).
      induction n; try nat_math.
      destruct n; intros.
        ¬ 0.
        ¬ (S n).
    specialize (H (length l2) Hge).
    destruct H as (m & H); apply lengthn in H.
    destruct H as (y & ys & H); subst.
    specialize (Hyp y); simpl in Hyp; cases_if×.
    assert (Hm : Mem a l2) by (specialize (Hyp a); simpl in Hyp; cases_if*; rewrite <- count_Mem; nat_math).
    assert (Heq : length l2 = length (a :: (removeOne a l2))).
      specialize (Hyp a); simpl in Hyp; cases_if×.
    elim (classic (length l2 = 0)); intro .
      apply length0 in ; rewrite in Hm; rewrites× Mem_nil_eq in Hm.
      rew_length; rewrites¬ length_rem1; nat_math.
    rewrite Heq; rew_length.
    specialize (IHl1 (removeOne a l2)).
    rewrite IHl1; try nat_math.
    introv; specialize (Hyp x).
    simpl in Hyp; cases_if×.
    rewrites¬ count_removeOne_pos; nat_math.
    rewrite plus_0_l in Hyp; rewrite Hyp.
    rewrites¬ count_removeOne_neg.
Qed.

End RemoveOne.


Section NoDup.
Variable A: Type.
Implicit Types l t: list A.
Implicit Types x y : A.

Lemma nodup_middle: l t y,
  noDup (l ++ y::t) → ¬Mem y (l ++ t) noDup (l ++ t).
Proof.
  introv H. induction l.
    simpls¬.
    rew_app in ×. simpls. destructs H.
    specializes IHl H0. splits×.
      rewrites Mem_app_or_eq in ×. assert ( ¬Mem a l ¬Mem a (y :: t)).
        split. introv H1. apply H. left¬. introv H1. apply H. right¬.
      destruct H1. rewrite <- app_cons. rewrites Mem_app_or_eq. introv H3.
      assert (¬Mem y l ¬Mem y t).
        split. introv . apply IHl. left¬. introv . apply IHl. right¬.
        destruct H4. assert (Mem y (a::l)).
          elim H3. introv . assumption. introv . false¬ H5.
        rewrite Mem_cons_eq in H6. assert (y = a).
          elim H6. introv . assumption. introv . false¬ H4.
        rewrite Mem_cons_eq in H2. rew_logic in H2. destruct H2. apply¬ H2.
      introv . apply H. rewrites Mem_app_or_eq in ×. right. rewrites× Mem_cons_eq.
Qed.

Lemma nodup_rem1 : l x, noDup lnoDup (removeOne x l).
Proof.
  introv Hnd. induction l; simpls¬.
    cases_if×.
    simpls. split.
      introv . apply Hnd. applys× mem_rem1_l.
      applys× IHl.
Qed.

Lemma nodup_app_inv: l t,
  noDup (l ++ t) → noDup l noDup t.
Proof.
  introv Hnd. splits.
    induction l.
      simpls¬.
      rew_app in Hnd. simpl in Hnd. destruct Hnd. simpl. split.
        rewrite Mem_app_or_eq in H. introv H1. apply H.
          left¬.
        applys¬ IHl.
    induction t.
      simpls¬.
      apply nodup_middle in Hnd. destruct Hnd.
      simpl. split.
        rewrite Mem_app_or_eq in H. introv H1. apply H.
          right¬.
        applys¬ IHt.
Qed.

Lemma nodup_app_comm_step: l t x, noDup (x::l ++ t) = noDup (l ++ x::t).
Proof.
  induction l; introv.
    simpls¬.
    rew_app. simpls. rewrite <- IHl. rew_logic.
    splits; introv H; destructs H; splits~;
    rewrite_all Mem_app_or_eq in *; rewrite_all Mem_cons_eq in *;
    rew_logic in *; rewrite_all Mem_app_or_eq in *; splits×.
Qed.

Lemma nodup_app_comm: l t, noDup (l ++ t) = noDup (t ++ l).
Proof.
  induction l; introv; rew_app¬.
    simpl. rewrite IHl.
    rewrite Mem_app_or_eq.
    assert ((Mem a l Mem a t) = (Mem a t Mem a l)).
      rew_logic. intuition.
    rewrite H. rewrite <- Mem_app_or_eq. clear H.
    assert ((¬ Mem a (t ++ l) noDup (t ++ l)) = noDup (a::t++l)). simpls¬.
    rewrite H. clear H IHl.
    apply nodup_app_comm_step.
Qed.

Lemma nodup_count : l,
  noDup l ( x, Mem x lcount x l = 1).
Proof.
  introv; split.
  inductions l; introv Hd Hm.
    rewrite× Mem_nil_eq in Hm.
    rewrite Mem_cons_eq in Hm; inverts Hm; simpl; cases_if*; inverts× Hd.
      rewrite <- count_Mem in H; nat_math.
  inductions l; introv Hc; constructor;
    assert (Hm : Mem a (a :: l)) by constructor; lets Hc´ : Hc; specialize (Hc a Hm); simpl in Hc; cases_if*;
    assert (Hnm : ¬ Mem a l) by (rewrite <- count_Mem; nat_math); auto.
  apply IHl; introv Hm´.
    elim (classic (x = a)); introv Hneq; substs×.
    specialize (Hc´ x); simpl in Hc´; cases_if*; rewrite plus_0_l in Hc´; apply Hc´; constructor¬.
Qed.

Lemma nodup_app_iff : l t, noDup (l ++ t) noDup l noDup t (from_list l \n from_list t = \{}).
Proof.
  induction l using (measure_induction length); destruct l; introv; [ | split]; try intro Hyp.
    simpl; rewrite from_list_nil; rewrite app_nil_l; rewrite× inter_empty_l.
    splits; try apply (nodup_app_inv _ _ Hyp).
    apply not_not_elim; intro Hnempty; apply inter_not_empty_exists in Hnempty.
    destruct Hnempty as (x & Hin).
    rewrite in_inter in Hin; repeat rewrite from_list_spec in Hin.
    eapply nodup_count with (x := x) in Hyp.
    repeat rewrite <- count_Mem in Hin.
    rewrite count_app_plus in Hyp; nat_math.
    applys× Mem_app_or.
    destruct Hyp as (Hnd1 & Hnd2 & Hninter).
    rewrite nodup_count in ×.
    introv Hm; rewrite count_app_plus; rewrite Mem_app_or_eq in Hm; inverts× Hm.
    assert (¬ Mem x t).
      introv H1; false.
      assert (Hin : x \in (from_list (a :: l) \n from_list t)).
        rewrite in_inter; split; rewrites¬ from_list_spec.
      rewrite <- fset_extens_iff in Hninter; specialize (Hninter x).
      rewrite in_empty in Hninter; rewrites¬ <- Hninter.
    rewrite (Hnd1 x H0); rewrite <- count_Mem in H1; nat_math.
    assert (¬ Mem x (a :: l)).
      introv H1; false.
      assert (Hin : x \in (from_list (a :: l) \n from_list t)).
        rewrite in_inter; split; rewrites¬ from_list_spec.
      rewrite <- fset_extens_iff in Hninter; specialize (Hninter x).
      rewrite in_empty in Hninter; rewrites¬ <- Hninter.
    rewrite (Hnd2 x H0); rewrite <- count_Mem in H1; nat_math.
Qed.

End NoDup.


Section SplitCombine.
Variables A B: Type.
Implicit Types l t : list A.
Implicit Types r s : list B.
Implicit Types a b c d : list (A×B).
Implicit Types x : A.
Implicit Types y : B.
Implicit Types z : (A×B).

Lemma mem_comb: l r x y, length l = length r
  Mem (x,y) (combine l r) → Mem x l Mem y r.
Proof.
  induction l; introv Hl Hm.
    simpls; rewrites× Mem_nil_eq in Hm.
  lets Hl´ : Hl; rew_length in Hl; symmetry in Hl; apply lengthn in Hl.
  destruct Hl as (b & lb´ & Heq); subst.
  simpl in Hm; inverts Hm; split; constructor; eapply IHl; assert (Hl´´: length l = length lb´) by auto; try apply Hl´´; try apply H0.
Qed.

Lemma length_combine: l r,
  length l = length rlength (combine l r) = length l.
Proof.
  induction l; simpls¬.
  introv Hl; lets Hl´ : Hl; rew_length in Hl; symmetry in Hl; apply lengthn in Hl.
  destruct Hl as (b & lb´ & Heq); subst.
  rew_length in *; rewrite IHl; nat_math.
Qed.

Lemma split_spec : (l : list (A × B)),
   l1 l2, (l1, l2) = split l.
Proof.
  induction l.
    simpl; ¬ (@nil A) (@nil B).
    destruct IHl as (l1l & l2l & Heql).
    rewrite (surjective_pairing a).
    simpl; rewrite <- Heql.
    ¬ (fst a :: l1l) (snd a :: l2l).
Qed.

Lemma combine_split : l r, length l = length r
      split (combine l r) = (l,r).
Proof.
  induction l; introv Hl; simpls¬.
    rew_length in Hl; symmetry in Hl; apply length0 in Hl; substs¬.
  lets Hl´ : Hl; rew_length in Hl; symmetry in Hl; apply lengthn in Hl.
  destruct Hl as (y & & Heq); subst.
  assert (Hl´´: length l = length ) by auto.
  specialize (IHl Hl´´); symmetry in IHl.
  rewrite (split_cons) with (l1 := l) (l2 := ); auto.
Qed.

Lemma fst_split_cons: a z,
  fst (split (z::a)) = (fst z) :: (fst (split a)).
Proof.
  introv.
  lets (l1a & l2a & Heqa) : (split_spec a); rewrite <- Heqa.
  rewrite (surjective_pairing z) at 1.
  rewrite split_cons with (l1 := l1a) (l2 := l2a); auto.
Qed.

Lemma snd_split_cons: a z,
  snd (split (z::a)) = (snd z) :: (snd (split a)).
Proof.
  introv.
  lets (l1a & l2a & Heqa) : (split_spec a); rewrite <- Heqa.
  rewrite (surjective_pairing z) at 1.
  rewrite split_cons with (l1 := l1a) (l2 := l2a); auto.
Qed.

Lemma split_length_l : a,
      length (fst (split a)) = length a.
Proof.
  induction a.
    simpls¬.
    rewrite fst_split_cons; rew_length; auto.
Qed.

Lemma split_length_r : a,
  length (snd (split a)) = length a.
Proof.
  induction a.
    simpls¬.
    rewrite snd_split_cons; rew_length; auto.
Qed.

Lemma fst_split_step: a b,
  fst (split (a ++ b)) = fst (split a) ++ fst (split b).
Proof.
  inductions a; introv.
    simpl; repeat rewrites¬ app_nil_l.
    rewrite fst_split_cons.
    repeat rewrite (app_cons); rewrite <- IHa.
    rewrites¬ fst_split_cons.
Qed.

Lemma fst_split: a b c d, fst (split (a ++ b ++ c ++ d)) =
  fst (split a) ++ fst (split b) ++ fst (split c) ++ fst (split d).
Proof.
  introv. rewrite_all¬ fst_split_step.
Qed.

Lemma snd_split_step: a b,
  snd (split (a ++ b)) = snd (split a) ++ snd (split b).
Proof.
  inductions a; introv.
    simpl; repeat rewrites¬ app_nil_l.
    rewrite snd_split_cons.
    repeat rewrite (app_cons); rewrite <- IHa.
    rewrites¬ snd_split_cons.
Qed.

Lemma snd_split: a b c d, snd (split (a ++ b ++ c ++ d)) =
  snd (split a) ++ snd (split b) ++ snd (split c) ++ snd (split d).
Proof.
  introv. rewrite_all¬ snd_split_step.
Qed.

Lemma split_combine_fs: a,
 a = combine (fst (split a)) (snd (split a)).
Proof.
  induction a.
    simpls¬.
    rewrite fst_split_cons; rewrite snd_split_cons.
    simpl; rewrite IHa at 1.
    rewrite (surjective_pairing a) at 1; auto.
Qed.

Lemma combine_inv: l r,
  length l = length rcombine l r = nill = nil r = nil.
Proof.
  introv Hl Hc. split.
    induction r.
      rewrite length_nil in Hl. apply length0 in Hl. rewrite¬ Hl.
      rewrite length_cons in Hl. apply lengthn in Hl.
       destruct Hl as (z & zs & Hz). rewrite Hz in Hc. simpls. false.
    symmetry in Hl. induction l.
      rewrite length_nil in Hl. apply length0 in Hl. rewrite¬ Hl.
      rewrite length_cons in Hl. apply lengthn in Hl.
       destruct Hl as (z & zs & Hz). rewrite Hz in Hc. simpls. false.
Qed.

Lemma combine_equal_inv_l: l t r s,
  length l = length rlength t = length s
  combine l r = combine t sl = t.
Proof.
  induction l; induction t; introv Hl1 Hl2 Hp.
    reflexivity.
    rewrite length_nil in Hl1. symmetry in Hl1. apply length0 in Hl1.
     rewrite length_cons in Hl2. symmetry in Hl2. apply lengthn in Hl2.
     destruct Hl2 as (z & zs & Hz). rewrite Hz in Hp. simpls. false.
    rewrite length_nil in Hl2. symmetry in Hl2. apply length0 in Hl2.
     rewrite length_cons in Hl1. symmetry in Hl1. apply lengthn in Hl1.
     destruct Hl1 as (z & zs & Hz). rewrite Hz in Hp. simpls. false.
    rewrite length_cons in Hl1. symmetry in Hl1.
     lets Hl1´: (lengthn r Hl1).
     rewrite length_cons in Hl2. symmetry in Hl2.
     lets Hl2´: (lengthn s Hl2).
     destruct Hl1´ as (b & bs & Hb). rewrite Hb in Hp.
     destruct Hl2´ as (c & cs & Hc). rewrite Hc in Hp. simpls.
     inverts Hp.
     erewrite× IHl.
       rewrite Hb in Hl1. rewrite length_cons in Hl1. nat_math.
       rewrite Hc in Hl2. rewrite length_cons in Hl2. nat_math.
Qed.

Lemma combine_equal_inv_r: r s l t,
  length l = length rlength t = length s
    combine l r = combine t sr = s.
Proof.
  induction r; induction s; introv Hl1 Hl2 Hp.
    reflexivity.
    rewrite length_nil in Hl1. apply length0 in Hl1. rewrite Hl1 in Hp.
     rewrite length_cons in Hl2. apply lengthn in Hl2.
     destruct Hl2 as (z & zs & Hz). rewrite Hz in Hp. simpls. false.
    rewrite length_nil in Hl2. apply length0 in Hl2. rewrite Hl2 in Hp.
     rewrite length_cons in Hl1. apply lengthn in Hl1.
     destruct Hl1 as (z & zs & Hz). rewrite Hz in Hp. simpls. false.
    rewrite length_cons in Hl1.
     lets Hl1´: (lengthn l Hl1).
     rewrite length_cons in Hl2.
     lets Hl2´: (lengthn t Hl2).
     destruct Hl1´ as (b & bs & Hb). rewrite Hb in Hp.
     destruct Hl2´ as (c & cs & Hc). rewrite Hc in Hp. simpls.
     inverts Hp.
     erewrite× IHr.
       rewrite Hb in Hl1. rewrite length_cons in Hl1. nat_math.
       rewrite Hc in Hl2. rewrite length_cons in Hl2. nat_math.
Qed.

Lemma combine_equal_inv: l t r s,
  length l = length rlength t = length s
    combine l r = combine t sl = t r = s.
Proof.
  introv Hl1 Hl2 Hc. split.
    applys× (combine_equal_inv_l l t r s).
    applys× (combine_equal_inv_r r s l t).
Qed.

Lemma combine_nodup_pair_unique_fst : l r,
  length l = length r
  noDup l
   x, Mem x l
             y, Mem y r
                      Mem (x, y) (combine l r)
                      ( , Mem (x, ) (combine l r) → = y).
Proof.
  induction l using (measure_induction length); destruct l; introv Hl Hnd Hm.
    rewrite× Mem_nil_eq in Hm.
  lets Hl´ : Hl; symmetry in Hl´; rew_length in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into r.
  rewrite Mem_cons_eq in Hm; inverts Hm.
     b; splits; simpls; try solve [constructor].
    introv Hm; rewrite Mem_cons_eq in Hm; inverts Hm.
      inverts¬ H0.
    apply mem_comb in H0; try solve [rew_length in *; nat_math]; false×.
    assert (Hneq : x a) by (simpls; intro Heq; subst; false*).
    assert (Hl´ : length l = length r) by (rew_length in *; nat_math).
    assert (Hlt : length l < length (a :: l)) by (rew_length; nat_math).
    assert (Hndl : noDup l) by simpls×.
    lets (y & Hmyr & Hmxy & Hfy) : (H l Hlt r Hl´ Hndl x H0).
     y; splits; simpls; try solve [constructor~].
      introv Hm; rewrite Mem_cons_eq in Hm; inverts Hm; auto; inverts× H1.
Qed.

Lemma combine_nodup_pair_unique_snd : r l, length l = length r
  noDup r y, Mem y r x, Mem x l Mem (x, y) (combine l r) ( , Mem (, y) (combine l r) → = x).
Proof.
  induction r using (measure_induction length); destruct r; introv Hl Hnd Hm.
    rewrite× Mem_nil_eq in Hm.
  lets Hl´ : Hl; rew_length in Hl´; apply lengthn in Hl´; destruct Hl´ as (a & & Heq); subst; rename into l.
  rewrite Mem_cons_eq in Hm; inverts Hm.
     a; splits; simpls; try solve [constructor].
    introv Hm; rewrite Mem_cons_eq in Hm; inverts Hm.
      inverts¬ H0.
    apply mem_comb in H0; try solve [rew_length in *; nat_math]; false×.
    assert (Hneq : y b) by (simpls; intro Heq; subst; false*).
    assert (Hl´ : length l = length r) by (rew_length in *; nat_math).
    assert (Hlt : length r < length (b :: r)) by (rew_length; nat_math).
    assert (Hndr : noDup r) by simpls×.
    lets ( & Hmyr & Hmxy & Hfy) : (H r Hlt l Hl´ Hndr y H0).
     ; splits; simpls; try solve [constructor~].
      introv Hm; rewrite Mem_cons_eq in Hm; inverts Hm; auto; inverts× H1.
Qed.

Lemma mem_fst_split_remdup : l r x, length l = length r
  Mem x (fst (split (remDup (combine l r)))) → Mem x l.
Proof.
  inductions l; introv Hl Hm; auto.
    lets Hl´ : Hl; symmetry in Hl´; rew_length in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into r.
    simpls; cases_if.
    elim (classic (x = a)); intro Hneq; subst; constructor; apply IHl with (r := r); auto.
    rewrite fst_split_cons in Hm; rewrite Mem_cons_eq in Hm; inverts× Hm; constructor; apply IHl with (r := r); auto.
Qed.

Lemma combine_exists_fst : l r x, length l = length r
  Mem x l y, Mem (x, y) (combine l r).
Proof.
  induction l; introv Hl Hm.
    simpls; rewrite× Mem_nil_eq in Hm.
    lets Hl´ : Hl; symmetry in Hl´; rew_length in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into r.
    simpl; rewrite Mem_cons_eq in Hm; inverts Hm.
       b; constructor.
      assert (Hl´ : length l = length r) by auto.
      lets (y & Hy) : (IHl r x Hl´ H).
       y; constructor¬.
Qed.

Lemma combine_exists_snd : r l y, length l = length r
  Mem y r x, Mem (x, y) (combine l r).
Proof.
  inductions r; introv Hl Hm.
    simpls; rewrite× Mem_nil_eq in Hm.
    lets Hl´ : Hl; rew_length in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into l.
    simpl; rewrite Mem_cons_eq in Hm; inverts Hm.
       b; constructor.
      assert (Hl´ : length l = length r) by auto.
      lets (x & Hx) : (IHr l y Hl´ H).
       x; constructor¬.
Qed.

Lemma combine_remdup_fst_iff : l r x, length l = length r
  (Mem x (fst (split (remDup (combine l r)))) Mem x l).
Proof.
  introv Hl; split; inductions l; try solve [simpls~];
  introv Hm; lets Hl´ : Hl; symmetry in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into r.
    elim (classic (x = a)); introv Hneq; subst; constructor.
    apply (IHl r); try solve [rew_length in *; nat_math].
    simpls; cases_if×.
    rewrite fst_split_cons in Hm; simpls.
    rewrite Mem_cons_eq in Hm; inverts× Hm.
    rewrite Mem_cons_eq in Hm; inverts Hm; simpl; cases_if×.
    apply (IHl r); try solve [rew_length in *; nat_math].
    apply mem_comb in H; try solve [rew_length in *; nat_math]; jauto.
    rewrite fst_split_cons; simpl; constructor.
    elim (classic (x = a)); introv Hneq; subst; rewrite fst_split_cons.
       simpl; constructor.
       constructor¬.
Qed.

Lemma combine_remdup_snd_iff : r l y, length l = length r
  (Mem y (snd (split (remDup (combine l r)))) Mem y r).
Proof.
  introv Hl; split; inductions r.
  rew_length in *; apply length0 in Hl; subst; simpls¬.
  introv Hm; lets Hl´ : Hl; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into l.
    elim (classic (y = a)); introv Hneq; subst; constructor.
    apply (IHr l); try solve [rew_length in *; nat_math].
    simpls; cases_if×.
    rewrite snd_split_cons in Hm; simpls.
    rewrite Mem_cons_eq in Hm; inverts× Hm.
    rew_length in *; apply length0 in Hl; subst; simpls¬.
    introv Hm; lets Hl´ : Hl; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into l.
    rewrite Mem_cons_eq in Hm; inverts Hm; simpl; cases_if×.
    apply (IHr l); try solve [rew_length in *; nat_math].
    apply mem_comb in H; try solve [rew_length in *; nat_math]; jauto.
    rewrite snd_split_cons; simpl; constructor.
    elim (classic (y = a)); introv Hneq; subst; rewrite snd_split_cons.
       simpl; constructor.
       constructor¬.
Qed.

Lemma combine_remdup_snd : l r y, length l = length r
  Mem y (snd (split (remDup (combine l r)))) → Mem y r.
Proof.
  inductions l; introv Hl Hm.
    simpls; rewrite× Mem_nil_eq in Hm.
    lets Hl´ : Hl; symmetry in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into r.
    elim (classic (y = b)); introv Hneq; subst; constructor.
    apply (IHl r); try solve [rew_length in *; nat_math].
    simpls; cases_if×.
    rewrite snd_split_cons in Hm; simpls.
    rewrite Mem_cons_eq in Hm; inverts× Hm.
Qed.

Lemma combine_remdup_count_fst : l r x, length l = length r
  count x (fst (split (remDup (combine l r)))) count x l.
Proof.
  induction l using (measure_induction length); destruct l.
    simpl; nat_math.
  introv Hl; lets Hl´ : Hl; symmetry in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into r.
  assert (Hl1 : length l < length (a :: l)) by (rew_length; nat_math).
  assert (Hl2 : length l = length r) by auto.
  simpl; repeat cases_if×.
    specialize (H l Hl1 r a Hl2); nat_math.
    rewrite fst_split_cons; simpl; cases_if×.
    specialize (H l Hl1 r a Hl2); nat_math.
    rewrite fst_split_cons; simpl; cases_if×.
Qed.

Lemma combine_remdup_count_snd : r l y, length l = length r
  count y (snd (split (remDup (combine l r)))) count y r.
Proof.
  induction r using (measure_induction length); destruct r; introv Hl.
    rew_length in *; apply length0 in Hl; subst; simpl; nat_math.
  lets Hl´ : Hl; apply lengthn in Hl´; destruct Hl´ as (a & & Heq); subst; rename into l.
  assert (Hl1 : length r < length (b :: r)) by (rew_length; nat_math).
  assert (Hl2 : length l = length r) by auto.
  simpl; repeat cases_if×.
    specialize (H r Hl1 l b Hl2); nat_math.
    rewrite snd_split_cons; simpl; cases_if×.
    specialize (H r Hl1 l b Hl2); nat_math.
    rewrite snd_split_cons; simpl; cases_if×.
Qed.

Lemma combine_count_2_fst : l r x, length l = length r
  count x (fst (split (remDup (combine l r)))) = 2 →
   y´´, y´´ Mem (x, ) (remDup (combine l r)) Mem (x, y´´) (remDup (combine l r)).
Proof.
  induction l using (measure_induction length); destruct l; introv Hl Hceq.
    simpls; nat_math.
  lets Hl´ : Hl; symmetry in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into r.
  assert (Hl1 : length l < length (a :: l)) by (rew_length; nat_math).
  assert (Hl2 : length l = length r) by auto.
  simpls; repeat cases_if×.
  elim (classic (x = a)); intro Hneq; subst; [clear H | ]; rewrite fst_split_cons in Hceq; simpls; cases_if×.
    assert (Hc : Mem a (fst (split (remDup (combine l r))))) by (rewrite <- count_Mem; nat_math); clear Hceq.
    rewrite combine_remdup_fst_iff in Hc; auto.
    lets (y & Hy) : combine_exists_fst a Hl2 Hc.
     b y; splits; try constructor¬.
      intro Heq; subst×.
      rewrites¬ mem_remdup_iff.
    rewrite plus_0_l in Hceq.
    lets ( & y´´ & Hneqy´y´´ & Hmy´ & Hmy´´) : (H l Hl1 r x Hl2 Hceq).
     y´´; splits~; simpls; rewrite Mem_cons_eq; right; auto.
Qed.

Lemma combine_count_2_snd : r l y, length l = length r
  count y (snd (split (remDup (combine l r)))) = 2 →
   x´´, x´´ Mem (, y) (remDup (combine l r)) Mem (x´´, y) (remDup (combine l r)).
Proof.
  induction r using (measure_induction length); destruct r; introv Hl Hceq.
    rew_length; apply length0 in Hl; subst; simpls; nat_math.
  lets Hl´ : Hl; apply lengthn in Hl´; destruct Hl´ as (a & & Heq); subst; rename into l.
  assert (Hl1 : length r < length (b :: r)) by (rew_length; nat_math).
  assert (Hl2 : length l = length r) by auto.
  simpls; repeat cases_if×.
  elim (classic (y = b)); intro Hneq; subst; [clear H | ]; rewrite snd_split_cons in Hceq; simpls; cases_if×.
    assert (Hc : Mem b (snd (split (remDup (combine l r))))) by (rewrite <- count_Mem; nat_math); clear Hceq.
    rewrite combine_remdup_snd_iff in Hc; auto.
    lets (x & Hx) : combine_exists_snd b Hl2 Hc.
     a x; splits; try constructor¬.
      intro Heq; subst×.
      rewrites¬ mem_remdup_iff.
    rewrite plus_0_l in Hceq.
    lets ( & y´´ & Hneqy´y´´ & Hmy´ & Hmy´´) : (H r Hl1 l y Hl2 Hceq).
     y´´; splits~; simpls; rewrite Mem_cons_eq; right; auto.
Qed.

Lemma nodup_combine_fst : l r, length l = length r
  noDup lnoDup (combine l r).
Proof.
  inductions l; introv Hl Hnd.
    simpls¬.
    lets Hl´ : Hl; symmetry in Hl´; rew_length in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into r.
    simpl; split.
      intro Hin; apply mem_comb in Hin; simpls×.
      apply IHl; simpls*; rew_length in *; nat_math.
Qed.

Lemma nodup_combine_snd : l r, length l = length r
  noDup rnoDup (combine l r).
Proof.
  introv; generalize l; clear l.
  inductions r; introv Hl Hnd.
    rew_length in Hl; apply length0 in Hl; subst; simpls¬.
    lets Hl´ : Hl; rew_length in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & & Heq); subst; rename into l.
    simpl; split.
      intro Hin; apply mem_comb in Hin; simpls×.
      apply IHr; simpls*; rew_length in *; nat_math.
Qed.

End SplitCombine.

Hint Resolve fst_split_cons snd_split_cons split_length_l split_length_r split_combine_fs.
Hint Rewrite fst_split_cons snd_split_cons split_length_l split_length_r
: rew_split.


Section SubLists.
Variables A B: Type.
Implicit Types x : A.
Implicit Types y : B.
Implicit Types l t u v : list A.
Implicit Types r s w : list B.
Implicit Types a b c d : list (A×B).

Lemma sublists_l: l r a b c d, length l = length r
  a ++ b ++ c ++ d = combine l r e f g h, l = e ++ f ++ g ++ h
   length e = length a length f = length b
   length g = length c length h = length d.
Proof.
  introv Hls Hcm.
   (fst(split a)) (fst(split b)) (fst(split c)) (fst(split d)).
  split. assert (fst (split (combine l r)) = fst (split (a++b++c++d))).
    rewrite¬ Hcm.
  rewrite¬ combine_split in H. simpl in H. rewrite¬ <- fst_split.
  splits; rewrite¬ split_length_l.
Qed.

Lemma sublists_r: l r a b c d, length l = length r
  a ++ b ++ c ++ d = combine l r e f g h, r = e ++ f ++ g ++ h
   length e = length a length f = length b
   length g = length c length h = length d.
Proof.
  introv Hls Hcm.
   (snd(split a)) (snd(split b)) (snd(split c)) (snd(split d)).
  split. assert (snd (split (combine l r)) = snd (split (a++b++c++d))).
    rewrite¬ Hcm.
  rewrite¬ combine_split in H. simpl in H. rewrite¬ <- snd_split.
  splits; rewrite¬ split_length_r.
Qed.

Lemma sublists_2: l t u v r, length (l ++ t ++ u ++ v) = length r
   e f g h, r = e ++ f ++ g ++ h
   length l = length e length t = length f
   length u = length g length v = length h.
Proof.
  introv H. asserts Hl: (length l length r).
    rewrite <- H. rewrite length_app; nat_math.
  lets ( & Hl´ & Ht) : (take_struct (length l) r Hl).
  assert (length (t ++ u ++ v) = length ).
    rewrite Ht in H. rewrite_all length_app in ×. rewrite¬ length_take in H. nat_math.
  asserts Hb: (length t length ).
    rewrite <- H0. rewrite length_app; nat_math.
  lets (r´´ & Hb´ & Ht´) : (take_struct (length t) Hb).
  assert (length (u ++ v) = length r´´).
    rewrite Ht´ in Ht. rewrite Ht in H. rewrite_all length_app in ×. rewrite¬ length_take in H. nat_math.
  asserts Hu: (length u length r´´).
    rewrite <- H1. rewrite length_app; nat_math.
  lets (r´´´ & Hu´ & Ht´´) : (take_struct (length u) r´´ Hu).
  assert (length v = length r´´´).
    rewrite Ht´´ in Ht´. rewrite Ht´ in Ht. rewrite Ht in H. rewrite_all length_app in ×. rewrite¬ length_take in H. nat_math.
  asserts Hv: (length v length r´´´).
    rewrite <- H2. nat_math.
  lets (r´´´´ & Hv´ & Ht´´´) : (take_struct (length v) r´´´ Hv).
   (take (length l) r) (take (length t) ) (take (length u) r´´) (take (length v) r´´´).
    split.
      assert (r´´´´ = nil).
        assert (length r´´´ = length (take (length v) r´´´ ++ r´´´´)).
          rewrite Ht´´´ at 1. reflexivity.
        apply length_zero_inv. rewrite length_app in H3. nat_math.
      rewrite H3 in Ht´´´. rew_app in Ht´´´. rewrite Ht´´´ in Ht´´.
        rewrite Ht´´ in Ht´. rewrite¬ Ht´ in Ht.
      splits×.
Qed.

Lemma take_drop_nth: n x l, (LibList.Nth n l x) → l = take n l ++ (x::nil) ++ drop (n+1) l.
Proof.
  induction n; introv Hn.
    inverts Hn. simpl. rew_app¬.
    inverts Hn. simpl. rewrite app_cons. rewrite¬ <- IHn.
Qed.

Lemma sublists_3: x l r, length l = length rMem x l
   y u v s w,
  l = u ++ (x::nil) ++ v
   r = s ++ (y::nil) ++ w
   length u = length s
   length v = length w.
Proof.
  introv Hls Hm.
  assert (LibList.mem x l).
    clear Hls. induction l.
      rewrite mem_nil. rewrite Mem_nil_eq in Hm. false.
      rewrite mem_cons. rewrite Mem_cons_eq in Hm. rew_reflect. destruct Hm.
        subst. left¬.
        right¬.
  lets (n & Hn): mem_Nth H. apply (take_drop_nth) in Hn.
  lets (e&f&g&h&Happ&Hl1&Hl2&Hl3&Hl4): sublists_2 (take n l) (x :: nil) (drop (n + 1) l) (nil:list A) r.
    rew_app in ×. rewrite¬ <- Hn.
  lets Hl2´: Hl2. rewrite length_cons in Hl2´. symmetry in Hl2´.
  apply lengthn in Hl2´. destruct Hl2´ as (y & & Hs).
  assert ( = nil).
    subst f. rewrite_all length_cons in Hl2. rewrite length_nil in Hl2.
    assert (length = 0). nat_math.
    apply length0 in H0. assumption.
  subst f .
   y (take n l) (drop (n+1) l) e (g++h). splits¬.
    rewrite length_app. rewrite length_nil in Hl4. nat_math.
Qed.

End SubLists.


Section Permutation.
Variables A B: Type.
Implicit Types l t u v : list A.
Implicit Types r s y z : list B.
Implicit Types a b c d : list (A×B).
Implicit Types x : A.

Lemma permut_len: l t, permut l tlength l = length t.
Proof.
  induction 1; simpls¬. rewrite <- IHrtclosure. inverts H.
    rew_length; nat_math.
Qed.

Lemma mem_of_permuts: l t x, permut l (x::t) → Mem x l.
Proof.
  introv H. inductions H; simpls¬.
    constructor.
    inverts H.
    rewrite_all× Mem_app_or_eq in×.
Qed.

Lemma permut_mem: l t x, permut l tMem x lMem x t.
Proof.
  introv Hp. inductions Hp.
    introv H. assumption.
    induction H. introv Hm.
    rewrite_all Mem_app_or_eq in Hm. rewrite_all Mem_app_or_eq in IHHp.
    applys× IHHp.
Qed.

Lemma permut_from_list: l t, permut l tfrom_list l = from_list t.
Proof.
  introv Hp; apply fset_extens; unfold subset; introv H.
    rewrite from_list_spec in ×. eapply permut_mem; eauto.
    rewrite from_list_spec in ×. apply permut_sym in Hp. eapply permut_mem; eauto.
Qed.

Lemma permut_count : l t, permut l t x, count x l = count x t.
Proof.
  introv Hp. inductions Hp; auto.
  induction H; introv; specialize (IHHp x).
  repeat rewrite count_app_plus; repeat rewrite count_app_plus in IHHp; nat_math.
Qed.

Lemma permut_of_nil: l, permut l nill = nil.
Proof.
  introv H. inductions H; simpls¬. inverts H.
  symmetry in H1; apply nil_eq_app_inv in H1; destruct H1.
  symmetry in H1; apply nil_eq_app_inv in H1; destruct H1.
  symmetry in H2; apply nil_eq_app_inv in H2; destruct H2.
  subst¬.
Qed.

Lemma permut_flip_first_two : l t x ,
  permut l (x :: :: t) → permut l ( :: x :: t).
Proof.
    introv Hp.
    replace ( :: x :: t) with (( :: nil) ++ (x :: nil) ++ t); auto.
    apply permut_trans with (l2 := (x :: nil) ++ ( :: nil) ++ t); try applys¬ permut_get_2; auto.
Qed.

Lemma permut_mem_exists : l x,
  Mem x l , permut l (x :: ).
Proof.
  induction l; introv Hm.
    rewrite× Mem_nil_eq in Hm.
    elim (classic (x = a)); intro Hneq; subst.
       l; apply permut_refl.
    inverts× Hm.
    specialize (IHl x H0); destruct IHl as (l´´ & Hl´´).
     (a :: l´´).
    apply permut_trans with (a :: x :: l´´); try (apply permut_flip_first_two; apply permut_refl).
    applys¬ permut_cons.
Qed.

Lemma permut_count_forall : l t,
  permut l t ( x, count x l = count x t).
Proof.
  introv; splits.
    intro Hp;applys¬ permut_count.
  generalize t; clear t; induction l using (measure_induction length).
  introv Hc.
  lets Hl : count_length Hc.
  destruct l.
  symmetry in Hl; rew_length in Hl; apply length0 in Hl; substs¬.
  lets Hl´ : Hl; unfold length at 1 in Hl; simpl in Hl; symmetry in Hl; apply lengthn in Hl.
  destruct Hl as (y & & Heq); subst.
  assert (Hl : length l = length ) by auto.
  elim (classic (a = y)); introv Heqay; subst.
    apply permut_cons; apply H.
      rew_length; nat_math.
      introv; specialize (Hc x).
      simpl in Hc; cases_if×.
      assert (Hmyl : Mem y l).
        specialize (Hc y); simpl in Hc; repeat cases_if×.
        rewrite <- count_Mem; nat_math.
      assert (Hmat´ : Mem a ).
        specialize (Hc a); simpl in Hc; repeat cases_if×.
        rewrite <- count_Mem; nat_math.
   lets Hexl : (permut_mem_exists Hmyl); destruct Hexl as ( & Hpl´).
   lets Hext : (permut_mem_exists Hmat´); destruct Hext as (t´´ & Hpt´´).
   apply permut_trans with (a :: y :: ); try applys¬ permut_cons.
   apply permut_trans with (y :: a :: t´´); try (applys¬ permut_cons; applys¬ permut_sym).
   apply permut_flip_first_two; repeat apply permut_cons; apply H.
     apply permut_len in Hpl´; rew_length in *; nat_math.
     introv; specialize (Hc x).
     apply permut_count with (x := x) in Hpl´.
     apply permut_count with (x := x) in Hpt´´.
     simpl in Hc; rewrite Hpl´ in Hc; rewrite Hpt´´ in Hc; simpl in Hc.
     repeat cases_if*; nat_math.
Qed.

Lemma permut_cons_iff : l1 l1´ x,
  permut l1 l1´ permut (x :: l1) (x :: l1´).
Proof.
  introv; split.
    applys¬ permut_cons.
  introv Hp.
  lets Hl : (permut_len Hp).
  lets Hm : Hp; rewrite permut_count_forall in Hm.
  rewrite permut_count_forall; introv.
  specialize (Hm x0).
  simpl in Hm; repeat cases_if×.
Qed.

Lemma permut_cons_rem1: l x,
  Mem x lpermut l (x::(removeOne x l)).
Proof.
  introv Hm. induction l; simpls.
    false. rewrite¬ Mem_nil_eq in Hm.
    cases_if.
      permut_simpl.
      permut_simpl. rew_app. applys× IHl.
      inverts× Hm.
Qed.

Lemma rem1_permuts: l t x, Mem x lMem x t
  permut (removeOne x l) (removeOne x t) → permut l t.
Proof.
  introv Hm1 Hm2 Hp.
  apply (permut_cons x) in Hp. eapply permut_trans.
    applys× permut_cons_rem1.
    apply permut_sym. eapply permut_trans.
      applys× permut_cons_rem1.
      applys¬ permut_sym.
Qed.

Lemma permut_rem1_r: l t x,
  permut (x::l) tpermut l (removeOne x t).
Proof.
  induction l; introv Hp.
  lets Hl : Hp; apply permut_len in Hl.
  apply permut_mem with (x := x) in Hp; try constructor.
  lets Hl´ : Hl; unfold length at 1 in Hl; simpl in Hl; symmetry in Hl; apply lengthn in Hl.
  destruct Hl as (y & & Heq); subst.
  assert ( = nil) by (apply length0; rew_length in *; nat_math); subst.
  inverts Hp; simpl; cases_if×.
    rewrite Mem_nil_eq in H0; intuition.

  repeat rewrite permut_count_forall; intros.
  assert (Heq : length (x :: a :: l) = length t) by applys¬ permut_len.
  lets Hl´ : Heq; rew_length in Heq; symmetry in Heq; apply lengthn in Heq.
  destruct Heq as (y & & Heq); subst.
  elim (classic (x0 = x)); introv Heq; subst.
    rewrite count_removeOne_pos; rewrite permut_count_forall in Hp.
    simpls; specialize (Hp x); repeat cases_if*; nat_math.
    apply count_Mem; specialize (Hp x); rewrite count_cons_pos in Hp; nat_math.
    rewrites¬ count_removeOne_neg; rewrite permut_count_forall in Hp.
    simpls; specialize (Hp x0); repeat cases_if*; nat_math.
Qed.

Lemma permut_rem1_l: t l x, Mem x t
  permut l (removeOne x t) → permut (x::l) t.
Proof.
  intros t. induction t; simpls; introv Hm Hp.
    false. rewrite¬ Mem_nil_eq in Hm.
    cases_if.
      permut_simpl. assumption.
      applys× rem1_permuts (x::l) (a::t) a.
        apply Mem_next. applys× mem_of_permuts.
        constructor.
      simpl. cases_if. cases_if.
      applys× IHt. inverts× Hm.
        eapply permut_sym in Hp. apply permut_rem1_r in Hp. applys¬ permut_sym.
Qed.

Lemma permut_rem1_lr: l t x, permut l tpermut (removeOne x l) (removeOne x t).
Proof.
  induction l; simpls; introv H.
    apply permut_sym in H. apply permut_of_nil in H. subst¬.
    cases_if.
      apply permut_rem1_r in H; auto.
      apply permut_rem1_l. apply permut_sym in H. apply mem_of_permuts in H.
      applys¬ mem_rem1_r.
      rewrite rem1_comm. apply IHl. apply permut_rem1_r in H; auto.
Qed.

Lemma remN_same_perm: l t, permut l tremoveN l t = nil.
Proof.
  induction l; introv Hp; simpls¬.
    apply permut_sym in Hp. apply permut_of_nil in Hp; auto.
    rewrite rem1_remN_comm. rewrite¬ IHl. apply¬ permut_rem1_r.
Qed.

Lemma permut_remN_mem: l t x, permut (x::l) tMem x (removeN l t).
Proof.
  induction l; introv Hp; simpls¬.
    eapply mem_of_permuts. applys× permut_sym.
    rewrite rem1_remN_comm. apply IHl. apply permut_rem1_r.
    apply permut_sym. eapply permut_trans. apply permut_sym. eauto.
    permut_simpl.
Qed.

Lemma permut_remN_r: l t u,
  permut (l ++ t) upermut l (removeN t u).
Proof.
  induction l; introv Hp; simpls.
    rew_list in Hp. apply remN_same_perm in Hp. rewrite¬ <- Hp.
    rew_list in Hp. apply permut_sym in Hp. lets Hm: mem_of_permuts Hp.
    apply permut_sym in Hp. lets : Hp. apply permut_rem1_r in Hp. specializes IHl Hp.
    rewrite <- rem1_remN_comm in IHl. apply permut_rem1_l in IHl; auto.
    apply permut_remN_mem in .
    clear IHl Hp Hm.
    induction l.
      simpls¬.
      rew_list in . simpls. apply IHl. applys× mem_rem1_l.
Qed.

Lemma permut_combine_step: l t r s,
  length l = length rlength t = length s
  combine (l ++ t) (r ++ s) = combine l r ++ combine t s.
Proof.
 induction l; introv H1 H2.
    symmetry in H1. apply length_zero_inv in H1. subst r. rew_app; simpls¬.

    remember H1. clear Heqe. rew_length in H1. symmetry in H1.
    apply lengthn in H1. destruct H1 as (a0 & r0 & Hr).
    subst r. rew_app. simpls. rew_app. rewrite¬ IHl.
Qed.

Lemma permut_combine: l t u v r s y z,
  length l = length rlength t = length s
  length u = length ylength v = length z
  permut (combine (l ++ t ++ u ++ v) (r ++ s ++ y ++ z))
  (combine (l ++ u ++ t ++ v) (r ++ y ++ s ++ z)).
Proof.
  introv H1 H2 H3 H4.
  rewrite_all permut_combine_step; rew_length; auto.
  permut_simpl.
Qed.

Lemma permut_nodup: l t, permut l tnoDup lnoDup t.
Proof.
  induction l; introv Hp Hnd.
    apply permut_sym in Hp. apply permut_of_nil in Hp. rewrite¬ Hp.
    assert (noDup (removeOne a t) → noDup t).
      clear IHl. gen l. induction t; introv Hp Hnd Hnd1; simpls¬.
        cases_if. split¬.
          introv . apply Hnd. rewrite <- permut_cons_iff in Hp.
          apply permut_sym in Hp. applys× permut_mem t l.
        split~; simpls.
          introv . apply Hnd1. applys¬ mem_rem1_r.
          apply permut_sym in Hp. apply permut_rem1_r in Hp. apply permut_sym in Hp.
          eapply IHt.
            simpl in Hp. cases_if¬. eassumption. split.
              introv . apply Hnd. applys× mem_rem1_l.
              applys× nodup_rem1.
            apply Hnd1.
    apply H. apply permut_rem1_r in Hp. simpls. applys× IHl.
Qed.

Lemma permut_ndfl: l t,
  noDup lnoDup t
  from_list l = from_list t
  permut l t.
Proof.
  intro l. induction l; simpls.
    introv Hnd1 Hnd2 Hfv. rewrite from_list_nil in Hfv.
      symmetry in Hfv. apply from_list_base in Hfv. rewrite¬ Hfv.
  introv Hnd1 Hnd2 Hfv. applys× permut_rem1_l.
    rewrite from_list_cons in Hfv. rewrite <- from_list_spec. rewrite <- Hfv.
      rewrite in_union. left. rewrite¬ in_singleton.
    applys× IHl.
      apply¬ nodup_rem1.
      rewrite from_list_cons in Hfv. apply from_union_to_rem in Hfv.
        rewrite Hfv. applys× from_list_rem1.
        applys× from_list_notin.
Qed.

Lemma permut_exists: l t,
  permut l t r, length l = length r
     s, permut r s permut (combine l r) (combine t s).
Proof.
  intros l t Hp. inductions Hp; introv Hl.
    ¬ r.
    inverts H.
    lets (rs1 & rs2 & rs3 & rs4 & Hrs & Hl1 & Hl2 & Hl3 & Hl4):
      (sublists_2 l1 l2 l3 l4 r Hl).
    assert (length (l1 ++ l3 ++ l2 ++ l4) = length (rs1 ++ rs3 ++ rs2 ++ rs4)).
      rewrite Hrs in Hl. rewrite_all length_app in *; nat_math.
    specialize (IHHp (rs1 ++ rs3 ++ rs2 ++ rs4) H). destruct IHHp as (ps & Hp´ & Hc´).
     ps. split.
      assert (permut r (rs1 ++ rs3 ++ rs2 ++ rs4)).
        rewrite Hrs. permut_simpl.
        eapply permut_trans. eassumption. assumption.
      forwards× Hpc: (permut_combine l1 l2 l3 l4).
        rewrite Hrs.
        eapply permut_trans. eassumption. assumption.
Qed.

Lemma permut_exists2: l r a b c d,
  length l = length ra ++ b ++ c ++ d = combine l r
   , permut l permut r
   length = length
   a ++ c ++ b ++ d = combine .
Proof.
  introv Hls Hcm.
  lets (l1 & l2 & l3 & l4 & Hc & Hll1 & Hll2 & Hll3 & Hll4):
    (sublists_l l r a b c d Hls Hcm).
  lets (r1 & r2 & r3 & r4 & Hc´ & Hlr1 & Hlr2 & Hlr3 & Hlr4):
    (sublists_r l r a b c d Hls Hcm).
  subst l r.
   (l1 ++ l3 ++ l2 ++ l4). (r1 ++ r3 ++ r2 ++ r4).
  splits.
    permut_simpl. permut_simpl.
    rewrite_all length_app; nat_math.
    do 3 rewrite permut_combine_step in Hcm; try rewrite_all length_app; try nat_math.
    apply length_app_inv in Hcm; destruct Hcm.
    apply length_app_inv in H0; destruct H0.
    apply length_app_inv in H1; destruct H1.
    subst.
    rewrite <- permut_combine_step; try nat_math.
    rewrite <- permut_combine_step; try rewrite_all length_app; try nat_math.
    rewrite¬ <- permut_combine_step; try rewrite_all length_app; try nat_math.
    symmetry. rewrite length_combine; nat_math.
    symmetry. rewrite length_combine; nat_math.
    symmetry. rewrite length_combine; nat_math.
    symmetry. rewrite_all length_app. rewrite_all length_combine; nat_math.
    symmetry. rewrite length_combine; nat_math.
    symmetry. rewrite_all length_app. rewrite_all length_combine; nat_math.
Qed.

Lemma noDup_fst_remDup_combine : l l1 l2 r r1 r2,
  length l = length rlength l1 = length r1length l2 = length r2
  noDup lnoDup l1noDup l2
  ( g, Mem g (combine l1 r1) → Mem g (combine l r)) → ( g, Mem g (combine l2 r2) → Mem g (combine l r)) →
    noDup (fst (split (remDup (combine (l1 ++ l2) (r1 ++ r2))))).
  Proof.
    introv Hl0 Hl1 Hl2 Hnd0 Hnd1 Hnd2 Hmem1 Hmem2.
    rewrite nodup_count.
    assert (Hl : length (l1 ++ l2) = length (r1 ++ r2)) by (repeat rewrite length_app; nat_math).
    introv Hm; lets Hm´ : Hm; rewrite combine_remdup_fst_iff in Hm´; auto.
    lets Hc : combine_remdup_count_fst (l1 ++ l2) (r1 ++ r2) x Hl.
    assert (Hc´ : count x (l1 ++ l2) 2).
      rewrite nodup_count in Hnd1, Hnd2; rewrite count_app_plus.
      elim (classic (Mem x l2)); elim (classic (Mem x l1)); introv Hmp Hmq;
      try specialize (Hnd1 x Hmp); try specialize (Hnd2 x Hmq); rewrite <- count_Mem in Hmp, Hmq; try nat_math.
    assert (Hc´´ : count x (fst (split (remDup (combine (l1 ++ l2) (r1 ++ r2))))) = 0
                   count x (fst (split (remDup (combine (l1 ++ l2) (r1 ++ r2))))) = 1
                   count x (fst (split (remDup (combine (l1 ++ l2) (r1 ++ r2))))) = 2) by nat_math.
    inverts Hc´´; try inverts H; auto.
      rewrite <- count_Mem in Hm; nat_math.
      assert (H10 : count x (l1 ++ l2) = 2) by nat_math; clear Hc´; false.
      rewrite count_app_plus in H10; elim (classic (Mem x l2)); elim (classic (Mem x l1)); introv Hmp Hmq;
      lets Hnd1bis : Hnd1; lets Hnd2bis : Hnd2;
      rewrite nodup_count in Hnd1bis, Hnd2bis;
      try specialize (Hnd1bis x Hmp); try specialize (Hnd2bis x Hmq); try solve [rewrite <- count_Mem in Hmp, Hmq; nat_math].
      apply combine_count_2_fst in H0; repeat rewrite length_app; try nat_math; destruct H0 as ( & y´´ & Hneqy´y´´ & Hmy´ & Hmy´´).
      assert (Hin : Mem (x, ) (combine l r) Mem (x, y´´) (combine l r)).
        rewrite mem_remdup_iff in *; rewrite permut_combine_step in *; auto; rewrite Mem_app_or_eq in *; auto.
        inverts Hmy´; inverts Hmy´´; jauto.
      destruct Hin as (Hin1 & Hin2).
      assert (Hmxl : Mem x l) by (apply mem_comb in Hin1; jauto).
      lets Hunl : combine_nodup_pair_unique_fst l r Hl0 Hnd0 x; specialize (Hunl Hmxl).
        destruct Hunl as (Y & HmY & HmlY & HmunqY).
      lets Hypy´ : HmunqY Hin1; lets Hypy´´ : HmunqY y´´ Hin2; subst y´´; jauto.
Qed.

Lemma noDup_snd_remDup_combine : l l1 l2 r r1 r2,
  length l = length rlength l1 = length r1length l2 = length r2
  noDup rnoDup r1noDup r2
  ( g, Mem g (combine l1 r1) → Mem g (combine l r)) → ( g, Mem g (combine l2 r2) → Mem g (combine l r)) →
    noDup (snd (split (remDup (combine (l1 ++ l2) (r1 ++ r2))))).
  Proof.
    introv Hl0 Hl1 Hl2 Hnd0 Hnd1 Hnd2 Hmem1 Hmem2.
    rewrite nodup_count.
    assert (Hl : length (l1 ++ l2) = length (r1 ++ r2)) by (repeat rewrite length_app; nat_math).
    introv Hm; lets Hm´ : Hm; rewrite combine_remdup_snd_iff in Hm´; auto.
    lets Hc : (combine_remdup_count_snd (r1 ++ r2) (l1 ++ l2) x Hl).
    assert (Hc´ : count x (r1 ++ r2) 2).
      rewrite nodup_count in Hnd1, Hnd2; rewrite count_app_plus.
      elim (classic (Mem x r2)); elim (classic (Mem x r1)); introv Hmp Hmq;
      try specialize (Hnd1 x Hmp); try specialize (Hnd2 x Hmq); rewrite <- count_Mem in Hmp, Hmq; try nat_math.
    assert (Hc´´ : count x (snd (split (remDup (combine (l1 ++ l2) (r1 ++ r2))))) = 0
                   count x (snd (split (remDup (combine (l1 ++ l2) (r1 ++ r2))))) = 1
                   count x (snd (split (remDup (combine (l1 ++ l2) (r1 ++ r2))))) = 2) by nat_math.
    inverts Hc´´; try inverts H; auto.
      rewrite <- count_Mem in Hm; nat_math.
      assert (H10 : count x (r1 ++ r2) = 2) by nat_math; clear Hc´; false.
      rewrite count_app_plus in H10; elim (classic (Mem x r2)); elim (classic (Mem x r1)); introv Hmp Hmq;
      lets Hnd1bis : Hnd1; lets Hnd2bis : Hnd2;
      rewrite nodup_count in Hnd1bis, Hnd2bis;
      try specialize (Hnd1bis x Hmp); try specialize (Hnd2bis x Hmq); try solve [rewrite <- count_Mem in Hmp, Hmq; nat_math].
      apply combine_count_2_snd in H0; repeat rewrite length_app; try nat_math; destruct H0 as ( & y´´ & Hneqy´y´´ & Hmy´ & Hmy´´).
      assert (Hin : Mem (, x) (combine l r) Mem (y´´, x) (combine l r)).
        rewrite mem_remdup_iff in *; rewrite permut_combine_step in *; auto; rewrite Mem_app_or_eq in *; auto.
        inverts Hmy´; inverts Hmy´´; jauto.
      destruct Hin as (Hin1 & Hin2).
      assert (Hmxl : Mem x r) by (apply mem_comb in Hin1; jauto).
      lets Hunl : combine_nodup_pair_unique_snd r l Hl0 Hnd0 x; specialize (Hunl Hmxl).
        destruct Hunl as (Y & HmY & HmlY & HmunqY).
      lets Hypy´ : HmunqY Hin1; lets Hypy´´ : HmunqY y´´ Hin2; subst y´´; jauto.
Qed.

End Permutation.

Section Permutation2.
Variables A B: Type.
Implicit Types l t u v : list A.
Implicit Types r s y z : list B.
Implicit Types a b c d : list (A×B).
Implicit Types x : A.

Lemma permut_inv_l: l t r s,
  length l = length rlength t = length s
    permut (combine l r) (combine t s) → permut l t.
Proof.
  introv Hl1 Hl2.
  set (lr := combine l r); set (ts := combine t s).
  intro Hp; inductions Hp; subst lr ts.
     lets H: combine_equal_inv.
     lets (H1 & H2): (>> combine_equal_inv A B l t r s Hl1 Hl2 x). rewrite¬ H1.
     inverts H.
     forwards¬ ( & & Hp1´ & Hp1´´ & Hl´ & H1´): (permut_exists2 l r l1 l2 l3 l4).
     eapply permut_trans. eassumption.
     applys IHHp; try eassumption; simpls¬. rewrite¬ H1´.
Qed.

Lemma permut_inv_r: r s l t,
  length l = length rlength t = length s
    permut (combine l r) (combine t s) → permut r s.
Proof.
  introv Hl1 Hl2.
  set (lr := combine l r); set (ts := combine t s).
  intro Hp; inductions Hp; subst lr ts.
    lets H: combine_equal_inv.
    lets (H1 & H2): (>> combine_equal_inv A B l t r s Hl1 Hl2 x). rewrite¬ H2.
     inverts H.
     lets¬ (xs´ & rs´ & Hp1´ & Hp1´´ & Hl´ & H1´): (permut_exists2 l r l1 l2 l3 l4).
     eapply permut_trans. eassumption.
    applys IHHp; try eassumption; simpls¬. rewrite¬ H1´.
Qed.

End Permutation2.


Section ToList.
Variables A: Type.
Implicit Types E F : fset A.
Implicit Types l : list A.
Implicit Types x : A.

Axiom from_to_list : E,
  from_list (to_list E) = E.

Axiom to_from_list : l,
  permut l (to_list (from_list l)).

Axiom nodup_tolist: E,
  noDup (to_list E).

Lemma permut_to_list: E F,
  E = Fpermut (to_list E) (to_list F).
Proof.
  introv H. rewrite H. permut_simpl.
Qed.

Lemma to_list_cons_union: E x, x \notin E
  permut (x::(to_list E)) (to_list (E \u \{x})).
Proof.
  introv Hni. applys¬ permut_ndfl.
    simpl. split.
      rewrite <- from_list_spec. rewrite¬ from_to_list.
      apply nodup_tolist.
    apply nodup_tolist.
    rewrite from_list_cons. rewrite_all from_to_list. rewrite¬ union_comm.
Qed.

Lemma rem1_to_list_perm: E x,
  permut (removeOne x (to_list E)) (to_list (E \- \{x})).
Proof.
  introv. applys¬ permut_ndfl.
    apply nodup_rem1. apply nodup_tolist.
    apply nodup_tolist.
    rewrite <- from_list_rem1. rewrite_all¬ from_to_list.
      apply nodup_tolist.
Qed.

Lemma remN_to_list_perm: E l,
  permut (removeN l (to_list E)) (to_list (E \- from_list l)).
Proof.
  induction l; simpls¬.
    rewrite from_list_nil. rewrite¬ remove_empty.
    rewrite from_list_cons. rewrite union_comm. rewrite remove_union.
    apply permut_sym. eapply permut_trans. apply permut_sym.
    apply rem1_to_list_perm. applys¬ permut_rem1_lr. applys¬ permut_sym.
Qed.

Lemma from_to_list_union : (l1 l2 : fset A),
  from_list (to_list l1 ++ to_list l2) = l1 \u l2.
Proof.
  introv; apply fset_extens; introv.
  rewrite from_list_spec; rewrite Mem_app_or_eq; intro Hm; elim Hm; clear Hm; intro Hm; rewrite in_union; [left | right]; rewrite <- from_to_list.
  induction (to_list l1).
    rewrites¬ Mem_nil_eq in Hm; false.
    rewrites¬ from_list_spec.
  induction (to_list l2).
    rewrites¬ Mem_nil_eq in Hm; false.
    rewrites¬ from_list_spec.
  rewrite in_union; intro Hm; elim Hm; clear Hm; intro Hm; rewrite from_list_spec; rewrite Mem_app_or_eq; [left | right]; rewrite <- from_to_list in Hm; rewrite from_list_spec in Hm; auto.
Qed.


Lemma Forall_forall: (P:AProp), ( x, P x) →
  ( xs, Forall (fun xP x) xs).
Proof.
  introv H. induction xs.
    apply Forall_nil.
    applys¬ Forall_cons.
Qed.

Lemma Forall_mem: xs P x, Mem x xsForall (fun xP x) xsP x.
Proof.
  induction xs; introv Hm Hf.
    rewrite Mem_nil_eq in Hm. false.
    rewrite Mem_cons_eq in Hm. inverts Hf. destruct Hm.
      subst¬.
      applys× IHxs.
Qed.

Lemma Forall_subset: (xs : list A) ys P, Forall (fun xP x) xs → (from_list ys \c from_list xs) → Forall (fun xP x) ys.
Proof.
  introv Hf Hs.
  rewrite <- Forall_Mem in *; introv Hm; specialize (Hf x).
  rewrite <- from_list_spec in *; auto.
Qed.

End ToList.