Require Import D5.

Module Recursives.

Fixpoint elem {A : Type} (x : A) (l : list A) : Prop :=
match l with
    | [] => False
    | h :: t => x = h \/ elem x t
end.

Fixpoint all {A : Type} (P : A -> Prop) (l : list A) : Prop :=
match l with
    | [] => True
    | h :: t => P h /\ all P t
end.

Lemma all_spec :
  forall (A : Type) (P : A -> Prop) (l : list A),
    all P l <-> Forall P l.

Fixpoint exactly
  {A : Type} (P : A -> Prop) (n : nat) (l : list A) : Prop :=
match l, n with
    | [], 0 => True
    | [], _ => False
    | h :: t, 0 => ~ P h /\ exactly P 0 t
    | h :: t, S n' =>
        (P h /\ exactly P n' t) \/ (~ P h /\ exactly P n t)
end.

Lemma exactly_spec :
  forall (A : Type) (P : A -> Prop) (n : nat) (l : list A),
    exactly P n l <-> Exactly P n l.

Lemma ex_spec :
  forall (A : Type) (P : A -> Prop) (l : list A),
    ex P l <-> exists x : A, elem x l /\ P x.

Lemma ex_nil :
  forall (A : Type) (P : A -> Prop),
    ex P [] <-> False.

Lemma ex_cons :
  forall (A : Type) (P : A -> Prop) (h : A) (t : list A),
    ex P (h :: t) <-> P h \/ ex P t.

Lemma ex_length :
  forall (A : Type) (P : A -> Prop) (l : list A),
    ex P l -> 1 <= length l.

Lemma ex_snoc :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    ex P (snoc x l) <-> ex P l \/ P x.

Lemma ex_app :
  forall (A : Type) (P : A -> Prop) (l1 l2 : list A),
    ex P (l1 ++ l2) <-> ex P l1 \/ ex P l2.

Lemma ex_rev :
  forall (A : Type) (P : A -> Prop) (l : list A),
    ex P (rev l) <-> ex P l.

Lemma ex_map :
  forall (A B : Type) (P : B -> Prop) (f : A -> B) (l : list A),
    ex P (map f l) -> ex (fun x : A => P (f x)) l.

Lemma ex_join :
  forall (A : Type) (P : A -> Prop) (ll : list (list A)),
    ex P (join ll) <->
    ex (fun l : list A => ex P l) ll.

Lemma ex_replicate :
  forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
    ex P (replicate n x) <-> 1 <= n /\ P x.

Lemma ex_nth :
  forall (A : Type) (P : A -> Prop) (l : list A),
    ex P l <->
    exists (n : nat) (x : A), nth n l = Some x /\ P x.

Lemma ex_remove :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    ex P l ->
    match remove n l with
        | None => True
        | Some (x, l') => ~ P x -> ex P l'
    end.

Lemma ex_take :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    ex P (take n l) -> ex P l.

Lemma ex_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    ex P (drop n l) -> ex P l.

Lemma ex_take_drop :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat),
    ex P l -> ex P (take n l) \/ ex P (drop n l).

Lemma ex_splitAt :
  forall (A : Type) (P : A -> Prop) (l l1 l2 : list A) (n : nat) (x : A),
    splitAt n l = Some (l1, x, l2) ->
      ex P l <-> P x \/ ex P l1 \/ ex P l2.

Lemma ex_insert :
  forall (A : Type) (P : A -> Prop) (l : list A) (n : nat) (x : A),
    ex P (insert l n x) <-> P x \/ ex P l.

Lemma ex_replace :
  forall (A : Type) (P : A -> Prop) (l l' : list A) (n : nat) (x : A),
    replace l n x = Some l' ->
      ex P l' <->
      ex P (take n l) \/ P x \/ ex P (drop (S n) l).

Lemma ex_filter :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P (filter p l) -> ex P l.

Lemma ex_filter_conv :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P l ->
      ex P (filter p l) \/
      ex P (filter (fun x : A => negb (p x)) l).

Lemma ex_filter_compat :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = false) -> ~ ex P (filter p l).

Lemma ex_partition :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l l1 l2 : list A),
    partition p l = (l1, l2) ->
      ex P l <-> ex P l1 \/ ex P l2.

Lemma ex_takeWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P (takeWhile p l) -> ex P l.

Lemma ex_takeWhile_compat :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    (forall x : A, P x <-> p x = false) -> ~ ex P (takeWhile p l).

Lemma ex_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P (dropWhile p l) -> ex P l.

Lemma ex_takeWhile_dropWhile :
  forall (A : Type) (P : A -> Prop) (p : A -> bool) (l : list A),
    ex P l -> ex P (takeWhile p l) \/ ex P (dropWhile p l).

Lemma ex_span :
  forall
    (A : Type) (P : A -> Prop) (p : A -> bool) (x : A) (l b e : list A),
      (forall x : A, P x <-> p x = true) ->
      span p l = Some (b, x, e) ->
        ex P l <-> ex P b \/ P x \/ ex P e.

Lemma ex_interesting :
  forall (A B : Type) (P : A * B -> Prop) (la : list A) (hb : B) (tb : list B),
    ex (fun a : A => ex (fun b : B => P (a, b)) tb) la ->
    ex (fun a : A => ex (fun b : B => P (a, b)) (hb :: tb)) la.

Lemma ex_zip :
  forall (A B : Type) (P : A * B -> Prop) (la : list A) (lb : list B),
    ex P (zip la lb) ->
      ex (fun a : A => ex (fun b : B => P (a, b)) lb) la.

Lemma ex_pmap :
  forall (A B : Type) (f : A -> option B) (P : B -> Prop) (l : list A),
    ex P (pmap f l) <->
      ex (fun x : A => match f x with | Some b => P b | _ => False end) l.

Lemma ex_intersperse :
  forall (A : Type) (P : A -> Prop) (x : A) (l : list A),
    ex P (intersperse x l) <->
    ex P l \/ (P x /\ 2 <= length l).

End Recursives.

Fixpoint list_eq_dec
  {A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1, l2 with
    | [], [] => true
    | [], _ => false
    | _, [] => false
    | h1 :: t1, h2 :: t2 => eq_dec h1 h2 && list_eq_dec eq_dec t1 t2
end.

Lemma list_eq_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l1 l2 : list A),
      reflect (l1 = l2) (list_eq_dec eq_dec l1 l2).

Definition elem_dec
  {A : Type} (eq_dec : A -> A -> bool) (x : A) (l : list A) : bool :=
    any (eq_dec x) l.

Lemma elem_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (x : A) (l : list A),
      reflect (elem x l) (elem_dec eq_dec x l).

Lemma In_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (x : A) (l : list A),
      reflect (In x l) (elem_dec eq_dec x l).

Fixpoint Dup_dec
  {A : Type} (eq_dec : A -> A -> bool) (l : list A) : bool :=
match l with
    | [] => false
    | h :: t => elem_dec eq_dec h t || Dup_dec eq_dec t
end.

Lemma Dup_dec_spec :
  forall
    (A : Type) (eq_dec : A -> A -> bool)
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l : list A),
      reflect (Dup l) (Dup_dec eq_dec l).

Lemma Exists_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A),
      reflect (Exists P l) (any p l).

Lemma Forall_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A),
      reflect (Forall P l) (all p l).

Definition Exactly_dec
  {A : Type} (p : A -> bool) (n : nat) (l : list A) : bool :=
    count p l =? n.

Lemma Exactly_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A) (n : nat),
      reflect (Exactly P n l) (Exactly_dec p n l).

Definition AtLeast_dec
  {A : Type} (p : A -> bool) (n : nat) (l : list A) : bool :=
    n <=? count p l.

Lemma AtLeast_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A) (n : nat),
      reflect (AtLeast P n l) (AtLeast_dec p n l).

Definition AtMost_dec
  {A : Type} (p : A -> bool) (n : nat) (l : list A) : bool :=
    count p l <=? n.

Lemma AtMost_dec_spec :
  forall
    {A : Type} {P : A -> Prop} {p : A -> bool}
    (P_dec_spec : forall x : A, reflect (P x) (p x))
    (l : list A) (n : nat),
      reflect (AtMost P n l) (AtMost_dec p n l).

Fixpoint Sublist_dec
  {A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l2 with
    | [] => false
    | h2 :: t2 =>
        list_eq_dec eq_dec l1 t2 || Sublist_dec eq_dec l1 t2
end.

Lemma Sublist_dec_spec :
  forall
    (A : Type) (eq_dec : A -> A -> bool)
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l1 l2 : list A),
      reflect (Sublist l1 l2) (Sublist_dec eq_dec l1 l2).

Fixpoint Prefix_dec
  {A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1, l2 with
    | [], _ => true
    | _, [] => false
    | h1 :: t1, h2 :: t2 => eq_dec h1 h2 && Prefix_dec eq_dec t1 t2
end.

Lemma Prefix_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l1 l2 : list A),
      reflect (Prefix l1 l2) (Prefix_dec eq_dec l1 l2).

Definition Suffix_dec
  {A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
    Prefix_dec eq_dec (rev l1) (rev l2).

Lemma Suffix_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l1 l2 : list A),
      reflect (Suffix l1 l2) (Suffix_dec eq_dec l1 l2).

Fixpoint Subseq_dec
  {A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1, l2 with
    | [], _ => true
    | _, [] => false
    | h1 :: t1, h2 :: t2 =>
        (eq_dec h1 h2 && Subseq_dec eq_dec t1 t2) ||
        Subseq_dec eq_dec l1 t2
end.

Lemma Subseq_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l1 l2 : list A),
      reflect (Subseq l1 l2) (Subseq_dec eq_dec l1 l2).

Fixpoint Incl_dec
  {A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1 with
    | [] => true
    | h :: t => elem_dec eq_dec h l2 && Incl_dec eq_dec t l2
end.

Lemma Incl_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l1 l2 : list A),
      reflect (Incl l1 l2) (Incl_dec eq_dec l1 l2).

Definition SetEquiv_dec
  {A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
    Incl_dec eq_dec l1 l2 && Incl_dec eq_dec l2 l1.

Lemma SetEquiv_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l1 l2 : list A),
      reflect (SetEquiv l1 l2) (SetEquiv_dec eq_dec l1 l2).

Fixpoint Permutation_dec
  {A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
match l1 with
    | [] => isEmpty l2
    | h :: t =>
        match removeFirst (eq_dec h) l2 with
            | None => false
            | Some (_, l2') => Permutation_dec eq_dec t l2'
        end
end.

Lemma Permutation_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l1 l2 : list A),
      reflect (Permutation l1 l2) (Permutation_dec eq_dec l1 l2).

Fixpoint Cycle_dec_aux
  {A : Type} (eq_dec : A -> A -> bool) (n : nat) (l1 l2 : list A) : bool :=
match n with
    | 0 => list_eq_dec eq_dec l1 l2
    | S n' =>
        list_eq_dec eq_dec l1 (drop n l2 ++ take n l2) ||
        Cycle_dec_aux eq_dec n' l1 l2
end.

Definition Cycle_dec
  {A : Type} (eq_dec : A -> A -> bool) (l1 l2 : list A) : bool :=
    Cycle_dec_aux eq_dec (length l1) l1 l2.

Lemma Cycle_dec_aux_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (m : nat) (l1 l2 : list A),
      reflect
        (exists n : nat, n <= m /\ l1 = drop n l2 ++ take n l2)
        (Cycle_dec_aux eq_dec m l1 l2).

Lemma Cycle_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (m : nat) (l1 l2 : list A),
      reflect (Cycle l1 l2) (Cycle_dec eq_dec l1 l2).

Definition Palindrome_dec
  {A : Type} (eq_dec : A -> A -> bool) (l : list A) : bool :=
    list_eq_dec eq_dec l (rev l).

Lemma Palindrome_dec_spec :
  forall
    {A : Type} {eq_dec : A -> A -> bool}
    (eq_dec_spec : forall x y : A, reflect (x = y) (eq_dec x y))
    (l : list A),
      reflect (Palindrome l) (Palindrome_dec eq_dec l).

Module sublists.

Fixpoint sublists {A : Type} (l : list A) : list (list A) :=
match l with
    | [] => []
    | h :: t => t :: sublists t
end.

Lemma sublists_spec :
  forall {A : Type} (l1 l2 : list A),
    Sublist l1 l2 -> elem l1 (sublists l2).

Lemma sublists_spec' :
  forall {A : Type} (l1 l2 : list A),
    elem l1 (sublists l2) -> Sublist l1 l2.

End sublists.

Module suffixes.

Fixpoint suffixes {A : Type} (l : list A) : list (list A) :=
  l ::
match l with
    | [] => []
    | h :: t => suffixes t
end.

Lemma suffixes_spec :
  forall {A : Type} (l1 l2 : list A),
    Suffix l1 l2 -> elem l1 (suffixes l2).

Lemma suffixes_spec' :
  forall {A : Type} (l1 l2 : list A),
    elem l1 (suffixes l2) -> Suffix l1 l2.

End suffixes.

Module prefixes.

Import suffixes.

Fixpoint prefixes {A : Type} (l : list A) : list (list A) :=
  [] ::
match l with
    | [] => []
    | h :: t => map (cons h) (prefixes t)
end.

Lemma prefixes_spec :
  forall {A : Type} (l1 l2 : list A),
    Prefix l1 l2 -> elem l1 (prefixes l2).

Lemma elem_map_cons :
  forall {A : Type} (h1 h2 : A) (t1 : list A) (t2 : list (list A)),
    elem (h1 :: t1) (map (cons h2) t2) -> h1 = h2.

Lemma prefixes_spec' :
  forall {A : Type} (l1 l2 : list A),
    elem l1 (prefixes l2) -> Prefix l1 l2.

End prefixes.

Module subseqs.

Fixpoint subseqs {A : Type} (l : list A) : list (list A) :=
match l with
    | [] => [[]]
| h :: t => map (cons h) (subseqs t) ++ subseqs t
end.

Compute subseqs [1; 2; 3; 4; 5].

Lemma Subseq_subseqs :
  forall (A : Type) (l1 l2 : list A),
    Subseq l1 l2 -> elem l1 (subseqs l2).

Lemma subseqs_Subseq :
  forall (A : Type) (l1 l2 : list A),
    elem l1 (subseqs l2) -> Subseq l1 l2.

End subseqs.

Module subsets.


Fixpoint subsets {A : Type} (l : list A) : list (list A) :=
match l with
    | [] => [[]]
| h :: t => subsets t ++ map (cons h) (subsets t)
end.

Import prefixes.

End subsets.

Module cycles.

Fixpoint cycles_aux {A : Type} (n : nat) (l : list A) : list (list A) :=
match n with
    | 0 => []
    | S n' => cycle n l :: cycles_aux n' l
end.

Compute cycles_aux 0 [1; 2; 3; 4; 5].
Compute cycles_aux 5 [1; 2; 3; 4; 5].

Definition cycles {A : Type} (l : list A) : list (list A) :=
match l with
    | [] => [[]]
| _ => cycles_aux (length l) l
end.

Compute cycles [].
Compute cycles [1].
Compute cycles [1; 2; 3; 4; 5].

Lemma Cycle_cycles_aux :
  forall (A : Type) (l1 l2 : list A),
    Cycle l1 l2 -> forall n : nat,
      elem l1 (cycles_aux (S (length l2) + n) l2).

End cycles.

Module Transpositions.

Inductive Perm {A : Type} : list A -> list A -> Prop :=
    | Perm_refl : forall l : list A, Perm l l
    | Perm_transp :
        forall (x y : A) (l1 l2 l3 l4 : list A),
          Perm (l1 ++ x :: l2 ++ y :: l3) l4 ->
            Perm (l1 ++ y :: l2 ++ x :: l3) l4.

Lemma Perm_cons :
  forall {A : Type} (h : A) (t1 t2 : list A),
    Perm t1 t2 -> Perm (h :: t1) (h :: t2).

Lemma Perm_trans :
  forall {A : Type} {l1 l2 l3 : list A},
    Perm l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.

Lemma Permutation_transpose :
  forall {A : Type} {x y : A} {l1 l2 l3 : list A},
    Permutation (l1 ++ x :: l2 ++ y :: l3) (l1 ++ y :: l2 ++ x :: l3).

Lemma Perm_Permutation :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Permutation l1 l2.

End Transpositions.

Module AdjacentTranspositions.

Inductive Perm {A : Type} : list A -> list A -> Prop :=
    | Perm_refl : forall l : list A, Perm l l
    | Perm_steptrans :
      forall (x y : A) (l1 l2 l3 : list A),
        Perm (l1 ++ y :: x :: l2) l3 -> Perm (l1 ++ x :: y :: l2) l3.

Lemma Perm_Permutation :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 -> Permutation l1 l2.

Lemma Perm_cons :
  forall {A : Type} (x : A) {l1 l2 : list A},
    Perm l1 l2 -> Perm (x :: l1) (x :: l2).

Lemma Perm_trans :
  forall {A : Type} {l1 l2 l3 : list A},
    Perm l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.

End AdjacentTranspositions.

Module Exchange.

Definition exchange {A : Type} (l1 l2 : list A) : Prop :=
  exists (x y : A) (r1 r2 : list A),
    l1 = r1 ++ x :: y :: r2 /\
    l2 = r1 ++ y :: x :: r2.

Inductive Perm {A : Type} : list A -> list A -> Prop :=
    | Perm_refl : forall l : list A, Perm l l
    | Perm_step_trans :
        forall l1 l2 l3 : list A,
          exchange l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Perm_cons :
  forall (A : Type) (x : A) (l1 l2 : list A),
    Perm l1 l2 -> Perm (x :: l1) (x :: l2).

Lemma Perm_trans :
  forall (A : Type) (l1 l2 l3 : list A),
    Perm l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Permutation_Perm :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> Perm l1 l2.

Lemma Perm_Permutation :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 -> Permutation l1 l2.

Lemma Perm_spec :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 <-> Permutation l1 l2.

Lemma Perm_count :
  forall (A : Type) (p : A -> bool) (l1 l2 : list A),
    Perm l1 l2 -> count p l1 = count p l2.

End Exchange.

Module Exactly.

Ltac inv H := inversion H; subst; clear H.

Definition Perm {A : Type} (l1 l2 : list A) : Prop :=
  forall (P : A -> Prop) (n : nat),
    Exactly P n l1 <-> Exactly P n l2.

Lemma Permutation_Exactly :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 ->
      forall (P : A -> Prop) (n : nat),
        Exactly P n l1 -> Exactly P n l2.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.

Lemma Perm_front_ex :
  forall {A : Type} {h : A} {t l : list A},
    Perm (h :: t) l ->
      exists l1 l2 : list A,
        l = l1 ++ h :: l2 /\ Perm t (l1 ++ l2).

Lemma Perm_Permutation :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Permutation l1 l2.

End Exactly.

Module AtLeast.

Ltac inv H := inversion H; subst; clear H.

Definition Perm {A : Type} (l1 l2 : list A) : Prop :=
  forall (P : A -> Prop) (n : nat),
    (AtLeast P n l1 <-> AtLeast P n l2).

Hint Constructors AtLeast : core.

Lemma Permutation_AtLeast :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 ->
      forall (P : A -> Prop) (n : nat),
        AtLeast P n l1 -> AtLeast P n l2.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.

Lemma AtLeast_1 :
  forall {A : Type} {P : A -> Prop} {l : list A},
    AtLeast P 1 l ->
      exists (x : A) (l1 l2 : list A),
        P x /\ l = l1 ++ x :: l2.

Lemma AtLeast_app_comm' :
  forall {A : Type} {P : A -> Prop} {n : nat} {l1 l2 : list A},
    AtLeast P n (l1 ++ l2) <-> AtLeast P n (l2 ++ l1).

Lemma AtLeast_cons_app :
  forall
    {A : Type} {P : A -> Prop} {n : nat}
    (x : A) (l1 l2 : list A),
      AtLeast P n (l1 ++ x :: l2) <->
      AtLeast P n (x :: l1 ++ l2).

Lemma Perm_front_ex :
  forall {A : Type} {h : A} {t l : list A},
    Perm (h :: t) l ->
      exists l1 l2 : list A,
        l = l1 ++ h :: l2 /\ Perm t (l1 ++ l2).

Lemma Perm_Permutation :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Permutation l1 l2.

Hint Constructors Exactly : core.

(* TODO *) Lemma AtLeast_Exactly :
  forall {A : Type} (l1 l2 : list A),
    (forall (P : A -> Prop) (n : nat),
      AtLeast P n l1 <-> AtLeast P n l2)
    <->
    (forall (P : A -> Prop) (n : nat),
      Exactly P n l1 <-> Exactly P n l2).

End AtLeast.

Module Count.

Definition perm {A : Type} (l1 l2 : list A) : Prop :=
  forall p : A -> bool, count p l1 = count p l2.

Lemma count_ex :
  forall (A : Type) (p : A -> bool) (l : list A),
    count p l = 0 \/
    exists (x : A) (l1 l2 : list A),
      p x = true /\ l = l1 ++ x :: l2.

Import Exchange.

Lemma Perm_perm :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 -> perm l1 l2.

Lemma perm_Perm :
  forall (A : Type) (l1 l2 : list A),
    perm l1 l2 -> Perm l1 l2.

End Count.

Module perms_select.

Fixpoint select {A : Type} (l : list A) : list (list A * list A) :=
match l with
    | [] => [([], [])]
    | h :: t => [([], l)] ++ map (fun '(a, b) => (h :: a, b)) (select t)
end.

Lemma select_app :
  forall {A : Type} {l1 l2 : list A},
    select (l1 ++ l2) =
      map (fun '(l, r) => (app l l2, r)) (select l1) ++
      map (fun '(l, r) => (app l1 l, r)) (select l2).

Fixpoint perms {A : Type} (l : list A) : list (list A) :=
match l with
    | [] => [[]]
| h :: t =>
        bind (fun ll =>
          map (fun '(l, r) => l ++ h :: r) (select ll)) (perms t)
end.

Compute select [1; 2; 3].
Compute perms [1; 2; 3].

Lemma Permutation_bind :
  forall {A B : Type} (f g : A -> list B),
    (forall x : A, Permutation (f x) (g x)) ->
      forall l : list A, Permutation (bind f l) (bind g l).

(* TODO: bind_app *)

Lemma bind_bind :
  forall {A B C : Type} (f : A -> list B) (g : B -> list C) (l : list A),
    bind g (bind f l) = bind (fun x : A => bind g (f x)) l.

Lemma Permutation_select_app :
  forall {A : Type} {l1 l2 : list A},
    Permutation (select (l1 ++ l2)) (select (l2 ++ l1)).

Lemma map_select :
  forall {A B : Type} (f : A -> B) (l : list A),
    select (map f l) = map (fun '(L, R) => (map f L, map f R)) (select l).

Lemma Permutation_perms :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> Permutation (perms l1) (perms l2).

Lemma elem_perms :
  forall (A : Type) (l : list A),
    elem l (perms l).

Lemma Permutation_perms' :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> elem l1 (perms l2).

End perms_select.

Module perms_ins.

Fixpoint ins {A : Type} (x : A) (l : list A) : list (list A) :=
match l with
    | [] => [[x]]
| h :: t => [x :: h :: t] ++ map (cons h) (ins x t)
end.

Fixpoint perms {A : Type} (l : list A) : list (list A) :=
match l with
    | [] => [[]]
| h :: t => bind (ins h) (perms t)
end.

Lemma len_ins :
  forall (A : Type) (x : A) (l : list A),
    length (ins x l) = S (length l).

Fixpoint nsum (l : list nat) : nat :=
match l with
    | [] => 0
    | h :: t => h + nsum t
end.

Lemma len_join :
  forall (A : Type) (ll : list (list A)),
    length (join ll) = nsum (map length ll).

Lemma len_perms :
  forall (A : Type) (l : list A),
    length (perms l) = fact (length l).

Lemma map_ins :
  forall (A B : Type) (f : A -> B) (x : A) (l : list A),
    map (map f) (ins x l) = ins (f x) (map f l).

Lemma ins_app :
  forall (A : Type) (x : A) (l1 l2 : list A),
    l1 = [] \/
    l2 = [] \/
      ins x (l1 ++ l2) =
      map (fun l => app l l2) (ins x l1) ++
      map (app l1) (ins x l2).

Lemma ins_snoc :
  forall (A : Type) (x y : A) (l : list A),
    ins x (snoc y l) =
    snoc (snoc x (snoc y l)) (map (snoc y) (ins x l)).

Lemma map_ext_eq :
  forall {A B : Type} {f g : A -> B} {l : list A},
    (forall x : A, f x = g x) ->
      map f l = map g l.

Lemma ins_rev :
  forall (A : Type) (x : A) (l : list A),
    ins x (rev l) = rev (map rev (ins x l)).

Lemma elem_ins :
  forall (A : Type) (x : A) (l : list A),
    elem (x :: l) (ins x l).

Lemma elem_perms :
  forall (A : Type) (l : list A),
    elem l (perms l).

Lemma Permutation_elem_ins :
  forall (A : Type) (x : A) (l1 l2 : list A),
    elem l2 (ins x l1) -> Permutation (x :: l1) l2.

Lemma Permutation_bind :
  forall (A B : Type) (f g : A -> list B) (l1 l2 : list A),
    (forall x : A, Permutation (f x) (g x)) ->
      Permutation l1 l2 ->
        Permutation (bind f l1) (bind g l2).

Lemma bind_comm :
  forall (A B C : Type) (f g: A -> list A) (l : list A),
    bind f (bind g l) =
    bind g (bind f l).

Lemma count_join :
  forall (A : Type) (p : A -> bool) (l : list (list A)),
    count p (join l) = nsum (map (count p) l).

Lemma nsum_app :
  forall l1 l2 : list nat,
    nsum (l1 ++ l2) = nsum l1 + nsum l2.

Fixpoint deepcount
  {A : Type} (p : A -> bool) (l : list (list A)) : nat :=
match l with
    | [] => 0
    | h :: t => count p h + deepcount p t
end.

Lemma bind_assoc :
  forall
    (A B C : Type) (f : A -> list B) (g : B -> list C) (la : list A),
      bind g (bind f la) = bind (fun x => bind g (f x)) la.

Lemma Permutation_bind_ins :
  forall (A : Type) (x y : A) (l : list A),
    Permutation
      (bind (ins x) (ins y l))
      (bind (ins y) (ins x l)).

Lemma Permutation_perms :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> Permutation (perms l1) (perms l2).

Lemma Permutation_perms' :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> elem l1 (perms l2).

Lemma perms_Permutation :
  forall {A : Type} {l1 l2 : list A},
    elem l1 (perms l2) -> Permutation l1 l2.

End perms_ins.

Module perms_cycles.

Import cycles.

Fixpoint perms {A : Type} (l : list A) : list (list A) :=
match l with
    | [] => [[]]
| h :: t =>
        join (map (fun t => cycles (cons h t)) (perms t))
end.

Compute cycles [1; 2].
Compute perms [3].
Compute perms [2; 3].
Compute cycles (map (cons 2) [[3]]).
Compute perms [1; 2; 3].
Compute perms [1; 2; 3; 4].

Require Import D4.

Fixpoint sum (l : list nat) : nat :=
match l with
    | [] => 0
    | h :: t => h + sum t
end.

Lemma len_join :
  forall {A : Type} (l : list (list A)),
    length (join l) = sum (map length l).

Lemma len_cycles_aux :
  forall {A : Type} (l : list A) (n : nat),
    length (cycles_aux n l) = n.

Lemma len_cycles :
  forall {A : Type} (l : list A),
    l <> [] -> length (cycles l) = length l.

Lemma sum_map_S :
  forall l : list nat,
    sum (map S l) = length l + sum l.

Lemma sum_replicate :
  forall n m : nat,
    sum (replicate n m) = n * m.

Lemma length_perms :
  forall {A : Type} (l : list A),
    length (perms l) = fact (length l) /\
      map length (perms l) =
      replicate (length (perms l)) (length l).

Lemma perms_spec :
  forall {A : Type} (l1 l2 : list A),
    elem l1 (perms l2) -> Permutation l1 l2.

Lemma perms_spec :
  forall {A : Type} (l1 l2 : list A),
    Permutation l1 l2 -> elem l1 (perms l2).

End perms_cycles.

Module Specs.

Import Count.

Import perms_select.

Lemma perm_perms :
  forall {A : Type} {l1 l2 : list A},
    perm l1 l2 -> elem l1 (perms l2).

End Specs.

(* Module SetPermDedup. *)

Inductive SameSet {A : Type} : list A -> list A -> Prop :=
    | SameSet_nil : SameSet [] []
    | SameSet_cons :
        forall (h : A) (t1 t2 : list A), SameSet t1 t2 -> SameSet (h :: t1) (h :: t2)
    | SameSet_swap :
        forall (x y : A) (l : list A), SameSet (y :: x :: l) (x :: y :: l)
    | SameSet_dedup :
        forall (h : A) (t : list A), SameSet (h :: t) (h :: h :: t)
    | SameSet_trans :
        forall l1 l2 l3 : list A, SameSet l1 l2 -> SameSet l2 l3 -> SameSet l1 l3.

Lemma SameSet_SetEquiv :
  forall {A : Type} {l1 l2 : list A},
    SameSet l1 l2 -> SetEquiv l1 l2.
Proof.
  induction 1; unfold SetEquiv in *; intro z.
    reflexivity.
    rewrite !elem_cons', IHSameSet. reflexivity.
    rewrite !elem_cons'. firstorder.
    rewrite !elem_cons'. firstorder.
    rewrite IHSameSet1, IHSameSet2. reflexivity.
Qed.

Lemma Permutation_SameSet :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> SameSet l1 l2.
Proof.
  induction 1; econstructor; eassumption.
Qed.

(* End SetPermDedup. *)

Module SetPermNoDup.

Definition Represents {A : Type} (l1 l2 : list A) : Prop :=
  Permutation l1 l2 /\ NoDup l2.

Inductive RepresentSameSet {A : Type} (l1 l2 : list A) : Prop :=
    | SameSet'' :
        forall l : list A,
          Represents l1 l -> Represents l2 l -> RepresentSameSet l1 l2.

Lemma RepresentSameSet_Represents :
  forall {A : Type} {l1 l2 : list A},
    RepresentSameSet l1 l2 -> SameSet l1 l2.
Proof.
  intros A l1 l2 [l [HP1 HN1] [HP2 HN2]].
  apply Permutation_SameSet.
  eapply Permutation_trans.
    eassumption.
    symmetry. assumption.
Qed.

Lemma SameSet_RepresentSameSet :
  forall {A : Type} {l1 l2 : list A},
    SameSet l1 l2 -> RepresentSameSet l1 l2.
Proof.
  induction 1.
    exists []; repeat constructor.
    admit.
    exists (x :: y :: l); constructor.
      constructor.
      constructor.
Abort.

End SetPermNoDup.

Module SetExists.

Definition SameSetEx {A : Type} (l1 l2 : list A) : Prop :=
  forall P : A -> Prop, Exists P l1 <-> Exists P l2.

Lemma SameSetEx_SetEquiv :
  forall {A : Type} {l1 l2 : list A},
    SameSetEx l1 l2 <-> SetEquiv l1 l2.
Proof.
  unfold SameSetEx, SetEquiv.
  split; intros.
    specialize (H (fun y => x = y)). rewrite !Exists_spec in H.
      firstorder; specialize (H x); specialize (H0 x); cbn in *; firstorder congruence.
    rewrite !Exists_spec. firstorder.
Qed.

End SetExists.

Module SetAdjacentTranspositionDedup.

Inductive AdjacentTransposition {A : Type} : list A -> list A -> Prop :=
    | AdjacentTransposition' :
        forall (x y : A) (l1 l2 : list A),
          AdjacentTransposition (l1 ++ x :: y :: l2) (l1 ++ y :: x :: l2).

Inductive AdjacentDedup {A : Type} : list A -> list A -> Prop :=
    | AdjacentDedup' :
        forall (x : A) (l1 l2 : list A),
          AdjacentDedup (l1 ++ x :: x :: l2) (l1 ++ x :: l2).

Inductive SameSetATD {A : Type} : list A -> list A -> Prop :=
    | SameSetATD_refl :
        forall l : list A, SameSetATD l l
    | SameSetATD_transp :
        forall l1 l2 l3 : list A,
          AdjacentTransposition l1 l2 -> SameSetATD l2 l3 -> SameSetATD l1 l3
    | SameSetATD_dedup :
        forall l1 l2 l3 : list A,
          AdjacentDedup l1 l2 -> SameSetATD l2 l3 -> SameSetATD l1 l3.

Inductive SameSetATD' {A : Type} (l1 : list A) : list A -> Prop :=
    | SameSetATD'_refl :
        SameSetATD' l1 l1
    | SameSetATD'_transp :
        forall l2 l3 : list A,
          SameSetATD' l1 l2 -> AdjacentTransposition l2 l3 -> SameSetATD' l1 l3
    | SameSetATD'_dedup :
        forall l2 l3 : list A,
          SameSetATD' l1 l2 -> AdjacentDedup l2 l3 -> SameSetATD' l1 l3.

Lemma SameSetATD_trans :
  forall {A : Type} {l1 l2 : list A},
    SameSetATD l1 l2 ->
      forall {l3 : list A}, SameSetATD l2 l3 -> SameSetATD l1 l3.
Proof.
  induction 1; intros.
    assumption.
    econstructor.
      eassumption.
      apply IHSameSetATD. assumption.
    econstructor 3.
      eassumption.
      apply IHSameSetATD. assumption.
Qed.

Lemma SameSetATD'_trans :
  forall {A : Type} {l1 l2 : list A},
    SameSetATD' l1 l2 ->
      forall {l3 : list A}, SameSetATD' l2 l3 -> SameSetATD' l1 l3.
Proof.
  induction 1; intros.
    assumption.
    econstructor.
      eassumption.
Restart.
  intros until 2. revert l1 H.
  induction H0; intros.
    assumption.
    econstructor.
      apply IHSameSetATD'. assumption.
      assumption.
    econstructor 3.
      apply IHSameSetATD'. assumption.
      assumption.
Qed.

Lemma SameSetATD'_spec :
  forall {A : Type} {l1 l2 : list A},
    SameSetATD' l1 l2 <-> SameSetATD l1 l2.
Proof.
  split.
    induction 1.
      constructor.
      apply (SameSetATD_trans IHSameSetATD'). econstructor.
        eassumption.
        constructor.
      apply (SameSetATD_trans IHSameSetATD'). econstructor 3.
        eassumption.
        constructor.
    induction 1.
      constructor.
      eapply SameSetATD'_trans.
        2: eassumption.
        econstructor.
          constructor.
          assumption.
      eapply SameSetATD'_trans.
        2: eassumption.
        econstructor 3.
          constructor.
          assumption.
Qed.

Lemma SameSetATD_SetEquiv :
  forall {A : Type} {l1 l2 : list A},
    SameSetATD l1 l2 -> SetEquiv l1 l2.
Proof.
  unfold SetEquiv.
  induction 1; intro.
    apply SetEquiv_refl.
    inv H. rewrite <- IHSameSetATD, !elem_app, !elem_cons'. firstorder.
    inv H. rewrite <- IHSameSetATD, !elem_app, !elem_cons'. firstorder.
Qed.

Lemma AdjacentTransposition_cons :
  forall {A : Type} {t1 t2 : list A},
    AdjacentTransposition t1 t2 ->
      forall h : A, AdjacentTransposition (h :: t1) (h :: t2).
Proof.
  induction 1.
  intro h.
  rewrite <- !app_cons_l.
  constructor.
Qed.

Lemma AdjacentDedup_cons :
  forall {A : Type} {t1 t2 : list A},
    AdjacentDedup t1 t2 ->
      forall h : A, AdjacentDedup (h :: t1) (h :: t2).
Proof.
  induction 1.
  intro h.
  rewrite <- !app_cons_l.
  constructor.
Qed.

Lemma SameSetATD_cons :
  forall {A : Type} {t1 t2 : list A},
    SameSetATD t1 t2 ->
      forall h : A, SameSetATD (h :: t1) (h :: t2).
Proof.
  induction 1; intros h.
    constructor.
    apply (@SameSetATD_transp _ _ (h :: l2)).
      apply AdjacentTransposition_cons. assumption.
      apply IHSameSetATD.
    apply (@SameSetATD_dedup _ _ (h :: l2)).
      apply AdjacentDedup_cons. assumption.
      apply IHSameSetATD.
Qed.

Lemma SetEquiv_SameSetATD :
  forall {A : Type} {l1 l2 : list A},
    SetEquiv l1 l2 -> SameSetATD l1 l2.
Proof.
  unfold SetEquiv.
  induction l1 as [| h1 t1];
  intros l2 H.
    admit.
    {
      assert (elem h1 l2).
        apply H. left.
      apply elem_spec in H0.
      destruct H0 as (l1 & l3 & H0); subst.
      admit.
    }
Admitted.

End SetAdjacentTranspositionDedup.

Module SetTranspositionDedup.

Inductive Transposition {A : Type} : list A -> list A -> Prop :=
    | Transposition' :
        forall (x y : A) (l1 l2 l3 : list A),
          Transposition (l1 ++ x :: l2 ++ y :: l3) (l1 ++ y :: l2 ++ x :: l3).

Inductive Dedup {A : Type} : list A -> list A -> Prop :=
    | Dedup' :
        forall (x : A) (l1 l2 l3 : list A),
          Dedup (l1 ++ x :: l2 ++ x :: l3) (l1 ++ x :: l2 ++ l3).

Inductive SameSetTD {A : Type} : list A -> list A -> Prop :=
    | SameSetTD_refl :
        forall l : list A, SameSetTD l l
    | SameSetTD_transp :
        forall l1 l2 l3 : list A,
          Transposition l1 l2 -> SameSetTD l2 l3 -> SameSetTD l1 l3
    | SameSetTD_dedup :
        forall l1 l2 l3 : list A,
          Dedup l1 l2 -> SameSetTD l2 l3 -> SameSetTD l1 l3.

Lemma SameSetTD_SetEquiv :
  forall {A : Type} {l1 l2 : list A},
    SameSetTD l1 l2 -> SetEquiv l1 l2.
Proof.
  unfold SetEquiv.
  induction 1; intro.
    apply SetEquiv_refl.
    inv H. rewrite <- IHSameSetTD, !elem_app, !elem_cons', !elem_app, !elem_cons'. firstorder.
    inv H. rewrite <- IHSameSetTD, !elem_app, !elem_cons', !elem_app, !elem_cons'. firstorder.
Qed.

End SetTranspositionDedup.

Module PermWeird.

Inductive Elem {A : Type} (x : A) : list A -> Type :=
    | Z : forall l : list A, Elem x (x :: l)
    | S : forall {t : list A}, Elem x t -> forall h : A, Elem x (h :: t).

Arguments Z {A x} _.
Arguments S {A x t} _ _.

Require Import H.

Definition Perm {A : Type} (l1 l2 : list A) : Type :=
  forall x : A, iso (Elem x l1) (Elem x l2).

Require Import Equality.

(* Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.
Proof.
  induction 1.
    red. intro. split with (coel := id) (coer := id).
      1-2: reflexivity.
    red. intro y. unfold Perm in *. destruct (IHPermutation y).
      esplit. Unshelve. all: cycle 4. 1-4: intro H'.
        inv H'.
          left.
          right. apply coel. assumption.
        inv H'.
          left.
          right. apply coer. assumption.
        dependent induction H'; cbn; congruence.
        dependent induction H'; cbn; congruence.
    red. intro z. esplit. Unshelve. all: cycle 3. 1-4: intro H'.
        inv H'.
          right. left.
          inv X.
            left.
            right. right. assumption.
        inv H'.
          right. left.
          inv X.
            left.
            right. right. assumption.
        do 2 (dependent induction H'; cbn; try congruence).
        do 2 (dependent induction H'; cbn; try congruence).
    intro H'. eapply iso_trans.
      apply IHPermutation1.
      apply IHPermutation2.
Qed.
 *)

(* Lemma Perm_Permutation :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Permutation l1 l2.
Proof.
  unfold Perm.
  induction l1 as | h1 t1; intros.
    destruct l2 as | h2 t2.
      constructor.
      specialize (H h2). destruct H.
        clear -coer. specialize (coer ltac:(left)). inv coer.
    destruct l2 as | h2 t2.
      specialize (H h1). destruct H.
        clear -coel. specialize (coel ltac:(left)). inv coel.
Admitted.
 *)
End PermWeird.