Module FormalML.utils.ListAdd

Require Import List Permutation EquivDec.
Require Import RelationClasses Morphisms.
Require Import Omega Lia Lra Rbase.
Require Import Relation_Definitions Sorted.

Require Import LibUtils BasicUtils.

Import ListNotations.

Section Map.

  Lemma removelast_map {A B : Type} (f:A->B) (l : list A) :
    removelast (map f l) = map f (removelast l).

  Lemma tl_map {A B : Type} (f:A->B) (l : list A) :
    tl (map f l) = map f (tl l).

  Lemma concat_map_swap_perm {A B C} (f:A->B->C) (l1:list A) (l2:list B) :
    Permutation (concat (map (fun x => map (fun y => f x y) l2) l1))
                (concat (map (fun x => map (fun y => f y x) l1) l2)) .
  
  Lemma map_app_interleave_perm {A B} (l:list A) (fl:list (A->B)) :
    Permutation (concat (map (fun f => map (fun x => f x) l) fl)) (concat (map (fun x => map (fun f => f x) fl) l)).

  Lemma map2_app_interleave_perm {A B} (l:list A) (f g:A->B) :
    Permutation (map f l ++ map g l) (concat (map (fun x => f x::g x::nil) l)).

End Map.

Section Fold.
  Context {A B C: Type}.

  Lemma fold_right_map
        (f:C -> A -> A) (g:B->C) (l:list B) (init:A) :
    fold_right f init (map g l) = fold_right (fun a b => f (g a) b) init l.

End Fold.

Lemma fold_right_assoc_abs {A} (f:A->A->A) (init:A) (l : list (list A))
      (assoc:forall x y z : A, f x (f y z) = f (f x y) z)
      (abs:forall x, f init x = x) :
  fold_right f init (concat l) =
  fold_right f init (map (fold_right f init) l).

Lemma fold_right_plus_concat (l : list (list R)) :
  fold_right Rplus R0 (concat l) =
  fold_right Rplus R0 (map (fold_right Rplus R0) l).

Lemma fold_right_plus_acc f acc l :
  fold_right (fun (a : nat) (b : R) => f a + b)%R acc l =
  (fold_right (fun (a : nat) (b : R) => f a + b)%R R0 l + acc)%R.

Section Seq.
  
  Lemma seq_shiftn {A:Type} (l:list A) (n:nat) :
    seq n (length l) = map (fun x => x + n)%nat (seq 0 (length l)).

  Lemma list_as_nthseq_start {A:Type} (l:list A) (d:A) (c:nat) : l = map (fun n => nth (n-c) l d) (seq c%nat (length l)).
  
  Lemma list_as_nthseq {A:Type} (l:list A) (d:A) : l = map (fun n => nth n l d) (seq 0%nat (length l)).

  Lemma seq_Sn s n : seq s (S n) = seq s n ++ [(s+n)]%nat.

  Lemma tl_seq n : tl (seq 0 n) = seq 1 (n-1).

  Lemma removelast_seq (n:nat) : removelast (seq 0 n) = seq 0 (n-1).

  Lemma seq_shiftn_map start len : seq start len = map (plus start) (seq 0 len).

End Seq.

Section fp.

  Lemma ForallOrdPairs_impl {A:Type} (R:A->A->Prop) (l:list A) (f:A->A) :
    ForallOrdPairs R l ->
    ForallOrdPairs (fun x y => R x y -> R (f x) (f y)) l ->
    ForallOrdPairs R (map f l).

  Lemma ForallPairs_all {A:Type} (R:A->A->Prop) (l:list A) :
    (forall x1 x2, R x1 x2) -> ForallPairs R l.

End fp.

Lemma nth_tl {A} idx (l:list A) d : nth idx (tl l) d = nth (S idx) l d.

Lemma nth_removelast_in {A} idx (l:list A) d :
  idx < pred (length l) ->
  nth idx (removelast l) d = nth idx l d.

Lemma nth_last {A} (l:list A) d: nth (pred (length l)) l d = last l d.

Lemma nth_hd {A} (l:list A) d: nth 0 l d = hd d l.

Lemma hd_app {A} (l1 l2:list A) d : l1 <> nil -> hd d (l1 ++ l2) = hd d l1.

Lemma last_rev {A} (l:list A) d : last l d = hd d (rev l).

Lemma last_app {A} (l1 l2:list A) d : l2 <> nil -> last (l1 ++ l2) d = last l2 d.

Lemma last_cons {A} (x:A) l y : last (x::l) y = last l x.

Lemma seq_last s n d :
  (n > 0)%nat ->
  last (seq s n) d = (s+n-1)%nat.

Lemma last_map {A B} (f:A->B) (l:list A) d : last (map f l) (f d) = f (last l d).

Lemma map_nth_in {A B} (f:A->B) l d1 n d2 :
  (n < length l)%nat ->
  nth n (map f l) d1 = f (nth n l d2).

Lemma map_nth_in_exists {A B} (f:A->B) l d1 n :
  (n < length l)%nat ->
  exists d2,
    nth n (map f l) d1 = f (nth n l d2).

Lemma nth_in_default {A} (l:list A) d1 d2 n :
  (n < length l)%nat ->
  nth n l d1 = nth n l d2.

Lemma Forall_app_iff {A} {P:A->Prop} {l1 l2} :
  Forall P (l1 ++ l2) <->
  Forall P l1 /\ Forall P l2.

Lemma StronglySorted_app_inv {A} {R:relation A} {l1 l2} :
  StronglySorted R (l1 ++ l2) ->
  StronglySorted R l1 /\ StronglySorted R l2.

Lemma StronglySorted_sub {A} (R1 R2:relation A) :
  subrelation R1 R2 ->
  forall l, StronglySorted R1 l -> StronglySorted R2 l.

Lemma StronglySorted_map_in {A B} (R1:relation A) (R2:relation B) (f:A->B) l :
  (forall x y, In x l /\ In y l -> R1 x y -> R2 (f x) (f y)) ->
  StronglySorted R1 l -> StronglySorted R2 (map f l).

Lemma StronglySorted_map {A B} (R1:relation A) (R2:relation B) (f:A->B) :
  Proper (R1 ==> R2) f ->
  forall l,
    StronglySorted R1 l -> StronglySorted R2 (map f l).

Lemma StronglySorted_compose {A B} R (f:A->B) (l:list A) :
  StronglySorted R (map f l) <->
  StronglySorted (fun x y => R (f x) (f y)) l.

Lemma StronglySorted_break {A} R (l:list A) x :
  StronglySorted R l ->
  In x l ->
  exists b c, l = b++x::c /\ Forall (fun y => R y x) b /\ Forall (R x) c.

Lemma StronglySorted_nth_lt {A} R (l:list A) idx1 idx2 d1 d2 :
  StronglySorted R l ->
  (idx2 < length l)%nat ->
  (idx1 < idx2)%nat ->
  R (nth idx1 l d1) (nth idx2 l d2).

Lemma StronglySorted_nth_le {A} R (l:list A) idx1 idx2 d1 d2 :
  reflexive _ R ->
  StronglySorted R l ->
  (idx2 < length l)%nat ->
  (idx1 <= idx2)%nat ->
  R (nth idx1 l d1) (nth idx2 l d2).

Section bucket.

  Context {A:Type} {R:relation A} (R_dec : forall x y, {R x y} + {~ R x y}).

  Fixpoint find_bucket (needle:A) (haystack:list A)
    := match haystack with
       | x::((y::_) as more) => if R_dec x needle
                                then if R_dec needle y
                                     then Some (x,y)
                                     else find_bucket needle more
                                else None
       | _ => None
       end.
  
  Lemma find_bucket_break {needle l a1 a2}:
    find_bucket needle l = Some (a1, a2) ->
    exists l1 l2,
      l = l1 ++ [a1; a2] ++ l2.

  Lemma middle_find_bucket needle l1 l2 a1 a2:
    transitive _ R ->
    antisymmetric _ R ->
    StronglySorted R (l1++[a1]) ->
    R a1 needle ->
    R needle a2 ->
    ~ R needle a1 ->
    find_bucket needle (l1 ++ a1::a2::l2) = Some (a1, a2).
  
  Lemma find_bucket_nth_finds needle l idx d1 d2:
    transitive _ R ->
    antisymmetric _ R ->
    StronglySorted R l ->
    S idx < length l ->
    R (nth idx l d1) needle ->
    R needle (nth (S idx) l d2) ->
    ~ R needle (nth idx l d1) ->
    find_bucket needle l = Some (nth idx l d1, nth (S idx) l d2).

  Lemma find_bucket_needle_in needle l a1 a2:
    find_bucket needle l = Some (a1, a2) ->
    R a1 needle /\ R needle a2.

  Lemma find_bucket_bucket_in needle l a1 a2 d1 d2:
    reflexive _ R ->
    StronglySorted R l ->
    find_bucket needle l = Some (a1, a2) ->
    R (hd d1 l) a1 /\ R a2 (last l d2).

  Lemma find_bucket_bounded_le_exists a b l (needle:A) :
    (forall x y, R x y \/ R y x) ->
    R a needle ->
    R needle b ->
    exists lower upper,
      find_bucket needle (a::l++[b]) = Some (lower, upper).

End bucket.

Lemma StronglySorted_seq s n : StronglySorted lt (seq s n).

Lemma length_S_tl {A : Type} (l : list A) :
  l <> nil ->
  length l = S (length (tl l)).

Lemma tl_length {A : Type} (l : list A) :
  length (tl l) = pred (length l).

Lemma removelast_length {A : Type} (l : list A) :
  length (removelast l) = pred (length l).

Section combining.

  Lemma combine_nth_in {A B : Type} (l : list A) (l' : list B) (n : nat) (x : A) (y : B) :
    n < min (length l) (length l') ->
    nth n (combine l l') (x, y) = (nth n l x, nth n l' y).

  Lemma combine_map {A B C D:Type} (f:A->C) (g:B->D) (l1:list A) (l2:list B) :
    combine (map f l1) (map g l2) = map (fun '(x,y) => (f x, g y)) (combine l1 l2).

  Lemma combine_self {A:Type} (l:list A) :
    combine l l = map (fun x => (x,x)) l.

  Lemma combine_nil_l {A B} (l:list B) : combine (@nil A) l = nil.

  Lemma combine_nil_r {A B} (l:list A) : combine l (@nil B) = nil.

  Lemma combine_swap {A B} (l1:list A) (l2:list B) : combine l1 l2 = map (fun xy => (snd xy, fst xy)) (combine l2 l1).

  Lemma combine_domain_eq {A B} (x:list A) (y:list B) :
    length x = length y -> domain (combine x y) = x.

  Lemma list_prod_map {A B C D:Type} (f:A->C) (g:B->D) (l1:list A) (l2:list B) :
    list_prod (map f l1) (map g l2) = map (fun '(x,y) => (f x, g y)) (list_prod l1 l2).

  Lemma list_prod_nil_l {A B} (l:list B) : list_prod (@nil A) l = nil.

  Lemma list_prod_nil_r {A B} (l:list A) : list_prod l (@nil B) = nil.

  Lemma list_prod_cons2_pred {A B} (l1:list A) a (l2:list B) :
    Permutation (list_prod l1 (a :: l2)) (map (fun x : A => (x, a)) l1 ++ list_prod l1 l2).

  Lemma list_prod_swap {A B} (l1:list A) (l2:list B) : Permutation (list_prod l1 l2) (map (fun xy => (snd xy, fst xy)) (list_prod l2 l1)).

  Instance list_prod_perm_proper1 {A B} : Proper ((@Permutation A) ==> eq ==> (@Permutation (A*B))) (@list_prod A B).

  Global Instance list_prod_perm_proper {A B} : Proper ((@Permutation A) ==> (@Permutation B) ==> (@Permutation (A*B))) (@list_prod A B).

  Lemma combine_incl_list_prod {A B} (l1:list A) (l2:list B) : incl (combine l1 l2) (list_prod l1 l2).

End combining.

Definition adjacent_pairs {A:Type} (l:list A) := (combine l (tl l)).

Definition adjacent_pairs_alt {A:Type} (l:list A) := (combine (removelast l) (tl l)).

Lemma adjacent_pairs_alt_eq {A:Type} (l:list A) :
  adjacent_pairs l = adjacent_pairs_alt l.

Lemma adjacent_pairs_length {A:Type} (l:list A) : length (adjacent_pairs l) = pred (length l).

Lemma adjacent_pairs_nth_in {A:Type} n (l:list A) d1 d2 :
  S n < length l ->
  nth n (adjacent_pairs l) (d1,d2) = (nth n l d1, nth (S n) l d2).

Lemma adjacent_pairs_map {A B:Type} (f:A->B) (l:list A) :
  adjacent_pairs (map f l) = map (fun '(x,y) => (f x, f y)) (adjacent_pairs l).

Lemma adjacent_pairs_seq s n :
  adjacent_pairs (seq s n) = map (fun i => (i, S i)) (seq s (pred n)).

Section folds_with_history.

  
  Definition fold_left_with_history_aux {A B : Type} (f:A -> B -> A) (l:list B) (init:A) (acc:list A) : list A
    := rev (let '(x,y) := (fold_left (fun '(a,hs) b => (f a b, a::hs)) l (init, acc)) in
            x::y).

  Definition fold_left_with_history {A B : Type} (f:A -> B -> A) (l:list B) (init:A) : list A
    := fold_left_with_history_aux f l init nil.

  Lemma fold_left_with_history_aux_len {A B : Type} (f:A -> B -> A) (l:list B) (init:A) (acc:list A) :
    (List.length (fold_left_with_history_aux f l init acc) = S (length l) + length acc)%nat.
  
  Lemma fold_left_with_history_len {A B : Type} (f:A -> B -> A) (l:list B) (init:A) :
    List.length (fold_left_with_history f l init) = S (length l).

  Fixpoint fold_left_partial_with_history_aux {A B : Type} (f : A -> B -> option A) (l:list B) (acc:A*list A) : list A + list A
    := match l with
       | [] => inl (rev (fst acc :: snd acc))
       | b :: t =>
         match f (fst acc) b with
         | None => inr (rev (fst acc :: snd acc))
         | Some a' =>
           fold_left_partial_with_history_aux f t (a', fst acc::snd acc)
         end
       end.

  Definition fold_left_partial_with_history {A B : Type} (f : A -> B -> option A) (l:list B) (init:A) : list A + list A
    := fold_left_partial_with_history_aux f l (init,nil).
  
  Lemma fold_left_partial_with_history_aux_ok {A B : Type} (f : A -> B -> option A) (l:list B) (init:A) (acc:list A) l' :
    fold_left_partial_with_history_aux f l (init,acc) = inl l' ->
    (List.length l' = S (length l) + length acc)%nat.
  
  Lemma fold_left_partial_with_history_ok {A B : Type} (f : A -> B -> option A) (l:list B) (init:A) l' :
    fold_left_partial_with_history f l init = inl l' ->
    List.length l' = S (length l).

  Lemma fold_left_partial_with_history_aux_err {A B : Type} (f : A -> B -> option A) (l:list B) (init:A) (acc:list A) l' :
    fold_left_partial_with_history_aux f l (init,acc) = inr l' ->
    (List.length l' < S (length l) + length acc)%nat.

  Lemma fold_left_partial_with_history_aux_total {A B : Type}
        (f : A -> B -> A) (l:list B) (init:A) (acc:list A) :
    fold_left_partial_with_history_aux (fun a b => Some (f a b)) l (init,acc) =
    inl (fold_left_with_history_aux f l init acc).


  Lemma fold_left_partial_with_history_total {A B : Type} (f : A -> B -> A) (l:list B) (init:A) :
    fold_left_partial_with_history (fun a b => Some (f a b)) l init = inl (fold_left_with_history f l init).
End folds_with_history.

Lemma nodup_not_nil (T : Type) (l : list T) (dec:forall (x y:T), {x = y} + {x <> y}) :
  l <> nil <-> nodup dec l <> nil.

Lemma map_in_inj_strong {A B} (f:A->B) a (l:list A) :
  (forall a b, In (f a) (map f l) -> In (f b) (map f l) -> f a = f b -> a = b) ->
  In (f a) (map f l) -> In a l.

Lemma nodup_map_inj {A B} decA decB (f:A->B) (l:list A) :
  (forall a b, In (f a) (map f l) -> In (f b) (map f l) -> f a = f b -> a = b) ->
  nodup decB (map f l) = map f (nodup decA l).

Lemma list_prod_concat {A B} (l1:list A) (l2:list B) : list_prod l1 l2 = concat (map (fun x => map (fun y => (x, y)) l2) l1).

Lemma nodup_const_map {A} (c r:A) dec (l : list A) :
  [c] = nodup dec (map (fun _ => c) (r :: l)).

Lemma concat_NoDup {A} (l:list (list A)) : NoDup (concat l) -> Forall (@NoDup A) l.

Lemma nodup_app2_incl {A} decA (l1 l2:list A) :
  incl l1 l2 ->
  nodup decA (l1 ++ l2) = nodup decA l2.

Lemma nodup_app_distr {A} decA (l1 l2:list A) :
  disjoint l1 l2 ->
  nodup decA (l1 ++ l2) = nodup decA l1 ++ nodup decA l2.

Lemma list_prod_nodup {A B} decA decB decAB (l1:list A) (l2:list B):
  nodup decAB (list_prod l1 l2) = list_prod (nodup decA l1) (nodup decB l2).

Lemma nodup_map_nodup {A B} decA decB (f:A->B) (l:list A) :
  nodup decB (map f (nodup decA l)) = nodup decB (map f l).


Lemma nodup_equiv {A} dec (l:list A) : equivlist (nodup dec l) l.

Lemma incl_nil_r {A} (l:list A) : incl l nil -> l = nil.

Lemma remove_one_nin {A} {dec:EqDec A eq} a (l:list A) :
  ~ In a l ->
  remove_one a l = l.

Lemma remove_one_app_nin {A} {dec:EqDec A eq} a (l1 l2:list A) :
  ~ In a l1 ->
  remove_one a (l1 ++ l2) = l1 ++ remove_one a l2.

Lemma remove_one_in_perm {A} {dec : EqDec A eq} (a:A) l :
  In a l ->
  Permutation l (a::remove_one a l).

Lemma remove_other_in {A} {dec : EqDec A eq} (a1 a2:A) l :
  a1 <> a2 ->
  In a1 l <-> In a1 (remove_one a2 l).

Lemma bminus_in_nin {A} {decA:EqDec A eq} a (l1 l2 : list A) :
  In a l1 -> ~ In a l2 -> In a (bminus l2 l1).

Lemma incl_front_perm {A} {decA:EqDec A eq} (l1 l2 : list A) :
  incl l2 l1 ->
  NoDup l2 ->
  {l3: list A |
    Permutation l1 (l2 ++ l3)}.

Instance equivlist_incl_part {A} : PartialOrder equivlist (@incl A).

Lemma NoDup_app_disj {A} (a b : list A) : NoDup (a ++ b) -> disjoint a b.

Lemma NoDup_perm_disj {A} (l1 l2 l3 : list A) :
  Permutation l1 (l2 ++ l3) ->
  NoDup l1 ->
  disjoint l2 l3.

Lemma incl_front_perm_nodup {A} (decA:EqDec A eq) (l1 l2 : list A) :
  incl l2 l1 ->
  {l3: list A |
    Permutation (nodup decA l1) (nodup decA l2 ++ l3)}.

Lemma Forallt_in {A} (decA:forall x y:A, {x=y} + {x <> y}) {X:A->Type} {l:list A} (ft:Forallt X l) {a} (pf:In a l) : X a.

Fixpoint Forallt_map {A B:Type} {X:A->Type} {l:list A} (f:forall a, X a -> B) (ft:Forallt X l) : list B
  := match ft with
     | Forallt_nil _ => nil
     | Forallt_cons _ x l px pl => f x px :: Forallt_map f pl
     end.

Lemma map_nil' {A B} (f:A->B) l :
  List.map f l = nil <-> l = nil.

Lemma map_nil {A B} (f : A -> B) (l : list A) :
  List.map f l = (@nil B) <-> l = (@nil A).

Lemma map_not_nil {A B} (l : list A) (f : A -> B):
  [] <> List.map f l <-> [] <> l.


Lemma not_nil_exists {A} (l : list A) :
  [] <> l <-> exists a, In a l.

Lemma list_prod_not_nil {A B} {la : list A} {lb : list B}(Hla : [] <> la) (Hlb : [] <> lb) :
  [] <> list_prod la lb.

Fixpoint applyn {A} (init : A) (g : A -> A) (n : nat) : A :=
  match n with
  | 0 => init
  | S k => g (applyn init g k)
  end.


Lemma concat_map_map {A} (l : list(list A)) (f : A -> R) :
  concat (map (map f) l) = map f (concat l).

Lemma ForallPairs_filter {A} R (l : list A) (p : A -> bool) :
  ForallPairs R l -> ForallPairs R (filter p l).

Lemma ForallOrdPairs_filter {A} R (l : list A) (p : A -> bool) :
  ForallOrdPairs R l -> ForallOrdPairs R (filter p l).

Lemma ForallOrdPairs_app_in {A R} {l1 l2:list A} : ForallOrdPairs R (l1 ++ l2) ->
                                                   forall x y, In x l1 -> In y l2 -> R x y.

Lemma filter_true {A} : forall p:list A, filter (fun _ => true) p = p.

Lemma filter_false {A} : forall p:list A, filter (fun _ => false) p = [].

Lemma Forall2_refl_in {A} R (l:list A) :
  Forall (fun x => R x x) l ->
  Forall2 R l l.

Lemma Forall2_perm {A} R (l1 l1' l2:list A) :
  Forall2 R l1 l2 ->
  Permutation l1 l1' ->
  exists l2', Permutation l2 l2' /\
         Forall2 R l1' l2'.


Global Instance ForallPairs_sublist {A} {R} : Proper (sublist --> Basics.impl) (@ForallPairs A R).

Lemma Forall2_map_rel {A B} (R:A->A->Prop) l1 l2 (f:A->B) :
  (forall x1 x2, In x1 l1 -> In x2 l2 -> R x1 x2 -> f x1 = f x2) ->
  Forall2 R l1 l2 ->
  map f l1 = map f l2.


Section equivlist.

Global Instance app_equivlist_proper {A} : Proper (equivlist ==> equivlist ==> equivlist) (@app A).

Lemma equivlist_const {A B} (b:B) (l:list A) :
  l <> nil ->
  equivlist (map (fun _ => b) l) (b::nil).
            
Lemma list_prod_fst_equiv {A B} (a:list A) (b:list B) : b <> nil -> equivlist (map fst (list_prod a b)) a.

Lemma list_prod_snd_equiv {A B} (a:list A) (b:list B) : a <> nil -> equivlist (map snd (list_prod a b)) b.


Global Instance list_prod_equivlist {A B} :
  Proper (equivlist ==> equivlist ==> equivlist) (@list_prod A B).

Global Instance map_equivlist_proper {A B}: Proper (pointwise_relation _ eq ==> equivlist ==> equivlist) (@map A B).
 
End equivlist.