Require Import Stdlib.Arith.Arith Stdlib.Vectors.FinFun.
Import Init.Nat.
Import List.ListNotations.

Require Import Utf8 Misc Utils.

Definition reflexive {A} (rel : A → A → bool) :=
  ∀ a, rel a a = true.

Fixpoint is_permutation {A} (eqb : A → A → bool) (la lb : list A) :=
  match la with
  | [] ⇒ match lb with [] ⇒ true | _ ⇒ false end
  | a :: la' ⇒
      match List_extract (eqb a) lb with
      | None ⇒ false
      | Some (bef, _, aft) ⇒ is_permutation eqb la' (bef ++ aft)
      end
  end.

Definition permutation {A} (eqb : A → _) la lb :=
  is_permutation eqb la lb = true.

Theorem permutation_cons_l_iff : ∀ A (eqb : A → _) a la lb,
  permutation eqb (a :: la) lb
  ↔ match List_extract (eqb a) lb with
     | Some (bef, _, aft) ⇒ permutation eqb la (bef ++ aft)
     | None ⇒ False
     end.


Theorem permutation_cons_inv : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb a,
  permutation eqb (a :: la) (a :: lb) → permutation eqb la lb.

Theorem permutation_app_inv_aux : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb lc ld a,
  a ∉ la
  → a ∉ lc
  → permutation eqb (la ++ a :: lb) (lc ++ a :: ld)
  → permutation eqb (la ++ lb) (lc ++ ld).


Theorem permutation_refl : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l, permutation eqb l l.

Theorem permutation_in_iff : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ [la lb], permutation eqb la lb → ∀ a, a ∈ la ↔ a ∈ lb.
Theorem permutation_sym : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb, permutation eqb la lb → permutation eqb lb la.

Theorem permutation_nil_l : ∀ {A} {eqb : A → _} l,
  permutation eqb [] l → l = [].

Theorem permutation_nil_r : ∀ {A} {eqb : A → _} l,
  permutation eqb l [] → l = [].

Theorem permutation_trans : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb lc,
  permutation eqb la lb → permutation eqb lb lc → permutation eqb la lc.


Theorem permutation_nil_nil : ∀ {A} {eqb : A → _}, permutation eqb [] [].

Theorem permutation_skip : ∀ {A} {eqb : A → _},
  reflexive eqb
  → ∀ a la lb, permutation eqb la lb → permutation eqb (a :: la) (a :: lb).

Theorem permutation_swap : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ a b la, permutation eqb (b :: a :: la) (a :: b :: la).


Theorem permutation_add_inv : ∀ {A} {eqb : A → _} (Heqb : equality eqb),
  ∀ a la lb,
  permutation eqb la lb
  → ∀ lc ld,
  permutation eqb (a :: lc) la
  → permutation eqb (a :: ld) lb
  → permutation eqb lc ld.


Theorem permutation_app_tail : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l l' tl,
  permutation eqb l l' → permutation eqb (l ++ tl) (l' ++ tl).

Theorem permutation_app_head : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l tl tl',
  permutation eqb tl tl' → permutation eqb (l ++ tl) (l ++ tl').

Theorem permutation_app : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l m l' m',
  permutation eqb l l'
  → permutation eqb m m'
  → permutation eqb (l ++ m) (l' ++ m').

Theorem permutation_cons_append : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l x, permutation eqb (x :: l) (l ++ [x]).

Theorem permutation_app_comm : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l l', permutation eqb (l ++ l') (l' ++ l).

Theorem permutation_cons_app : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l l1 l2 a,
  permutation eqb l (l1 ++ l2)
  → permutation eqb (a :: l) (l1 ++ a :: l2).

Theorem permutation_middle : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb a,
  permutation eqb (a :: la ++ lb) (la ++ a :: lb).

Theorem permutation_elt : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ (la lb lc ld : list A) (a : A),
  permutation eqb (la ++ lb) (lc ++ ld)
  → permutation eqb (la ++ a :: lb) (lc ++ a :: ld).

Theorem permutation_rev_l : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l, permutation eqb (List.rev l) l.

Theorem permutation_rev_r : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l, permutation eqb l (List.rev l).

Theorem permutation_length : ∀ {A} {eqb : A → _} {la lb},
  permutation eqb la lb → List.length la = List.length lb.

Theorem permutation_app_inv : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb lc ld a,
  permutation eqb (la ++ a :: lb) (lc ++ a :: ld)
  → permutation eqb (la ++ lb) (lc ++ ld).
Theorem permutation_app_inv_l : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l l1 l2,
  permutation eqb (l ++ l1) (l ++ l2) → permutation eqb l1 l2.

Theorem permutation_app_inv_r : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l l1 l2,
  permutation eqb (l1 ++ l) (l2 ++ l) → permutation eqb l1 l2.

Theorem permutation_length_1 : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ a b,
  permutation eqb [a] [b] → a = b.

Theorem permutation_length_1_inv_l :
  ∀ {A} {eqb : A → _} (Heqb : equality eqb) a l,
  permutation eqb [a] l → l = [a].

Theorem permutation_length_1_inv_r :
  ∀ {A} {eqb : A → _} (Heqb : equality eqb) a l,
  permutation eqb l [a] → l = [a].

Theorem NoDup_permutation : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb,
  List.NoDup la
  → List.NoDup lb
  → (∀ x : A, x ∈ la ↔ x ∈ lb)
  → permutation eqb la lb.
Theorem NoDup_permutation_bis : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb,
  List.NoDup la
  → List.length lb ≤ List.length la
  → List.incl la lb
  → permutation eqb la lb.

Theorem permutation_NoDup : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ [la lb],
  permutation eqb la lb → List.NoDup la → List.NoDup lb.

Theorem permutation_map : ∀ {A B} [eqba : A → _] [eqbb : B → _],
  equality eqba →
  equality eqbb →
  ∀ (f : A → B) (la lb : list A),
  permutation eqba la lb → permutation eqbb (List.map f la) (List.map f lb).


Theorem List_rank_loop_extract : ∀ A (la : list A) f i,
  List_rank_loop i f la =
  match List_extract f la with
  | Some (bef, _, _) ⇒ i + List.length bef
  | None ⇒ i + List.length la
  end.

Theorem List_rank_extract : ∀ A (la : list A) f,
  List_rank f la =
  match List_extract f la with
  | Some (bef, _, _) ⇒ List.length bef
  | None ⇒ List.length la
  end.

Theorem List_rank_not_found : ∀ n l i,
  permutation Nat.eqb l (List.seq 0 n)
  → i < n
  → List_rank (Nat.eqb i) l ≠ List.length l.


Definition option_eqb {A} (eqb : A → A → bool) ao bo :=
  match (ao, bo) with
  | (Some a, Some b) ⇒ eqb a b
  | _ ⇒ false
  end.

Fixpoint permutation_assoc_loop {A} eqb (la : list A) lbo :=
  match la with
  | [] ⇒ []
  | a :: la' ⇒
      match List_extract (λ bo, option_eqb eqb bo (Some a)) lbo with
      | Some (befo, _, afto) ⇒
          List.length befo ::
            permutation_assoc_loop eqb la' (befo ++ None :: afto)
      | None ⇒ []
      end
  end.

Definition permutation_assoc {A} (eqb : A → _) la lb :=
  permutation_assoc_loop eqb la (List.map Some lb).

Definition permutation_fun {A} (eqb : A → _) la lb i :=
  let j := List_rank (Nat.eqb i) (permutation_assoc eqb la lb) in
  if j =? List.length la then 0 else j.

Fixpoint filter_Some {A} (lao : list (option A)) :=
  match lao with
  | [] ⇒ []
  | Some a :: lao' ⇒ a :: filter_Some lao'
  | None :: lao' ⇒ filter_Some lao'
  end.

Theorem fold_permutation_assoc : ∀ {A} {eqb : A → _} la lb,
  permutation_assoc_loop eqb la (List.map Some lb) =
  permutation_assoc eqb la lb.

Theorem filter_Some_inside : ∀ A l1 l2 (x : option A),
  filter_Some (l1 ++ x :: l2) =
    filter_Some l1 ++
    match x with
    | Some a ⇒ a :: filter_Some l2
    | None ⇒ filter_Some l2
    end.

Theorem filter_Some_map_Some : ∀ A (la : list A),
  filter_Some (List.map Some la) = la.

Theorem permutation_assoc_loop_length : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lbo,
  permutation eqb la (filter_Some lbo)
  → List.length (permutation_assoc_loop eqb la lbo) = List.length la.

Theorem permutation_assoc_length : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ {la lb},
  permutation eqb la lb
  → List.length (permutation_assoc eqb la lb) = List.length la.

Theorem permutation_assoc_loop_ub : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lbo i,
  permutation eqb la (filter_Some lbo)
  → i < List.length la
  → List.nth i (permutation_assoc_loop eqb la lbo) 0 < List.length lbo.

Theorem permutation_assoc_loop_None_inside : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lbo lco,
  permutation_assoc_loop eqb la (lbo ++ None :: lco) =
  List.map (λ i, if i <? List.length lbo then i else S i)
    (permutation_assoc_loop eqb la (lbo ++ lco)).
Theorem filter_Some_app : ∀ A (l1 l2 : list (option A)),
  filter_Some (l1 ++ l2) = filter_Some l1 ++ filter_Some l2.

Theorem permutation_assoc_loop_nth_nth : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ d la lbo i j,
  permutation eqb la (filter_Some lbo)
  → i < List.length la
  → List.nth i (permutation_assoc_loop eqb la lbo) 0 = j
  → List.nth i la d = unsome d (List.nth j lbo None).

Theorem unmap_Some_app_cons : ∀ A (a : A) la lbo lco,
  List.map Some la = lbo ++ Some a :: lco
  → lbo = List.map Some (filter_Some lbo) ∧
    lco = List.map Some (filter_Some lco) ∧
    la = filter_Some lbo ++ a :: filter_Some lco.

Theorem permutation_permutation_assoc : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ {la lb},
  permutation eqb la lb
  → permutation Nat.eqb (permutation_assoc eqb la lb)
      (List.seq 0 (List.length la)).

Theorem map_permutation_assoc : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ d [la lb],
  permutation eqb la lb
  → la = List.map (λ i, List.nth i lb d) (permutation_assoc eqb la lb).

Theorem permutation_fun_nth : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ d la lb i,
  permutation eqb la lb
  → i < List.length la
  → List.nth i lb d = List.nth (permutation_fun eqb la lb i) la d.

Theorem permutation_nth : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb d,
  permutation eqb la lb
  ↔ (let n := List.length la in
     List.length lb = n ∧
     ∃ f : nat → nat,
     FinFun.bFun n f ∧
     FinFun.bInjective n f ∧
     (∀ x : nat, x < n → List.nth x lb d = List.nth (f x) la d)).
Theorem permutation_partition : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ f la lb lc,
  List.partition f la = (lb, lc)
  → permutation eqb la (lb ++ lc).
Fixpoint transp_loop {A} (eqb : A → A → bool) i la lb :=
  match lb with
  | [] ⇒ []
  | b :: lb' ⇒
      match List_extract (eqb b) la with
      | Some ([], _, la2) ⇒ transp_loop eqb (S i) la2 lb'
      | Some (a :: la1, _, la2) ⇒
          (i, S (i + List.length la1)) ::
          transp_loop eqb (S i) (la1 ++ a :: la2) lb'
      | None ⇒ []
      end
  end.

Definition transp_list {A} (eqb : A → _) la lb := transp_loop eqb 0 la lb.

Definition swap_d {A} d i j (la : list A) :=
   List.map
     (λ k, List.nth (if k =? i then j else if k =? j then i else k) la d)
     (List.seq 0 (List.length la)).

Definition swap {A} i j (la : list A) :=
  match la with
  | [] ⇒ []
  | d :: _ ⇒ swap_d d i j la
  end.

Definition apply_transp_list {A} trl (la : list A) :=
  List.fold_left (λ lb ij, swap (fst ij) (snd ij) lb) trl la.

Definition shift_transp i trl :=
  List.map (λ ij, (fst ij + i, snd ij + i)) trl.

Theorem fold_apply_transp_list : ∀ A trl (la : list A),
  List.fold_left (λ lb ij, swap (fst ij) (snd ij) lb) trl la =
  apply_transp_list trl la.

Theorem transp_loop_shift : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ i la lb,
  transp_loop eqb i la lb = shift_transp i (transp_list eqb la lb).

Theorem swap_length : ∀ A (la : list A) i j,
  List.length (swap i j la) = List.length la.

Theorem apply_transp_list_shift_1_cons : ∀ A (a : A) la trl,
  (∀ ij, ij ∈ trl → fst ij < snd ij < List.length la)
  → apply_transp_list (shift_transp 1 trl) (a :: la) =
    a :: apply_transp_list trl la.

Theorem in_transp_loop_length : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb,
  List.length la = List.length lb
  → ∀ i j k,
  (i, j) ∈ transp_loop eqb k la lb
  → i < j < k + List.length la.

Theorem in_transp_list_length : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb,
  List.length la = List.length lb
  → ∀ i j,
  (i, j) ∈ transp_list eqb la lb
  → i < j < List.length la.

Theorem permutation_transp_list : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb,
  permutation eqb la lb
  → apply_transp_list (transp_list eqb la lb) la = lb.

Theorem swap_d_inside : ∀ A (d : A) l1 l2 l3 x y,
  swap_d d (List.length l1) (S (List.length (l1 ++ l2)))
    (l1 ++ x :: l2 ++ y :: l3) =
  l1 ++ y :: l2 ++ x :: l3.

Theorem permutation_transp_inside : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ l1 l2 l3 x y,
  permutation eqb (l1 ++ y :: l2 ++ x :: l3) (l1 ++ x :: l2 ++ y :: l3).

Theorem permutation_swap_any : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ i j la,
  i < j < List.length la
  → permutation eqb (swap i j la) la.

Theorem iter_list_permut : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ T (d : T) (op : T → T → T) (l1 l2 : list A) f
  (op_d_l : ∀ x, op d x = x)
  (op_d_r : ∀ x, op x d = x)
  (op_comm : ∀ a b, op a b = op b a)
  (op_assoc : ∀ a b c, op a (op b c) = op (op a b) c),
  permutation eqb l1 l2
  → iter_list l1 (λ (c : T) i, op c (f i)) d =
    iter_list l2 (λ (c : T) i, op c (f i)) d.

Theorem incl_incl_permutation : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb,
  List.NoDup la
  → List.NoDup lb
  → la ⊂ lb
  → lb ⊂ la
  → permutation eqb la lb.
Theorem permutation_firstn : ∀ {A} {eqb : A → _} d,
  equality eqb →
  ∀ P n la lb,
  (∀ i, i < n → P (List.nth i la d) ∧ P (List.nth i lb d))
  → (∀ i,
      n ≤ i < List.length la
      → ¬ P (List.nth i la d) ∧ ¬ P (List.nth i lb d))
  → permutation eqb la lb
  → permutation eqb (List.firstn n la) (List.firstn n lb).
Theorem permutation_app_permutation_l : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ la lb lc ld,
  permutation eqb (la ++ lb) (lc ++ ld)
  → permutation eqb la lc
  → permutation eqb lb ld.

Theorem permutation_filter : ∀ {A} {eqb : A → _},
  equality eqb →
  ∀ f la lb,
  permutation eqb la lb
  → permutation eqb (List.filter f la) (List.filter f lb).