Module RList

Section RList.
  Require Import List ListSet.
  Require Import Bool.

  Require Import RUtil.

  Require Import Permutation.
  Require Import Equivalence.
  Require Import Morphisms.
  Require Import Setoid.
  Require Import EquivDec.
  Require Import RelationClasses.
  Require Import Omega.

  Section misc.
    Context {A:Type}.

    Definition singleton {A} (x:A) : list A := x::nil.
    
    Lemma is_nil_dec (l:list A) : {l = nil} + {l <> nil}.

    Fixpoint lflatten (l:list (list A)) : list A :=
      match l with
      | nil => nil
      | l1 :: l' =>
        l1 ++ (lflatten l')
      end.

    Lemma flat_map_app {B} (f:A->list B) l1 l2 :
      flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2.
    
    Lemma map_nil f l :
      map f l = (@nil A) <-> l = (@nil A).
    
    Lemma eq_means_same_length :
      forall (l1 l2:list A),
        l1 = l2 -> (length l1) = (length l2).

    Lemma app_cons_middle (l1 l2:list A) (a:A) :
      l1 ++ (a::l2) = (l1 ++ (a::nil))++l2.

  End misc.

  Lemma map_app_break {A B:Type} (f:A->B) {a b c} :
    map f a = b ++ c ->
    {b':list A & {c' : list A | a = b' ++ c' /\ b = map f b' /\ c = map f c'}}.

  Lemma map_inj_strong {A B} (f g:A->B) (l1 l2:list A)
        (inj:forall (x y:A), In (f x) (map f l1) -> In (g y) (map g l2) -> f x = g y -> x = y) :
    map f l1 = map g l2 ->
    l1 = l2.
  
  Lemma map_inj {A B} (f g:A->B) (l1 l2:list A)
        (inj:forall (x y:A), f x = g y -> x = y) :
    map f l1 = map g l2 ->
    l1 = l2.
  
  Section folds.
    Context {A B C: Type}.
    
    Lemma fold_left_map
          (f:A -> C -> A) (g:B->C) (l:list B) (init:A) :
      fold_left f (map g l) init = fold_left (fun a b => f a (g b)) l init.

    Lemma fold_left_ext
          (f g:A -> B -> A) (l:list B) (init:A) :
      (forall x y, f x y = g x y) ->
      fold_left f l init = fold_left g l init.

    Lemma fold_right_app_map_singleton l :
    fold_right (fun a b : list A => a ++ b) nil
              (map (fun x : A => (x::nil)) l) = l.

  Lemma fold_right_perm (f : A -> A -> A)
        (assoc:forall x y z : A, f x (f y z) = f (f x y) z)
        (comm:forall x y : A, f x y = f y x) (l1 l2:list A) (unit:A)
        (perm:Permutation l1 l2) :
    fold_right f unit l1 = fold_right f unit l2.

  End folds.

  Section Forall.
    Context {A:Type}.

    Lemma Forall_dec_defined {P} :
      (forall x:A, {P x} + { ~ P x }) ->
      forall l:list A, {Forall P l} + {~ Forall P l}.

  End Forall.
  
  Section filter.
    Context {A:Type}.

    Lemma filter_length :
      forall (p:A -> bool), forall (l:list A),
          length l >= length (filter p l).

    Lemma filter_smaller :
      forall (p:A -> bool), forall (l:list A), forall (x:A),
            filter p l <> x::l.

    Lemma filter_filter :
      forall (p:A -> bool), forall (s:list A),
          filter p (filter p s) = filter p s.

    Lemma filter_not_filter:
      forall (p:A -> bool), forall (s:list A),
            filter p (filter (fun x => negb (p x)) s) = nil.

    Lemma filter_id_implies_pred :
      forall (p:A -> bool), forall (l:list A),
          filter p l = l -> forall (y:A), (In y l -> (p y = true)).

    Lemma filter_nil_implies_not_pred :
      forall (p:A -> bool), forall (l:list A),
          filter p l = nil -> forall (y:A), (In y l -> (p y = false)).

    Lemma filter_comm:
      forall (x:list A) (p1 p2: A -> bool),
        (filter p1 (filter p2 x)) = (filter p2 (filter p1 x)).

    Lemma filter_and:
      forall (x:list A) (p1 p2: A -> bool),
        (filter p1 (filter p2 x)) = (filter (fun a => andb (p1 a) (p2 a)) x).

    Lemma filter_eq:
      forall (p1 p2:A -> bool),
        (forall x:A, p1 x = p2 x) -> (forall l:list A, filter p1 l = filter p2 l).

    Lemma false_filter_nil {f} {l:list A} :
      (forall x, In x l -> f x = false) -> filter f l = nil.

    Lemma filter_app (f:A->bool) l1 l2 :
      filter f (l1 ++ l2) = filter f l1 ++ filter f l2.

    Lemma Forall_filter {P} {l:list A} f :
      Forall P l -> Forall P (filter f l).
  
    Lemma find_filter f (l:list A) : find f l = hd_error (filter f l).

    Lemma filter_ext (f g : A -> bool) (l : list A) :
      (forall x, In x l -> f x = g x) ->
      filter f l = filter g l.

    Lemma true_filter (f : A -> bool) (l : list A) :
      (forall x : A, In x l -> f x = true) -> filter f l = l.

  End filter.

  
        Lemma forall_in_dec {A:Type} P (l:list A)
          (dec:forall x, In x l -> {P x} + {~ P x}):
      {forall x, In x l -> P x} + {~ forall x, In x l -> P x}.

    Lemma exists_in_dec {A:Type} P (l:list A)
          (dec:forall x, In x l -> {P x} + {~ P x}):
      {exists x, In x l /\ P x} + {~ exists x, In x l /\ P x}.

    Lemma exists_nforall_in_dec {A:Type} P (l:list A)
          (dec:forall x, In x l -> {P x} + {~ P x}):
      {exists x, In x l /\ P x} + {forall x, In x l -> ~P x}.

      Lemma existsb_ex {A : Type} (f : A -> bool) (l : list A) :
       existsb f l = true -> {x : A | In x l /\ f x = true}.


  Section perm_equiv.
    Context {A:Type}.
    Context {eqdec:EqDec A eq}.

    Definition ldeqA := (@Permutation A).

    Definition rbag := list A.

    Global Instance perm_equiv : Equivalence (@Permutation A).
  End perm_equiv.
    
  Section list2.
    Context {A B:Type}.

    Section fb2.
      Context (f:A->B->bool).
      Fixpoint forallb2 (l1:list A) (l2:list B): bool :=
        match l1,l2 with
          | nil, nil => true
          | a1::l1, a2::l2 => f a1 a2 && forallb2 l1 l2
          | _, _ => false
        end.

      Lemma forallb2_forallb : forall (l1:list A) (l2:list B),
                                 (length l1 = length l2) ->
                                 forallb (fun xy => f (fst xy) (snd xy)) (combine l1 l2) = forallb2 l1 l2.

      Lemma forallb2_forallb_true : forall (l1:list A) (l2:list B),
                                      (length l1 = length l2 /\ forallb (fun xy => f (fst xy) (snd xy)) (combine l1 l2) = true)
                                      <->
                                      forallb2 l1 l2 = true.

      Lemma forallb2_Forallb : forall l1 l2, forallb2 l1 l2 = true <-> Forall2 (fun x y => f x y = true) l1 l2.

    End fb2.
  
    Lemma Forall2_incl : forall (f1 f2:A->B->Prop) l1 l2,
                           (forall x y, In x l1 -> In y l2 -> f1 x y-> f2 x y) ->
                           Forall2 f1 l1 l2 -> Forall2 f2 l1 l2.

    Lemma forallb2_eq : forall (f1 f2:A->B->bool) l1 l2,
                          (forall x y, In x l1 -> In y l2 -> f1 x y = f2 x y) ->
                          forallb2 f1 l1 l2 = forallb2 f2 l1 l2.

  End list2.

  Section forall2.
  
    Lemma forallb2_sym {A B} : forall (f:A->B->bool) {l1 l2},
      forallb2 f l1 l2 = forallb2 (fun x y => f y x) l2 l1.

    Lemma Forall2_map {A B C D} (f:C->D->Prop) (g:A->C) (h:B->D) a b:
      Forall2 (fun x y => f (g x) (h y)) a b <-> Forall2 f (map g a) (map h b).

    Lemma Forall2_map_f {A B C D} (f:C->D->Prop) (g:A->C) (h:B->D) a b:
      Forall2 (fun x y => f (g x) (h y)) a b -> Forall2 f (map g a) (map h b).

    Lemma Forall2_map_b {A B C D} (f:C->D->Prop) (g:A->C) (h:B->D) a b:
      Forall2 f (map g a) (map h b) -> Forall2 (fun x y => f (g x) (h y)) a b.

    Lemma Forall2_length {A B} (f:A->B->Prop) a b:
      Forall2 f a b -> length a = length b.

    Global Instance Forall2_refl {A} R `{Reflexive A R} : Reflexive (Forall2 R).

    Global Instance Forall2_sym {A} R `{Symmetric A R} : Symmetric (Forall2 R).

    Global Instance Forall2_trans {A} R `{Transitive A R} : Transitive (Forall2 R).

  Global Instance Forall2_pre {A} R `{PreOrder A R} : PreOrder (Forall2 R).

  Global Instance Forall2_part_eq {A} R `{PartialOrder A eq R } :
    PartialOrder eq (Forall2 R).
  
  Lemma Forall2_trans_relations_weak {A B C}
        (R1:A->B->Prop) (R2:B->C->Prop) (R3:A->C->Prop):
    (forall a b c, R1 a b -> R2 b c -> R3 a c) ->
    forall a b c, Forall2 R1 a b -> Forall2 R2 b c -> Forall2 R3 a c.

    Lemma Forall2_eq {A} (l1 l2:list A): Forall2 eq l1 l2 <-> l1 = l2.

    Lemma Forall2_flip {A B} {P:A->B->Prop} {l1 l2} :
      Forall2 P l1 l2 -> Forall2 (fun x y => P y x) l2 l1.
  
    Lemma Forall2_In_l {A B} {P:A->B->Prop} {l1 l2 a} :
      Forall2 P l1 l2 ->
      In a l1 ->
      exists b,
        In b l2 /\
        P a b.

    Lemma Forall2_In_r {A B} {P:A->B->Prop} {l1 l2 b} :
      Forall2 P l1 l2 ->
      In b l2 ->
      exists a,
        In a l1 /\
        P a b.

  Lemma Forall2_app_tail_inv {A B} P l1 l2 a1 a2 :
     @Forall2 A B P (l1 ++ (a1::nil)) (l2 ++ (a2::nil)) ->
     Forall2 P l1 l2 /\ P a1 a2.
   
  Lemma filter_Forall2_same {A B} P f g (l1:list A) (l2:list B) :
    Forall2 P l1 l2 ->
    map f l1 = map g l2 ->
    Forall2 P (filter f l1) (filter g l2).

  Lemma Forall2_map_Forall {A B:Type} (P:A->B->Prop) (f:A->B) l :
    Forall2 P l (map f l) <-> Forall (fun x => P x (f x)) l.
  
  End forall2.

  Section forallb_ordpairs.

    Fixpoint forallb_ordpairs {A} f (l:list A)
      := match l with
         | nil => true
         | x::ls => forallb (f x) ls && forallb_ordpairs f ls
         end.

    Lemma forallb_ordpairs_ForallOrdPairs {A} f (l:list A) :
      forallb_ordpairs f l = true <-> (ForallOrdPairs (fun x y => f x y = true) l).
    
    Lemma forallb_ordpairs_ext {A} f1 f2 (l:list A) :
      (forall x y, In x l -> In y l -> f1 x y = f2 x y) ->
      forallb_ordpairs f1 l = forallb_ordpairs f2 l.

    Fixpoint forallb_ordpairs_refl {A} (f:A->A->bool) (l:list A)
      := match l with
         | nil => true
         | x::ls => forallb (f x) (x::ls) && forallb_ordpairs_refl f ls
         end.

    Lemma forallb_ordpairs_refl_conj A f (l:list A) :
      forallb_ordpairs_refl f l = forallb_ordpairs f l && forallb (fun x => f x x) l.

        Lemma forallb_ordpairs_app_cons {A} f (l:list A) x :
    forallb_ordpairs f l = true ->
    forallb (fun y => f y x) l = true ->
    forallb_ordpairs f (l ++ x::nil) = true.
  
  Lemma forallb_ordpairs_refl_app_cons {A} f (l:list A) x :
    forallb_ordpairs_refl f l = true ->
    f x x = true ->
    forallb (fun y => f y x) l = true ->
    forallb_ordpairs_refl f (l ++ x::nil) = true.

  End forallb_ordpairs.

  Lemma app_cons_cons_expand {A} (l:list A) a b :
    l ++ a::b::nil = (l ++ a ::nil)++b::nil.
  
  Section remove.
    Context {A:Type}.
    Context {eqdec:EqDec A eq}.
    
    Lemma remove_in_neq
          (l : list A) (x y : A) : x <> y ->
                                   (In x l <-> In x (remove eqdec y l)).

    Lemma list_in_remove_impl_diff x y l:
      In x (remove eqdec y l) -> x <> y.
    
    Lemma list_remove_append_distrib:
      forall (v:A) (l1 l2:list A),
        remove eqdec v l1 ++ remove eqdec v l2 = remove eqdec v (l1 ++ l2).

    Lemma list_remove_idempotent:
      forall v l,
        remove eqdec v (remove eqdec v l) = remove eqdec v l.

    Lemma list_remove_commute:
      forall v1 v2 l,
        remove eqdec v1 (remove eqdec v2 l) = remove eqdec v2 (remove eqdec v1 l).

    Remark list_remove_in v1 v2 l1 l2:
      (In v1 l1 -> In v1 l2) ->
      In v1 (remove eqdec v2 l1) -> In v1 (remove eqdec v2 l2).

    Lemma remove_inv v n l:
      In v (remove eqdec n l) -> In v l /\ v <> n.

    Lemma not_in_remove_impl_not_in:
      forall x v l,
        x <> v ->
        ~ In x (remove eqdec v l) ->
        ~ In x l.

    Fixpoint remove_all (x : A) (l : list A) : list A :=
      match l with
      | nil => nil
      | y::tl => if (x == y) then (remove_all x tl) else y::(remove_all x tl)
      end.

    Global Instance remove_all_proper : Proper (eq ==> ldeqA ==> ldeqA) remove_all.

    Lemma remove_all_filter x l:
      remove_all x l = filter (nequiv_decb x) l.
    
    Lemma remove_all_app (v:A) l1 l2
      : remove_all v (l1 ++ l2) = remove_all v l1 ++ remove_all v l2.

    Lemma fold_left_remove_all_In {l init a} :
      In a (fold_left (fun (a : list A) (b : A) =>
                       filter (nequiv_decb b) a) l init)
      -> In a init /\ ~ In a l.

  End remove.

  Lemma nin_remove {A} dec (l:list A) a :
    ~ In a l -> remove dec a l = l.

  Section repall.
    Context {A:Type}.
    Context `{eqdec:EqDec A eq}.

    Definition replace_all l v n
      := map (fun x => if eqdec x v then n else x) l.
    
    Lemma replace_all_nin l v n :
      ~ In v l ->
      map (fun x => if eqdec x v then n else x) l = l.

    Lemma replace_all_remove_neq l v0 v n:
      v <> v0 -> n <> v0 ->
      remove eqdec v0
             (map (fun x => if eqdec x v then n else x)
                  l) =
      (map (fun x => if eqdec x v then n else x)
           (remove eqdec v0 l)).

    Lemma remove_replace_all_nin l v v' :
      ~ In v' l ->
      remove eqdec v' (replace_all l v v') =
      remove eqdec v l.

    Definition flat_replace_all l (v:A) n
      := flat_map (fun x => if eqdec x v then n else (x::nil)) l.

    Lemma flat_replace_all_nil l (v:A) :
      flat_replace_all l v nil = @remove_all A eqdec v l.

    Lemma flat_replace_all_app l1 l2 (v:A) n
      : flat_replace_all (l1 ++ l2) v n
        = flat_replace_all l1 v n ++ flat_replace_all l2 v n.

    Lemma fold_left_remove_all_nil_in_inv {B} {x ps l}:
      In x (fold_left
              (fun (h : list nat) (xy : nat * B) =>
                 remove_all (fst xy) h)
              ps l) ->
      In x l.

    Lemma fold_left_remove_all_nil_in_inv' {x ps l}:
      In x (fold_left
              (fun (h : list nat) (xy : nat) =>
                 remove_all xy h)
              ps l) ->
      In x l.

    Lemma fold_left_remove_all_nil_in_not_inv' {x ps l}:
      In x (fold_left
              (fun (h : list nat) (xy : nat ) =>
                 remove_all xy h)
              ps l) ->
      ~ In x ps.
    
    Lemma replace_all_remove_eq (l : list A) (v n : A) :
      map (fun x : A => if eqdec x v then n else x) (remove eqdec v l) = (remove eqdec v l).

  End repall.

  Section incl.

    Definition cut_down_to {A B} {dec:EqDec A eq} (l:list (A*B)) (l2:list A) :=
      filter (fun a => existsb (fun z => (fst a) ==b z) l2) l.

    Lemma cut_down_to_in
          {A B} {dec:EqDec A eq}
          (l:list (A*B)) l2 a :
      In a (cut_down_to l l2) <-> In a l /\ In (fst a) l2 .

    Lemma cut_down_to_app {A B} {dec:EqDec A eq}
          (l l':list (A*B)) l2 :
      cut_down_to (l++l') l2 = cut_down_to l l2 ++ cut_down_to l' l2.
   
    Lemma incl_dec {A} {dec:EqDec A eq} (l1 l2:list A) :
      {incl l1 l2} + {~ incl l1 l2}.

    Global Instance incl_pre A : PreOrder (@incl A).


    Lemma set_inter_contained {A} dec (l l':list A):
      (forall a, In a l -> In a l') ->
      set_inter dec l l' = l.

    Lemma set_inter_idempotent {A} dec (l:list A):
      set_inter dec l l = l.

    Lemma set_inter_comm_in {A} dec a b :
      (forall x, In x (@set_inter A dec a b) -> In x (set_inter dec b a)) .
  
   Lemma nincl_exists {A} {dec:EqDec A eq} (l1 l2:list A) :
     ~ incl l1 l2 -> {x | In x l1 /\ ~ In x l2}.

  End incl.

  Section equivlist.
    Context {A:Type}.

    Definition equivlist (l l':list A)
      := forall x, In x l <-> In x l'.

    Global Instance equivlist_equiv : Equivalence equivlist.

    Global Instance Permutation_equivlist :
      subrelation (@Permutation A) equivlist.

    Lemma equivlist_in {l1 l2} : equivlist l1 l2 -> (forall x:A, In x l1 -> In x l2).
  
    Lemma equivlist_incls (l1 l2:list A) :
      equivlist l1 l2 <-> (incl l1 l2 /\ incl l2 l1).

    Global Instance equivlist_In_proper : Proper (eq ==> equivlist ==> iff) (@In A).

    Lemma equivlist_dec {dec:EqDec A eq} (l1 l2:list A) :
      {equivlist l1 l2} + {~ equivlist l1 l2}.
   
    Lemma equivlist_nil {l:list A} : equivlist l nil -> l = nil.

    Lemma app_idempotent_equivlist (l:list A) :
      equivlist (l++l) l.
    
    Lemma app_commutative_equivlist (l1 l2:list A) :
      equivlist (l1++l2) (l2++l1).
    
    Lemma app_contained_equivlist (a b:list A) :
      incl b a ->
      equivlist (a ++ b) a.

    Lemma set_inter_equivlist dec a b :
      equivlist (@set_inter A dec a b) (set_inter dec b a) .

    Global Instance set_inter_equivlist_proper dec : Proper (equivlist ==> equivlist ==> equivlist) (@set_inter A dec).

  Lemma equivlist_cons l1 l2 (s:A) :
    equivlist l1 l2 ->
    equivlist (s::l1) (s::l2).

  Global Instance equivlist_filter :
    Proper (eq ==> equivlist ==> equivlist) (@filter A).
  
  Global Instance equivlist_remove_all {dec:EqDec A eq} :
    Proper (eq ==> equivlist ==> equivlist) (@remove_all A dec).

    Lemma incl_list_dec (dec:forall x y:A, {x = y} + {x <> y}) (l1 l2:list A) : {(forall x, In x l1 -> In x l2)} + {~(forall x, In x l1 -> In x l2)}.

  End equivlist.

      Lemma set_inter_assoc {A} dec a b c:
        @set_inter A dec (set_inter dec a b) c
        = set_inter dec a (set_inter dec b c).
     
  Section Assym_over.
  
    Definition asymmetric_over {A} R (l:list A) :=
      forall x y, In x l-> In y l -> ~R x y -> ~R y x -> x = y.
  
    Lemma asymmetric_asymmetric_over {A} {R} :
      (forall x y:A, ~R x y -> ~R y x -> x = y) ->
      forall l, asymmetric_over R l .

    Lemma asymmetric_over_incl {A} {R} {l2:list A}
      : asymmetric_over R l2 ->
        forall l1,
          (forall x, In x l1 -> In x l2) ->
          asymmetric_over R l1.

    Lemma asymmetric_over_equivlist {A} {R} {l1 l2:list A} :
      equivlist l1 l2 ->
      (asymmetric_over R l1 <->
       asymmetric_over R l2).
    
    Lemma asymmetric_over_cons_inv {A} {R} {a:A} {l1} :
      asymmetric_over R (a::l1) ->
      asymmetric_over R l1.

    Hint Resolve asymmetric_over_cons_inv.

    Lemma asymmetric_over_swap {A} R {a b:A} {l1} :
      asymmetric_over R (a::b::l1) ->
      asymmetric_over R (b::a::l1).

  End Assym_over.

  
  Global Instance perm_in {A} : Proper (eq ==> (@Permutation A) ==> iff) (@In A).
  
  Lemma NoDup_perm' {A:Type} {a b:list A} : NoDup a -> Permutation a b -> NoDup b.
  
  Global Instance NoDup_perm {A:Type} :
    Proper (@Permutation A ==> iff) (@NoDup A).

  Lemma NoDup_Permutation' {A : Type} (l l' : list A) :
    NoDup l ->
    NoDup l' -> equivlist l l' -> Permutation l l'.

  Lemma NoDup_rev {A:Type} (l:list A) : NoDup (rev l) <-> NoDup l.

  Lemma NoDup_app_inv {A:Type} {a b:list A} : NoDup (a++b) -> NoDup a.
  
  Hint Resolve NoDup_app_inv.

  Lemma NoDup_app_inv2 {A:Type} {a b:list A} : NoDup (a++b) -> NoDup b.

  Lemma NoDup_dec {A:Type} {dec:EqDec A eq} (l:list A): {NoDup l} + {~NoDup l}.
  
  Section disj.
    Definition disjoint {A:Type} (l1 l2:list A)
      := forall x, In x l1 -> In x l2 -> False.

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

    Lemma disjoint_cons_inv1 {A:Type} {a:A} {l1 l2} :
      disjoint (a :: l1) l2 -> disjoint l1 l2 /\ ~ In a l2.

    Lemma disjoint_app_l {A} (l1 l2 l3:list A) :
    disjoint (l1 ++ l2) l3 <-> (disjoint l1 l3 /\ disjoint l2 l3).

   Lemma disjoint_app_r {A} (l1 l2 l3:list A) :
    disjoint l1 (l2 ++ l3) <-> (disjoint l1 l2 /\ disjoint l1 l3).


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

    Global Instance disjoint_sym {A:Type} : Symmetric (@disjoint A).

  End disj.

  Lemma unmap_NoDup {A B} (f:A->B) l :
    NoDup (map f l) -> NoDup l.
  
  Lemma map_inj_NoDup {A B} (f:A->B)
            (inj:forall x y, f x = f y -> x = y) (l:list A) :
        NoDup l ->
        NoDup (map f l).

  Lemma filter_NoDup {A} (f:A->bool) l :
    NoDup l -> NoDup (filter f l).

  Fixpoint zip {A B} (l1:list A) (l2: list B) : option (list (A * B)) :=
    match l1 with
    | nil =>
      match l2 with
      | nil => Some nil
      | _ => None
      end
    | x1 :: l1' =>
      match l2 with
      | nil => None
      | x2 :: l2' =>
        match zip l1' l2' with
        | None => None
        | Some l3 =>
          Some ((x1, x2) :: l3)
        end
      end
    end.

End RList.