# 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.