(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basics/lists/list.ma".
include "basics/relations.ma".

inductive permutation (A : Type[0]) : relation (list A) ≝
| perm_nil : permutation A [ ] [ ]
| perm_skip : ∀x, l1, l2. permutation A l1 l2 → permutation A (x :: l1) (x :: l2)
| perm_swap : ∀x, y, l. permutation A (x :: y :: l) (y :: x :: l)
| perm_trans : transitive ? (permutation A).

interpretation "list permutation" 'napart l1 l2 = (permutation ? l1 l2).

lemma perm_refl : ∀A.reflexive ? (permutation A).
#A #l elim l /2/ qed.

lemma perm_symm : ∀A.symmetric ? (permutation A).
#A #l #m #H elim H /2 by perm_nil, perm_skip, perm_swap, perm_trans/
qed.

lemma perm_nil_eq_nil : ∀A.∀l : list A.[ ] ≈ l → l = [ ].
#A #l lapply (refl (list A) [ ])
generalize in match [ ] in ⊢ (??%?→%); #m #EQ #H lapply EQ -EQ elim H
[ //
| #x #l1 #l2 #H #IH #EQ destruct
| #x #y #l #EQ destruct
| #l1 #l2 #l3 #H1 #H2 #IH1 #IH2 #EQ1 lapply (IH1 EQ1) #EQ2 destruct /2/
]
qed.

lemma perm_nil_cons : ∀A,x.∀l : list A.¬ [ ] ≈ x :: l.
#A #x #l % #H lapply (perm_nil_eq_nil … H) #ABS destruct qed.

lemma perm_append_r : ∀A.∀l,m1,m2 : list A.m1 ≈ m2 → l @ m1 ≈ l @ m2.
#A #l elim l /3 by perm_skip/ qed.

lemma perm_append : ∀A.∀l1,l2,m1,m2 : list A.l1 ≈ l2 → m1 ≈ m2 → l1 @ m1 ≈ l2 @ m2.
#A #l1 #l2 #m1 #m2 #H lapply m2 lapply m1 -m1 -m2
elim H
[ //
| /3 by perm_skip/
| /3 by perm_swap, perm_trans, perm_append_r/
| #l1' #l2' #l3' #H1 #H2 #IH1 #IH2 #m #n #G %4{(l2'@m)}
  [ @IH1 @perm_refl
  | @IH2 @G
  ]
]
qed.

lemma perm_append_l : ∀A.∀l1, l2, m : list A. l1 ≈ l2 → l1 @ m ≈ l2 @ m.
/2 by perm_append/ qed.

lemma perm_move_hd : ∀A,x.∀pre, post : list A. x :: pre @ post ≈ pre @ x :: post.
#A #x #pre lapply x -x elim pre
[ //
| #hd #tl #IH #x #post
  %4{(hd :: x :: tl @ post) (perm_swap …)} @perm_skip @IH
]
qed.

lemma perm_swap_inside : ∀A.∀x,y.∀pre, mid, post : list A.
  pre @ x :: mid @ y :: post ≈ pre @ y :: mid @ x :: post.
#A #x #y #pre #mid #post @perm_append_r
%4{(mid @ x :: y :: post) (perm_move_hd …)}
%4{(mid @ y :: x :: post)} /2 by perm_swap, perm_symm, perm_append_r/
qed.

lemma perm_swap_append : ∀A.∀l1, l2 : list A. l1 @ l2 ≈ l2 @ l1.
#A #l1 elim l1
[ #l2 >append_nil @perm_refl
| #hd #tl #IH #l2
  %4{(hd :: l2 @ tl)} /2 by perm_skip/
]
qed.

lemma perm_All : ∀A,P,l1,l2.All A P l1 → l1 ≈ l2 → All A P l2.
#A #P #l1 #l2 #H #G lapply H -H elim G -G
[ *%
| #x #l1' #l2' #G #IH * #Px #Pl1' %{Px} @IH @Pl1'
| #x #y #l * #Px * #Py #Pl %{Py} %{Px Pl}
| #l1' #l2' #l3' #H1 #H2 #IH1 #IH2 /3/
]
qed.

lemma perm_Exists : ∀A,P,l1,l2.Exists A P l1 → l1 ≈ l2 → Exists A P l2.
#A #P #l1 #l2 #H #G lapply H -H elim G -G
[ *
| #x #l1' #l2' #G #IH * [#Px %1{Px} | #Pl %2 @IH @Pl]
| #x #y #l * [#Px %2 %1{Px} | * [#Py %1{Py} | #Pl %2 %2{Pl}]]
| #l1' #l2' #l3' #H1 #H2 #IH1 #IH2 /3 by /
]
qed.

lemma perm_length : ∀A.∀l1, l2 : list A. l1 ≈ l2 → |l1| = |l2|.
#A #l1 #l2 #H elim H -H normalize //
qed.

lemma perm_singleton_eq : ∀A,x.∀l : list A.[x] ≈ l → l = [x].
#A #x #l lapply (refl ? ([x]))
generalize in match ([x]) in ⊢ (??%?→%);
#m #EQ #H lapply EQ -EQ lapply x -x elim H
[ #x #EQ destruct
| #x #l1 #l2 #G #IH #y #EQ destruct >(perm_nil_eq_nil … G) %
| #x #y #l' #z #EQ destruct
| #l1 #l2 #l3 #H1 #H2 #IH1 #IH2 #x #K lapply (IH1 ? K) >K #EQ >(IH2 ? EQ) @EQ
]
qed.

lemma perm_map : ∀A,B,f,m,l.m ≈ l → map A B f m ≈ map A B f l.
#A #B #f #m #l #H elim H -H /2 by perm_skip, perm_swap, perm_trans/
qed.

lemma perm_filter : ∀A,f,m,l.m ≈ l → filter A f m ≈ filter A f l.
#A #f #m #l #H elim H -H [1,4: /2 by perm_trans/]
[ #x #l' #m' #H #IH normalize elim (f x) normalize /2 by perm_skip/
| #x #y #l' normalize elim (f y) elim (f x) normalize //
]
qed.

lemma perm_reverse : ∀A.∀l : list A.l ≈ reverse A l.
#A #l elim l [//]
#hd #tl normalize >rev_append_def >append_nil #IH >rev_append_def
%4{(tl @ [hd])}
[ <(append_nil ? tl) in ⊢(??%?); @perm_move_hd
| @perm_append_l @IH
]
qed.

lemma permutation_ind_bis : ∀A.∀P : relation (list A).
  (P [ ] [ ]) →
  (∀x,l,l'.l ≈ l' → P l l' → P (x :: l) (x :: l')) →
  (∀x,y,l,l'.l ≈ l' → P l l' → P (x :: y :: l) (y :: x :: l')) →
  (∀l,l',l''.l ≈ l' → P l l' → l' ≈ l'' → P l' l'' → P l l'') →
  ∀l,l'.l ≈ l' → P l l'.
#A #P #H1 #H2 #H3 #H4 #l #l' #H elim H /2/
[2: #l1 #l2 #l3 #G1 #G2 #G3 #G4 @(H4 … G1 G3 G2 G4)]
#x #y #l1 @H3 //
elim l1 [@H1] #hd #tl #Ptl @H2 //
qed.

lemma Exists_split : ∀A,P,l.Exists A P l → ∃x,pre,post.l = pre @ x :: post ∧ P x.
#A #P #l elim l [2: #hd #tl #IH] *
[ #Phd %{hd} %{[]} %{tl} /2 by conj/
| #Ptl elim (IH Ptl) #x * #pre * #post
  * #EQ #Px
  %{x} %{(hd :: pre)} %{post} >EQ /2 by conj/
]
qed.

lemma perm_middle_inv : ∀A.∀x.∀l1,l2,m1,m2 : list A.
  l1 @ x :: l2 ≈ m1 @ x :: m2 → l1 @ l2 ≈ m1 @ m2.
#A #x #l1 #l2 #m1 #m2
lapply (refl … (l1 @ x :: l2))
generalize in match (l1 @ x :: l2) in ⊢ (??%?→%);
lapply (refl … (m1 @ x :: m2))
generalize in match (m1 @ x :: m2) in ⊢ (??%?→%);
#l #EQl #m #EQm #H
lapply EQm -EQm lapply EQl -EQl
lapply m2 -m2 lapply m1 -m1 lapply l2 -l2 lapply l1 -l1
lapply x -x
@(permutation_ind_bis … H) -H
[ #x #l1 #l2 #m1 #m2 #H elim (nil_to_nil … (sym_eq ??? H)) #_ #ABS destruct
| #hd #tl1 #tl2 #H #IH #x
  * [2: #hdl1 #tll1] #l2
  * [2,4: #hdm1 #tlm1] #m2 normalize
  #EQ1 #EQ2 destruct
  [ %2 @(IH … (refl …) (refl …))
  | %4{H} @perm_symm @perm_move_hd
  | %4{(perm_move_hd …) H}
  | @H
  ]
| #hd1 #hd2 #tl1 #tl2 #H #IH #x
  * [2: #hdl1 * [2: #hdl1' #tll1]] #l2
  * [2,4,6: #hdm1 * [2,4,6: #hdm1' #tlm1 ]] #m2 normalize
  #EQ1 #EQ2 destruct
  [ %4{? (perm_swap …)} %2 %2 @(IH … (refl …)(refl …))
  | %4{? (perm_skip … H)}
    %4{? (perm_skip …) (perm_swap …)} @perm_symm @perm_move_hd
  | %2 %4{? H} @perm_symm @perm_move_hd
  | %4{?? (perm_skip … H)} change with (? :: (? :: ?) @ ? ≈ (? :: ?) @ ? :: ?)
    @perm_move_hd
  | %2{H}
  | %2{H}
  | %2 %4{?? H} @perm_move_hd
  | %2{H}
  | %2{H}
  ]
| #l1' #l2' #l3' #H1 #IH1 #H2 #IH2 #x #l1 #l2 #m1 #m2 #G2 #G1
  cut (Exists ? (eq ? x) l2')
  [ @(perm_Exists … H1) >G1 @Exists_mid %] #x_in_l2'
  elim (Exists_split … x_in_l2') #y * #pre * #post * #EQ #EQ' destruct(EQ')
  %4{? (IH1 … EQ G1) (IH2 … G2 EQ)}
]
qed.

lemma perm_split : ∀A,x.∀pre,post,l : list A.pre@x :: post ≈ l →
  ∃pre',post'.l = pre' @ x :: post' ∧ pre @ post ≈ pre' @ post'.
#A #x #pre #post #l #H
cut (Exists ? (eq ? x) l)
[ @(perm_Exists … H) /2 by Exists_mid/ ] #G
elim (Exists_split … G) -G #y * #pre' * #post' * #EQ #EQ' destruct(EQ')
%{pre'} %{post'} %{EQ}
>EQ in H; @perm_middle_inv
qed.

lemma perm_cons_inv : ∀A.∀x.∀l1,l2 : list A.x :: l1 ≈ x :: l2 → l1 ≈ l2.
#A #x #l1 #l2 change with ([ ] @ ? ≈ [ ] @ ? → ?) #H
@(perm_middle_inv … H)
qed.

lemma perm_cons_split : ∀A.∀x.∀l1,l2 : list A.x :: l1 ≈ l2 →
  ∃pre,post.l2 = pre @ x :: post ∧ l1 ≈ pre @ post.
#A #x #l1 #l2 change with ([ ] @ ? ≈ ? → ?) @perm_split qed.

lemma map_append_inv : ∀A,B,f,l,m1,m2.map A B f l = m1 @ m2 →
  ∃l1,l2.map … f l1 = m1 ∧ map … f l2 = m2 ∧ l = l1 @ l2.
#A #B #f #l elim l
[ #y #m normalize #H @(nil_append_elim … (sym_eq … H)) %{[]} %{[]} %%%
| #hd #tl #IH * [ * [2: #hd' #tl' ] | #hd' #tl' #m2] normalize #EQ destruct
  [ %{[]} % [2: %%% |]
  | elim (IH … e0) #m1' * #m2' ** #H1 #H2 #H3 destruct
    change with ((? :: ?) @ ?) in match (? :: ? @ ?);
    % [2: % [2: %%% ]|]
  ]
]
qed.

lemma injective_map_perm : ∀A,B,f,m,l.injective ?? f → map A B f m ≈ map A B f l → m ≈ l.
#A #B #f #m elim m
[ #l #H normalize cases l [//] #hd #tl #G
  lapply (perm_nil_eq_nil … G) normalize #ABS destruct
| #hd #tl #IH #l #H normalize #G
  elim (perm_cons_split ???? G) #pre * #post * #EQ #K
  elim(map_append_inv … EQ) #pre' ** normalize [2: #hd' #tl']
  ** #EQ1 #EQ2 #EQ3 destruct
  lapply (H … e0) #EQ' destruct
  %4{(perm_move_hd …)} %2 @(IH … H) <map_append @K
]
qed.
   
lemma perm_append_l_inv : ∀A.∀l,m1,m2 : list A.
  l @ m1 ≈ l @ m2 → m1 ≈ m2.
#A #l elim l
[ //
| #hd #tl #IH normalize #m1 #m2 #H @IH @(perm_cons_inv … H)
]
qed.

lemma perm_append_r_inv : ∀A.∀l1,l2,m : list A.
  l1 @ m ≈ l2 @ m → l1 ≈ l2.
#A #l1 #l2 #m #H
@(perm_append_l_inv ? m)
%4{(perm_swap_append …)} %4{H} @perm_swap_append
qed.

lemma perm_cons_append_inv : ∀A,a.∀l,m1,m2 : list A.
  a :: l ≈ m1 @ a :: m2 → l ≈ m1 @ m2.
#A #a #l #m1 #m2 change with ([ ] @ ? ≈ ? → ?) @perm_middle_inv
qed.

lemma perm_singletons : ∀A.∀x,y : A.[x]≈[y] → x = y.
#A #x #y #H cut (Exists ? (eq ? x) [y])
[ @(perm_Exists … H) %1 % ] * // *
qed.

lemma perm_pair_inv : ∀A.∀x,y.∀l : list A.[x;y] ≈ l → l = [x;y] ∨ l = [y;x].
#A #x #y #l change with ([ ] @ x :: ? ≈ l → ?) #H
elim (perm_split ????? H) #pre * #post * #EQ #G
>EQ in H; #H lapply (perm_middle_inv ?????? H) normalize
<EQ #K 
lapply (perm_singleton_eq ??? K) cases pre in EQ ⊢ %; [2: #hd #tl]
normalize #EQ1 #EQ2 destruct [2: %1 %]
@(nil_append_elim … e0) normalize %2 %
qed.

lemma perm_pairs : ∀A.∀x,y,z,w : A.[x;y]≈[z;w] →
  (x = z ∧ y = w) ∨ (x = w ∧ y = z).
#A #x #y #z #w #H elim (perm_pair_inv ???? H) #EQ destruct /3 by or_introl, or_intror, conj/
qed.
 
(* include for AC ops *)
include "arithmetics/bigops.ma".

lemma fold_permute : ∀A,B.∀nil.∀op : ACop B nil.∀p,f.∀l,m : list A.
  l ≈ m → \fold[op,nil]_{i ∈ l | p i} (f i) = \fold[op, nil]_{i ∈ m | p i} (f i).
#A #B #nil #op #p #f #l #m #H elim H -H
[ //
| #x #l1 #l2 #H #IH normalize >IH %
| #x #y #l' normalize cases (p x) cases (p y) normalize [1: |*: // ]
  >assoc >assoc >comm in ⊢ (??(????%?)?); %
| //
]
qed.